Equations Over Finite State Machines - The Unknown Component Problem: Theory and Applications - page 61

a b c

v/u

i/o u/v

i/u,o

a 1 A

d e

i/o

i v

u

c a b

i/o

A B

u,o

u

v

f

i v

u

aA cA aB bA

o u

g

i v

u

aA cA aB bA

u

o

h

i v

u

aA cA aB bA

o u

o

Fig. 3.13 Illustration of Example 3.31 .( a ) FSM M A ;( b )FSMM C ;( c )FSMM B ;( d )FAofA D
L r .M A /;( e )FAofB *f i g[f o g ,whereB D L r .M B /;( f )FAofA \ B *f i g[f o g \ .IO/ ? ;

*f u g[f v g

( g )FAofPref.A/ \ Pref.B/ *f i g[f o g \ P r ef ..IO/ ? / *f u g[f v g ;( h )FAofprefix.U [ V/-

deadlock-free, but not prefix .U [ V/-convergent language

neither .U [ V/-convergent (since i *f u g[f v g includes i u . v C u / ? that is a subset of
the language) nor .U [ V/-deadlock-free (˛i u cannot be extended to a string ending
by o, against the definition of .U [ V/-deadlock-free).
Finally Fig. 3.13 h shows a language that is .U [ V/-deadlock-free, but not

.U [ V/-convergent.
Theo rem 3. 32. Let B be an .I 2 [ U /.V [ O 2 / -progressive solution of A ˘ X
C [ .IO/ ? and let A be .I 1 [ V /.U [ O 1 / -progressive. If B is compositionally
prefix .U [ V/ -convergent, then B is compositionally prefix .U [ V/ -deadlock-free.

Proof. Since the components A and B are progressive, their composition
Pref .A/ * I 2 [ O 2 \ Pref .B/ * I 1 [ O 1 \ Pref ..IO/ ? / * U [ V is deadlock-free, i.e., it
never stops because a component does not have a transition under a given input. If
the composition is also .U [ V/-convergent, there can be no livelocks, i.e., there
are no cycles labeled with actions from the set U [ V . Therefore an external input,
after a finite path labeled with internal actions, must be followed by an external
output.

t