Safety, liveness and fairness in temporal logic
Formal Aspects of Computing1994Vol. 6(5), pp. 495–511
Citations Over Time
Abstract
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.