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.
翻译：普通 FIFO 机器的基本决定问题, 如可达性和无限制性, 其不可减轻性是众所周知的。 在本文中, 我们通过只考虑输入限制的运行( 即通过特定频道发送的信息序列属于特定约束语言 ), 来为普通 FIFO 机器提供对通用模型的不协调性。 我们通过将该模型降为有限制零测试的反制机器, 证明合理的可达性( 通过扩展、 控制- 状态可达性、 不受约束性、 僵局等) 问题是可以消化的。 这种机器的子类是输入- 字母限制的机器、 平式机器、 线性 FIFO 网和单基因机器, 其中一些问题已经被证明是可裁量的。 这些理论结果可以构成一个基础, 用于根据对输入限制的机器的分析来核查普通 FIFO 机器。
相关内容
微信扫码咨询专知VIP会员