We discuss an efficient variation of state exploration for two communicating finite state machines. In particular, we propose to divide the task of generating all reachable states into two independent subtasks. In each subtask, only the states reachable by forcing maximal progress for one machine are generated. Since the two subtasks are completely independent, and since in most instances the time and storage requirements for each subtask are less than those for the original task, maximal Progress state exploration can save time and/or storage over conventional state exploration.

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.

LetMandNbe two communicating finite state machines which exchange one type of message. We develope a polynomial algorithm to detect whether or notMandNcan reach a deadlock. The time complexity of the algorithm isO(m^{3}n^{3}and its space isO(mn)wheremandnare the numbers of states inMandN, respectively. The algorithm can also be used to verify that two communicating machines which exchange many types of messages are deadlock-free.