Efficient Detection of Global Properties in Distributed Systems Using Partial-Order Methods

A new approach 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 predicate \Phi, or Def \Phi (read "definitely \Phi"), meaning the system definitely passed through a global state satisfying \Phi. Detection can be done easily by straightforward state-space search; this is essentially what Cooper and Marzullo proposed. We show that the persistent-set technique, a well-known partial-order method for optimizing state-space search, provides efficient detection. This approach achieves the same worst-case asymptotic time complexity as two special-purpose detection algorithms of Garg and Waldecker that detect Poss \Phi and Def \Phi for a restricted but important class of predicates. For Poss \Phi, our approach applies to arbitrary predicates and thus is more general than Garg and Waldecker's algorithm. We apply our algorithm for Poss..