无穷状态系统互模拟判定算法
文献类型：学位论文
| 作者 | 陈海燕 |
| 学位类别 | 博士 |
| 答辩日期 | 2008-05-29 |
| 授予单位 | 中国科学院研究生院 |
| 授予地点 | 中国科学院软件研究所 |
| 导师 | 柳欣欣 |
| 关键词 | 互模拟等价 BPA BPP 可判定 Tableau 关系最粗划分 |
| 其他题名 | Algorithms for the Decidability of Bisimularity for Infinite-State System |
| 学位专业 | 计算机软件与理论 |
| 中文摘要 | 因为无穷状态系统拥有无穷多个状态，基于它的可判定性理论更加复杂，对于无穷状态系统的强、弱互模拟等价的判定比有穷状态系统的判定更有难度。我们对无穷状态系统BPA（Basic Process Algebra）、BPP(Basic Parallel Processes)进程的互模拟等价的判定算法进行研究。研究BPA、BPP模型的行为，判断它们的互模拟等价。 首先，我们用tableau方法解决了totally normed BPA的弱互模拟等价的判定问题。我们研究与弱互模拟紧密相关的分解属性。同时，为了使弱互模拟判定具有分解属性，提出了相对于$\Gamma$的弱互模拟（weak bisimulation w.r.t $\Gamma$）的定义，该定义是基于Hirshfeld的``弱互模拟相当''概念提炼得到。它是使用tableau方法证明可判定性的基础。然后，提出了tableau的规则，证明tableau方法的有限性，可靠性以及完备性。同时，简单分析其时间复杂度。 接着，我们使用tableau方法解决了totally normed BPP的弱互模拟等价判定问题。由于其同样没有像证明normed BPP强互模拟所使用的分解属性，因此，为了使tableau方法得以应用，我们应用``控制''和``改进''的概念，它是使用tableau方法证明可判定性的基础。根据BPP进程的特点，提出适用于弱互模拟判定的tableau的规则，同样给出tableau方法的有限性，可靠性以及完备性的证明，也显示如何从tableau系统获得一个可靠且完备的判定totally normed BPP进程弱互模拟等价的等式理论。 然后，我们将判定totally normed BPA的弱互模拟的限定条件减弱，使其norm值可以为零。这样，就会产生无穷分支的问题。为了更好的对问题的描述，我们应用弱迁移关系符号化特征的定义，分析了tableau方法得以应用的条件，提出新的规则解决无穷分支的问题。同样，给出tableau方法的有限性，可靠性以及完备性的证明。 最后，我们使用关系最粗划分（Relational Coarsest Partition）算法判定normed BPA的强互模拟等价。突破了这种算法只被用于证明有穷状态系统的等价问题，我们所做的工作是将这种算法应用于无穷状态系统的互模拟判定。因为它要求对系统的所有状态进行划分，但是，无穷状态系统的状态数是无穷多个，没有办法将它们全部枚举出来。我们的工作是将无穷状态空间的问题转化到有穷状态空间上解决，使得RCP算法得以应用。 |
| 英文摘要 | Because infinite-state systems have the infinite states, the decidability problems on the infinite-state systems are more complicated. The decidability of strong bisimulation, weak bisimulation on them is more difficult than the finite-state system. We shall study algorithms about bisimulation uivalences for infinite-state systems such as BPA (Basic Process Algebra), BPP (Basic Parallel Processes). We will study the behaviors of the BPA, BPP models, and judge their bisimulation equivalences. Firstly, we settle decidability of weak bisimulation equivalence for totally normed BPA using the tableau method. We study the decomposition property, it is intensely relevant with weak bisimulation. And for making weak bisimulation having the decomposition property, we propose the notion of weak bisimulation w.r.t $\Gamma$, which is obtained by refining Hirshfeld's notion of weak bisimulation up to. It is the basis of using the tableau method to prove the decidability. Then we bring forward the tableau rules, and prove the finiteness, soundness and completeness of the tableau method. And we roughly analyze its complexity. Then， we settle decidability of weak bisimulation equivalence for totally normed BPP using the tableau method. Because of no decomposition property like being founded in proving strong bisimulation for normed BPP, we apply the concept of ``controlling'' and ``improving'' for making the tableau method be used, it is the base to use the tableau method to prove decidability of weak bisimulation. According to the characteristic BPP processes we propose the tableau rules applied in the decidability for weak bisimulation. Similar we prove the finiteness, soundness and completeness of the tableau method. We also show how to derive a complete axiomatisation for weak bisimulation of totally normed BPP from the decidability proof. And then, we weak the limit of the decidability of weak bisimilarity for totally normed BPA and make whose norm value can be zero. So it is capable of producing the problem of infinite branching. We can use a finite symbolic characterisation to settle the question of infinite branching. For much better description to problem, we apply the notion of a numerical index on the weak transition. The condition applying the tableau method having been analyzed, we get new rules to resolve infinite branching problems. Then we prove the finiteness, soundness and completeness of the tableau method. Finally, we use the relational coarsest partition algorithm to decide strong bisimulation for normed BPA. Having broken this algorithm only being used to decide the equivalence problem for the finite-state system, our work makes it applied in the infinite state system. Because it requires that all states of system are divided, but the infinite-state system has infinite many states. We have no way to numerate all the states. Now our work translates infinite-state space problem into finite-state space, and it can make RCP algorithm be feasible. |
| 公开日期 | 2011-03-17 |
| 源URL | [http://124.16.136.157/handle/311060/6208]  |
| 专题 | 软件研究所_软件所图书馆_早期 |
| 推荐引用方式 GB/T 7714 | 陈海燕. 无穷状态系统互模拟判定算法[D]. 中国科学院软件研究所. 中国科学院研究生院. 2008. |
入库方式： OAI收割
来源：软件研究所
浏览0
下载0
收藏0
其他版本
除非特别说明，本系统中所有内容都受版权保护，并保留所有权利。