Liveness-Preserving Simulation Relations

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 inproof obligation of the form: if a concrete and abstract execution “correspond” via the on, 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. To define liveness, we generalize the...

• Type: Conference
• Year: 1999
• Where: PODC
• Authors: Paul C. Attie
• Keywords: Abstract Execution, Distributed And Parallel Computing, Liveness Properties, PODC 1999, Reasoning