Symbolic transition graph and its early bisimulation checking algorithms for the π-calculus  

作　　者：李舟军 陈火旺 王兵山 

出　　处：《Science China(Technological Sciences)》1999年第4期342-353,共12页中国科学（技术科学英文版）

基　　金：Project partially supported by the 863 Hi-Tech Project (Grant No. 863-306-ZT05-06-1);the National Natural Science Foundation of China (Grant No. 69873045).

摘　　要：Symbolic transition graph is proposed as an intuitive and compact semantic model for the π-calculus processes.Various versions (strong/weak, ground/symbolic) of early operational semantics are given to such graphs. Based on them the corresponding versions of early bisimulation equivalences and observation congruence are defined. The notions of symbolic observation graph and symbolic congruence graph are also introduced, and followed by two theorems ensuring the elimination of τ-cycles and τ-edges. Finally algorithms for checking strong/weak early bisimulation equivalences and observation congruence are presented together with their correctness proofs. These results fuse and generalize the strong bisimulation checking algorithm for value-passing processes and the verification technique for weak bisimulation of pure-CCS to the finite control π-calculus.Symbolic transition graph is proposed as an intuitive and compact semantic model for the π-calculus processes. Various versions (strong/weak, ground/symbolic) of early operational semantics are given to such graphs. Based on them the corresponding versions of early bisimulation equivalences and observation congruence are defined. The notions of symbolic observation graph and symbolic congruence graph are also introduced, and followed by two theorems ensuring the elimination of τ-cycles and τ-edges. Finally algorithms for checking strong/weak early bisimulation, equivalences and observation congruence are presented together with their correctness proofs. These results fuse and generalize the strong bisimulation checking algorithm for value-passing processes and the verification technique for weak bisimulation of pure-CCS to the finite control π-calculus.

关 键 词：Π-CALCULUS SYMBOLIC TRANSITION GRAPH BISIMULATION observation CONGRUENCE predicate equation system. 

分 类 号：O241.4[理学—计算数学]