Hardware Reference
In-Depth Information
a
b
a
b
c
a
p
0
p
1
p
2
p
3
s
0
s
1
c
d
a
a
c
0
c
1
i
0
i
1
a
,
c
b
,
c
c
2
a
,
b
,
c
e
f
a
,
b
a
b
c
0
i
0
i
1
i
2
g
h
a
,
c
a
c
0
i
0
i
1
Fig. 15.5
Illustration
o
f Example
15.14
.(
a
)Plant
P
;(
b
) Specification
S
;(
c
) Largest progressive
Pref
solution
C
D
cProg
..P
[
S/
/
;(
d
) Composition
P
\
C
;(
e
) Non-progressive solution
C
non
prog
;
(
f
) Composition
P
\
C
non
prog
;(
g
) Progressive solution
C
prog
;(
h
) Composition
P
\
C
prog
progressive solutions are shown, respectively, in Fig.
15.5
e,g, while the non-trim
and trim compositions of the plant and of the controller are shown, respectively, in
Fig.
15.5
f, h.
Pref
Pref
,
Denote by
cProg
..P
[
S/
/
the largest pro
gr
essive reduction of
.P
[
S/
Pref
. The following theorem
i.e., the largest progressive solution contained in
.P
[
S/
characterizes progressive supervisors.
Theorem 15.15.
A prefix-closed solution
L
of the equation
P
\
X
D
S
is progres-
Pref
sive if and only if Pref
.S /
L
cProg
..P
[
S/
/
.
Proof.
Suppose that there is a pre
fix
-closed solution
C
i
that is not progressive and
Pref
such that
Pref
.S /
C
i
cProg
..P
[
S/
/
. Then there is a string
˛
2
C
i
under
which
P
\
C
i
reaches a state that is not co-accessible.
Search WWH ::
Custom Search