This paper investigates a model of communications protocols based on finite-state machines. The goal is to determine how to ensure that protocols are "well-formed," meaning they respond only to events that can actually occur. The paper explores the extent to which this problem is solvable and presents an approach to solving it. The model uses explicit finite-state machines to represent processes and implicit queues to represent channels. Processes communicate by sending messages through these channels. The model is as powerful as programming languages in terms of expressive power, but it is less powerful in modeling processes than Petri nets. However, it is more powerful in modeling channels, as the FIFO property is built in. The paper defines a protocol as a quadruple consisting of processes, their states, messages, and a transition function. It then defines the concept of a well-formed protocol, which requires that all executable receptions are specified. The paper also introduces the concept of stable N-tuples, which are reachable global states with all channels empty. These are useful for detecting synchronization losses. The paper presents an approach to ensuring that a protocol is well-formed. This approach is based on syntactical properties derived from notions of physical causality and completeness. The approach is developed for a protocol synthesizer and is based on analyzing the protocol's structure to ensure that all receptions are specified and that no deadlocks occur. The paper also discusses the problem of determining whether a protocol is well-formed. It shows that this problem is undecidable for general protocols but solvable for certain classes of protocols, such as those with bounded channels. The paper presents an algorithm for finding all the receptions that must be specified as a result of a transmission and an algorithm for finding all the stable N-tuples. The correctness of these algorithms is established in the paper. The paper concludes that the model is suitable for representing and analyzing communication protocols, particularly in situations where propagation delay is not negligible and where the protocol parties and communication medium can be considered as separate entities. The paper also discusses the importance of identifying stable N-tuples for detecting synchronization losses and the need for approximate solutions when a complete solution is not available.This paper investigates a model of communications protocols based on finite-state machines. The goal is to determine how to ensure that protocols are "well-formed," meaning they respond only to events that can actually occur. The paper explores the extent to which this problem is solvable and presents an approach to solving it. The model uses explicit finite-state machines to represent processes and implicit queues to represent channels. Processes communicate by sending messages through these channels. The model is as powerful as programming languages in terms of expressive power, but it is less powerful in modeling processes than Petri nets. However, it is more powerful in modeling channels, as the FIFO property is built in. The paper defines a protocol as a quadruple consisting of processes, their states, messages, and a transition function. It then defines the concept of a well-formed protocol, which requires that all executable receptions are specified. The paper also introduces the concept of stable N-tuples, which are reachable global states with all channels empty. These are useful for detecting synchronization losses. The paper presents an approach to ensuring that a protocol is well-formed. This approach is based on syntactical properties derived from notions of physical causality and completeness. The approach is developed for a protocol synthesizer and is based on analyzing the protocol's structure to ensure that all receptions are specified and that no deadlocks occur. The paper also discusses the problem of determining whether a protocol is well-formed. It shows that this problem is undecidable for general protocols but solvable for certain classes of protocols, such as those with bounded channels. The paper presents an algorithm for finding all the receptions that must be specified as a result of a transmission and an algorithm for finding all the stable N-tuples. The correctness of these algorithms is established in the paper. The paper concludes that the model is suitable for representing and analyzing communication protocols, particularly in situations where propagation delay is not negligible and where the protocol parties and communication medium can be considered as separate entities. The paper also discusses the importance of identifying stable N-tuples for detecting synchronization losses and the need for approximate solutions when a complete solution is not available.