Hardware Reference
In-Depth Information
(maximal) simulation relation in general is stronger than language containment,
i.e., (maximal) simulation relation implies language containment, but not vice
versa. We use a (maximal) simulation relation instead of language containment
to avoid determinizing and so obtain an algorithm of polynomial complexity
bounded by
O.jS A jjS C jjT A jjT C j/
,where jS A j
( jS C j ) is the number of states
of
M A
(
M C )and jT A j
( jT C j )
is the
size
of the
transition relation of
M A
(
M C ).
An approach based on simulation relations has been followed also in [9-12],
a series of papers devoted to the model matching problem and its variants from
discrete control theory. These papers give a solvability condition based on the notion
of a simulation relation between inverse automata, which characterize the possible
output sequences generated by an FSM.
Definition 13.1.3. Let a NDFSM
F DhS;I;O;T;ri be given. Let
I .s/ Dfi 2
Ij9s 0 2 .i;s/g denote the set of applicable inputs at state
s
.The inverse automaton
F 1 DhS;O; 1 ;ri ,where
of
F
is a non-deterministic finite state automaton
1 O S S
.o;s;s 0 / 2 1 ”9i 2 I .s/ .i;s;s 0 ;o/2 T:
The inverse automaton of a given FSM is obtained by using its output labels as input
labels.
The existence of a simulation relation between the inverse automaton of
M C ,
M C DhY;S; 1 ;ri , and that of
M A DhY;S 1 ; 1 ;r 1 i , enables to prove
M A ,
that the output sequences generated by
M A .In[12],
the following necessary and sufficient condition for the existence of a solution to the
FSM model matching problem is proved.
M C can also be generated by
Theorem 13.2. Let the plant
M C be DFSMs. The FSM model
matching problem is solvable if and only if there exists a simulation relation under
which
M A and the model
M C sim M 1
M 1
C
M 1
A
, i.e.,
is simulated by
.
A
This theorem holds both for the controller's topology (with the unknown controller
forming a closed loop with the known plant) and the cascade topology (with the
unknown controller as the head FSM and the known plant as the tail FSM), since
the solvability condition does not depend on whether the connection is closed-loop
or open-loop. Therefore the equation is solvable for the closed-loop topology iff it
is solvable for the open-loop topology iff
M C sim M 1
.
In addition, it is shown that for each such simulation relation, say
A
'
, it is possible
M ' , that actually generates the sequence of inputs
to build a corresponding machine
u for
M C . It is also shown that every
solution is in a one-to-one correspondence with a simulation relation.
Notice that the method of simulation relations is considered as an alternative
to language equations for the controller's topology (with the caveats mentioned in
this section), but it is not a replacement to solving language equations for general
topologies like the rectification topology.
M A to match the sequence of outputs of
Search WWH ::




Custom Search