DROPS

Document

DOI: 10.4230/LIPIcs.CONCUR.2021.14

A Unifying Framework for Deciding Synchronizability

Authors: Benedikt Bollig, Cinzia Di Giusto, Alain Finkel, Laetitia Laversa, Etienne Lozes, and Amrita Suresh

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

Abstract

Several notions of synchronizability of a message-passing system have been introduced in the literature. Roughly, a system is called synchronizable if every execution can be rescheduled so that it meets certain criteria, e.g., a channel bound. We provide a framework, based on MSO logic and (special) tree-width, that unifies existing definitions, explains their good properties, and allows one to easily derive other, more general definitions and decidability results for synchronizability.

Cite as

Benedikt Bollig, Cinzia Di Giusto, Alain Finkel, Laetitia Laversa, Etienne Lozes, and Amrita Suresh. A Unifying Framework for Deciding Synchronizability. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 14:1-14:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{bollig_et_al:LIPIcs.CONCUR.2021.14,
  author =	{Bollig, Benedikt and Di Giusto, Cinzia and Finkel, Alain and Laversa, Laetitia and Lozes, Etienne and Suresh, Amrita},
  title =	{{A Unifying Framework for Deciding Synchronizability}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{14:1--14:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.14},
  URN =		{urn:nbn:de:0030-drops-143917},
  doi =		{10.4230/LIPIcs.CONCUR.2021.14},
  annote =	{Keywords: communicating finite-state machines, message sequence charts, synchronizability, MSO logic, special tree-width}
}

Document

DOI: 10.4230/LIPIcs.CONCUR.2020.49

Bounded Reachability Problems Are Decidable in FIFO Machines

Authors: Benedikt Bollig, Alain Finkel, and Amrita Suresh

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract

The undecidability of basic decision problems for general FIFO machines such as reachability and unboundedness is well-known. In this paper, we provide an underapproximation for the general model by considering only runs that are input-bounded (i.e. the sequence of messages sent through a particular channel belongs to a given bounded language). We prove, by reducing this model to a counter machine with restricted zero tests, that the rational-reachability problem (and by extension, control-state reachability, unboundedness, deadlock, etc.) is decidable. This class of machines subsumes input-letter-bounded machines, flat machines, linear FIFO nets, and monogeneous machines, for which some of these problems were already shown to be decidable. These theoretical results can form the foundations to build a tool to verify general FIFO machines based on the analysis of input-bounded machines.

Cite as

Benedikt Bollig, Alain Finkel, and Amrita Suresh. Bounded Reachability Problems Are Decidable in FIFO Machines. In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 49:1-49:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{bollig_et_al:LIPIcs.CONCUR.2020.49,
  author =	{Bollig, Benedikt and Finkel, Alain and Suresh, Amrita},
  title =	{{Bounded Reachability Problems Are Decidable in FIFO Machines}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{49:1--49:17},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.49},
  URN =		{urn:nbn:de:0030-drops-128615},
  doi =		{10.4230/LIPIcs.CONCUR.2020.49},
  annote =	{Keywords: FIFO machines, reachability, underapproximation, counter machines}
}

Search Results

Documents authored by Suresh, Amrita

A Unifying Framework for Deciding Synchronizability

Abstract

Cite as

Bounded Reachability Problems Are Decidable in FIFO Machines

Abstract

Cite as

Thanks for your feedback!

Could not send message