A logical encoding of the π-calculus: Model checking mobile processes using tabled resolution. 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.
Keywords for this software
References in zbMATH (referenced in 9 articles , 1 standard article )
Showing results 1 to 9 of 9.
- Saeedloei, Neda: A logical encoding of timed (\pi)-calculus (2014)
- Guelev, Dimitar P.; Dam, Mads: An epistemic predicate (\mathrmCTL^*) for finite control (\pi)-processes (2011)
- Gupta, Gopal; Saeedloei, Neda; DeVries, Brian; Min, Richard; Marple, Kyle; Kluźniak, Feliks: Infinite computation, co-induction and computational logic (2011)
- Singh, Anu; Ramakrishnan, C. R.; Smolka, Scott A.: A process calculus for mobile ad hoc networks (2010)
- Baldan, Paolo; Bracciali, Andrea; Brodo, Linda; Bruni, Roberto: Deducing interactions in partially unspecified biological systems (2007)
- Baldan, P.; Bracciali, A.; Bruni, R.: A semantic framework for open processes (2007)
- Aziz, Benjamin; Hamilton, Geoff; Gray, David: A static analysis of cryptographic processes: the denotational approach (2005)
- Yang, Ping; Ramakrishnan, C. R.; Smolka, Scott A.: A logical encoding of the (\pi)-calculus: model checking mobile processes using tabled resolution (2004) ioport
- Yang, Ping; Ramakrishnan, C. R.; Smolka, Scott A.: A logical encoding of the (\pi)-calculus: Model checking mobile processes using tabled resolution (2003)