Boundedness, empty channel detection, and synchronization for communicating finite automata (Q1819939)

Communicating finite automata are built out of a net of finite state machines (CFSM) each of which can make local moves, send/receive messages (to/from another component machine) and test the input/output channel on emptiness. The channels may be organized as FIFO queues (FIFO network of CFSM) or as multisets with priority (given by a partial order relation on the (finite) set of messages). A system of CFSM is said to be bounded iff there is a bound k such that in any reachable state of the system on any channel there are at most k messages. The main result of the paper is the decidability of the boundedness problem for a FIFO-system of two CFSM, where one of the two machines is allowed to send only a single type of message to the other. The authors give a nondeterministic logspace decision procedure using a simulation by a restricted 3-counter machine. This is in contrast to the undecidability of the boundedness problem for 2-dimensional vector addition systems with states (VASS) and similar systems of two CFSM with undecidable boundedness problem.