摘要：The decidability and complexity of reachability problems and model-checkingfor flat counter machines have been explored in detail. However, only fewresults are known for flat (lossy) FIFO machines, only in some particular cases(a single loop or a single bounded expression). We prove, by establishingreductions between properties, and by reducing SAT to a subset of theseproperties that many verification problems like reachability, non-termination,unboundedness are NP-complete for flat FIFO machines, generalizing similarexisting results for flat counter machines. We also show that reachability isNP-complete for flat lossy FIFO machines and for flat front-lossy FIFOmachines. We construct a trace-flattable system of many counter machinescommunicating 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 thetheoretical foundations and open the way to build a verification tool for(general) FIFO machines based on analysis of flat sub-machines.
关键词：Computer Science - Computational Complexity;Computer Science - Logic in Computer Science;Theory of computation - Parallel computing models
