On the refinement of liveness properties of distributed systems

Research output: Contribution to journalArticlepeer-review

2 Scopus citations


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.

Original languageEnglish (US)
Pages (from-to)1-46
Number of pages46
JournalFormal Methods in System Design
Issue number1
StatePublished - Aug 2011
Externally publishedYes


  • Automata
  • Liveness
  • Proof diagrams
  • Refinement
  • Simulation relations

ASJC Scopus subject areas

  • Software
  • Theoretical Computer Science
  • Hardware and Architecture


Dive into the research topics of 'On the refinement of liveness properties of distributed systems'. Together they form a unique fingerprint.

Cite this