Abstract
We present MMC, a model checker for mobile systems specified in the style of the π-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 π-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 π-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 of Abadi and Gordon. Our experimental data show that MMC outperforms other known tools for model checking the π-calculus.
| Original language | English |
|---|---|
| Pages (from-to) | 38-66 |
| Number of pages | 29 |
| Journal | International Journal on Software Tools for Technology Transfer |
| Volume | 6 |
| Issue number | 1 |
| DOIs | |
| State | Published - 2004 |
Keywords
- Logic programming
- Mobile processes
- Model checking
- Tabled resolution
- π-calculus
Fingerprint
Dive into the research topics of 'A logical encoding of the π-calculus: Model checking mobile processes using tabled resolution'. Together they form a unique fingerprint.Cite this
- APA
- Author
- BIBTEX
- Harvard
- Standard
- RIS
- Vancouver