A formal characterization for safety properties and liveness properties is given in terms of the structure of the Buchi 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. © 1987 Springer-Verlag.
CITATION STYLE
Alpern, B., & Schneider, F. B. (1987). Recognizing safety and liveness. Distributed Computing, 2(3), 117–126. https://doi.org/10.1007/BF01782772
Mendeley helps you to discover research relevant for your work.