平坦FIFO系统的验证
Verification of Flat FIFO Systems
AI总结：
本文通过归约证明平坦FIFO机器及有损变体的可达性等问题为NP完全，并构造互模拟系统以支持模型检测，为FIFO机器验证工具奠定基础。
摘要：
平坦计数器机器的可达性问题与模型检测的可判定性和复杂性已被详细研究。然而，对于平坦（有损）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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
