Decidability of the termination problem for completely specified protocols

Summary In 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. Alain Finkel is a Professor of Computer Science at the Ecole Normale Supérieure of Cachan. His research is concerned with the models of concurrency and the practical possibilities to verify and to validate distributed systems. He is also interested by the cognitive interfaces.