Bounded Reachability Problems are Decidable in FIFO Machines

TL;DR

This paper introduces a decidable underapproximation for FIFO machines by focusing on input-bounded runs, enabling the analysis of complex properties like reachability through reduction to counter machines.

Contribution

It establishes the decidability of rational-reachability in input-bounded FIFO machines by reducing the problem to counter machines with restricted zero tests, expanding the class of analyzable models.

Findings

Decidability of rational-reachability in input-bounded FIFO machines.

Reduction of FIFO reachability problems to counter machine analysis.

Applicability to various subclasses like input-letter-bounded and flat machines.

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.