On the refinement of liveness properties of distributed systems

We present a new approach, based on simulation relations, for reasoning about liveness properties of distributed systems. Our contribution consists of (1) a formalism for defining liveness properties, (2) a proof method for liveness properties based on that formalism, and (3) two expressive completeness results: our formalism can express any liveness property which satisfies a natural "robustness" condition; and also any liveness property at all, provided that history variables can be used. To define liveness, we generalize complemented-pairs (Streett) automata to an infinite state-space, and an infinite number of complemented-pairs. Our proof method provides two techniques: one for refining liveness properties across levels of abstraction, and another for refining liveness properties within a level of abstraction. The first is based on extending simulation relations so that they relate the liveness properties of an abstract automaton to those of a concrete automaton. The second is based on a deductive method for inferring new liveness properties of an automaton from already established liveness properties of the same automaton. This deductive method is diagrammatic, and is based on constructing "lattices" of liveness properties.