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.
No takes yet. Share an insight, caveat, or question.
A. Prasad Sistla (1994) studied this question.
Synapse has enriched 5 closely related papers on similar clinical questions. Consider them for comparative context: