##
A Logical Encoding of the Pi-Calculus: Model Checking Mobile Processes
Using Tabled Resolution

We present MMC, a model checker for mobile systems specified in the style
of the pi-calculus. MMC's development builds on that of XMC, a model
checker for an expressive extension of Milner's value-passing calculus
implemented using the XSB tabled logic-programming engine. MMC addresses the
salient issues that arise in the pi-calculus, including scope extrusion and
intrusion, and dynamic generation of new names to avoid name capture.
We show that logic programming provides an efficient implementation platform
for model checking pi-calculus specifications, and can be used to obtain an
exact encoding of the pi-calculus's transitional semantics. Moreover, MMC
is easily extended to handle process expressions in the spi-calculus of Abadi
and Gordon. Our experimental data show that MMC outperforms other known
tools for model checking the pi-calculus.