本文已被：浏览 1265次 下载 1798次
Received:March 21, 2016 Revised:April 05, 2016
Received:March 21, 2016 Revised:April 05, 2016
中文摘要: 带发散性说明的分支互模拟是van Glabbeek和Weijland提出的一个概念，并被用来定义等价关系.该等价关系应该是最弱的一个发散性保持的并且满足分支互模拟性质的等价关系.然而在概念提出时并没有提供这些重要性质的证明，并且我们认为在原定义的基础上这个证明是不显然的.本文通过co-induction的手段利用染色迹的概念定义了着色完全迹等价，并证明该等价关系是最弱的一个保持发散的并且满足分支互模拟性质的等价关系.然后我们证明了着色完全迹等价关系和≈b△是相同的，因而补充了van Glabbeek和Weijland的工作，即证明了≈b△是最弱的一个保持发散的并且是满足分支互模拟性质的等价关系.
中文关键词: 分支互模拟等价关系 发散性 发散性保持 co-induction定义 染色迹
Abstract:The notion of branching bisimulation with explicit divergence was introduced by van Glabbeek and Weijland.It is used to define an equivalence relation ≈b△,which means to be the weakest equivalence with the property of branching bisimulation and divergence preservation.However,in that paper it only claims that ≈b△ is an equivalence with such properties without proofs,and as it turns out that the proving is not obvious.In this paper we introduce an equivalence relation called coloured complete trace equivalence,and prove that it is the weakest equivalence which has the property of branching bisimulation equivalence and is also divergence preserving.We then prove that the coloured complete trace equivalence coincides with ≈b△,thus supplementing the work of van Glabbeek and Weijland.
文章编号： 中图分类号： 文献标志码：
基金项目:国家自然科学基金（NSFC-91418204）
引用文本：
廖文琪,柳欣欣.关于并发系统分支互模拟关系发散性保持的研究.计算机系统应用,2016,25(12):215-220
LIAO Wen-Qi,LIU Xin-Xin.Branching Bisimulation with Explicit Divergence in Concurrent Systems.COMPUTER SYSTEMS APPLICATIONS,2016,25(12):215-220
廖文琪,柳欣欣.关于并发系统分支互模拟关系发散性保持的研究.计算机系统应用,2016,25(12):215-220
LIAO Wen-Qi,LIU Xin-Xin.Branching Bisimulation with Explicit Divergence in Concurrent Systems.COMPUTER SYSTEMS APPLICATIONS,2016,25(12):215-220
