T. Chen, T. Han, and J. Lu (PRC)
Mobile processes, x-calculus, Open bisimulation, Symbolic open bisimulation, Proof system.
The x-calculus is an important evolution for mobile pro cess calculi. Open bisimulation is widely studied for calculus. However hitherto, the study on the algebra theory x-calculus is mainly carried out in the non-symbolic frame work. In this paper, we apply the symbolic approach to the research of x-calculus. We present an alternative char acterization of strong open bisimulation without universal quantification over substitutions. We show that this sym bolic bisimulation equivalence coincides with the standard open bisimulation. Based on the symbolic semantics we present a symbolic proof system to axiomatize open bisim ulation. The result can be seen as the basis of automated algorithms and tools to decide the open bisimulation and gives us more insights into the algebra theory of x-calculus with mismatch.
Important Links:
Go Back
