Hardware Reference
In-Depth Information
a
i,o
i,o
i,o
u,v
u,v
b
i,o
i,o
i,o
u,v
u,v
i,o
u,v
O/
?
Fig. 3.14
Illustration of Example
3.33
.(
a
)FAof.I
[
*
.U
[
V;l
D
1/
;(
b
)FAof.I
[
O/
?
*
.U
[
V;l
D
2/
. In both cases it is I
Df
i
g
, O
Df
o
g
, U
Df
u
g
and V
Df
v
g
Theorem 3.35.
A solution
M
B
of
M
A
˘
l
M
X
M
C
is also a compositionally
.U
[
V/
-convergent solution of
M
A
˘
M
X
M
C
.
If
M
A
and
M
B
are also complete FSMs, then
M
B
is a compositionally prefix
I.U
[
V/
?
O
-progressive and compositionally
I
?
O
-progressive solution of
M
A
˘
M
X
M
C
.
Proof.
By construction, a solution M
B
of M
A
˘
l
M
X
M
C
is compositionally
.U
[
V/-convergent. A solution M
B
of M
A
˘
l
M
X
M
C
is also a solution of
M
A
˘
M
X
M
C
, because when l
D1
the operator
˘
l
becomes the operator
˘
.
By Theorem
3.32
, the fact that M
B
is compositionally .U
[
V/-convergent,
together with the completeness of M
A
and M
B
, imply that M
B
is compositionally
prefix I.U
[
V/
?
O-progressive and therefore compositionally I
?
O-progressive.
t
However, in general M
A
˘
M
X
M
C
may be solvable despite the fact that
M
A
˘
l
M
X
M
C
has no solution. For instance, this may happen when M
A
˘
M
X
M
C
has no compositionally I.U
[
V/
?
O-progressive solution. If the equation M
A
˘
l
M
X
M
C
has no complete solution, it is open whether there is a compositionally
I.U
[
V/
?
O-progressive solution of M
A
˘
M
X
M
C
.
Search WWH ::
Custom Search