Liveness in Timed and Untimed Systems

9 years 7 months ago
Liveness in Timed and Untimed Systems
When provingthe correctness of algorithmsin distributed systems, one generally considers safety conditions and liveness conditions. The Input Output I O automaton model and its timed version have been used successfully, but have focused on safety conditions and on a restricted form of liveness called fairness. In this paper we develop a new I O automaton model, and a new timed I O automaton model, that permit the veri cation of general liveness properties on the basis of existing veri cation techniques. Our models include a notion of environment-freedom which generalizes the idea of receptiveness of other existing formalisms, and enables the use of compositional veri cation techniques. The presentation includes an embedding of the untimed model into the timed model which preserves allthe interesting attributes of the untimed model. Thus, our models constitute a coordinated framework for the description of concurrent and distributed systems satisfying general liveness properties.
Rainer Gawlick, Roberto Segala, Jørgen F. S
Added 09 Aug 2010
Updated 09 Aug 2010
Type Conference
Year 1994
Authors Rainer Gawlick, Roberto Segala, Jørgen F. Søgaard-Andersen, Nancy A. Lynch
Comments (0)