Hardware Reference
In-Depth Information
L
fin
.
A
2
/
D
L
fin
.
A
1
/
.However,
A
2
when interpreted over infinite words recognizes
the language
L
!
.
A
2
/
Df
w
W
b
occurs infinitely many times in
w
g
, that is different
from the one of
A
1
. For instance, the infinite word
.ab/
!
belongs to
L
!
.
A
2
/
but not
to
L
!
.
A
1
/
.
This example shows that the determinization operation for finite automata does
not preserve the language recognized by a Buchi automaton. Even more, this fact
can be seen as the corollary of a more general result, stating that deterministic
Buchi automata are not closed under complementation. Indeed, it can be proved
the
!
-language recognized by
A
1
is not recognizable by any deterministic Buchi
automaton
.
To that purpose, we need the following characterization, stating that deterministic
Buchi automata accept
-words that have infinitely many prefixes accepted as finite
words, so roughly speaking deterministic Buchi automata are the natural extension
of automata over finite words.
!
L
A
!
is accepted by a deterministic B uchi automaton
if and only if there is a regular set
Theorem 4.8.
A language
!
W
W
A
?
such that
L
D
.
Proof (Adapted from [98]).
Let
A
D
.Q;A;;q
0
;F/
be a deterministic Buchi
A
0
automaton and
D
.Q;A;;q
0
;F/
be the corresponding deterministic finite
A
0
have the same underlying structure and differ only by the
acceptance condition). Let
automaton (
A
and
W
D
L.
A
0
/
A
?
be the language recognized by
A
0
.
!
W
Thethesisisthat
L.
A
/
D
.
!
W
We prove first that
L.
A
/
.Let
˛
2
L.
A
/
. From the acceptance condition of
deterministic Buchi automata we have that
A
accepts an
!
-word
˛
if and only if the
run
r
˛
of
A
under
˛
satisfies Inf
.r
˛
/
\
F
¤;
, i.e., the set of states visited infinitely
often by
r
˛
intersects the set of final states
F
. It follows that there are infinitely
!
W
by definition of
!
such that
w
2
W
˛
2
many prefixes
w
of
˛
, i.e.,
W
.
Now we prove that
!
!
W
W
L.
A
/
. Suppose that
˛
2
.Foreveryprefix
w
of
˛
with
w
2
W
D
L.
A
0
/
A
0
over
w
may be seen as a prefix of the
, the accepting run of
unique run
r
˛
of
A
over
˛
(unique because
A
is a deterministic Buchi automaton).
Therefore Inf
.r
˛
/
\
F
¤;
and so
˛
2
L.
A
/
.
t
Notice that in the proof of Theorem
4.8
the hypothesis that the Buchi automaton is
deterministic is used in proving that
!
W
L.
A
/
(whereas it is not needed in proving
!
W
that
).
As a check, suppose to remove that hypothesis. Then the statement that
L.
A
/
A
accepts
A
0
to a final state is false.
Indeed from Example
4.7
consider the non-deterministic automaton
˛
if there are infinitely many prefixes of
˛
that drive
A
1
(set in this
˛
D
.ab/
!
; there are infinitely many prefixes of
proof
A
D
A
1
)andthe
!
-word
˛
.ab/
n
;n
1;
A
0
to a final state and so they are finite words
of the form
that drive
in
W
, but it is false that
A
accepts
˛
, because there is no final state that occurs
infinitely often in any run
r
˛
of
A
and so there is no accepting run
r
˛
.
Search WWH ::
Custom Search