Verification of Flat FIFO Systems
| Autor: | Finkel, Alain, Praveen, M. |
|---|---|
| Přispěvatelé: | Laboratoire Spécification et Vérification [Cachan] (LSV), École normale supérieure - Cachan (ENS Cachan)-Centre National de la Recherche Scientifique (CNRS), Chennai Mathematical Institute [Inde], ANR-17-CE40-0028,BRAVAS,IDEAL-BASED ALGORITHMS FOR VASSES AND WELL-STRUCTURED SYSTEMS(2017) |
| Jazyk: | angličtina |
| Rok vydání: | 2019 |
| Předmět: |
FOS: Computer and information sciences
termination [INFO.INFO-CC]Computer Science [cs]/Computational Complexity [cs.CC] Computer Science - Logic in Computer Science ACM: F.: Theory of Computation/F.1: COMPUTATION BY ABSTRACT DEVICES/F.1.1: Models of Computation counters flat systems ACM: F.: Theory of Computation/F.1: COMPUTATION BY ABSTRACT DEVICES [SCCO.COMP]Cognitive science/Computer science 0102 computer and information sciences 02 engineering and technology Computational Complexity (cs.CC) 01 natural sciences 0202 electrical engineering electronic engineering information engineering Infinite state systems 000 Computer science knowledge general works FIFO [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] ACM: F.: Theory of Computation/F.3: LOGICS AND MEANINGS OF PROGRAMS/F.3.1: Specifying and Verifying and Reasoning about Programs Logic in Computer Science (cs.LO) Computer Science - Computational Complexity Theory of computation - Parallel computing models 010201 computation theory & mathematics Computer Science 020201 artificial intelligence & image processing complexity reachability |
| Zdroj: | CONCUR 2019 CONCUR 2019, Aug 2019, AMSTERDAM, Netherlands |
| ISSN: | 1860-5974 |
| Popis: | Logical Methods in Computer Science ; Volume 16, Issue 4 ; 1860-5974 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|