Information Technology Reference
In-Depth Information
3.1 Supervisory Control Theory
Generally, a DES can either be described by textual expressions, such as regular expres-
sions or graphically by for instance Petri nets or automata. In this paper, we focus on
deterministic finite automata.
Definition 1.
A deterministic finite automaton (DFA), is a five-tuple:
(
Q,Σ,δ,q
init
,Q
m
)
where:
-
Q
is a finite set of states;
-
Σ
is a non-empty finite set of events;
-
δ
:
Q
×
Σ
→
Q
is a partial transition function which expresses the state transitions;
-
q
init
∈
Q
is the initial state;
Q
is a set of marked or accepting states.
The composition of two or more automata is realized by the
full synchronous composi-
tion
[9].
Definition 2.
Let
A
i
=(
Q
i
,Σ
i
,δ
i
,q
init
,Q
i
m
)
,i
=1
,
2
be two DFAs. The full syn-
chronous composition of
A
1
and
A
2
is
-
Q
m
⊆
Σ
2
,δ
1
2
,q
1
2
A
1
A
2
=(
Q
1
2
,Σ
1
init
,Q
1
m
×
Q
2
m
)
∪
where:
-
Q
1
2
⊆
Q
1
×
Q
2
;
-
q
1
2
q
init
,q
init
init
=
;
⎧
⎨
δ
1
(
q
1
,σ
)
δ
2
(
q
2
,σ
)if
σ
Σ
1
Σ
2
×
∈
∩
δ
1
(
q
1
,σ
)
q
2
Σ
1
Σ
2
×{
}
if
σ
∈
\
-
δ
1
2
(
q
1
,q
2
,σ
)=
q
1
δ
2
(
q
2
,σ
)
Σ
2
Σ
1
{
}×
if
σ
∈
\
⎩
undefined otherwise
.
As described in Section 1, the goal of SCT is to automatically synthesize a minimally
restrictive supervisor
S
, which guarantees the behavior of the plant
P
always fulfills the
given specification
Sp
. Here if the plant is given as a number of sub-plants
P
1
,...,P
n
,
the plant can be obtained by performing the full synchronous composition operation on
these sub-plants. Thus
P
=
P
1
Sp
m
.
In SCT, events in the alphabet
Σ
can either be controllable or uncontrollable. Hence,
Σ
can be divided into two disjoint subsets, the controllable event set
Σ
c
and the un-
controllable event set
Σ
u
. The supervisor is only allowed to restrict controllable events
from occurring in the plant.
Additionally, given a plant
P
and a specification
Sp
, two properties [1,2] that the
supervisor ought to have are:
-
Controllability
:Let
Σ
u
be the set of uncontrollable event set. The supervisor
S
is
never allowed to disable any uncontrollable event that might be generated by the
plant
P
.
-
Non-blocking
: This is a progress property enforced by the supervisor
S
,which
guarantees that at least one marked state is always reachable in the closed-loop
system,
S
...
P
n
. Similarly,
Sp
=
Sp
1
...
P
.
