×

zbMATH — the first resource for mathematics

Defining liveness. (English) Zbl 0575.68030
A formal definition for liveness properties is proposed. It is argued that this definition captures the intuition that liveness properties stipulate that ’something good’ eventually happens during execution. A topological characterization of safety and liveness is given. Every property is shown to be the intersection of a safety property and a liveness property.

MSC:
68N25 Theory of operating systems
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Alpern, B.; Schneider, F.B.; Demers, A.J., A note on safety without stuttering, (1985), In preparation
[2] Lamport, L., Proving the correctness of multiprocess programs, IEEE trans. software engineering, SE-3, 2, 125-143, (1977) · Zbl 0349.68006
[3] Lamport, L., Basic concepts, ()
[4] Lamport, L.; Schneider, F.B., The ‘hoare logic’ of CSP and all that, ACM trans. programming languages and systems, 6, 2, 281-296, (1984) · Zbl 0536.68017
[5] Manna, Z.; Pnueli, A., Temporal verification of concurrent programs: the temporal framework for concurrent programs, () · Zbl 0481.68019
[6] Manna, Z.; Pnueli, A., Verification of concurrent programs: proving eventualities by well-founded ranking, ()
[7] Owicki, S.; Lamport, L., Proving liveness properties of concurrent programs, ACM trans. programming languages and systems, 4, 3, 455-495, (1982) · Zbl 0483.68013
[8] G. Plotkin, Private communication, 1983.
[9] G. Plotkin, Private communication, 1984.
[10] Sistla, A.P., Characterization of safety and liveness properties in temporal logic, (1984), Univ. of Massachusetts at Amherst MA, Extended abstract
[11] Smyth, M.B., Power domains and predicate transformers: A topological view, (), 662-675 · Zbl 0533.68018
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.