| Summary: | 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.
|
|---|