Hardware Reference
In-Depth Information
Intuitively,
M
A
can be controlled if and only if for all input
i
that the environment
produces, the controller
M
B
can input a
v
to the plant, under which both
M
A
and
0
A
0
C
M
C
produce the same output and go respectively to next states
s
and
s
,atwhich
the same property holds. It is the case that
any
pair of states
.s
A
;s
C
/
such that
s
C
“simulates”
s
A
and the same holds for the next states, are in
H
max
.
To construct
H
max
, start with all the states in the two machines in
H
max
.Then
keep a given pair
.s
A
;s
C
/
in
H
max
if and only if for every
i
, there exists a
v
,such
0
A
0
C
that for every
o
,
M
A
and
M
C
make transitions to
s
and
s
respectively, for which
0
A
;s
0
C
/
0
A
;s
0
C
/
.s
is also in
H
max
. If this condition is not met, drop
.s
from
H
max
and iterate until a fixed point is obtained.
H
max
is a simulation relation and is the
maximal simulation relation.
The main result, proved in [68] and restated in its complete form in [66], follows.
Theorem 13.1.
Suppose that
M
A
is a deterministic FSM and that
M
C
is a
deterministic or pseudo non-deterministic FSM.
If
.r
A
;r
C
/ 62 H
max
, the maximal controller does not exist.
If
.r
A
;r
C
/ 2 H
max
, the maximal controller
M
X
DhS
X
[f
F
g;.I;O/;V;T
X
;r
X
i
is obtained by the following construction:
1.
r
X
D .r
A
;r
C
/
, and
2.
S
X
Df.s
A
;s
C
/ 2 S
A
S
C
j .s
A
;s
C
/ 2 H
max
g
, and
.i;o/=
v
!
M
X
.s
v
=o
!
M
A
s
i=o
!
M
C
s
0
A
;s
0
C
// , Œ.s
A
0
A
/ ^ .s
C
0
C
/ ^ .s
0
A
;s
0
C
/ 2
3.
..s
A
;s
C
/
, and
4. add transitions from a state
H
max
.s
A
;s
C
/
to
F
under
.i;o/=
v if and only if there is no
transition in
M
A
under v
=o
. There is also a transition from
F
to
F
on
=
.
0
A
;s
0
C
/
There is a transition in the controller from
.s
A
;s
C
/
to
.s
on input
.i;o/
with
0
A
output
v
, if and only if there is a transition from
s
A
to
s
on
v
in
M
A
, and a transition
0
C
0
A
;s
0
C
/ 2 H
max
.
from
s
C
to
s
on
i
in
M
C
, both producing the same output
o
,and
.s
The transitions related to
F
capture the behaviors which are present in
M
X
but
are never exercised in the composition of
M
A
and
M
X
; they correspond to the
antecedent of the implication in the definition of
H
max
, i.e., it is a don't care
condition about what the controller does on
.i;o/=
v
if
v
=o
is not in the behavior
of the plant at
s
A
.
M
X
is a maximal solution with respect to language containment,
because the existence of a simulation relation is equivalent to language containment,
when
Notice that
M
C
are deterministic or pseudo non-deterministic
1
.
M
A
and
M
X
is a
maximal solution with respect to the (maximal) simulation relation. However,
we
When
M
C
is nondeterministic (and not pseudo non-deterministic),
may
miss
some
solutions
with
respect
to
language
containment,
since
1
We remind that the underlying automaton of a pseudo non-deterministic FSM is deterministic,
and that for deterministic automata not only the existence of a simulation relation implies language
containment but also the vice versa holds.
Search WWH ::
Custom Search