Benedikt Bollig ; Alain Finkel ; Amrita Suresh - Bounded Reachability Problems are Decidable in FIFO Machines

lmcs:7485 - Logical Methods in Computer Science, January 20, 2022, Volume 18, Issue 1 -
Bounded Reachability Problems are Decidable in FIFO MachinesArticle

Authors: Benedikt Bollig ; Alain Finkel ; Amrita Suresh

    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.

    Volume: Volume 18, Issue 1
    Published on: January 20, 2022
    Accepted on: November 19, 2021
    Submitted on: May 17, 2021
    Keywords: Computer Science - Logic in Computer Science,Computer Science - Formal Languages and Automata Theory


    Consultation statistics

    This page has been seen 995 times.
    This article's PDF has been downloaded 549 times.