Abstract
We present an optimizing compiler for the π-calculus that significantly improves the time and space performance of the MMC model checker. MMC exploits the similarity between the manner in which resolution techniques handle variables in a logic program and the manner in which the operational semantics of the π-calculus handles names by representing π-calculus names in MMC as Prolog variables, with distinct names represented by distinct variables. Given a π-calculus process P, our compiler for MMC produces an extremely compact representation of P’s symbolic state space as a set of transition rules. It also uses AC unification to recognize states that are equivalent due to symmetry.
Research supported in part by NSF grants CCR-9876242, CCR-9988155, IIS-0072927, CCR-0205376, CCR-0311512, ARO grants DAAD190110003 and DAAD190110019, and ONR grant N000140110967.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: The spi calculus. In: Proceedings of CCS, pp. 36–47. ACM Press, New York (1997)
Bachmair, L., Chen, T., Ramakrishnan, I.V.: Associative-commutative discrimination nets. In: Gaudel, M.-C., Jouannaud, J.-P. (eds.) CAAP 1993, FASE 1993, and TAPSOFT 1993. LNCS, vol. 668, pp. 61–74. Springer, Heidelberg (1993)
Chaki, S., Rajamani, S.K., Rehof, J.: Types as models: model checking messagepassing programs. In: Proceedings of POPL, pp. 45–57 (2002)
Chen, W., Warren, D.S.: Tabled evaluation with delaying for general logic programs. Journal of the ACM 43(1), 20–74 (1996)
Dam, M.: Proof systems for pi-calculus logics. Logic for Concurrency and Synchronisation (2001)
Delzanno, G., Etalle, S.: Transforming a proof system into Prolog for verifying security protocols. In: LOPSTR (2001)
Delzanno, G., Podelski, A.: Model checking in CLP. In: Proceedings of Tools and Algorithms for Construction and Analysis of Systems (1999)
Dong, Y., Du, X., Holzmann, G., Smolka, S.A.: Fighting livelock in the i- Protocol: A case study in explicit-state model checking. Software Tools for Technology Transfer 4(2) (2003)
Dong, Y., Ramakrishnan, C.R.: An optimizing compiler for efficient model checking. In: Proceedings of FORTE, pp. 241–256 (1999)
Emerson, E.A., Sistla, A.P.: Symmetry and model checking. Formal Methods in System Design: An International Journal 9(1/2), 105–131 (1996)
Gupta, G., Pontelli, E.: A constraint based approach for specification and verification of real-time systems. In: IEEE Real-Time Systems Symposium (1997)
Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering 23(5), 279–295 (1997)
Igarashi, A., Kobayashi, N.: A generic type system for the pi-calculus. Theoretical Computer Science 311(1-3), 121–163 (2004)
Kirchner, H., Moreau, P.-E.: Promoting rewriting to a programming language: a compiler for non-deterministic rewrite programs in associative-commutative theories. J. Functional Prog. 11(2), 207–251 (2001)
Lin, H.: Symbolic bisimulation and proof systems for the π-calculus. Technical report, School of Cognitive and Computer Science, U. of Sussex, UK (1994)
Lloyd, J.W.: Foundations of Logic Programming. Springer, Heidelberg (1984)
Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, Parts I and II. Information and Computation 100(1), 1–77 (1992)
Orava, F., Parrow, J.: An algebraic verification of a mobile network. Journal of Formal Aspects of Computing 4, 497–543 (1992)
Pierce, B.C., Turner, D.N.: Pict: a programming language based on the picalculus. In: Proof, Language, and Interaction: Essays in Honour of Robin Milner, pp. 455–494. MIT Press, Cambridge (2000)
Ramakrishna, Y.S., Ramakrishnan, C.R., Ramakrishnan, I.V., Smolka, S.A., Swift, T.L., Warren, D.S.: Efficient model checking using tabled resolution. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254. Springer, Heidelberg (1997)
Song, H., Compton, K.J.: Verifying pi-calculus processes by Promela translation. Technical Report CSE-TR-472-03, Univ. of Michigan (2003)
Stickel, M.E.: A unification algorithm for associative-commutative unification. Journal of the ACM 28(3), 423–434 (1981)
Urbina, L.: Analysis of hybrid systems in CLP(R). In: Constraint Programming, CP (1996)
Victor, B.: The Mobility Workbench user’s guide. Technical report, Department of Computer Systems, Uppsala University, Sweden (1995)
The, X.: XSB logic programming system v2.5 (2002), Available under GPL, from http://xsb.sourceforge.net
Yang, P., Ramakrishnan, C.R., Smolka, S.A.: A logical encoding of the π- calculus: Model checking mobile processes using tabled resolution. Proceedings of VMCAI, 2003. Extended version in Software Tools for Technology Transfer 6(1), 38–66 (2004)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Yang, P., Dong, Y., Ramakrishnan, C.R., Smolka, S.A. (2005). A Provably Correct Compiler for Efficient Model Checking of Mobile Processes. In: Hermenegildo, M.V., Cabeza, D. (eds) Practical Aspects of Declarative Languages. PADL 2005. Lecture Notes in Computer Science, vol 3350. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30557-6_10
Download citation
DOI: https://doi.org/10.1007/978-3-540-30557-6_10
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-24362-5
Online ISBN: 978-3-540-30557-6
eBook Packages: Computer ScienceComputer Science (R0)