Verification of Flat FIFO Systems
Verification of Flat FIFO Systems
复制标题
Flat FIFO 系统的验证
DOI：
--
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
M. Praveen
中科院分区：
文献类型：
--
作者：
A. Finkel;M. Praveen
详细探讨了可达性问题的可判定性和复杂性以及平面计数器机器的模型检查。然而，对于平坦（有损）FIFO 机器，仅在某些特定情况下（单个循环或单个有界表达式）已知很少的结果。我们通过建立属性之间的约简，以及通过将 SAT 约简为这些属性的子集，证明许多验证问题（例如可达性、非终止性、无界性）对于扁平 FIFO 机器来说是 NP 完全的，从而概括了扁平计数器机器的类似现有结果。我们还表明，对于平坦有损 FIFO 机器和平坦前端有损 FIFO 机器，可达性是 NP 完全的。我们构建了一个由许多计数器机器通过集合点进行通信的跟踪扁平系统，该系统与给定的扁平 FIFO 机器非常相似，它允许对原始扁平 FIFO 机器进行模型检查。我们的结果奠定了理论基础，并为基于扁平子机分析构建（通用）FIFO 机验证工具开辟了道路。
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.