Hardware Reference
In-Depth Information
Now we show that there is no deterministic Buchi automaton that accepts the
language
L
!
.
A
1
/
Df
˛
2
A
!
˛
gD
f
˛
2
A
!
W9
<!
n˛.n/
D
a
g
. It is enough to show that there is no regular set
W
A
?
such that
W
a
occurs a finite number of times in
!
W
L
!
.
A
1
/
D
. Suppose by contradiction that there is such a set
!
W
b
!
2
L
!
.
A
1
/
D
b
n
1
b
!
has infinitely
W
.Since
,thereis
n
1
such that
2
W
(
b
n
1
2
W
many prefixes in
W
, in particular there will be a prefix
). Similarly, since
b
n
1
ab
!
2
L
!
.
A
1
/
D
!
,thereis
n
2
such that
b
n
1
ab
n
2
2
W
. Iterating the reasoning,
W
we construct an
!
-word
˛
D
b
n
1
ab
n
2
ab
n
3
:::
with infinitely many prefixes in
W
.
By definition of
!
!
W
,but
!
W
D
L
!
.
A
1
/
˛
2
L
!
.
A
1
/
,
˛
2
and so
,whichisa
W
contradiction since
˛
contains infinitely many occurrences of
a
and so cannot be in
L
!
.
A
1
/
.
Hence, the following theorem holds.
Theorem 4.9.
The
class
of
!
-languages
recognized
by
deterministic
B uchi
automata is
strictly included
in the class of
!
-languages recognized by non-
deterministic B uchi automata.
Moreover, deterministic Buchi automata are not closed under complementation.
Example 4.10.
Consider the example in Fig.
4.2
b. If we interpret it as a co-Buchi
automaton with the final state interpreted as the persistent state, the language
accepted is the set of
. Compare it with the
discussion in Example
4.7
to understand the duality between Buchi and co-Buchi
conditions.
!
-words with finite occurrences of
a
Definition 4.1.5.
A
Muller automaton
is a 5-tuple
A
D
.Q;A;;q
0
;
F
/
,where
Q
is a finite set of states,
A
is a finite set of symbols,
q
0
2
Q
is the initial state,
F
2
Q
is a collection of sets of final states, and
Q
A
Q
is the transition
relation.
Arun
over an
!
-word
˛
is
accepting
if Inf
./
2
F
. The automaton
A
accepts
an
!
-word
˛
if there is an accepting run of
A
over
˛
. The language
L
.
A
/
accepted
by
A
is the set of
!
-words accepted by
A
.
Given a deterministic Buchi automaton, a deterministic Muller automaton equiva-
lent to it can be defined with the accepting condition
F
Df
S
2
2
Q
j
S
\
F
¤;g
.
We state a few basic theorems about Muller automata.
Theorem 4.11.
Non-deterministic Muller automata accept
!
-regular languages
and vice versa.
Finally, the languages accepted by deterministic Muller automata are the same
as the languages accepted by non-deterministic Buchi automata. So deterministic
Muller automata have the same expressive power as nondeterministic Muller
automata.
Theorem 4.12 (McNaughton).
An
-regular (i.e., accepted by a
Buchi automaton) if and only if it is accepted by a deterministic Muller automaton.
!
-language is
!
Search WWH ::
Custom Search