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 extension of Milner's value-passing calculus implemented using the XSB tabled logic-programming engine -- and addresses the salient issues that arise in mobile processes: scope extrusion and intrusion, and dynamic generation of new names. We show that the management of logical variables in logic programming makes it especially suitable as an efficient implementation platform for model checking mobile processes, 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. Our experimental data shows that MMC outperforms other known tools for model checking mobile processes.