Safety, liveness and fairness in temporal logic
- 1 September 1994
- journal article
- Published by Association for Computing Machinery (ACM) in Formal Aspects of Computing
- Vol. 6 (5) , 495-511
- https://doi.org/10.1007/bf01211865
Abstract
In this paper we present syntactic characterization of temporal formulas that express various properties of interest in the verification of concurrent programs. Such a characterization helps us in choosing the right techniques for proving correctness with respect to these properties. The properties that we consider include safety properties, liveness properties and fairness properties. We also present algorithms for checking if a given temporal formula expresses any of these properties.Keywords
This publication has 17 references indexed in Scilit:
- Completing the temporal pictureTheoretical Computer Science, 1991
- Recognizing safety and livenessDistributed Computing, 1987
- Modalities for model checking: branching time logic strikes backScience of Computer Programming, 1987
- Safety without stutteringInformation Processing Letters, 1986
- Automatic verification of finite-state concurrent systems using temporal logic specificationsACM Transactions on Programming Languages and Systems, 1986
- Defining livenessInformation Processing Letters, 1985
- The complexity of propositional linear temporal logicsJournal of the ACM, 1985
- Can message buffers be axiomatized in linear temporal logic?Information and Control, 1984
- Alternative semantics for temporal logicsTheoretical Computer Science, 1983
- Proving Liveness Properties of Concurrent ProgramsACM Transactions on Programming Languages and Systems, 1982