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.MFCS.2021.13
URN: urn:nbn:de:0030-drops-144532
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/14453/
Go to the corresponding LIPIcs Volume Portal

Baldan, Paolo ; Carraro, Alberto ; Padoan, Tommaso

(Un)Decidability for History Preserving True Concurrent Logics

pdf-format:
LIPIcs-MFCS-2021-13.pdf (0.8 MB)

Abstract

We investigate the satisfiability problem for a logic for true concurrency, whose formulae predicate about events in computations and their causal (in)dependencies. Variants of such logics have been studied, with different expressiveness, corresponding to a number of true concurrent behavioural equivalences. Here we focus on a mu-calculus style logic that represents the counterpart of history-preserving (hp-)bisimilarity, a typical equivalence in the true concurrent spectrum of bisimilarities.
It is known that one can decide whether or not two 1-safe Petri nets (and in general finite asynchronous transition systems) are hp-bisimilar. Moreover, for the logic that captures hp-bisimilarity the model-checking problem is decidable with respect to prime event structures satisfying suitable regularity conditions. To the best of our knowledge, the problem of satisfiability has been scarcely investigated in the realm of true concurrent logics.
We show that satisfiability for the logic for hp-bisimilarity is undecidable via a reduction from domino tilings. The fragment of the logic without fixpoints, instead, turns out to be decidable. We consider these results a first step towards a more complete investigation of the satisfiability problem for true concurrent logics, which we believe to have notable solvable cases.

BibTeX - Entry

@InProceedings{baldan_et_al:LIPIcs.MFCS.2021.13,
  author =	{Baldan, Paolo and Carraro, Alberto and Padoan, Tommaso},
  title =	{{(Un)Decidability for History Preserving True Concurrent Logics}},
  booktitle =	{46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)},
  pages =	{13:1--13:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-201-3},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{202},
  editor =	{Bonchi, Filippo and Puglisi, Simon J.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2021/14453},
  URN =		{urn:nbn:de:0030-drops-144532},
  doi =		{10.4230/LIPIcs.MFCS.2021.13},
  annote =	{Keywords: Event structures, history-preserving bisimilarity, true concurrent behavioural logics, satisfiability, decidability, domino systems}
}

Keywords: Event structures, history-preserving bisimilarity, true concurrent behavioural logics, satisfiability, decidability, domino systems
Collection: 46th International Symposium on Mathematical Foundations of Computer Science (MFCS 2021)
Issue Date: 2021
Date of publication: 18.08.2021

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