论文部分内容阅读
带发散性说明的分支互模拟是van Glabbeek和Weijland提出的一个概念,并被用来定义等价关系≈b△.该等价关系应该是最弱的一个发散性保持的并且满足分支互模拟性质的等价关系.然而在概念提出时并没有提供这些重要性质的证明,并且我们认为在原定义的基础上这个证明是不显然的.本文通过co-induction的手段利用染色迹的概念定义了着色完全迹等价,并证明该等价关系是最弱的一个保持发散的并且满足分支互模拟性质的等价关系.然后我们证明了着色完全迹等价关系和≈b△是相同的,因而补充了van Glabbeek