License: Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2023.34
URN: urn:nbn:de:0030-drops-190289
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/19028/
Go to the corresponding LIPIcs Volume Portal

Liu, Tiange ; Tiu, Alwen ; de Groot, Jim

Modal Logics for Mobile Processes Revisited

pdf-format:
LIPIcs-CONCUR-2023-34.pdf (0.7 MB)

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.

BibTeX - Entry

@InProceedings{liu_et_al:LIPIcs.CONCUR.2023.34,
  author =	{Liu, Tiange and Tiu, Alwen and de Groot, Jim},
  title =	{{Modal Logics for Mobile Processes Revisited}},
  booktitle =	{34th International Conference on Concurrency Theory (CONCUR 2023)},
  pages =	{34:1--34:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-299-0},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{279},
  editor =	{P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/19028},
  URN =		{urn:nbn:de:0030-drops-190289},
  doi =		{10.4230/LIPIcs.CONCUR.2023.34},
  annote =	{Keywords: pi-calculus, modal logic, intuitionistic logic, bisimilarity}
}

Keywords: pi-calculus, modal logic, intuitionistic logic, bisimilarity
Collection: 34th International Conference on Concurrency Theory (CONCUR 2023)
Issue Date: 2023
Date of publication: 07.09.2023

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI