## Abstract:

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 shows that MMC outperforms other known tools for model checking the pi-calculus.

## Bibtex Entry:

@article{YRS:STTT04, author = {Ping Yang and C. R. Ramakrishnan and Scott A. Smolka}, title = {A Logical Encoding of the pi-Calculus: Model Checking Mobile Processes Using Tabled Resolution}, journal = {International Journal on Software Tools for Technology Transfer ({STTT})}, volume = {6}, number = {1}, pages = {38--66}, note = {http://springerlink.metapress.com/openurl.asp?genre=article&id=doi:10.1007/s10009-003-0136-3}, year = {2004} }

Full Paper: |
[pdf] |

Home | Papers

C. R. Ramakrishnan

`(cram@cs.sunysb.edu)`