Hardware Reference
In-Depth Information
The computation of the largest subset of compositionally prefix .U [ V/-
deadlock-free solutions and of the largest subset of compositionally prefix .U [ V/-
convergent solutions requires further investigation. The former problem appears
similar to the one of finding the largest subset of compositionally I.U [ V/ ?
O-progressive solutions. About the latter problem, when S FSM is not composi-
tionally prefix .U [ V/-convergent, then the largest compositionally prefix .U [
V/-convergent solution does not exist and each finite IO-prefix-closed subset of
S FSM is a compositionally prefix .U [ V/-convergent solution. It is an open
question whether there is the largest complete prefix .U
[ V/-convergent solution.
3.4.3
FSM Equations Under Bounded Parallel Composition
Here we discuss the solutions whose composition with the context produces an
external output after at most l internal actions. One could build an analogy with
Moore solutions of synchronous equations. We provide in the sequel the key steps
to solve FSM equations under bounded parallel composition.
Definition 3.4.5. The l -bounded parallel composition of FSMs M B , over input
alphabet I 2 [ U and output alphabet O 2 [ V , with M A , over input alphabet I 1 [ V
and output alphabet O 1 [ U , yields the FSM M A ˘ l M B with language
.IO/ ?
L.M A ˘ l M B /
D L.M A / ˘ l L.M B / \
D h L.M A / * I 2 [ O 2
* .U [ V;l/ i
[ O/ ?
+ I [ O \ .IO/ ? :
\ L.M B / * I 1 [ O 1
\ .I
When l
D1 , it reduces to the definition of parallel composition of FSMs.
[
O/ ?
* .U [ V;l D 1/
[
Example 3.33. Fig. 3.14 a,b show the automata of .I
and .I
O/ ?
* .U [ V;l D 2/ , with I Df i g , O Df o g , U Df u g
and V
Df v g .Thewordsin.I
[
O/ ?
* .U [ V;1/
[ O/ ?
are obtained from those in .I
by inserting anywhere in them
[ V/ 1
[ O/ ?
* .U [ V;2/
words from .U
Df ; u ; v g ;thewordsin.I
are obtained
[ O/ ?
[ V/ 2
from those in .I
by inserting anywhere in them words from .U
D
f ; u ; v ; uu ; uv ; vu ; vv g .
Proposition 3.34. FSM M B is a solution of the equation M A ˘ l M X M C ,where
M A and M C are FSMs, iff M B is a reduction of the FSM M S FSM associated with
S FSM ,where S FSM
is obtained by applying Procedure 3.1.3 to S ,where S
D
.A * I 2 [ O 2 \ .C
\ .IO/ ? / * .U [ V;l/ / + I 2 [ U [ V [ O 2 .
If S FSM
D; then no FSM is a solution. S FSM
is the largest compositionally
.U
[ V/ -convergent solution of M A ˘ l M X M C .
The largest complete FSM solution M Prog.S FSM /
is found, if it exists, by
Procedure 3.1.4 .
Search WWH ::




Custom Search