In formal verification (a methodology from computer science), finite state model checking needs to find a Büchi automaton (BA) equivalent to a given linear temporal logic (LTL) formula, i.e., such that the LTL formula and the BA recognize the same ω-language. There are algorithms that translate an LTL formula to a BA. This transformation is normally done in two steps. The first step produces a generalized Büchi automaton (GBA) from a LTL formula. The second step translates this GBA into a BA, which involves a relatively easy construction. Since LTL is strictly less expressive than BA, the reverse construction is not always possible. The algorithms for transforming LTL to GBA differ in their construction strategies but they all have a common underlying principle, i.e., each state in the constructed automaton represents a set of LTL formulas that are expected to be satisfied by the remaining input word after occurrence of the state during a run.
Transformation from LTL to GBA Here, two algorithms are presented for the construction. The first one provides a declarative and easy-to-understand construction. The second one provides an algorithmic and efficient construction. Both the algorithms assume that the input formula f is constructed using the set of propositional variables AP and f is in negation normal form. For each LTL formula f' without ¬ as top symbol, let neg(f') = ¬f' and neg(¬f') = f'. For a special case f'=true, let neg(true) = false.
Declarative construction Before describing the construction, we need to present a few auxiliary definitions. For an LTL formula f, Let cl( f ) be the smallest set of formulas that satisfies the following conditions:
cl( f ) is closure of sub-formulas of f under neg. Note that cl( f ) may contain formulas that are not in negation normal form. The subsets of cl( f ) are going to serve as states of the equivalent GBA. We aim to construct the GBA such that if a state corresponds to a subset M ⊆ cl( f ) then the GBA has an accepting run starting from the state for a word if and only if the word satisfies every formula in M and violates every formula in cl( f ) \ M. For this reason, we will not consider each formula set M that is clearly inconsistent or subsumed by a strict superset M' such that M and M' are equiv-satisfiable. A set M ⊆ cl( f ) is maximally consistent if it satisfies the following conditions:
Let cs( f ) be the set of maximally consistent subsets of cl( f ). We are going to use only cs( f ) as the states of GBA.
GBA construction An equivalent GBA to f is A= ({init}∪cs( f ), 2AP, Δ,{init},F), where
Δ = Δ1 ∪ Δ2 (M, a, M') ∈ Δ1 iff ( M' ∩AP ) ⊆ a ⊆ {p ∈ AP | ¬p ∉ M' } and: X f1 ∈ M iff f1 ∈ M'; f1 U f2 ∈ M iff f2 ∈ M or ( f1 ∈ M and f1 U f2 ∈ M' ); f1 R f2 ∈ M iff f1 ∧ f2 ∈ M or ( f2 ∈ M and f1 R f2 ∈ M' ) Δ2 = { (init, a, M') | ( M' ∩AP ) ⊆ a ⊆ {p ∈ AP | ¬p ∉ M' } and f ∈ M' } For each f1 U f2 ∈ cl( f ), {M ∈ cs( f ) | f2 ∈ M or ¬(f1 U f2) ∈ M } ∈ F The three conditions in definition of Δ1 ensure that any run of A does not violate semantics of the temporal operators. Note that F is a set of sets of states. The sets in F are defined to capture a property of operator U that can not be verified by comparing two consecutive states in a run, i.e., if f1 U f2 is true in some state then eventually f2 is true at some state later.
Gerth et al. algorithm The following algorithm is due to Gerth, Peled, Vardi, and Wolper. A verified construction mechanism of this by Schimpf, Merz and Smaus is also available. The previous construction creates exponentially many states upfront and many of those states may be unreachable. The following algorithm avoids this upfront construction and has two steps. In the first step, it incrementally constructs a directed graph. In the second step, it builds a labeled generalized Büchi automaton (LGBA) by defining nodes of the graph as states and directed edges as transitions. This algorithm takes reachability into account and may produce a smaller automaton but the worst-case complexity remains the same. The nodes of the graph are labeled by sets of formulas and are obtained by decomposing formulas according to their Boolean structure, and by expanding the temporal operators in order to separate what has to be true immediately from what has to be true from the next state onwards. For example, let us assume that an LTL formula f1 U f2 appears in the label of a node. f1 U f2 is equivalent to f2 ∨ ( f1 ∧ X(f1 U f2) ). The equivalent expansion suggests that f1 U f2 is true in one of the following two conditions.
f1 holds at the current time and (f1 U f2) holds at the next time step, or f2 holds at the current time step The two cases can be encoded by creating two states (nodes) of the automaton and the automaton may non-deterministically jump to either of them. In the first case, we have offloaded a part of burden of proof in the next time step therefore we also create another state (node) that will carry the obligation for next time step in its label. We also need to consider temporal operator R that may cause such case split. f1 R f2 is equivalent to ( f1 ∧ f2) ∨ ( f2 ∧ X(f1 R f2) ) and this equivalent expansion suggests that f1 R f2 is true in one of the following two conditions.
f2 holds at the current time and (f1 R f2) holds at the next time step, or ( f1 ∧ f2) holds at the current time step. To avoid many cases in the following algorithm, let us define functions curr1, next1 and curr2 that encode the above equivalences in the following table.
We have also added disjunction case in the above table since it also causes a case split in the automaton. Following are the two steps of the algorithm.
… excerpt ends here. Continue reading the full article.
