On the Refinement of Liveness Properties of Distributed Systems

TL;DR

This paper introduces a novel simulation-based approach for verifying liveness properties in distributed automata, enabling reasoning over finite execution fragments and broadening the scope of expressible properties.

Contribution

It provides a formalism and proof method for liveness verification that simplifies reasoning and extends expressiveness compared to existing methods.

Findings

Formalism can express all liveness properties satisfying robustness.

Proof method reduces reasoning to finite execution fragments.

Achieves expressive completeness with history variables.

Abstract

We present a new approach for reasoning about liveness properties of distributed systems, represented as automata. Our approach is based on simulation relations, and requires reasoning only over finite execution fragments. Current simulation-relation based methods for reasoning about liveness properties of automata require reasoning over entire executions, since they involve a proof obligation of the form: if a concrete and abstract execution ``correspond'' via the simulation, and the concrete execution is live, then so is the abstract execution. 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: firstly, our formalism can express any liveness property which satisfies a natural ``robustness'' condition, and secondly, our formalism can express any liveness property at all, provided that history variables can be used