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
    0 references
    0 references
    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
    0 references
    safety
    0 references
    liveness
    0 references
    Buechi automaton
    0 references
    0 references
    0 references