Verification of Finite-Control Pi-Calculus Systems

Algorithmic techniques for model checking typically explore a subset of the state space of a concurrent system. The state space can be generated according to a set of operational semantics rules. We proposed a new symbolic operational semantics for the finite-control pi-calculus called the constructive semantics. When constructing derivations, traditional operational semantics can arbitrarily rename bound names of processes due to alpha-conversion. Furthermore, the same names can be used repeatedly with different binding occurrences. Our constructive semantics has the advantage that it is more deterministic than the traditional operational semantics since it carefully controls the manner in which alpha-conversions are performed and, as a consequence, can be efficiently encoded. We have proved the soundness and completeness of the constructive semantics with respect to the traditional semantics. We then encoded the constructive semantics directly using XSB tabled logic programming. The key to this encoding is the treatment of the pi-calculus names as Prolog variables and the use of Prolog's resolution mechanism to generate new names. We have shown through extensive experiments that this version of MMC outperforms other known tools for model checking the pi-calculus.