Recognizing Safety and Liveness.
CORNELL UNIV ITHACA NY DEPT OF COMPUTER SCIENCE
Pagination or Media Count:
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.
- Computer Programming and Software