In formal verification

Formal verification

In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics .- Usage :Formal verification can be...

,
the model checking

Model checking

In computer science, model checking refers to the following problem:Given a model of a system, test automatically whether this model meets a given specification....

 method needs to obtain a Büchi automaton

Büchi automaton

In computer science and automata theory, a Büchi automaton is a type of ω-automaton, which extends a finite automaton to infinite inputs. It accepts an infinite input sequence iff there exists a run of the automaton that visits one of the final states infinitely often. Büchi automata recognize the...

(BA) from a Linear temporal logic

Linear temporal logic

In logic, Linear temporal logic is a modal temporal logic with modalities referring to time. In LTL, one can encode formulae about the future of paths such as that a condition will eventually be true, that a condition will be true until another fact becomes true, etc. It is a fragment of the more...

(LTL) formula.
There are algorithms that translates a LTL formula to an equivalent BA
, i.e., the LTL formula and the BA recognizes the same ω-language.
This transformation is normally done in two steps.
The first step produces a generalized Büchi automaton

Generalized Büchi automaton

In automata theory, generalized Büchi automaton is a variant of Büchi automaton. The difference with the Büchi automaton is its accepting condition, i.e., a set of sets of states. A run is accepted by the automaton if it visits at least one state of every set of the accepting condition infinitely...

(GBA) from a LTL formula.
The second step translates this GBA into a BA, which involves relatively
easy construction.
Since LTL is strictly less expressive than BA, the reverse construction is not possible.

There are multiple algorithm for transforming LTL to GBA.
These algorithms differ in their construction strategies but they
all have 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', 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 a LTL formula f, Let cl( f ) be a smallest set of formulas that satisfies the following conditions:

true ∈ cl( f ) f ∈ cl( f ) if f1 ∈ cl( f ) then neg(f1) ∈ cl( f ) if X f1 ∈ cl( f ) then f1 ∈ cl( f )

if f1 ∧ f2 ∈ cl( f ) then f1,f2 ∈ cl( f ) if f1 ∨ f2 ∈ cl( f ) then f1,f2 ∈ cl( f ) if f1 U f2 ∈ cl( f ) then f1,f2 ∈ cl( f ) if f1 R f2 ∈ cl( f ) then f1,f2 ∈ cl( f )

cl( f ) is closure of sub-formulas of f under negation.
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 want that a state labelled by a subset M ⊂ cl( f ) will accept a word iff it satisfies every formula in M and violates every formula in cl( f )/M.
For this reason,
we will exclude each formula subset M that is clearly inconsistent
or subsumed by a strictly super set M' such that M and M' are equiv-satisfiable.
A set M ⊂ cl( f ) is consistent if it satisfies the following conditions:

true ∈ M f1 ∈ M iff ¬f1 ∉ M

f1 ∧ f2 ∈ M iff f1 ∈ M and f2 ∈ M f1 ∨ f2 ∈ M iff f1 ∈ M or f2 ∈ M

Let cs( f ) be set of consistent subsets of cl( f ).
We are going to use only cs( f ) as the states of GBA.

An equivalent GBA

Generalized Büchi automaton

In automata theory, generalized Büchi automaton is a variant of Büchi automaton. The difference with the Büchi automaton is its accepting condition, i.e., a set of sets of states. A run is accepted by the automaton if it visits at least one state of every set of the accepting condition infinitely...

 to f is A= ({init}∪cs( f ), 2^AP, Δ,{init},F), where

• Δ = Δ₁ ∪ Δ₂
  • (M, a, M') ∈ Δ₁ iff ( M' ∩AP ) ⊆ a ⊆ {p ∈ AP | ¬p ∉ M' } and:
    • X f₁ ∈ M iff f₁ ∈ M';
    • f₁ U f₂ ∈ M iff f₂ ∈ M or ( f₁ ∈ M and f₁ U f₂ ∈ M' );
    • f₁ R f₂ ∈ M iff f₁ ∧ f₂ ∈ M or ( f₂ ∈ M and f₁ R f₂ ∈ M' )
  • Δ₂ = { (init, a, M') | ( M' ∩AP ) ⊆ a ⊆ {p ∈ AP | ¬p ∉ M' } and f ∈ M' }
• For each f₁ U f₂ ∈ cl( f ),  {M ∈ cs( f ) | f₂ ∈ M or ¬(f₁ U f₂) ∈ M } ∈ F

The three conditions in definition of Δ₁ ensure that any run of A does not violate semantics of the temporal operators.
Note that F is a set of sets.
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 f₁ U f₂ is true in some state then eventually f₂ is true at some state later.

Proof of correctness of the above construction

Let ω-word w= a₁, a₂,... over alphabet 2^AP. Let wⁱ = a_i, a_i+1,... .
Let M_w = { f' ∈ cl(f) | w f' }, which we call satisfying set.
Due to the definition of cs(f), M_w ∈ cs(f).
We can define a sequence
ρ_w = init, M_w¹, M_w²,... .
Due to the definition of A,
if w f then ρ_w must be an accepting run of A over w.

Conversely, lets assume A accepts w.
Let ρ = init, M₁, M₂,... be a run of A over w.
The following theorem completes the rest of the correctness proof.

Theorem 1: For all i > 0, M_wⁱ = M_i.

Proof: The proof is by induction on the structure of f' ∈ cl(f).

• Base cases:
  • f' = true. By definitions, f' ∈ M_wⁱ and f' ∈ M_i.
  • f' = p. By definition of A, p ∈ M_i iff p ∈ a_i iff p ∈ M_wⁱ.
• Induction steps:
  • f' = f₁ ∧ f₂. Due to the definition of consistent sets, f₁ ∧ f₂ ∈ M_i iff f₁ ∈ M_i and f₂ ∈ M_i. Due to induction hypothesis, f₁ ∈ M_wⁱ and f₂ ∈ M_wⁱ. Due to definition of satisfying set, f₁ ∧ f₂ ∈ M_wⁱ.
  • f' = ¬f₁, f' = f₁ ∨ f₂, f' = X f₁ or f' = f₁ R f₂. The proofs are very similar to the last one.
  • f' = f₁ U f₂. The proof of equality is divided in two entailment proofs.
    • If f₁ U f₂ ∈ M_i, then f₁ U f₂ ∈ M_wⁱ. By the definition of the transitions of A, we can have the following two cases.
      • f₂ ∈ M_i. By induction hypothesis, f₂ ∈ M_wⁱ. So, f₁ U f₂ ∈ M_wⁱ.
      • f₁ ∈ M_i and f₁ U f₂ ∈ M_i+1. And due to the acceptance condition of A, there is at least one index j ≥ i such that f₂ ∈ M_j. Let j' be the smallest of these indices. We prove the result by induction on k = {j',j'-1,...,i+1,i}. If k = j', then f₂ ∈ M_k, we apply same argument as in the case of f₂ ∈ M_i. If i ≤ k < j', then f₂ ∉ M_k, and so f₁ ∈ M_k and f₁ U f₂ ∈ M_k+1. Due to induction hypothesis on f', we have f₁ ∈ M_w^k. Due to induction hypothesis on indices, we also have f₁ U f₂ ∈ M_w^k+1. Due to definition of the semantics of LTL, f₁ U f₂ ∈ M_w^k.
    • If f₁ U f₂ ∈ M_wⁱ, then f₁ U f₂ ∈ M_i. Due to the LTL semantics, we can have the following two cases.
      • f₂ ∈ M_wⁱ. By induction hypothesis, f₂ ∈ M_i. So, f₁ U f₂ ∈ M_i.
      • f₁ ∈ M_wⁱ and f₁ U f₂ ∈ M_wⁱ⁺¹. Due to the LTL semantics, there is at least one index j ≥ i such that f₂ ∈ M_j. Let j' be the smallest of these indices. Proceed now as in proof of the converse entailment.

Due to the above theorem, M_w¹ = M₁. Due to the definition of the transitions of A, f ∈ M₁. Therefore, f ∈ M_w¹ and w f.

Gerth et al. algorithm

The following algorithm is due to Gerth, Peled, Vardi

Moshe Y. Vardi

Moshe Ya'akov Vardi is a Professor of Computer Science at Rice University, USA. He is the Karen Ostrum George Professor in Computational Engineering, Distinguished Service Professor, and Director of the Computer and Information Technology Institute...

, and Wolper.
The above construction creates exponentially many states upfront and many of those states may be unreachable.
The following algorithm has two steps.
In step one, it incrementally constructs a directed graph stored in a tableaux.In step two, it builds an 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 on. For example, let us assume that an LTL formula f₁ U f₂ appears in the label of a node.
f₁ U f₂ is equivalent to f₂ ∨ ( f₁ ∧ X(f₁ U f₂) ).
The equivalent expansion suggests that f₁ U f₂ is true in one of the following two conditions.

1. f₁ holds in the current time and (f₁ U f₂) holds in the next time step, or
2. f₂ holds in the current time step

We can encode this logic 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.
f₁ R f₂ is equivalent to ( f₁ ∧ f₂) ∨ ( f₂ ∧ X(f₁ R f₂) )
and this equivalent expansion suggests that f₁ R f₂ is true in one of the following two conditions.

1. f₂ holds in the current time and (f₁ R f₂) holds in the next time step, or
2. ( f₁ ∧ f₂) holds in the current time step.

To avoid many cases in the following algorithm, let us define functions new1, next1 and new2 that encode the above equivalences in the following table.

f	new1(f)	next1(f)	new2(f)
f1 U f2	{f1}	{ f1 U f2 }	{f2}
f1 R f2	{f2}	{ f1 R f2 }	{f1,f2}
f1 ∨ f2	{f2}	∅	{f1}

We have also added disjunction case in the above table since it also cause a case split in the automaton.

Following are the two steps of the algorithm.

Step 1. create_graph

In the following box, we present the first part of the algorithm that builds a directed graph. 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.
The set Nodes stores the set of nodes in the graph. The map Incoming maps each node of Nodes to a subset of Nodes ∪ {init}, which defines the set of incoming edges.
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.
Now and Next map each node of Nodes to a set of LTL formulas.
For a node q, Now(q) denotes the set of formulas that must be satisfied by the rest of the input word if the automaton is currently at node(state) q.
Next(q) denotes the set of 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.

typedefs
LTL: LTL formulas
LTLSet: Sets of LTL formulas
NodeSet: Sets of graph nodes ∪ {init}

globals
Nodes : set of graph nodes := ∅
Incoming: Nodes → NodeSet := ∅
Now : Nodes → LTLSet := ∅
Next : Nodes → LTLSet := ∅

function create_graph(LTL f){
expand({f}, ∅, ∅, {init} )
return (Nodes, Now, Incoming)
}

function expand(LTLSet new, LTLSet old, LTLSet next, NodeSet incoming){
1: if new = ∅ then
2: if ∃q ∈ Nodes: Next(q)=next ∧ Now(q)=old then
3: Incoming(q) := Incoming(q) ∪ incoming
4: else
5: q := new_node
6: Nodes := Nodes ∪ {q}
7: Incoming(q) := incoming
8: Now(q) := old
9: Next(q) := next
10: expand(Next(q), ∅, ∅, {q})
11: else
12: f ∈ new
13: new := new\{f}
14: old := old ∪ {f}
15: match f with
16: | true, false, p, or ¬p, where p ∈ AP →
17: if f = false ∨ neg(f) ∈ old then
18: skip
19: else
20: expand(new, old, next, incoming)
21: | f₁ ∧ f₂ →
22: expand(new ∪ {f₁,f₂}, old, next, incoming)
23: | X g →
24: expand(new, old, next ∪ {g}, incoming)
25: | f₁ ∨ f₂, f₁ U f₂, or f₁ R f₂ →
26: expand(new ∪ (new1(f)/old), old, next ∪ next1(f), incoming)
27: expand(new ∪ (new2(f)/old), old, next, incoming)
28: return
}

The code of expand is labelled with line numbers for easy reference.
Each call to expand aims to add a node and its successors nodes in the graph.
The parameters of the call describes a potential new node.
The first parameter new contains the set of formulas that are yet to be expanded. The second parameter old contains the set of formulas that are already expanded.
The third parameter next is the set of the formula using which successor node will be created.
The fourth parameter incoming defines set of incoming edges when the node is added to the graph.
At line 1, the if condition checks if new contains any formula to be expanded.
If the new is empty then at line 2 the if condition checks if there already exists a state q' with same set of expanded formulas.
If that is the case then then we do not add a redundant node, but we add parameter incoming in Incoming(q') at line 3.
Otherwise, we add a new node q using the parameters at lines 5--9
and we start expanding a successor node of q using next(q) as its unexpanded
set of formulas at line 10.
In the case new is not empty then we have more formulas to expand and
control jumps from line 1 to 12.
At lines 12--14, a formula f from new is selected and moved to old.
Depending on structure of f, rest of the function executes.
If f is a literal then expansion continues at line 20, but if old already contains
neg(f) or f=false then old contains an inconsistent formula and we discard this node by not making any recursive all at line 18.
If f = f₁ ∧ f₂ then f₁ and f₂ are added to new and a recursive call is made for further expansion at line 22.
If f = X f₁ then f₁ is added to next for the successor of the current node under consideration at line 24.
If f = f₁ ∨ f₂, f = f₁ U f₂, or f = f₁ R f₂ then the current node is divided into two nodes
and for each node a recursive call is made. For the recursive calls, new and next are modified using functions new1, next1, and new2 that were defined in the above table.
Step 2. LGBA construction
Let (Nodes, Now, Incoming) = create_graph(f).
An equivalent LGBA to f is A=(Nodes, 2^AP, L, Δ, Q₀, F), where

• L = { (q,a) | q ∈ Nodes and (Now(q) ∩ AP) ⊆ a ⊆ {p ∈ P | ¬p ∉ Now(q) } }
• Δ = {(q,q')| q,q' ∈ Nodes and q ∈ Incoming(q') }
• Q₀ = { q ∈ Nodes | init ∈ Now(q) }
• F = { { q ∈ Nodes | f₂ ∈ Now(q) or (f₁ U f₂) ∉ Now(q) } | f₁ U f₂ ∈ cl( f ) }

Note that node labels in the algorithmic construction does not not contain negation of sub-formulas of f. In the declarative construction a node has the set of formulas that are expected to be true. The algorithmic construction ensures the correctness without the need of all the true formulas to be present in a node label.