TY - GEN
T1 - Computing strong/weak bisimulation equivalences and observation congruence for value-passing processes
AU - Li, Zhoujun
AU - Chen, Huowang
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 1999.
PY - 1999
Y1 - 1999
N2 - We introduce an improved version of the symbolic transition graph with assignment (STGA) of Lin. The distinction of our model is that the assignment of a transition is performed after rather than before the action. Consequently, it has two advantages over the original one: on one hand, most regular value-passing processes can be represented more intuitively and compactly as such graphs; on the other hand, the natural definitions of symbolic double transitions can be given. The rules which generate the improved STGAs from regular value-passing processes are presented. The various versions (late/early, ground/symbolic) of strong operational semantics and strong bisimulation are given to such graphs, respectively. Our strong bisimulation algorithms are based on the late strong bisimulation algorithm of Lin, however, ours are more concise and practical. Finally, the improved STGAs are generalized to both symbolic observation graphs with assignments and symbolic congruence graphs with assignments, and therefore weak bisimulation equivalence and observation congruence can be checked, respectively.
AB - We introduce an improved version of the symbolic transition graph with assignment (STGA) of Lin. The distinction of our model is that the assignment of a transition is performed after rather than before the action. Consequently, it has two advantages over the original one: on one hand, most regular value-passing processes can be represented more intuitively and compactly as such graphs; on the other hand, the natural definitions of symbolic double transitions can be given. The rules which generate the improved STGAs from regular value-passing processes are presented. The various versions (late/early, ground/symbolic) of strong operational semantics and strong bisimulation are given to such graphs, respectively. Our strong bisimulation algorithms are based on the late strong bisimulation algorithm of Lin, however, ours are more concise and practical. Finally, the improved STGAs are generalized to both symbolic observation graphs with assignments and symbolic congruence graphs with assignments, and therefore weak bisimulation equivalence and observation congruence can be checked, respectively.
UR - https://www.scopus.com/pages/publications/84948976914
U2 - 10.1007/3-540-49059-0_21
DO - 10.1007/3-540-49059-0_21
M3 - 会议稿件
AN - SCOPUS:84948976914
SN - 3540657037
SN - 9783540657033
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 300
EP - 314
BT - Tools and Algorithms for the Construction and Analysis of Systems - 5th International Conference, TACAS 1999 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 1999, Proceedings
A2 - Rance Cleaveland, W.
PB - Springer Verlag
T2 - 5th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS 1999 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 1999
Y2 - 22 March 1999 through 28 March 1999
ER -