Efficient detection of a locally stable predicate in a distributed system

We present an efficient approach to detect a locally stable predicate in a distributed computation. Examples of properties that can be formulated as locally stable predicates include termination and deadlock of a subset of processes. Our algorithm does not require application messages to be modified to carry control information (e.g., vector timestamps), nor does it inhibit events (or actions) of the underlying computation. The worst-case message complexity of our algorithm is O(n(m+1))$O(n(m+1))$, where n$n$ is the number of processes in the system and m$m$ is the number of events executed by the underlying computation. We show that, in practice, its message complexity should be much lower than its worst-case message complexity. The detection latency of our algorithm is O(d)$O(d)$ time units, where d$d$ is the diameter of communication topology. Our approach also unifies several known algorithms for detecting termination and deadlock. We also show that our algorithm for detecting a locally stable predicate can be used to efficiently detect a stable predicate that is a monotonic function of other locally stable predicates.