### 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.