The paper investigates a model of communication protocols based on finite-state machines, focusing on ensuring that protocols are "well-formed" by specifying responses to only those events that can actually occur. The authors explore the solvability of this problem and present an approach to achieving it. They define a protocol as a quadruple consisting of sets of states, initial states, message sets, and a partial function that maps states to successor states. The paper discusses the limitations of different protocol models, such as parallel programs and Petri nets, and introduces a model using explicit finite-state machines and implicit queues to represent channels. This model is particularly suitable for protocols with propagation delays and separate entities for protocol parties and communication media. The authors define the problem of identifying all executable receptions and stable N-tuples (reachable global states with all channels empty) in a protocol. They show that while the problem is undecidable in general, it can be solved for protocols with bounded channels and for protocols with two processes and one unbounded channel. The paper presents a solution for tree protocols, which are restricted forms of protocols that help in characterizing executable receptions and stable N-tuples. The solution involves constructing tree protocols and using a function \( L \) to determine the conditions under which a reception is executable. The paper also discusses termination criteria for expanding tree protocols to ensure that no new receptions or stable N-tuples are missed in the general protocol.The paper investigates a model of communication protocols based on finite-state machines, focusing on ensuring that protocols are "well-formed" by specifying responses to only those events that can actually occur. The authors explore the solvability of this problem and present an approach to achieving it. They define a protocol as a quadruple consisting of sets of states, initial states, message sets, and a partial function that maps states to successor states. The paper discusses the limitations of different protocol models, such as parallel programs and Petri nets, and introduces a model using explicit finite-state machines and implicit queues to represent channels. This model is particularly suitable for protocols with propagation delays and separate entities for protocol parties and communication media. The authors define the problem of identifying all executable receptions and stable N-tuples (reachable global states with all channels empty) in a protocol. They show that while the problem is undecidable in general, it can be solved for protocols with bounded channels and for protocols with two processes and one unbounded channel. The paper presents a solution for tree protocols, which are restricted forms of protocols that help in characterizing executable receptions and stable N-tuples. The solution involves constructing tree protocols and using a function \( L \) to determine the conditions under which a reception is executable. The paper also discusses termination criteria for expanding tree protocols to ensure that no new receptions or stable N-tuples are missed in the general protocol.