Abstract:
We present MMC, a model checker for mobile systems specified in the style of the pi-calculus. MMC's development builds on our experience gained in developing XMC, a model checker for an extension of Milner's value-passing calculus implemented using the XSB tabled logic-programming system. MMC, however, is not simply an extension of XMC; rather it is virtually a complete re-implementation that 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 tabled \comment{that the management of variables in logic programming makes it} logic programming is especially suitable as 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. Our experimental data shows that MMC outperforms other known tools for model checking the pi-calculus.
Bibtex Entry:
@inproceedings{YRS:VMCAI03, 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}, booktitle = {Verification, Model Checking and Abstract Interpretation ({VMCAI})}, address = {New York, NY}, month = {January}, series = {Lecture Notes in Computer Science}, volume = {2575}, publisher = {Springer}, pages = {116--131}, year = {2003} }
| Full Paper: | [pdf] |
C. R. Ramakrishnan
(cram@cs.sunysb.edu)