In formal verification, 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.
The first step produces a generalized Büchi automaton (GBA) from a LTL formula.
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.
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.
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.
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.
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.
create_graph is the entry function, which expects the input formula f in the negation normal form.
It calls recursive function expand that builds the graph by populating global variables Nodes, Incoming, Now, and Next.
Incoming of a node may also contain a special symbol init that is used in the final automaton construction to decide the set of initial states.
Next(q) denotes the set of formulas that must be satisfied by the rest of the input word if the automaton is currently at the next node(state) after q.
If the curr is empty then at line 2 the if condition checks if there already exists a state q' with same set of expanded formulas.
In the case curr is not empty, then we have more formulas to expand and control jumps from line 1 to 12.
The algorithmic construction ensures the correctness without the need of all the true formulas to be present in a node label.