AN APPROACH TO CYCLIC PROTOCOL VALIDATION

In this paper, the notion of fair reachability is generalized to cycli c protocols with more than two processes, where all the processes in a protocol are connected via a unidirectional ring and each process mig ht contain internal transitions and can be non-deterministic. We ident ify 'indefiniteness' as a new type of logical error due to reachable i nternal transition cycles. By properly incorporating internal transiti ons into the formulation, we show that, with a few modifications, all the previous results established for cyclic protocols without non-dete rministic and internal transitions still hold in the augmented model. Furthermore, by combining fair progress and maximal progress during st ate exploration, we prove that the following three problems are all de cidable for Q, the class of cyclic protocols with finite fair reachabl e state spaces: (I) global state reachability; (2) abstract state reac hability; and (3) execution cycle reachability. In the course of the i nvestigation, we also show that detection of k-indefiniteness and k-li velock are decidable for Q.