Recognizing Safety and Liveness.
Abstract
Informally, a safety property stipulates that some 'bad thing' does not happen during execution of a program and a liveness property stipulates that some 'good thing' does happen (eventually). Distinguishing between safety and liveness properties has merit because proving that a program satisfies a safety property involves and invariance argument while proving that a program satisfies a liveness property involves a well-foundness argument. Thus, knowing whether a property is safety or liveness suffices for deciding on a technique to prove that the propterty holds. Formal characterizations for safety properties and liveness properties are given in terms of the structure of the Buchi automation that specifies the property. The characterizations permit a property to be decomposed into a safety property and a liveness property whose conjuction is the orginal. The characterizations also give insight into techniques required to prove safety and liveness properties. Keywords: Concurrent programs; Safety; Liveness; Property recognizers; Buchi automata; Logic.
Document Details
- Document Type
- Technical Report
- Publication Date
- Jan 01, 1986
- Accession Number
- ADA164783
Entities
People
- Bowen Alpern
- Fred B. Schneider
Organizations
- Cornell University