Generalized Büchi automaton
Encyclopedia
In automata theory
, generalized Büchi automaton (GBA) 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 often. Generalized büchi automata (GBA) is equivalent in expressive power with Büchi automata; a transformation is given here.
In formal verification
,
the model checking
method needs to obtain an automaton from a LTL
formula that specifies the program property.
There are algorithms
that translate a LTL
formula
into a GBA
for this purpose.
The notion of GBA was introduced specifically for this translation.
A accepts exactly those runs in which the set of infinitely often occurring states contains at least a state from each F1,...,Fn.
For more comprehensive formalism see also ω-automaton
.
LGBA was introduced by Gerth et al.
Formally, a labeled generalized Büchi automaton is a tuple A = (Q, Σ, L, Δ,Q0,{F1,...,Fn}) that consists of the following components:
Let w = a1a2 ... be an ω-word over the alphabet Σ.
r1,r2, ... is a run of A on the word w if
r1 ∈ Q0 and for each i ≥ 0,
ri+1 ∈ Δ(ri) and ai ∈ L(ri).
A accepts exactly those runs in which the set of infinitely often occurring states contains at least a state from each F1,...,Fn.
To obtain the non-labeled version, the labels are moved from the nodes to the incoming transitions.
Automata theory
In theoretical computer science, automata theory is the study of abstract machines and the computational problems that can be solved using these machines. These abstract machines are called automata...
, generalized Büchi automaton (GBA) is a variant of 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...
. 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 often. Generalized büchi automata (GBA) is equivalent in expressive power with Büchi automata; a transformation is given here.
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 an automaton from a LTL
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...
formula that specifies the program property.
There are algorithms
Linear temporal logic to Büchi automaton
In formal verification,the model checking method needs to obtain a Büchi automaton from a Linear temporal logic formula.There are algorithms that translates a LTL formula to an equivalent BA...
that translate a LTL
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...
formula
into a GBA
for this purpose.
The notion of GBA was introduced specifically for this translation.
Formal definition
Formally, a generalized Büchi automaton is a tuple A = (Q,Σ,Δ,Q0,{F1,...,Fn}) that consists of the following components:- Q is a finite set. The elements of Q are called the states of A.
- Σ is a finite set called the alphabet of A.
- Δ: Q × Σ → 2Q is a function, called the transition relation of A.
- Q0 is a subset of Q, called the initial states.
- {F1,...,Fn} is the acceptance condition, where for each 1≤i≤n, Fi ⊆ Q .
A accepts exactly those runs in which the set of infinitely often occurring states contains at least a state from each F1,...,Fn.
For more comprehensive formalism see also ω-automaton
Ω-automaton
In automata theory, a branch of theoretical computer science, an ω-automaton is a deterministic or nondeterministic automaton that runs on infinite, rather than finite, strings as input...
.
Labeled generalized Büchi automaton
Labeled generalized Büchi automaton(LGBA) is another variation in which input is associated as labels with the states rather than with the transitions.LGBA was introduced by Gerth et al.
Formally, a labeled generalized Büchi automaton is a tuple A = (Q, Σ, L, Δ,Q0,{F1,...,Fn}) that consists of the following components:
- Q is a finite set. The elements of Q are called the states of A.
- Σ is a finite set called the alphabet of A.
- L: Q → 2Σ is a function, called the labeling function of A.
- Δ: Q → 2Q is a function, called the transition relation of A.
- Q0 is a subset of Q, called the initial states.
- {F1,...,Fn} is the acceptance condition, where for each 1≤i≤n, Fi ⊆ Q .
Let w = a1a2 ... be an ω-word over the alphabet Σ.
r1,r2, ... is a run of A on the word w if
r1 ∈ Q0 and for each i ≥ 0,
ri+1 ∈ Δ(ri) and ai ∈ L(ri).
A accepts exactly those runs in which the set of infinitely often occurring states contains at least a state from each F1,...,Fn.
To obtain the non-labeled version, the labels are moved from the nodes to the incoming transitions.