On characterization of safety and liveness properties in temporal logic

Abstract

In the verification of concurrent programs two kinds of properties are of primary importance and have been extensively investigated ([3]): safety properties and liveness properties. Safety properties assert that something bad never happens while liveness properties assert that something good will eventually happen. In this paper we investigate the possibility of syntactically characterizing safety properties and liveness properties in temporal logic.