Towards Generalised Half-Duplex Systems

TL;DR

This paper introduces greedy systems as a promising generalization of binary half-duplex FIFO automata, maintaining desirable properties and enabling analysis of multi-party communication protocols.

Contribution

It defines greedy systems, proves they preserve key properties of binary half-duplex systems, and relates them to multiparty mailbox communication models.

Findings

Greedy systems retain polynomial-time decidability properties.

They effectively generalize binary half-duplex systems to multi-party settings.

Greedy systems are closely related to multiparty mailbox communication models.

Abstract

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.