We generalize the technique of fair reachability analysis to multi-cyclic protocols modeled as networks of communicating finite state machines, where a number of cyclic protocols are interconnected in such a way that any two component cyclic protocols share at most one process and each channel in the protocol belongs to exactly one component cyclic protocol. By composing the fair reachability relations of the component cyclic protocols, we prove that the set of fair reachable states of a multi-cyclic protocol is exactly the set of reachable states that are of equal channel length with respect to each of its component cyclic protocols. As a result, each deadlock state is fair reachable, and deadlock detection is decidable for the class of multi-cyclic protocols whose fair reachable state spaces are finite. Under the assumption that the underlying communication topology of a protocol is strongly connected, we show that fair reachability analysis is inherently infeasible for logical correctness validation beyond multi-cyclic protocols.

We adapt the partial order state reduction techniques developed for Petri nets and labeled transition systems to the validation of multi-process protocols modeled as communicating finite state machines. We identify two specific partial order reduction methods in this context: (1) maximal partial order reachability analysis, which is a generalization of maximal reachability analysis to protocols with n/spl ges/2 processes; and (2) simultaneous partial order reachability analysis, which is a counterpart of fair reachability analysis for protocols with n/spl ges/2 processes and arbitrary communication topologies. We study the logical error detection capabilities of each method and show that these two methods, when used together, provide complete logical error coverage for bounded multi-process protocols.

In this paper, the notion of fair reachability is generalized to cyclic protocols with n/spl ges/2 machines. It is shown that each fair reachable state is of equal channel length and each deadlock state is fair reachable. As a result, deadlock detection is decidable for P, the class of cyclic protocols whose fair reachable state spaces are finite. The concept of simultaneous unboundedness is defined and the lack of it is shown to be a necessary and sufficient condition for a protocol to be in P. Through finite extension of the fair reachable state space, it is also shown that detection of unspecified receptions, unboundedness, and nonexecutable transitions are all decidable for P. Furthermore, it is shown that any protocol in P is logically correct if and only if there is no logical error in its fair reachable state space. This study demonstrates that for the class P, our generalized fair reachability analysis technique not only can achieve substantial state reduction but also maintains very competitive logical error coverage. Therefore, it is a very useful technique to prove logical correctness for a wide variety of cyclic protocols.

We study three reachability problems for cyclic protocols: (1) global state reachability; (2) abstract state reachability; and (3) execution cycle reachability. By combining fair progress and maximal progress during state exploration, we prove that these three problems an all decidable for Q, the class of cyclic protocols with finite fair reachable state spaces. In the course of the investigation, we also show that detection of k-indefiniteness and k-livelock an decidable for Q.

In this paper, we extend the generalized fair reachability notion to cyclic protocols with nondeterministic and internal transitions. By properly incorporating internal transitions into the formulation of fair progress vectors, we prove that with only a few modifications, all the results established for cyclic protocols without nondeterministic and internal transitions still hold even if nondeterministic and internal transitions are allowed. We identify indefiniteness as a new type of logical error resulting from reachable internal execution cycles and show that it can also be detected for the class of cyclic protocols with finite fair reachable state spaces with finite extension.

In a previous paper, we generalized the fair reachability notion to cyclic protocols with n/spl ges/2 machines and showed that deadlock detection is decidable for /spl Pscr/, the class of cyclic protocols whose fair reachable state spaces are finite. In this paper, we show that detection of unspecified receptions, unboundedness, and nonexecutable transitions are all decidable for class /spl Pscr/ via finite extension of the fair reachable state space. This study shows that for the class /spl Pscr/, our generalized fair reachability analysis technique not only achieves substantial state reduction but also maintains very competitive logical error coverage. Therefore, it is a viable state reduction technique.>