文章基本信息

标题：Verification of Flat FIFO Systems
本地全文：下载
作者：Alain Finkel ; M. Praveen
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2019
卷号：140
页码：1-17
DOI：10.4230/LIPIcs.CONCUR.2019.12
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：Infinite state systems; FIFO; counters; flat systems; reachability; termination; complexity