中国科学院软件研究所机构知识库
Advanced  
ISCAS OpenIR  > 软件所图书馆  > 早期
题名:
无穷状态系统互模拟判定算法
作者: 陈海燕
答辩日期: 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.
内容类型: 学位论文
URI标识: http://ir.iscas.ac.cn/handle/311060/6208
Appears in Collections:中科院软件所图书馆_早期

Files in This Item:
File Name/ File Size Content Type Version Access License
10001_200418015029022陈海燕_paper.pdf(929KB)----限制开放-- 联系获取全文

Recommended Citation:
陈海燕. 无穷状态系统互模拟判定算法[D]. 中国科学院软件研究所. 中国科学院研究生院. 2008-05-29.
Service
Recommend this item
Sava as my favorate item
Show this item's statistics
Export Endnote File
Google Scholar
Similar articles in Google Scholar
[陈海燕]'s Articles
CSDL cross search
Similar articles in CSDL Cross Search
[陈海燕]‘s Articles
Related Copyright Policies
Null
Social Bookmarking
Add to CiteULike Add to Connotea Add to Del.icio.us Add to Digg Add to Reddit
所有评论 (0)
暂无评论
 
评注功能仅针对注册用户开放,请您登录
您对该条目有什么异议,请填写以下表单,管理员会尽快联系您。
内 容:
Email:  *
单位:
验证码:   刷新
您在IR的使用过程中有什么好的想法或者建议可以反馈给我们。
标 题:
 *
内 容:
Email:  *
验证码:   刷新

Items in IR are protected by copyright, with all rights reserved, unless otherwise indicated.

 

 

Valid XHTML 1.0!
Copyright © 2007-2017  中国科学院软件研究所 - Feedback
Powered by CSpace