一句话：提出输入有界欠近似，将 FIFO 机器的有界可达性归约到受限零测试计数器机，证明其可判定。
一般 FIFO 机器的可达性、无界性等基本判定问题已知不可判定。本文提出输入有界欠近似：只考虑在某通道上发送的消息序列属于给定有界语言的运行。作者将该模型归约到带受限零测试的计数器机，从而证明 rational-reachability 问题可判定，并由此得到控制状态可达性、无界性、死锁等问题的可判定性。该机器类涵盖 input-letter-bounded 机器、flat 机器、线性 FIFO 网和 monogeneous 机器等已有可判定子类。这些结果为基于输入有界机器分析来构建一般 FIFO 机器验证工具提供了理论基础。
The undecidability of basic decision problems for general FIFO machines such as reachability and unboundedness is well-known. In this paper, we provide an underapproximation for the general model by considering only runs that are input-bounded (i.e. the sequence of messages sent through a particular channel belongs to a given bounded language). We prove, by reducing this model to a counter machine with restricted zero tests, that the rational-reachability problem (and by extension, control-state reachability, unboundedness, deadlock, etc.) is decidable. This class of machines subsumes input-letter-bounded machines, flat machines, linear FIFO nets, and monogeneous machines, for which some of these problems were already shown to be decidable. These theoretical results can form the foundations to build a tool to verify general FIFO machines based on the analysis of input-bounded machines.
@article{paperbot1736,
title = {Bounded Reachability Problems are Decidable in FIFO Machines},
author = {Benedikt Bollig and Alain Finkel and Amrita Suresh},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 1},
year = {2022},
doi = {10.46298/lmcs-18(1:19)2022}
}