Hardware Reference
In-Depth Information
Notice that the difference with respect to the expansion operator is that in the latter
the expansion is with respect to an alphabet
V
disjoint from
˙
(and again we add
self-loops for every symbol in
V
), whereas extension here is performed with respect
to a sub-alphabet
.
Now we provide an operational test for a weak controller, by proving that
˙
u
c
˙
C
is a
C
*
˙
u
c
is a solution of
solution of
P
\
p
X
D
S
if and only if
P
\
X
D
S
.
Theorem 15.18.
A prefix-closed solution
C
of the equation
P
\
X
D
S
is a weak
C
*
˙
u
c
is a
controller under partial controllability with respect to
˙
u
c
if and only if
prefix-closed solution of the equation
P
\
X
D
S
.
P
\
p
C
D
P
\
C
*
˙
u
c
.
Proof.
We s h ow t h a t
.p;;p
0
/
.c;;c
0
/
If
62
˙
u
c
or
2
˙
u
c
and there are transitions
in
P
and
in
..p; c/; ; .p
0
;c
0
//
C
then in both intersections there is a transition
.
.p;;p
0
/
If
2
˙
u
c
and there is a transition
in
P
and there is no transition from
..p; c/; ; .p
0
;c//
state
c
under
in
C
then in both intersections there is a transition
.
t
Theorem 15.19.
Givenaplant
P
, a specification
S
and a set of uncontrollable
actions
˙
u
c
there exists a controller if and only if there exists a weak controller.
Proof.
If
Let
C
be a controller, i.e.,
P
\
C
D
S
and at each state
.p; c/
in
P
\
C
,
if an uncontrollable action
is defined at
p
then
is defined at
c
too. Thus an action
can be undefined at state
c
of
C
if and only if for each state
.p; c/
of
P
\
C
the
P
\
C
*
˙
u
c
action
is undefined at
P
, i.e.,
D
P
\
C
D
S
, meaning that
C
is a
weak controller.
P
\
C
*
˙
u
c
Only if
Let
C
be a weak controller, then by Theorem
15.18
D
S
.
C
*
˙
u
c
,then
C
*
˙
u
c
is a
Since each uncontrollable action is defined at each state of
controller under partial controllability.
t
However, we notice that the set of all controllers under partial controllability is a
proper subset of the set of all weak controllers, as shown.
Example 15.20.
Consider
˙
Df
a; b
g
,
˙
uc
Df
a
g
,
P
Df
; a; b
g
,
S
Df
a
g
.
C
Df
g
is a weak controller (it stutters when
P
issues
a
), but is not a controller (it cannot
disable
a
).
Example 15.21.
Consider
˙
Df
a; b; c
g
,
˙
u
c
Df
c
g
. Figure
15.6
ashowsthe
plant
P
. Figure
15.6
b shows the specification
S
, which coincides with the smallest
controller under partial controllability
C
D
Pref
.S /
,since
P
\
C
D
S
. Figure
15.6
c
P
\
C
*
˙
u
c
w
shows a weak controller
C
w
,since
D
P
\
p
C
w
D
S
.However,
C
w
is not
a controller under partial controllability (
c
0
).
An interesting question is whether Theorem
15.7
can be generalized to partial
controllability (but with the restricted hypothesis that the languages of
c
2
˙
u
c
is not defined at
P
and
S
are prefix-closed) to characterize all controllers
C
by means of the interval
Pref
Pref
.S /
C
.P
[
S/
:
Search WWH ::
Custom Search