Recognizing safety and liveness (Q1100884)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | Recognizing safety and liveness |
scientific article |
Statements
Recognizing safety and liveness (English)
0 references
1987
0 references
A formal characterization for safety properties and liveness properties is given in terms of the structure of the Buechi automaton that specifies the property. The characterizations permit a property to be decomposed into a safety property and a liveness property whose conjunction is the original. The characterizations also give insight into techniques required to prove a large class of safety and liveness properties.
0 references
safety
0 references
liveness
0 references
Buechi automaton
0 references
0 references