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