Modal Logics for Nominal Transition Systems

Authors Joachim Parrow, Johannes Borgström, Lars-Henrik Eriksson, Ramunas Gutkovas, Tjark Weber



PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2015.198.pdf
  • Filesize: 454 kB
  • 14 pages

Document Identifiers

Author Details

Joachim Parrow
Johannes Borgström
Lars-Henrik Eriksson
Ramunas Gutkovas
Tjark Weber

Cite AsGet BibTex

Joachim Parrow, Johannes Borgström, Lars-Henrik Eriksson, Ramunas Gutkovas, and Tjark Weber. Modal Logics for Nominal Transition Systems. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 198-211, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.CONCUR.2015.198

Abstract

We define a uniform semantic substrate for a wide variety of process calculi where states and action labels can be from arbitrary nominal sets. A Hennessy-Milner logic for these systems is introduced, and proved adequate for bisimulation equivalence. A main novelty is the use of finitely supported infinite conjunctions. We show how to treat different bisimulation variants such as early, late and open in a systematic way, and make substantial comparisons with related work. The main definitions and theorems have been formalized in Nominal Isabelle.
Keywords
  • Process algebra
  • nominal sets
  • bisimulation
  • modal logic

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. Martín Abadi and Cédric Fournet. Mobile values, new names, and secure communication. In Proceedings of POPL'01, pages 104-115. ACM, January 2001. Google Scholar
  2. Martín Abadi and Andrew D. Gordon. A calculus for cryptographic protocols: The Spi calculus. Journal of Information and Computation, 148(1):1-70, 1999. Google Scholar
  3. Samson Abramsky. A domain equation for bisimulation. Journal of Information and Computation, 92(2):161-218, 1991. Google Scholar
  4. Jesper Bengtson, Magnus Johansson, Joachim Parrow, and Björn Victor. Psi-calculi: a framework for mobile processes with nominal data and logic. Logical Methods in Computer Science, 7(1), 2011. Google Scholar
  5. Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, and Dmitriy Traytel. Truly modular (co)datatypes for Isabelle/HOL. In G. Klein and R. Gamboa, editors, Proc. of ITP 2014, volume 8558 of LNCS, pages 93-110. Springer, 2014. Google Scholar
  6. Maria Grazia Buscemi and Ugo Montanari. CC-Pi: A constraint-based language for specifying service level agreements. In Rocco De Nicola, editor, Proceedings of ESOP 2007, volume 4421 of LNCS, pages 18-32. Springer, 2007. Google Scholar
  7. Maria Grazia Buscemi and Ugo Montanari. Open bisimulation for the concurrent constraint pi-calculus. In Sophia Drossopoulou, editor, Proceedings of ESOP 2008, volume 4960 of LNCS, pages 254-268. Springer, 2008. Google Scholar
  8. Muffy Calder, Savi Maharaj, and Carron Shankland. A modal logic for full LOTOS based on symbolic transition systems. The Computer Journal, 45(1):55-61, 2002. Google Scholar
  9. Matteo Cimini, Mohammad Reza Mousavi, Michel A. Reniers, and Murdoch J. Gabbay. Nominal SOS. Electron. Notes Theor. Comput. Sci., 286:103-116, September 2012. Google Scholar
  10. Rocco De Nicola and Michele Loreti. Multiple-labelled transition systems for nominal calculi and their logics. Mathematical Structures in Computer Science, 18(1):107-143, 2008. Google Scholar
  11. E. Allen Emerson. Model checking and the mu-calculus. In DIMACS Series in Discrete Mathematics, pages 185-214. American Mathematical Society, 1997. Google Scholar
  12. Ulrik Frendrup, Hans Hüttel, and Jesper Nyholm Jensen. Modal logics for cryptographic processes. Electr. Notes Theor. Comput. Sci., 68(2):124-141, 2002. Google Scholar
  13. Arild Martin Møller Haugstad, Anders Franz Terkelsen, and Thomas Vindum. A modal logic for the fusion calculus. Unpublished, University of Aalborg, http://vbn.aau.dk/ws/files/61067487/1149104946.pdf, 2006.
  14. Matthew Hennessy and Xinxin Liu. A modal logic for message passing processes. Acta Informatica, 32(4):375-393, 1995. Google Scholar
  15. Matthew Hennessy and Robin Milner. Algebraic laws for nondeterminism and concurrency. J. ACM, 32(1):137-161, 1985. Google Scholar
  16. Dexter Kozen. Results on the propositional mu-calculus. Theoretical Computer Science, 27(3):333-354, 1983. Special Issue Ninth International Colloquium on Automata, Languages and Programming (ICALP) Aarhus, Summer 1982. Google Scholar
  17. Kim G. Larsen. Proof systems for Hennessy-Milner logic with recursion. In M. Dauchet and M. Nivat, editors, Proc. of CAAP'88, volume 299 of LNCS, pages 215-230. Springer, 1988. Google Scholar
  18. Robin Milner. Communication and Concurrency. Prentice Hall, 1989. Google Scholar
  19. Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, I. Inf. Comput., 100(1):1-40, 1992. Google Scholar
  20. Robin Milner, Joachim Parrow, and David Walker. Modal logics for mobile processes. Theoretical Computer Science, 114(1):149-171, 1993. Google Scholar
  21. Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel. Isabelle/HOL - A Proof Assistant for Higher-Order Logic, volume 2283 of LNCS. Springer, 2002. Google Scholar
  22. Joachim Parrow, Johannes Borgström, Lars-Henrik Eriksson, Ramūnas Gutkovas, and Tjark Weber. Modal logics for nominal transition systems. Technical Report 2015-021, Department of Information Technology, Uppsala University, June 2015. Google Scholar
  23. Joachim Parrow and Björn Victor. The fusion calculus: Expressiveness and symmetry in mobile processes. In Proc. of LICS 1998, pages 176-185. IEEE CS Press, 1998. Google Scholar
  24. Michael Pedersen. Logics for the applied pi calculus. Master’s thesis, Aalborg University, 2006. BRICS RS-06-19. Google Scholar
  25. Andrew M. Pitts. Nominal Sets. Cambridge University Press, 2013. Google Scholar
  26. Davide Sangiorgi. A theory of bisimulation for the π-calculus. In Eike Best, editor, Proceedings of CONCUR'93, volume 715 of LNCS, pages 127-142. Springer, 1993. Google Scholar
  27. Christian Urban and Cezary Kaliszyk. General bindings and alpha-equivalence in Nominal Isabelle. Logical Methods in Computer Science, 8(2), 2012. Google Scholar
  28. Lucian Wischik and Philippa Gardner. Explicit fusions. Theoretical Computer Science, 304(3):606-630, 2005. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail