Efficient Symbolic Detection of Global Properties in Distributed Systems
Abstract:
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