• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>13th International Conference on CONCUR 2002 - Concurrency Theory, Aug 20-23, 2002, Brno, Czech Republic >Weak Bisimulation is Sound and Complete for PCTL
【24h】

Weak Bisimulation is Sound and Complete for PCTL

机译：PCTL的弱双仿真是完整的

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

We investigate weak bisimulation of probabilistic systems in the presence of nondeterminism, i.e. labelled concurrent Markov chains (LCMC) with silent transitions. We build on the work of Philippou, Lee and Sokolsky [17] for finite state LCMCs. Their definition of weak bisimulation destroys the additivity property of the probability distributions, yielding instead capacities. The mathematics behind capacities naturally captures the intuition that when we deal with nondeterminism we must work with estimates on the possible probabilities. Our analysis leads to three new developments: 1. We identify an axiomatization of "image finiteness" for countable state systems and present a new definition of weak bisimulation for these LCMCs. We prove that our definition coincides with that of Philippou, Lee and Sokolsky for finite state systems. 2. We show that bisimilar states have matching computations. The notion of matching involves linear combinations of transitions. This idea is closely related to the use of randomized schedulers. 3. We study a minor variant of the probabilistic logic pCTL―the variation arises from an extra path formula to address action labels. We show that bisimulation is sound and complete for this variant of pCTL.
机译：我们在不确定性的存在下研究概率系统的弱双仿真，即带有静默过渡的标记并发马尔可夫链（LCMC）。我们基于Philippou，Lee和Sokolsky [17]在有限状态LCMC方面的工作。他们对弱双仿真的定义破坏了概率分布的可加性，从而产生了容量。能力背后的数学自然地抓住了直觉，即当我们处理不确定性问题时，我们必须对可能的概率进行估计。我们的分析带来了三个新进展：1.我们确定了可数状态系统的“图像有限性”公理化，并为这些LCMC提供了弱双仿真的新定义。我们证明，对于有限状态系统，我们的定义与Philippou，Lee和Sokolsky的定义一致。 2.我们证明双相似状态具有匹配的计算。匹配的概念涉及过渡的线性组合。这个想法与随机调度程序的使用紧密相关。 3.我们研究了概率逻辑pCTL的一个较小变体-该变体来自于解决动作标签的额外路径公式。我们表明，对于pCTL的这种变体，双模拟是合理且完整的。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号