CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Symbolic Supervisory Control of Resource Allocation Systems

Zhennan Fei (Institutionen för signaler och system, Automation)
Göteborg : Chalmers University of Technology, 2014. ISBN: 978-91-7597-007-3.- 208 s.

Supervisory control theory (SCT) is a formal model-based methodology for verification and synthesis of supervisors for discrete event systems (DES). The main goal is to guarantee that the closed-loop system fulfills given specifications. SCT has great promise to assist engineers with the generation of reliable control functions. This is, for instance, beneficial to manufacturing systems where both products and production equipment might change frequently.

The industrial acceptance of SCT, however, has been limited for at least two reasons: (i) the analysis of DES involves an intrinsic difficulty known as the state-space explosion problem, which makes the explicit enumeration of enormous state-spaces for industrial systems intractable; (ii) the synthesized supervisor, represented as a deterministic finite automaton (FA) or an extended finite automaton (EFA), is not straightforward to implement in an industrial controller.

In this thesis, to address the aforementioned issues, we study the modeling, synthesis and supervisor representation of DES using binary decision diagrams (BDDs), a compact data structure for representing DES models symbolically. We propose different kinds of BDD-based algorithms for exploring the symbolically represented state-spaces in an effort to improve the abilities of existing supervisor synthesis approaches to handle large-scale DES and represent the obtained supervisors appropriately.

Following this spirit, we bring the efficiencies of BDD into a particular DES application domain -- deadlock avoidance for resource allocation systems (RAS) -- a problem that arises in many technological systems including flexible manufacturing systems and multi-threaded software. We propose a framework for the effective and computationally efficient development of the maximally permissive deadlock avoidance policy (DAP) for various RAS classes. Besides the employment of symbolic computation, special structural properties that are possessed by RAS are utilized by the symbolic algorithms to gain additional efficiencies in the computation of the sought DAP. Furthermore, to bridge the gap between the BDD-based representation of the target DAP and its actual industrial realization, we extend this work by introducing a procedure that generates a set of "guard" predicates to represent the resulting DAP.

The work presented in this thesis has been implemented in the SCT tool Supremica. Computational benchmarks have manifested the superiority of the proposed algorithms with respect to the previously published results. Hence, the work holds a strong potential for providing robust, practical and efficient solutions to a broad range of supervisory control and deadlock avoidance problems that are experienced in the considered DES application domain.

Nyckelord: Supervisory Control Theory, Discrete Event System, Resource Allocation System, Binary Decision Diagram.

Den här publikationen ingår i följande styrkeområden:

Läs mer om Chalmers styrkeområden  

Denna post skapades 2014-05-01. Senast ändrad 2015-01-16.
CPL Pubid: 197435


Läs direkt!

Lokal fulltext (fritt tillgänglig)

Institutioner (Chalmers)

Institutionen för signaler och system, Automation (2005-2017)


Informations- och kommunikationsteknik

Chalmers infrastruktur


Datum: 2014-05-20
Tid: 10:15
Lokal: Room HC2, Hörsalsvägen 11, Göteborg
Opponent: Professor Stéphane Lafortune, Department of Electrical Engineering and Computer Science, University of Michigan, USA

Ingår i serie

Doktorsavhandlingar vid Chalmers tekniska högskola. Ny serie 3688