All Title Author
Keywords Abstract


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

Keywords: mobile processes,π,-calculus,bisimulation,decision procedure
计算机模拟
,有限控制,π-计算

Full-Text   Cite this paper   Add to My Lib

Abstract:

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.

Full-Text

comments powered by Disqus