Alain Finkel ; M. Praveen - Verification of Flat FIFO Systems

lmcs:5999 - Logical Methods in Computer Science, October 14, 2020, Volume 16, Issue 4 - https://doi.org/10.23638/LMCS-16(4:4)2020
Verification of Flat FIFO Systems

Authors: Alain Finkel ; M. Praveen

    The decidability and complexity of reachability problems and model-checking for flat counter machines have been explored in detail. However, only few results are known for flat (lossy) FIFO machines, only in some particular cases (a single loop or a single bounded expression). We prove, by establishing reductions between properties, and by reducing SAT to a subset of these properties that many verification problems like reachability, non-termination, unboundedness are NP-complete for flat FIFO machines, generalizing similar existing results for flat counter machines. We also show that reachability is NP-complete for flat lossy FIFO machines and for flat front-lossy FIFO machines. We construct a trace-flattable system of many counter machines communicating via rendez-vous that is bisimilar to a given flat FIFO machine, which allows to model-check the original flat FIFO machine. Our results lay the theoretical foundations and open the way to build a verification tool for (general) FIFO machines based on analysis of flat sub-machines.


    Volume: Volume 16, Issue 4
    Published on: October 14, 2020
    Accepted on: August 10, 2020
    Submitted on: December 25, 2019
    Keywords: Computer Science - Computational Complexity,Computer Science - Logic in Computer Science,Theory of computation - Parallel computing models

    Linked data

    Source : ScholeXplorer IsCitedBy ARXIV 2105.06723
    Source : ScholeXplorer IsCitedBy DOI 10.46298/lmcs-18(1:19)2022
    Source : ScholeXplorer IsCitedBy DOI 10.4230/lipics.concur.2020.49
    Source : ScholeXplorer IsCitedBy DOI 10.48550/arxiv.2105.06723
    • 2105.06723
    • 10.46298/lmcs-18(1:19)2022
    • 10.4230/lipics.concur.2020.49
    • 10.48550/arxiv.2105.06723
    Bounded Reachability Problems are Decidable in FIFO Machines
    Bollig, Benedikt ; Finkel, Alain ; Suresh, Amrita ;

    1 Document citing this article

    Share

    Consultation statistics

    This page has been seen 498 times.
    This article's PDF has been downloaded 207 times.