@inbook{0e56611fbc95445ba2e8b5edfdf4c90f,
title = "A logical encoding of the π-calculus: Model checking mobile processes using tabled resolution",
abstract = "We present MMC, a model checker for mobile systems specified in the style of the π-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 π-calculus, including scope extrusion and intrusion, and dynamic generation of new names to avoid name capture. We show that tabled logic programming is especially suitable as an efficient implementation platform for model checking π-calculus specifications, and can be used to obtain an exact encoding of the π-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 π-calculus.",
author = "Ping Yang and Ramakrishnan, \{C. R.\} and Smolka, \{Scott A.\}",
year = "2003",
doi = "10.1007/3-540-36384-x\_12",
language = "English",
isbn = "9783540003489",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "116--131",
editor = "Zuck, \{Lenore D.\} and Attie, \{Paul C.\} and Agostino Cortesi and Supratik Mukhopadhyay",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
}