Liveness in timed and untimed systems
type: Item
instance of: scholarly article
title: Liveness in timed and untimed systems
zbMATH Open document ID: 0917.68152
author: Roberto Segala
author: Rainer Gawlick
author: Jørgen Søgaard-Andersen
author: Nancy Lynch
published in: Information and Computation
publication date: 1998-11-10T00:00:00Z
review text: When proving the correctness of algorithms in 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 verification of general liveness properties on the basis of existing verification techniques. Our models include a notion of receptiveness which extends the idea of receptiveness of other existing formalisms, and enables the use of compositional verification techniques. The presentation includes an embedding of the untimed model into the timed model which preserves all the 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. \(\copyright\) Academic Press.
reviewed by: Luisa Gargano
Mathematics Subject Classification ID: 68Q45
zbMATH DE Number: 1220699
zbMATH Keywords: safety
zbMATH Keywords: liveness
zbMATH Keywords: receptiveness
MaRDI profile type: Publication
full work available at URL: inco.1997.2671
OpenAlex ID: W2016014698
cites work: The existence of refinement mappings
cites work: Defining liveness
cites work: Testing equivalences for processes
cites work: Q3777424
cites work: A proof of the Kahn principle for input/output automata
cites work: Forward and backward simulations. I. Untimed Systems
cites work: Forward and backward simulations. II: Timing-based systems
cites work: A note on fairness in I/O automata
cites work: Quiescence, fairness, testing, and the notion of implementation
DOI: 10.1006/INCO.1997.2671
description: scientific article; zbMATH DE number 1220699