Information Technology Reference
In-Depth Information
such a control function efficiently and represent it appropriately. Since the synthesis
task involves a series of reachability computations, as DESs becoming more compli-
cated, the traditional explicit state-space traversal algorithm may be intractable due to
the state-space explosion problem
. By using binary decision diagrams (BDD) [6,7], the
supervisor can be represented and computed symbolically such that the state-space ex-
plosion problem is alleviated to some extent. However, the symbolic computation is not
a silver bullet. Transforming from the traditional explicit state-space traversal algorithm
into a BDD-based computation scheme does not guarantee that the algorithm will be-
come remarkably efficient. Thus numerous researches have been performed to improve
the efficiency of symbolic computations. In this paper, we mainly focus on partitioning
techniques, which decompose the state-space into a set of structural components and
utilize these partitioned components to realize efficient reachability computations.
With BDD-based traversal algorithms, some larger DESs could be solved without
causing the state-space explosion. Meanwhile, another problem is arising from the
BDD representation of the resultant supervisor. Since the original models have been
reformulated and encoded, it is cumbersome for the users to relate each state with the
corresponding BDD variables. Therefore, it is more convenient and natural to represent
the supervisor in a form similar to the models. In [8], a promising approach is pre-
sented, where a set of minimal and tractable logic expressions, referred to as guards,
are extracted from the supervisor and attached to the original models of the closed-loop
system. However, this approach computes the supervisor symbolically based on the
conjunctive partitioning technique. This might lead to the state-space explosion, due to
the large number of intermediate BDD nodes.
The main contribution of this paper is adapting a symbolic supervisory synthesis
approach to the guard generation procedure, to make it applicable for industrially in-
teresting applications. The approach automatically synthesizes a supervisor by taking
the advantage of the disjunctive partitioning technique. The monolithic state-space is
then split into a set of simpler components and the reachability search is performed
structurally with a set of heuristic decisions. Moreover, the guard generation procedure
is tailored to use the partitioned structure to extract the simplified guards and attach
them to the original models. Finally, a comparison of algorithm efficiency between two
partitioning techniques is made by applying them to a set of benchmark examples.
The paper is organized as follows: For the readers who might be unfamiliar with Su-
pervisory Control Theory, Section 2 gives an informal and brief explanation. Section 3
provides some preliminaries that are used throughout the paper. The symbolic supervi-
sory synthesis and the guard generation procedure will be discussed in detail in Section
4 and 5. In Section 6, we apply what we have discussed and implemented to several real
case studies. Finally, we end up with some conclusions in Section 7.
2
Motivating Example
For readers who might be unfamiliar with SCT, the following simple example gives a
brief overview and states what the exact problem this paper is about to solve.
