Faster Possibility Detection by Combining Two Approaches

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