Generalized Büchi automaton

<h2 id="formal-definition">Formal definition</h2>
Formally, a generalized Büchi automaton is a tuple A = (Q,Σ,Δ,Q0, 
 
 
 
 
 
 F
 
 
 
 
 {\displaystyle {\cal {F}}}
 
) that consists of the following components:

<ul><li>Q is a <a href="/facts/Finite_set/za1newlP">finite set</a>. The elements of Q are called the states of A.</li>
<li>Σ is a finite set called the alphabet of A.</li>
<li>Δ: Q × Σ → 2Q is a function, called the transition relation of A.</li>
<li>Q0 is a subset of Q, called the initial states.</li>
<li>
 
 
 
 
 
 F
 
 
 
 
 {\displaystyle {\cal {F}}}
 
 is the acceptance condition, which is made up of zero or more accepting sets. Each accepting set 
 
 
 
 
 F
 
 i
 
 
 ∈
 
 
 F
 
 
 
 
 {\displaystyle F_{i}\in {\cal {F}}}
 
 is a subset of Q.</li></ul>
A accepts exactly those runs in which the set of infinitely often occurring states contains at least one state from each accepting set 
 
 
 
 
 F
 
 i
 
 
 ∈
 
 
 F
 
 
 
 
 {\displaystyle F_{i}\in {\cal {F}}}
 
. Note that there may be no accepting sets, in which case any infinite run trivially satisfies this property.
For more comprehensive formalism see also <a href="/facts/%CE%A9-automaton/wXtY3hVu">ω-automaton</a>.

<h2 id="labeled-generalized-bchi-automaton">Labeled generalized Büchi automaton</h2>
Labeled generalized Büchi automaton is another variation in which input is matched to labels on the states rather than on the transitions. It was introduced by Gerth et al.<a class="footnote-ref" id="fnref:5" href="#fn:5">5</a>
Formally, a labeled generalized Büchi automaton is a tuple A = (Q, Σ, L, Δ,Q0,
 
 
 
 
 
 F
 
 
 
 
 {\displaystyle {\cal {F}}}
 
) that consists of the following components:

<ul><li>Q is a <a href="/facts/Finite_set/za1newlP">finite set</a>. The elements of Q are called the states of A.</li>
<li>Σ is a finite set called the alphabet of A.</li>
<li>L: Q → 2Σ is a function, called the labeling function of A.</li>
<li>Δ: Q → 2Q is a function, called the transition relation of A.</li>
<li>Q0 is a subset of Q, called the initial states.</li>
<li>
 
 
 
 
 
 F
 
 
 
 
 {\displaystyle {\cal {F}}}
 
 is the acceptance condition, which is made up of zero or more accepting sets. Each accepting set 
 
 
 
 
 F
 
 i
 
 
 ∈
 
 
 F
 
 
 
 
 {\displaystyle F_{i}\in {\cal {F}}}
 
 is a subset of Q.</li></ul>
Let w = a1a2 ... be an <a href="/facts/%CE%A9-language/sJwjxW2U">ω-word</a> over the alphabet Σ. 
The sequence 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 one state from each accepting set 
 
 
 
 
 F
 
 i
 
 
 ∈
 
 
 F
 
 
 
 
 {\displaystyle F_{i}\in {\cal {F}}}
 
. Note that there may be no accepting sets, in which case any infinite run trivially satisfies this property.
To obtain the non-labeled version, the labels are moved from the nodes to the incoming transitions.

<h2 id="references">References</h2>

<ol>
<li id="fn:1">M. Y. Vardi and P. Wolper, Reasoning about infinite computations, Information and Computation, 115(1994), 1–37. <a href="/wiki/Moshe_Vardi" target="_blank">/wiki/Moshe_Vardi</a> <a href="#fnref:1" class="footnote-back-ref">↩</a></li>
<li id="fn:2">Y. Kesten, Z. Manna, H. McGuire, A. Pnueli, A decision algorithm for full propositional temporal logic, CAV’93, Elounda, Greece, LNCS 697, Springer–Verlag, 97-109. <a href="/wiki/Amir_Pnueli" target="_blank">/wiki/Amir_Pnueli</a> <a href="#fnref:2" class="footnote-back-ref">↩</a></li>
<li id="fn:3">R. Gerth, D. Peled, M.Y. Vardi and P. Wolper, "Simple On-The-Fly Automatic Verification of Linear Temporal Logic," Proc. IFIP/WG6.1 Symp. Protocol Specification, Testing, and Verification (PSTV95), pp. 3-18, Warsaw, Poland, Chapman & Hall, June 1995. <a href="#fnref:3" class="footnote-back-ref">↩</a></li>
<li id="fn:4">P. Gastin and D. Oddoux, Fast LTL to Büchi automata translation, Thirteenth Conference on Computer Aided Verification (CAV ′01), number 2102 in LNCS, Springer-Verlag (2001), pp. 53–65. <a href="#fnref:4" class="footnote-back-ref">↩</a></li>
<li id="fn:5">R. Gerth, D. Peled, M.Y. Vardi and P. Wolper, "Simple On-The-Fly Automatic Verification of Linear Temporal Logic," Proc. IFIP/WG6.1 Symp. Protocol Specification, Testing, and Verification (PSTV95), pp. 3-18, Warsaw, Poland, Chapman & Hall, June 1995. <a href="#fnref:5" class="footnote-back-ref">↩</a></li>
</ol>

Generalized Büchi automaton open-in-new

Generalized Büchi automaton