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

If S FSM is compositionally I -progressive, then S FSM is the largest compositionally
I -progressive solution of the equation. However, not every non-empty subset
of S FSM inherits the feature of being compositionally I -progressive. If S FSM
is not compositionally I -progressive, then denote by cP rog.S FSM / the largest
compositionally I -progressive subset of S FSM . Conceptually cP rog.S FSM / is
obtained from S FSM

by deleting each string ˛ such that, for some i 2 I ,there

\ S FSM

is no . u ; v ;o/ 2 U V O such that ˛.i; u ; v ;o/ 2 A " I 2 O 2

" I 1 O 1 .The

following procedure tells how to compute cP rog.S FSM /.
Procedure 3.3.1. Input: Largest prefix-closed solution S FSM of synchronous equa-
tion A X C and context A ; Output: Largest compositionally I -progressive
prefix-closed solution cP rog.S FSM / .
1. Initialize i to 1 and S i to S FSM .

2. Compute R i

D A " I 2 O 2 \ S i

" I 1 O 1 .

If the language R i is I -progressive then cP rog.S FSM / D S i .

Otherwise
(a) Obtain Prog.R i /,thelargestI -progressive subset of R i , by using Proce-
dure 3.1.2 .
(b) Compute T i

D S i n .R i n Prog.R i // # I 2 U V O 2 .

3. If T iFSM D; then cP rog.S FSM / D; .

Otherwise
(a) Assign the language T iFSM to S i C 1 .
(b) Increment i by 1 and go to 2.

Theorem 3.23. Procedure 3.3.1 returns the largest compositionally I -progressive
(prefix-closed) solution, if it terminates.

Theorem 3.24. Procedure 3.3.1 terminates.

The proofs can be found in [148].
A sufficient condition to insure that A " I 2 O 2 \ S FSM
" I 1 O 1

is an I -progressive FSM

language is that S FSM

" I 1 O 1 or A " I 2 O 2 satisfy the Moore property (see Theorem 3.12
for a related statement proved for complete FSMs). If S FSM is Moore then it is
the largest Moore solution of the equation. However, not every non-empty subset of
S FSM inherits the feature of being Moore. If S FSM is not Moore, then denote by
Moore .S FSM / the largest Moore subset of S FSM .Theset Moore .S FSM / is obtained
by deleting from S FSM each string which causes S FSM to fail the Moore property.
Proposition 3.25. If Moore .S FSM / ¤; , then it is the largest Moore solution of the
equation A X C . Otherwise the equation A X C has no Moore solution.

To compute the largest Moore FSM that is a solution, it is sufficient to apply
Procedure 3.1.5 to the FSM M S FSM associated with S FSM , as justified by
Theorem 3.9 . The result is the largest Moore FSM solution, of which every
deterministic Moore solution is a reduction.