Hardware Reference
In-Depth Information
!
4.2.3
Parallel Equations Over
-Languages
Definition 4.2.4.
Given
the
pairwise
disjoint
alphabets
I;U;V
and
O
,the
C
.I
[
U
[
V/
!
,
S
.I
[
V
[
O/
!
,andthesets
!
-languages
E
D
I
[
V
[
O
and
H
D
U
[
V
[
O
,
C
˘
!E
X
S
(or
C
˘
!E
X
D
S
)isa
!
-parallel equation
,
with respect to the unknown
!
-language
X
over alphabet
H
.
B
H
!
is a
solution
of the equation
An
!
-language
C
˘
!E
X
S
(or
C
˘
!E
X
D
S
)if
C
˘
!E
B
S
(or
C
˘
!E
B
D
S
).
C
˘
!E
B
S
)is
solvable
if a solution exists.
A solution is called the
largest
solution, if it contains every solution.
(or
C
˘
!E
B
D
S
In [24] the following statement is proved.
Theorem 4.17.
A solvable
equati
on
C
˘
!E
X
S
over
!
-languages has the
largest solution
.C
˘
!H
S/
,where
S
denotes
the complement of
S
.
If
C
˘
!E
.C
˘
!H
S/
D
S
,then
.C
˘
!H
S/
is the largest solution of the equation
C
˘
!E
X
D
S
.
Any
!
-solution of the equation
C
˘
!E
B
D
S
is contained in
.C
˘
!H
S/
, but not
every
is a solution of the equation.
As done for finitary languages, solving an equation over
!
-language contained in
.C
˘
!H
S/
!
-regular languages
reduces to transforming the operator over
!
-languages to operations over the
corresponding
!
-automata that accept them.
4.2.4
Operations Over
!
-Automata
4.2.4.1
!
-Expansion of
!
-Automata
Proposition 4.18.
GivenaBuchi automaton
A
D
.Q;A;;q
0
;F/
accepting a
given
!
-regular language
L
over the alphabet
A
and an alphabet
B
disjoint from
A
, consider the B uchi automaton
A
*
!B
, derived from
A
as follows:
for every state
s
2
Q
n
F
and every symbol
b
2
B
, add a self-loop
.s;b;s/
;for
s
0
, a transition
.s;b;s
0
/
every state
s
2
F
, add a non-accepting state
, a self-loop
.s
0
;b;s
0
/
.s
0
;a;s
00
/
under every symbol
b
2
B
and a transition
for every transition
.s;a;s
00
/
where.
Then
A
*
!B
accepts the
B
-expansion
L
*
!B
of the language
L
accepted by
A
.
Example 4.19.
Given the automaton
A
over
A
Df
a;c
g
shown in Fig.
4.3
a, b shows
A
*
!B
,where
B
Df
b
g
. Notice that the operators for standard expansion of finitary
languages and
!
-expansion act differently on the automata. For instance, for
!
-
expansion we do not add self-loops at accepting states, otherwise
L.
A
*
!B
/
would
not be equal to
.L.
A
//
*
!B
.
Search WWH ::
Custom Search