2026-07-23T19:13:09Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:12861 2024-03-06T10:50:52Z ddc:004 open_access

Bounded Reachability Problems Are Decidable in FIFO Machines Bollig, Benedikt Finkel, Alain Suresh, Amrita FIFO machines reachability underapproximation counter machines 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Benedikt Bollig and Alain Finkel and Amrita Suresh 2020 Is Part Of LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2020.49 urn:nbn:de:0030-drops-128615 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.49 eng https://creativecommons.org/licenses/by/3.0/legalcode