Computing Bisimulations for Finite-Control π-Calculus
Computing Bisimulations for Finite-Controlπ-Calculus

Symbolic bisimulation avoids the infinite branching problem caused by instantiating input names with all names in the standard definition of bisimulation in π-calculus. However, it does not automatically lead to an efficient algorithm, because symbolic bisimulation is indexed by conditions on names, and directly manipulating such conditions can be computationally costly. In this paper a new notion of bisimulation is introduced, in which the manipulation of maximally consistent conditions is replaced with a systematic employment of schematic names. It is shown that the new notion captures symbolic bisimulation in a precise sense. Based on the new definition an efficient algorithm, which instantiates input names “on-the-fly”, is presented to check bisimulations for finite-control π-calculus. Supported by the National Natural Science Foundation of China. LIN Huimin, born in 1947, received the Ph.D. degree from the Institute of Software, Chinese Academy of Sciences, in 1986. He was elected a Member of Chinese Academy of Sciences in 1999. His research interests include concurrency, process algebra, model checking, real-time systems, verification algorithms and tools, formal method, program specification and validation, abstract data types.