Document Open Access Logo

Modal Logics for Mobile Processes Revisited

Authors Tiange Liu, Alwen Tiu, Jim de Groot



PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2023.34.pdf
  • Filesize: 0.68 MB
  • 17 pages

Document Identifiers

Author Details

Tiange Liu
  • School of Computing, The Australian National University, Canberra, Ngunnawal Country, Australia
Alwen Tiu
  • School of Computing, The Australian National University, Canberra, Ngunnawal Country, Australia
Jim de Groot
  • School of Computing, The Australian National University, Canberra, Ngunnawal Country, Australia

Acknowledgements

We thank Ross Horne for various insightful discussions on the subtlety of the mismatch operator, and the anonymous reviewers for their careful reading of the paper and their helpful feedback on an earlier version of this paper.

Cite AsGet BibTex

Tiange Liu, Alwen Tiu, and Jim de Groot. Modal Logics for Mobile Processes Revisited. In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, pp. 34:1-34:17, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.CONCUR.2023.34

Abstract

We revisit the logical characterisations of various bisimilarity relations for the finite fragment of the π-calculus. Our starting point is the early and the late bisimilarity, first defined in the seminal work of Milner, Parrow and Walker, who also proved their characterisations in fragments of a modal logic (which we refer to as the MPW logic). Two important refinements of early and late bisimilarity, called open and quasi-open bisimilarity, respectively, were subsequently proposed by Sangiorgi and Walker. Horne, et. al., showed that open and quasi-bisimilarity are characterised by intuitionistic modal logics: OM (for open bisimilarity) and FM (for quasi-open bisimilarity). In this work, we attempt to unify the logical characterisations of these bisimilarity relations, showing that they can be characterised by different sublogics of a unifying logic. A key insight to this unification derives from a reformulation of the four bisimilarity relations (early, late, open and quasi-open) that uses an explicit name context, and an observation that these relations can be distinguished by the relative scoping of names and their instantiations in the name context. This name context and name substitution then give rise to an accessibility relation in the underlying Kripke semantics of our logic, that is captured logically by an S4-like modal operator. We then show that the MPW, the OM and the FM logics can be embedded into fragments of our unifying classical modal logic. In the case of OM and FM, the embedding uses the fact that intuitionistic implication can be encoded in modal logic S4.

Subject Classification

ACM Subject Classification
  • Theory of computation → Process calculi
  • Theory of computation → Modal and temporal logics
Keywords
  • pi-calculus
  • modal logic
  • intuitionistic logic
  • bisimilarity

Metrics

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

References

  1. Martín Abadi, Bruno Blanchet, and Cédric Fournet. The applied pi calculus: Mobile values, new names, and secure communication. J. ACM, 65(1):1:1-1:41, 2018. URL: https://doi.org/10.1145/3127586.
  2. Martín Abadi and Andrew D. Gordon. A calculus for cryptographic protocols: The spi calculus. In Richard Graveman, Philippe A. Janson, Clifford Neuman, and Li Gong, editors, CCS '97, Proceedings of the 4th ACM Conference on Computer and Communications Security, Zurich, Switzerland, April 1-4, 1997, pages 36-47. ACM, 1997. URL: https://doi.org/10.1145/266420.266432.
  3. Martín Abadi and Andrew D. Gordon. A bisimulation method for cryptographic protocols. Nord. J. Comput., 5(4):267, 1998. Google Scholar
  4. Ki Yung Ahn, Ross Horne, and Alwen Tiu. A characterisation of open bisimilarity using an intuitionistic modal logic. In Roland Meyer and Uwe Nestmann, editors, 28th International Conference on Concurrency Theory, CONCUR 2017, September 5-8, 2017, Berlin, Germany, volume 85 of LIPIcs, pages 7:1-7:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2017.7.
  5. Ki Yung Ahn, Ross Horne, and Alwen Tiu. A characterisation of open bisimilarity using an intuitionistic modal logic. Logical Methods in Computer Science, 17, 2021. Google Scholar
  6. Johannes Borgström and Uwe Nestmann. On bisimulations for the spi calculus. In Hélène Kirchner and Christophe Ringeissen, editors, Algebraic Methodology and Software Technology, 9th International Conference, AMAST 2002, Saint-Gilles-les-Bains, Reunion Island, France, September 9-13, 2002, Proceedings, volume 2422 of Lecture Notes in Computer Science, pages 287-303. Springer, 2002. URL: https://doi.org/10.1007/3-540-45719-4_20.
  7. A. Chagrov and M. Zakharyaschev. Modal Logic. Oxford University Press, Oxford, 1997. Google Scholar
  8. Ulrik Frendrup, Hans Hüttel, and Jesper Nyholm Jensen. Modal logics for cryptographic processes. In Uwe Nestmann and Prakash Panangaden, editors, 9th International Workshop on Expressiveness in Concurrency, EXPRESS 2002, Satellite Workshop from CONCUR 2002, Brno, Czech Republic, August 19, 2002, volume 68 of Electronic Notes in Theoretical Computer Science, pages 124-141. Elsevier, 2002. URL: https://doi.org/10.1016/S1571-0661(05)80368-8.
  9. Matthew Hennessy and Robin Milner. Algebraic laws for nondeterminism and concurrency. J. ACM, 32(1):137-161, 1985. URL: https://doi.org/10.1145/2455.2460.
  10. Ross Horne, Ki Yung Ahn, Shang-Wei Lin, and Alwen Tiu. Quasi-open bisimilarity with mismatch is intuitionistic. In Anuj Dawar and Erich Grädel, editors, Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12, 2018, pages 26-35. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209125.
  11. Ross Horne and Sjouke Mauw. Discovering epassport vulnerabilities using bisimilarity. Log. Methods Comput. Sci., 17(2):24, 2021. URL: https://doi.org/10.23638/LMCS-17(2:24)2021.
  12. Hans Hüttel and Michael D. Pedersen. A logical characterisation of static equivalence. In Marcelo Fiore, editor, Proceedings of the 23rd Conference on the Mathematical Foundations of Programming Semantics, MFPS 2007, New Orleans, LA, USA, April 11-14, 2007, volume 173 of Electronic Notes in Theoretical Computer Science, pages 139-157. Elsevier, 2007. URL: https://doi.org/10.1016/j.entcs.2007.02.032.
  13. Robin Milner. A Calculus of Communicating Systems, volume 92 of Lecture Notes in Computer Science. Springer, 1980. URL: https://doi.org/10.1007/3-540-10235-3.
  14. Robin Milner, Joachim Parrow, and David Walker. A calculus of mobile processes, II. Information & Computation, 100:41-77, 1992. URL: https://doi.org/10.1016/0890-5401(92)90009-5.
  15. Robin Milner, Joachim Parrow, and David Walker. Modal logics for mobile processes. Theor. Comput. Sci., 114(1):149-171, 1993. URL: https://doi.org/10.1016/0304-3975(93)90156-N.
  16. Ugo Montanari and Marco Pistore. An introduction to history dependent automata. In Andrew D. Gordon, Andrew M. Pitts, and Carolyn L. Talcott, editors, Second Workshop on Higher-Order Operational Techniques in Semantics, HOOTS 1997, Stanford, CA, USA, December 8-12, 1997, volume 10 of Electronic Notes in Theoretical Computer Science, pages 170-188. Elsevier, 1997. URL: https://doi.org/10.1016/S1571-0661(05)80696-6.
  17. Ugo Montanari and Marco Pistore. History dependent automata. Technical report, Università di Pisa, 1998. Google Scholar
  18. Joachim Parrow, Johannes Borgström, Lars-Henrik Eriksson, Ramunas Gutkovas, and Tjark Weber. Modal logics for nominal transition systems. Log. Methods Comput. Sci., 17(1), 2021. URL: https://lmcs.episciences.org/7137.
  19. Michael David Pedersen. Logics for the applied pi calculus. BRICS Report Series, 13(19), December 2006. URL: https://doi.org/10.7146/brics.v13i19.21923.
  20. Davide Sangiorgi. A theory of bisimulation for the pi-calculus. In Eike Best, editor, CONCUR '93, 4th International Conference on Concurrency Theory, Hildesheim, Germany, August 23-26, 1993, Proceedings, volume 715 of Lecture Notes in Computer Science, pages 127-142. Springer, 1993. URL: https://doi.org/10.1007/3-540-57208-2_10.
  21. Davide Sangiorgi, Naoki Kobayashi, and Eijiro Sumii. Environmental bisimulations for higher-order languages. ACM Trans. Program. Lang. Syst., 33(1):5:1-5:69, 2011. URL: https://doi.org/10.1145/1889997.1890002.
  22. Davide Sangiorgi and David Walker. On barbed equivalences in pi-calculus. In Kim Guldstrand Larsen and Mogens Nielsen, editors, CONCUR 2001 - Concurrency Theory, 12th International Conference, Aalborg, Denmark, August 20-25, 2001, Proceedings, volume 2154 of Lecture Notes in Computer Science, pages 292-304. Springer, 2001. URL: https://doi.org/10.1007/3-540-44685-0_20.
  23. Davide Sangiorgi and David Walker. The pi-calculus: a Theory of Mobile Processes. Cambridge university press, 2003. Google Scholar
  24. Alwen Tiu. A trace based bisimulation for the spi calculus: An extended abstract. In Zhong Shao, editor, Programming Languages and Systems, 5th Asian Symposium, APLAS 2007, Singapore, November 29-December 1, 2007, Proceedings, volume 4807 of Lecture Notes in Computer Science, pages 367-382. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-76637-7_25.
  25. Alwen Tiu and Jeremy E. Dawson. Automating open bisimulation checking for the spi calculus. In Proceedings of the 23rd IEEE Computer Security Foundations Symposium, CSF 2010, Edinburgh, United Kingdom, July 17-19, 2010, pages 307-321. IEEE Computer Society, 2010. URL: https://doi.org/10.1109/CSF.2010.28.
  26. Alwen Tiu and Dale Miller. Proof search specifications of bisimulation and modal logics for the pi-calculus. ACM Trans. Comput. Log., 11(2):13:1-13:35, 2010. URL: https://doi.org/10.1145/1656242.1656248.
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