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.