Hardware Reference
In-Depth Information
4.2
Equations Over
!
-Languages
We s aw t h a t B ¨uchi automata have an underlying structure as finite automata,
augmented with an infinitary acceptance condition. Buchi automata accept
!
-
regular languages; two automata are
!
-equivalent if they accept the same language,
and automaton
A
is an
!
-reduction of automaton
B
if the
!
-language of
A
is a
subset of the
.
One might conjecture that the solution to an equation over
!
-language of
B
-languages could be
obtained by solving the corresponding equation over their finitary counterparts, and
then computing the limit of the latter solution to obtain the solution of the original
equation over
!
!
-languages, however the following example shows that it is not true
in general.
Example 4.13.
Given
I
Df
i
1
;i
2
g
,
U
Df
u
1
;
u
2
g
, consider the
!
-regular languages
C
!
D
..i
1
C
i
2
/.
u
1
C
u
2
//
?
.i
1
u
1
/
!
C
.i
2
u
2
/
!
and
S
!
D
.i
1
C
i
2
/
?
i
1
.
C
!
and
Then the regular languages of the finite prefixes of the
!
-languages
S
!
are, respectively,
Pref.C
!
/
D
..i
1
C
i
2
/.
u
1
C
u
2
//
?
.i
1
u
1
/
?
C
.i
2
u
2
/
?
and
.S
!
/
D
.i
1
C
i
2
/
?
i
1
D
.i
1
C
i
2
/
?
.
The largest solution of the equation
Pref
Pref
.C
!
/
˘
X
Pref
.S
!
/
is the language
u
1
C
u
2
/
?
, whose limit is
!
u
1
C
u
2
/
!
.
L
D
.
L
D
.
u
1
C
u
2
/
?
/
*
I
D
.
u
1
C
u
2
C
i
1
C
i
2
/
?
, whose intersection with
Indeed,
L
*
I
D
..
.C
!
/
.C
!
/
.C
!
/
\
L
*
I
/
+
I
D
.
.C
!
//
+
I
D
Pref
is equal to
Pref
.Then
.
Pref
Pref
.i
1
C
i
2
/
?
i
1
C
i
2
D
.i
1
C
i
2
/
?
D
.S
!
/
Pref
. Moreover,
L
is the largest solution,
because
L
is the universal language on alphabet
U
.
However,
!
u
1
C
u
2
/
!
is not a solution of
C
!
˘
!
X
S
!
. Indeed, while
L
D
.
!
L
u
2
2
L
.C
!
/
˘
X
.S/
!
,theword
u
2
2
is a solution of
Pref
Pref
is not a
C
!
˘
!
X
!
S
!
.
The reason is that the word
solution of the equation
.i
2
u
2
/
!
2
.
u
2
/
*
!I
(the
-expansion of
u
2
!
to alphabet
.i
2
u
2
/
!
2
C
!
\
!
..
u
1
C
u
2
/
!
/
*
!I
(the
C
!
and
I
), the word
!
-intersection of
u
1
C
u
2
/
!
/
*
!I
), and the word
i
2
D
..i
2
u
2
/
!
/
+
!I
62
S
!
(
..i
2
u
2
/
!
/
+
!I
is the
..
.i
2
u
2
/
!
to alphabet
!
-restriction of
I
).
-languages
described by Buchi automata, following the exposition in [24] and in the Master's
Thesis by V. Bushkov to which we are indebted [23]. A similar blueprint could
be followed to extend synchronous equations to
In this section we describe how to extend parallel equations to
!
!
-languages described by Buchi
automata, but we are not going to work it out here.
4.2.1
Expansion and Restriction of
!
-Languages
Definition 4.2.1.
Given
the
disjoint
alphabets
A
and
B
,an
!
-language
L
!
2
.A
[
B/
!
W
A
!
.˛/
D
defined over
A
, and the mapping
such that
Search WWH ::
Custom Search