Towards Generalised Half-Duplex Systems

Cinzia Di Giusto
Loïc Germerie Guizouarn
Etienne Lozes

FIFO automata are finite state machines communicating through FIFO queues. They can be used for instance to model distributed protocols. Due to the unboundedness of the FIFO queues, several verification problems are undecidable for these systems. In order to model-check such systems, one may look for decidable subclasses of FIFO systems. Binary half-duplex systems are systems of two FIFO automata exchanging over a half-duplex channel. They were studied by Cece and Finkel who established the decidability in polynomial time of several properties. These authors also identified some problems in generalising half-duplex systems to multi-party communications. We introduce greedy systems, as a candidate to generalise binary half-duplex systems. We show that greedy systems retain the same good properties as binary half-duplex systems, and that, in the setting of mailbox communications, greedy systems are quite closely related to a multiparty generalisation of half-duplex systems.

In Julien Lange, Anastasia Mavridou, Larisa Safina and Alceste Scalas: Proceedings 14th Interaction and Concurrency Experience (ICE 2021), Online, 18th June 2021, Electronic Proceedings in Theoretical Computer Science 347, pp. 22–37.
Published: 2nd October 2021.

ArXived at: https://dx.doi.org/10.4204/EPTCS.347.2 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org