Decidability of the termination problem for completely specified protocols
Decidability of the termination problem for completely specified protocols
复制标题
完全指定协议的终止问题的可判定性
作者：
A. Finkel
总结在本文中，我们提出了一类新的协议，称为完全指定协议。每个协议都表示为通信有限状态机的系统。完全指定的协议类使得有限状态机可以接收的每个消息也可以在有限状态机的每个本地状态中接收。这些协议很重要，因为它们允许对无界 fifo 通道进行建模，并可以确定终止问题，即可达性树是否有限。我们的技术的一个例子是使用有关链路协议的实际问题给出的。
SummaryIn this paper, we present a new class of protocols called completely specified protocols. Each protocol is represented as a system of Communicating Finite State Machines. The class of completely specified protocols is such that each message that can be received by a Finite State Machine, can also be received in every local state of the Finite State Machine. These protocols are important because they allow for modelling unbounded fifo channels and make it possible to decide the Termination Problem, that is whether the reachability tree is finite or not. An example of our techniques is given using a practical problem concerning link protocols.