Closed Covers: To Verify Progress for Communicating Finite State Machines

Abstract

Consider communicating finite state machines which exchange messages over unbounded FIFO channels. We discuss a technique to verify that the communication between a given pair of such machines will progress indefinitely; this implies that the communication is free from deadlocks and unspecified receptions. The technique is based on finding a set of global states for the communicating pair such that the following two conditions (along with other conditions) are satisfied: 1) the initial global state is in that set; and 2) starting from any global state in that set, an ``acyclic version'' of the communicating pair must reach a global state in that set. We call such a set a closed cover, and show that the existence of a closed cover for a communicating pair is sufficient to guarantee indefinite communication progress. We also show that in many practical instances, if the communication is guaranteed to progress indefinitely, then the existence of a closed cover is necessary.