Complementation of Büchi automaton
Encyclopedia
In automata theory
, complementation of a Büchi automaton is construction
of another Büchi automaton
that recognizes complement of the ω-regular language recognized by the given Büchi automaton. Existence of algorithms for this construction proves that the set of ω-regular languages and Büchi automata are closed under complementation.
This construction is particularly hard relative to the constructions for the other closure properties of Büchi automata. The first construction was presented by Büchi in 1962. Later, other constructions were developed that enabled efficient and optimal complementation
.
in a logical form.
Here, we have his construction in the modern notation used in automata theory.
Let A = (Q,Σ,Δ,Q0,F) be a Büchi automaton.
Let ~A be an equivalence relation over Σ+ such that
for each v,w ∈ Σ+,
v ~A w iff for all p,q ∈ Q,
A has a run from p to q over v iff this is possible over w
and furthermore
A has a run via F from p to q over v iff this is possible over w.
By definition,
each map f:Q → 2Q × 2Q
defines a class of ~A.
We denote the class by Lf.
We interpret f in the following way.
w ∈ Lf iff
for each state p ∈ Q and (Q1,Q2)= f(p),
w can move automaton A from p
to each state in Q1 and to each state in Q2 via a state
in F.
Note that Q2 ⊆ Q1.
The following three theorems provides a construction of the complement Büchi automaton
using the equivalence classes of ~A.
Theorem 1: ~A has finitely many equivalent classes and each class is a regular language
.
Proof:
Since there are finitely many f:Q → 2Q × 2Q, ~A has finitely many equivalent classes.
Now we show that Lf is a regular language.
For p,q ∈ Q and i ∈ {0,1},
let Ai,p,q = ( {0,1}×Q,Σ,Δ1∪Δ2,{(0,p)},{(i,q)} )
be a nondeterministic finite automaton,
where
Δ1 =
{ ((0,q1),(0,q2)) | (q1,q2) ∈ Δ} ∪
{ ((1,q1),(1,q2)) | (q1,q2) ∈ Δ},
and
Δ2 =
{ ((0,q1),(1,q2)) |
q1 ∈ F ∧ (q1,q2) ∈ Δ
}.
Let Q' ⊆ Q.
Let αp,Q' = ∩{ L(A1,p,q) |q ∈ Q'},
which is the set of words that can move A from p to all the states in Q'
via some state in F.
Let βp,Q' = ∩{ L(A0,p,q)-L(A1,p,q)-ε |q ∈ Q'},
which is the set of non-empty words that can move A from p to all the states in Q'
and does not have a run that passes through any state in F.
Let γp,Q' = ∩{ Σ+-L(A0,p,q) |q ∈ Q'},
which is the set of non-empty words that can not move A from p to any of the
states in Q'.
By definitions,
Lf = ∩{ αp,Q2∩
βp,Q1-Q2∩
γp,Q-Q1
|(Q1,Q2)=f(p) ∧ p ∈ Q}.
Theorem 2: For each w ∈ Σω,
there are ~A classes Lf and Lg such that
w ∈ Lf(Lg)ω.
Proof:
We will use infinite Ramsey theorem
to prove this theorem.
Let w =a0a1... and w(i,j) = ai...aj-1.
Consider the set of natural numbers N.
Let equivalence classes of ~A be the colors of subsets of N
of size 2.
We assign the colors as follows.
For each i < j,
let the color of {i,j} be the equivalence class in which w(i,j) occurs.
Due to infinite Ramsey theorem, we can find infinite set X ⊆ N
such that each subset of X of size 2 has same color.
Let 0 < i0 < i1 < i2 .... ∈ X.
Let f be a defining map of an equivalence class such that
w(0,i0) ∈ Lf.
Let g be a defining map of an equivalence class such that
for each j>0,w(ij-1,ij) ∈ Lg.
Therefore, w ∈ Lf(Lg)ω.
Theorem 3: Let Lf and Lg be equivalence classes
of ~A.
Lf(Lg)ω is either subset of L(A) or
disjoint from L(A).
Proof:
Lets suppose word w ∈ L(A) ∩ Lf(Lg)ω.
Otherwise theorem holds trivially.
Let r be the accepting run of A over input w.
We need to show that each word w' ∈ Lf(Lg)ω
is also in L(A), i.e., there exist a run r' of A over input w' such that
states in F occurs in r' infinitely often.
Since w ∈ Lf(Lg)ω,
let w0w1w2... = w such that w0 ∈ Lf and for each i > 0, wi ∈ Lg.
Let si be the state in r after consuming w0...wi.
Let I be a set of indices such that i ∈ I iff the run segment in r
from si to si+1 contains a state from F.
I must be an infinite set.
Similarly, we can split the word w'.
Let w'0w'1w'2... = w' such that w'0 ∈ Lf and for each i > 0, w'i ∈ Lg.
We construct r' inductively in the following way.
Let first state of r' be same as r. By definition of Lf,
we can choose a run segment on word w'0 to reach s0.
By induction hypothesis,
we have a run on w'0...w'i that reaches to si.
By definition of Lg,
we can extend the run along the word segment w'i+1 such that
the extension reaches si+1 and visits a state in F if i ∈ I.
The r' obtained from this process will have infinitely many run segments
containing states from F, since I is infinite set.
Therefore, r' is an accepting run and w' ∈ L(A).
Due to the above theorems, we can represent Σω-L(A)
as finite union of ω-regular languages of the from Lf(Lg)ω, where Lf and Lg are equivalence classes of ~A.
Therefore, Σω-L(A) is an ω-regular language.
We can translate the language into a Büchi automaton. This construction is doubly exponential in terms of size of A.
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...
, complementation of a Büchi automaton is construction
Automata construction
In automata theory, automata construction is an important mathematical technique used to demonstrate the existence of an automaton with a certain desired property...
of another 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...
that recognizes complement of the ω-regular language recognized by the given Büchi automaton. Existence of algorithms for this construction proves that the set of ω-regular languages and Büchi automata are closed under complementation.
This construction is particularly hard relative to the constructions for the other closure properties of Büchi automata. The first construction was presented by Büchi in 1962. Later, other constructions were developed that enabled efficient and optimal complementation
.
Büchi's construction
Büchi presented a doubly exponential complement constructionin a logical form.
Here, we have his construction in the modern notation used in automata theory.
Let A = (Q,Σ,Δ,Q0,F) be a Büchi automaton.
Let ~A be an equivalence relation over Σ+ such that
for each v,w ∈ Σ+,
v ~A w iff for all p,q ∈ Q,
A has a run from p to q over v iff this is possible over w
and furthermore
A has a run via F from p to q over v iff this is possible over w.
By definition,
each map f:Q → 2Q × 2Q
defines a class of ~A.
We denote the class by Lf.
We interpret f in the following way.
w ∈ Lf iff
for each state p ∈ Q and (Q1,Q2)= f(p),
w can move automaton A from p
to each state in Q1 and to each state in Q2 via a state
in F.
Note that Q2 ⊆ Q1.
The following three theorems provides a construction of the complement Büchi automaton
using the equivalence classes of ~A.
Theorem 1: ~A has finitely many equivalent classes and each class is a regular language
Regular language
In theoretical computer science and formal language theory, a regular language is a formal language that can be expressed using regular expression....
.
Proof:
Since there are finitely many f:Q → 2Q × 2Q, ~A has finitely many equivalent classes.
Now we show that Lf is a regular language.
For p,q ∈ Q and i ∈ {0,1},
let Ai,p,q = ( {0,1}×Q,Σ,Δ1∪Δ2,{(0,p)},{(i,q)} )
be a nondeterministic finite automaton,
where
Δ1 =
{ ((0,q1),(0,q2)) | (q1,q2) ∈ Δ} ∪
{ ((1,q1),(1,q2)) | (q1,q2) ∈ Δ},
and
Δ2 =
{ ((0,q1),(1,q2)) |
q1 ∈ F ∧ (q1,q2) ∈ Δ
}.
Let Q' ⊆ Q.
Let αp,Q' = ∩{ L(A1,p,q) |q ∈ Q'},
which is the set of words that can move A from p to all the states in Q'
via some state in F.
Let βp,Q' = ∩{ L(A0,p,q)-L(A1,p,q)-ε |q ∈ Q'},
which is the set of non-empty words that can move A from p to all the states in Q'
and does not have a run that passes through any state in F.
Let γp,Q' = ∩{ Σ+-L(A0,p,q) |q ∈ Q'},
which is the set of non-empty words that can not move A from p to any of the
states in Q'.
By definitions,
Lf = ∩{ αp,Q2∩
βp,Q1-Q2∩
γp,Q-Q1
|(Q1,Q2)=f(p) ∧ p ∈ Q}.
Theorem 2: For each w ∈ Σω,
there are ~A classes Lf and Lg such that
w ∈ Lf(Lg)ω.
Proof:
We will use infinite Ramsey theorem
to prove this theorem.
Let w =a0a1... and w(i,j) = ai...aj-1.
Consider the set of natural numbers N.
Let equivalence classes of ~A be the colors of subsets of N
of size 2.
We assign the colors as follows.
For each i < j,
let the color of {i,j} be the equivalence class in which w(i,j) occurs.
Due to infinite Ramsey theorem, we can find infinite set X ⊆ N
such that each subset of X of size 2 has same color.
Let 0 < i0 < i1 < i2 .... ∈ X.
Let f be a defining map of an equivalence class such that
w(0,i0) ∈ Lf.
Let g be a defining map of an equivalence class such that
for each j>0,w(ij-1,ij) ∈ Lg.
Therefore, w ∈ Lf(Lg)ω.
Theorem 3: Let Lf and Lg be equivalence classes
of ~A.
Lf(Lg)ω is either subset of L(A) or
disjoint from L(A).
Proof:
Lets suppose word w ∈ L(A) ∩ Lf(Lg)ω.
Otherwise theorem holds trivially.
Let r be the accepting run of A over input w.
We need to show that each word w' ∈ Lf(Lg)ω
is also in L(A), i.e., there exist a run r' of A over input w' such that
states in F occurs in r' infinitely often.
Since w ∈ Lf(Lg)ω,
let w0w1w2... = w such that w0 ∈ Lf and for each i > 0, wi ∈ Lg.
Let si be the state in r after consuming w0...wi.
Let I be a set of indices such that i ∈ I iff the run segment in r
from si to si+1 contains a state from F.
I must be an infinite set.
Similarly, we can split the word w'.
Let w'0w'1w'2... = w' such that w'0 ∈ Lf and for each i > 0, w'i ∈ Lg.
We construct r' inductively in the following way.
Let first state of r' be same as r. By definition of Lf,
we can choose a run segment on word w'0 to reach s0.
By induction hypothesis,
we have a run on w'0...w'i that reaches to si.
By definition of Lg,
we can extend the run along the word segment w'i+1 such that
the extension reaches si+1 and visits a state in F if i ∈ I.
The r' obtained from this process will have infinitely many run segments
containing states from F, since I is infinite set.
Therefore, r' is an accepting run and w' ∈ L(A).
Due to the above theorems, we can represent Σω-L(A)
as finite union of ω-regular languages of the from Lf(Lg)ω, where Lf and Lg are equivalence classes of ~A.
Therefore, Σω-L(A) is an ω-regular language.
We can translate the language into a Büchi automaton. This construction is doubly exponential in terms of size of A.