Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2019.12
URN: urn:nbn:de:0030-drops-109147
URL: https://drops.dagstuhl.de/opus/volltexte/2019/10914/
Finkel, Alain ; Praveen, M.
Verification of Flat FIFO Systems
| pdf-format: |
|
Abstract
The decidability and complexity of reachability problems and model-checking for flat counter systems have been explored in detail. However, only few results are known for flat FIFO systems, 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 systems, generalizing similar existing results for flat counter systems. We construct a trace-flattable counter system that is bisimilar to a given flat FIFO system, which allows to model-check the original flat FIFO system. Our results lay the theoretical foundations and open the way to build a verification tool for (general) FIFO systems based on analysis of flat subsystems.
BibTeX - Entry
@InProceedings{finkel_et_al:LIPIcs:2019:10914,
author = {Alain Finkel and M. Praveen},
title = {{Verification of Flat FIFO Systems}},
booktitle = {30th International Conference on Concurrency Theory (CONCUR 2019)},
pages = {12:1--12:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-121-4},
ISSN = {1868-8969},
year = {2019},
volume = {140},
editor = {Wan Fokkink and Rob van Glabbeek},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2019/10914},
URN = {urn:nbn:de:0030-drops-109147},
doi = {10.4230/LIPIcs.CONCUR.2019.12},
annote = {Keywords: Infinite state systems, FIFO, counters, flat systems, reachability, termination, complexity}
}
| Keywords: | Infinite state systems, FIFO, counters, flat systems, reachability, termination, complexity | |
| Seminar: | 30th International Conference on Concurrency Theory (CONCUR 2019) | |
| Issue date: | 2019 | |
| Date of publication: | 20.08.2019 |
