Information Technology Reference
In-Depth Information
Symbolic State-Space Exploration and Guard
Generation in Supervisory Control Theory
Zhennan Fei, Sajed Miremadi, Knut Akesson, and Bengt Lennartson
Automation Research Group, Department of Signals and Systems
Chalmers University of Technology, G oteborg, Sweden
{zhennan,miremads,knut,bengt.lennartson}@chalmers.se
Abstract.
Supervisory Control Theory (SCT) is a model-based framework for
automatically synthesizing a supervisor that minimally restricts the behavior of a
plant such that given specifications is fulfilled. The main obstacle which prevents
SCT from having a major industrial breakthrough is that the supervisory synthe-
sis, consisting of a series of reachability tasks, suffers from the state-space ex-
plosion problem. To alleviate this problem, a well-known strategy is to represent
and explore the state-space symbolically by using Binary Decision Diagrams.
Based on this principle, an alternative symbolic state-space traversal approach,
depending on the disjunctive partitioning technique, is presented in this paper. In
addition, the approach is adapted to the prior work, the guard generation proce-
dure, to extract compact propositional formulae from a symbolically represented
supervisor. These propositional formulae, referred to as guards, are then attached
to the original model, resulting in a modular and comprehensible representation
of the supervisor.
Keywords:
Supervisory control theory, State-space exploration, Binary decision
diagrams, Partitioning techniques, Propositional formulae.
1
Introduction
The analysis of reactive systems has been paid much attention by researchers and scien-
tists in the computer science community. One of the classic methods to analyze reactive
systems is utilizing formal verification techniques, such as model checking, to verify
whether the considered system fulfills specifications. Nevertheless, from the control
engineering point of view, instead of verifying the correctness of the system, a con-
troller which guarantees that the system always behaves according to specifications is
preferred. Supervisory Control Theory (SCT) [1,2] provides such a control-theoretic
framework to design a device, called the
supervisor
, for reactive systems, referred to as
Discrete Event Systems (DESs). Given the model of a DES to be controlled, the
plant
,
and the intended behavior, the
specification
, the supervisor can be automatically syn-
thesized, guaranteeing that the closed-loop system fulfills given specifications. SCT has
been applied for various applications in different areas such as automated manufactur-
ing lines and embedded systems [3,4,5].
Generally, a supervisor is a function that, given a set of events, restricts the plant to
execute desired events according to the specification. A typical issue is how to realize
