Abstract. A new algorithm is presented for detecting whether a particular computation of an asynchronous distributed system satisfies Poss Φ (read “possibly Φ”), meaning the system could have passed through a global state satisfying Φ. Like the algorithm of Cooper and Marzullo, Φ may be any global state predicate; and like the algorithm of Garg and Waldecker, Poss Φ is detected quite efficiently if Φ has a certain structure. The new algorithm exploits the structure of some predicates Φ not handled by Garg and Waldecker’s algorithm to detect Poss Φ more efficiently than is possible with any algorithm that, like Cooper and Marzullo’s, evaluates Φ on every global state through which the system could have passed. A second algorithm is also presented for off-line detection of Poss Φ. It uses Strassen’s scheme for fast matrix multiplication. The intrinsic complexity of off-line and on-line detection of Poss Φ is discussed.
Scott D. Stoller, Fred B. Schneider