一句话：证明平坦 FIFO 机及其有损/前端有损变体的多类验证问题为 NP 完全，并给出可模型检测的等价系统构造。
论文研究平坦（flat）FIFO 机及有损/前端有损变体的验证问题。此前仅有单循环或单有界表达式等特殊情形结果。作者通过性质间归约以及将 SAT 归约到部分性质，证明可达性、非终止、无界性等许多验证问题对平坦 FIFO 机是 NP 完全的，推广了平坦计数器机的相应结果；并证明有损与前端有损平坦 FIFO 机的可达性也是 NP 完全的。为支持模型检测，他们构造一个通过 rendez-vous 通信的多计数器机系统，其行为与给定平坦 FIFO 机互模拟且可 trace-flatten。该结果为基于平坦子机分析构建通用 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.