Supervisory Control of Concurrent Systems

Increasing complexity in engineering projects raises difficult challenges in industry and requires effective tools for correct-by-construction design or design verification. This book addresses the design of such tools for correct-by-construction synthesis of supervisors for systems and specifications represented in the discrete-event framework. The approach employed uses Petri nets as discrete-event models and structural methods for the synthesis of supervisors, and may lead to significant computational benefits.Highlighting recent progress in the design of supervisors by structural methods, the book represents a novel contribution to the field. One of the main features of the presentation is the demonstration that structural methods can address a variety of supervisor specifications under diverse supervision settings.Additional features of the text:* Applications of the methods presented are emphasized by considering various concurrency assumptions as well as types of system uncontrollability and unobservability.* Treatment of the supervision problem for decentralized settings and hybrid dynamical systems. * A focus on both theory and practice: formal proofs are provided in a sound mathematical setting to guarantee performance and correctness; at the same time, the authors have worked out the relevant details to ensure the methods are ready to implement in software.* Many of the presented methods have been realized in software as functions of a MATLAB toolbox, which have been used to solve many of the examples of the book.The work is self-contained and includes necessary background on Petri nets and supervision. Requiring only basic knowledge of undergraduate-level discrete mathematics, the text is accessible to a broad audience. Researchers and developers from various engineering fields may find effective means to reduce the complexity of design problems in the discrete-event setting. Graduate students may use the work as a self-study reference, and portions of the text may be used in advanced courses on discrete-event systems.