On the bisimulation proof method
On the bisimulation proof method
复制标题
DOI：
10.1017/s0960129598002527
复制
发表时间：
1998-10
影响因子：
0.5
通讯作者：
D. Sangiorgi
中科院分区：
文献类型：
--
作者：
D. Sangiorgi
在进程之间建立双向相似性最流行的方法是展示双向模拟关系。根据定义，如果[Rscr]进展到[Rscr]本身，即[Rscr]中的进程对可以相互匹配，并且它们的派生再次在[Rscr]中，则[Rscr]是一种双向模拟关系。我们研究了该方法的推广，目的是减少要展示的关系的大小，从而减轻建立双相似结果所需的证明工作。我们允许关系[Rscr]前进到不同的关系[Fscr]([Rscr])，其中[Fscr]是关系上的函数。可以以这种方式安全使用的函数(即，如果[Rscr]进展到[Fscr]([Rscr])，则[Rscr]仅包括双相似进程对)是健全的。我们给出了一个保证可靠性的简单条件。我们证明了声音函数类包含非平凡函数，并研究了该类关于各种重要函数构造子的闭包性质，如合成、并和迭代。这些性质允许我们从简单的声音函数构造复杂的声音函数，从而构建复杂的生物相似性证明技术。从进程代数CCS和π演算中提取的各种非平凡的例子支持了我们的证明技术的有效性。它们包括方程唯一解的证明和复制算子的几个性质的证明。其中，有一个新的结果证明了采用简单形式的前缀保护复制作为π演算中唯一的复制形式是合理的。
The most popular method for establishing bisimilarities among processes is to exhibit bisimulation relations. By definition, [Rscr ] is a bisimulation relation if [Rscr ] progresses to [Rscr ] itself, i.e., pairs of processes in [Rscr ] can match each other's actions and their derivatives are again in [Rscr ]. We study generalisations of the method aimed at reducing the size of the relations to be exhibited and hence relieving the proof work needed to establish bisimilarity results. We allow a relation [Rscr ] to progress to a different relation [Fscr ] ([Rscr ]), where [Fscr ] is a function on relations. Functions that can be safely used in this way (i.e., such that if [Rscr ] progresses to [Fscr ] ([Rscr ]), then [Rscr ] only includes pairs of bisimilar processes) are sound. We give a simple condition that ensures soundness. We show that the class of sound functions contains non-trivial functions and we study the closure properties of the class with respect to various important function constructors, like composition, union and iteration. These properties allow us to construct sophisticated sound functions – and hence sophisticated proof techniques for bisimilarity – from simpler ones. The usefulness of our proof techniques is supported by various non-trivial examples drawn from the process algebras CCS and π-calculus. They include the proof of the unique solution of equations and the proof of a few properties of the replication operator. Among these, there is a novel result that justifies the adoption of a simple form of prefix-guarded replication as the only form of replication in the π-calculus.