DROPS

Document

DOI: 10.4230/LIPIcs.CONCUR.2024.22

An Automata-Based Approach for Synchronizable Mailbox Communication

Authors: Romain Delpy, Anca Muscholl, and Grégoire Sutre

Published in: LIPIcs, Volume 311, 35th International Conference on Concurrency Theory (CONCUR 2024)

Abstract

We revisit finite-state communicating systems with round-based communication under mailbox semantics. Mailboxes correspond to one FIFO buffer per process (instead of one buffer per pair of processes in peer-to-peer systems). Round-based communication corresponds to sequences of rounds in which processes can first send messages, then only receive (and receives must be in the same round as their sends). A system is called synchronizable if every execution can be re-scheduled into an equivalent execution that is a sequence of rounds. Previous work mostly considered the setting where rounds have fixed size. Our main contribution shows that the problem whether a mailbox communication system complies with the round-based policy, with no size limitation on rounds, is PSPACE-complete. For this we use a novel automata-based approach, that also allows to determine the precise complexity (PSPACE) of several questions considered in previous literature.

Cite as

Romain Delpy, Anca Muscholl, and Grégoire Sutre. An Automata-Based Approach for Synchronizable Mailbox Communication. In 35th International Conference on Concurrency Theory (CONCUR 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 311, pp. 22:1-22:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{delpy_et_al:LIPIcs.CONCUR.2024.22,
  author =	{Delpy, Romain and Muscholl, Anca and Sutre, Gr\'{e}goire},
  title =	{{An Automata-Based Approach for Synchronizable Mailbox Communication}},
  booktitle =	{35th International Conference on Concurrency Theory (CONCUR 2024)},
  pages =	{22:1--22:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-339-3},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{311},
  editor =	{Majumdar, Rupak and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2024.22},
  URN =		{urn:nbn:de:0030-drops-207947},
  doi =		{10.4230/LIPIcs.CONCUR.2024.22},
  annote =	{Keywords: Concurrent programming, Mailbox communication, Verification}
}

Search Results

Documents authored by Delpy, Romain

An Automata-Based Approach for Synchronizable Mailbox Communication

Abstract

Cite as

Thanks for your feedback!

Could not send message