Efficient Symbolic Detection of Global Properties in Distributed Systems


A new approach is presented for detecting whether a computation of an asynchronous distributed system satisfies Poss Phi (read ``possibly Phi''), meaning the system could have passed through a global state satisfying property Phi. Previous general-purpose algorithms for this problem explicitly enumerate the set of global states through which the system could have passed during the computation. The new approach is to represent this set symbolically, in particular, using ordered binary decision diagrams. We describe an implementation of this approach, suitable for off-line detection of properties, and compare its performance to the enumeration-based algorithm of Alagar & Venkatesan. In typical cases, the new algorithm is significantly faster. We have measured over 400-fold speedup in some cases.
Scott Stoller's Home Page