Synthesis of Communicating Finite-State Machines with Guaranteed Progress

Abstract

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 machineM, and constructs two communicating machinesM'andN'such that 1)M'is constructed fromMby adding some receiving transitions to it, and 2) the communication betweenM'andN'is bounded and free from deadlocks, unspecified receptions, nonexecutable transitions, and state ambiguities. The second algorithm takes the two machinesM'andN'which result from the first algorithm, and computes the smallest possible capacities for the two channels between them. Both algorithms require anO(st)time, wheresis the number of states in the given machineM, andtis the number of state transitions inM; thus, the methodology is practical to use.