Information Technology Reference
In-Depth Information
Example 1.
Consider a resource booking problem where two industrial robots need to
book two resources in opposite order to carry out their tasks. To avoid collisions, a
constraint requires that two robots are not allowed to occupy two zones simultaneously.
Figure 1 shows one way to model the system as the state machines, or
deterministic
finite automata
. Figure 1a and 1b depict the robot (plant) models and Fig. 1c and 1d
depict the resource (specification) models. The states having an incoming arrow from
outside denote the beginning of the task, while the states having double circles, called
marked states
, denote the accomplishment of the task. The event
use
R
1
means that
Robot
A
uses Resource
1
. The other events can be interpreted similarly. The goal of
the SCT is to automatically synthesize a
minimally restrictive
supervisor from these
modular models. Traditionally, to do this, the algorithm starts with the composition
(formally described in Section 3.1) of all the automata as the initial candidate super-
visor
S
0
(Fig. 1e). Then the undesirable states will be removed iteratively. Generally,
undesirable states can either be blocking or uncontrollable. A state is blocking when no
marked state can be reached, while uncontrollable states are defined in Section 3.1. In
Fig. 1e, we have one blocking state
q
2
,q
2
,q
2
,q
2
, which depicts the situation where
Robot
A
has booked Resource
1
and is trying to book Resource
2
, while Robot
B
has
booked Resource
2
and is trying to book Resource
1
. In such case, none of the robots
can do other movements, which is a blocking situation. After removing the blocking
state together with the associated transitions, a non-blocking supervisor is produced.
It can be observed that for such a simple example, the composed automaton contains
9
states. With a DES getting more complicated, the composed automaton will become
significantly larger. To alleviate this problem, a well known strategy is to represent the
state space symbolically by using
Binary Decision Diagrams
(BDD). In [8], based on
this principle, an alternative approach is presented, where guards are generated to pre-
vent the controlled system to reach undesirable states. The advantage of this approach is
that it never constructs the composed automaton, which means that an incomprehensi-
ble BDD representation of the supervisor is avoided. Instead, the approach characterizes
a supervisor by a set of minimal guards that are attached to the original models to rep-
resent the supervisor behavior. Figure 2 shows the application of the guard generation
to the example, where the variables
v
A
,
v
B
,
v
C
,
v
D
are introduced to hold the current
states of the corresponding automata.
The intention of this paper is to improve the guard generation procedure by introduc-
ing an alternative symbolic approach. This approach, which is based on the disjunctive
partitioning technique, partitions the transition function into a set of simple but struc-
tural components. These components, having the disjunctive connection relation be-
tween each other, therefore can be used to search the state-space without constructing a
total transition function for the composed automaton. Besides, to keep the intermediate
number of BDD nodes as small as possible, the approach includes a set of selection
heuristics to search the state-space in a structural way.
3
Preliminaries
This section provides some preliminaries which are used throughout the rest of the
paper.
