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] |
C. R. Ramakrishnan
(cram@cs.sunysb.edu)