Synthesis of Communicating Finite-State Machines with Guaranteed Progress

We present a methodology to synthesize two communicating finite-state machines which exchange messages over two one-directional, FIFO channels. The methodology consists of two algorithms. The first algorithm takes one machine , and constructs two communicating machines and such that 1) is constructed from by adding some receiving transitions to it, and 2) the communication between and is bounded and free from deadlocks, unspecified receptions, nonexecutable transitions, and state ambiguities. The second algorithm takes the two machines and which result from the first algorithm, and computes the smallest possible capacities for the two channels between them. Both algorithms require an time, where is the number of states in the given machine , and is the number of state transitions in ; thus, the methodology is practical to use.