Hardware Reference
In-Depth Information
Definition 4.1.2. A Buchi 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 Q
is the set of final states, and
Q A Q
is the transition relation.
Arun
over an
!
-word
˛
is accepting if Inf
./ \ F ¤; . A language is
!
-regular if and only if it is accepted by a Buchi automaton.
The final states of a finite automaton can be interpreted as the recurrent states of a
Buchi automaton, where accepting runs visit final states infinitely often. We get a
co-B uchi automaton if the acceptance condition identifies a subset of states called
co-final states or persistent states , where an accepting run finally never leaves the
co-final states. The final states of a finite automaton can be interpreted as the
persistent states of a co-Buchi automaton, where accepting runs eventually stay in
the set of final states.
The following closure properties hold for
!
-languages.
V A ? is regular, then
V ! is
Proposition 4.1. 1. If
!
-regular.
V A ? is regular and
L A ! is
2. If
!
-regular, then
V:L
is
!
-regular.
L 1 ;L 2 A ! are
3. If
-regular.
Moreover, there are effective constructions to obtain the automata of the resulting
languages.
!
-regular, then
L 1 [ L 2 and
L 1 \ L 2 are
!
-regular expression has the form S U i :V !
i
Definition 4.1.3. An
!
, where for all
1 i n
V i are regular expressions.
Theorem 4.2 (B uchi - 1960). For every B uchi automaton there is an
,
U i and
!
-regular
expression that defines the same
!
-language and vice versa.
˛ 2 A ! is definitively periodic if there are u
2 A ?
Definition 4.1.4. Aword
;
v
˛ D uv ! .
such that
Corollary 4.3. Every non-empty
!
-regular language contains an infinitely periodic
!
-word.
The language of a Buchi automaton is non-empty if and only if its transition
graph has a cycle that contains a final state reachable from the initial state.
L A ! is
L D A ! n L
Theorem 4.4 (B uchi - 1960). If
!
-regular, then
is
!
-
regular. There is an effective construction to build a Buchi automaton accepting
L
from the B uchi automaton accepting
L
.
However the construction is computationally very hard, as discussed in [42,53,122].
Buchi automata over infinite words might appear as a direct extension of finite
automata from finite words to infinite words, sharing the same underlying transition
structure with acceptance conditions made infinitary instead than finitary. However
the following examples highlight the fundamental differences.
Example 4.5. Figure 4.1 shows three examples of automata
A 1 ,
A 2 and
A 3 , with
L ! . A 1 / D L ! . A 2 / D L ! . A 3 / Df .ab/ ! g ;however,their
respective finitary languages are
the same
!
-language
fin
. A 1 / Df .ab/ ? .a C / g ,
fin
. A 2 / Df .ab/ ? g ,
L
L
 
Search WWH ::




Custom Search