Hardware Reference
In-Depth Information
Chapter 4
Equations Over
!
-Automata
4.1
!
-Languages and
!
-Automata
An infinite word over an alphabet
A
,or
!
-word, is an infinite sequence of symbols of
A
!
is the set of
A
!
.Moreover,
A
.
!
-words on
A
.An
!
-language on
A
is a subset of
A
1
D
A
?
[
A
!
.An
!
-word may be written as
˛
D
˛.0/˛.1/:::
,where
˛.i/
2
A
for every
i
0
;if
n
m
,
˛.n;m/
D
˛.n/:::˛.m
1/˛.m/
and
˛.n;
1
/
D
. The notations
9
!
n
˛.n/˛.n
C
1/:::
stands for 'there are infinitely many
n
'and
9
<!
n
W
A
?
,wedefinethesets
stands for 'there are finitely many
n
'. Given a set
w
i
2
W
g
,
!
W
!
Df
˛
2
A
!
j
˛
D
W
Df
˛
2
A
!
j9
!
n˛.0;n/
2
W
g
w
0
w
1
:::;
Inf.˛/
Df
a
2
A
j9
!
n˛.n/
D
a
g
. Given an
(also called
lim.W/
), and
!
-
language
L
,
Pref.L/
denotes (by overloading) the sets of finite prefixes of the
words in
L
.
Definition 4.1.1.
A
!
-automaton
is a 5-tuple
A
D
.Q;A;;q
0
;/
,where
is a
Boolean formula defining the acceptance conditions.
1
A
run
of
A
under an
!
-word
˛
is an
!
-word
r
˛
over the alphabet of the states in
Q
such that
r
˛
.0/
D
q
0
, and, for every
i
0
,
.r
˛
.i/;˛.i/;r
˛
.i
C
1/
2
.
Arun
r
˛
under an
!
-word
˛
is
accepting
if
.
Inf
.r
˛
//
is true, i.e., the set of
states of
r
˛
visited infinitely often satisfies the condition
.
An
!
-word
˛
is
accepted
if there exists an accepting run
r
˛
under
˛
.
The language
accepted
by the
!
-automaton
A
with acceptance condition
,
˛
2
A
!
, i.e., the strings for which there is a
L.
A
/
, is the set of accepted strings
run of states
r
˛
visited by
˛
such that
.
Inf
.r
˛
//
is true (the set of states visited
infinitely often by
r
˛
satisfies the condition
).
1
For a B uchi automaton
is
a
disjunct
iv
e formula representing the subset of states
F
Q
;for
aco-Buchi automaton
is
:
F
,where
F
is disjunctive formula representing the set
Q
n
F
;fora
,where
F
2
Q
; for a Rabin automaton
Muller automat
on
is
_
F
2
F
.
^
f
2
F
f
^
q
62
F
:
q/
is
_
i
D
1
.L
i
^:
.U
i
//
,where
L
i
;U
i
;1
i
n;
are disjunctive formulas; for a Street automaton
^
i
D
1
.L
i
^:
.U
i
//
is
,where
L
i
;U
i
;1
i
n;
are disjunctive formulas.
Search WWH ::
Custom Search