Buchi Automata, And Verifying Safety And Liveness

B¨uchi automata, and Verifying Safety and Liveness: B¨uchi automata are automata whose languages contain only infinite strings. The ability to model infinite strings is important because of the fact that all bugs can be described in the context of infinite executions. We now elaborate on these potentially unusual sounding, but rather simple, ideas. Broadly speaking, all errors (bugs) in reactive systems can be classified into two classes: safety (property) violations and liveness (property) violations.

• Safety violations are bugs that can be presented and explained to someone in the form of finite executions (finite sequence of states) ending in erroneous states. Some examples of systems that exhibit safety violations are the following:

− two people who, following a faulty protocol, walk opposite in a narrow dark corridor and collide;
− an elevator which, when requested to go to the 13th floor, proceeds to do so with its doors wide open;
− a process P which acquires a lock L and dies, thus permanently blocking another process, say Q, from acquiring L.

All finite executions of the form s1 . . . sk can be modeled as infinite executions that infinitely repeat the last state, namely s1s2 . . . (sk)ω. Modeling finite executions as infinite executions allows one to employ B¨uchi automata.

• Liveness violations are bugs that can be presented and explained to someone only in the form of an infinite execution in which a desired state never occurs. In practice, liveness violations are those that end in a bad “lasso” shaped cyclic execution path which does not contain the desired state. Examples of liveness violations are:

− two people who, following a faulty protocol, engage in a perpetual ‘dance,’ trying to pass each other in a narrow well-lit corridor;
− an elevator that permanently oscillates between the 12th and 14th floors when requested to go to the 13th floor;
− A process P which acquires a lock L precisely before another process Q tries to acquire it, and releases the lock precisely after Q has decided to back off and retry; this sequence repeats infinitely.

All infinite executions in finite state systems can be cast into the form s1s2 . . . (sj . . . sk)ω where the reachable bad cycle (sj . . . sk)ω is called the “lasso.” Liveness verification of finite state systems reduces to finding one of these reachable lassos.

Model checking methods based on the use of B¨uchi automata help detect safety and liveness violations through language containment of B¨uchi automata.