Formal specification and synthesis of procedural controllers for process systems (Q1912012)

In this publication of the Lectures Notes, the tools and the methods for formal specification and synthesis of specialized controllers for hybrid (continuous and event-driven) processes are developed. The method is based on an extension of the supervisory control theory, capable of issuing controllable transitions and on consistent behaviour specifications of the system. The process is modelled using labelled finite state machines (FSM) suitably extended to consider intensive manipulations with states, while the behaviour is modelled using predicate logic statements and linear temporal logic (LTL). At the first stage, the dynamic specifications are exposed as LTL statements. At the second stage, the statements are translated into structures like labelled FSM and Petri Nets -- (the author calls them, \(a\)-machines). The structure of an \(a\)-machine is amenable to the formal proof of correctness. Having obtained a local controller for each specification, a global controller is introduced as the conjunction of all local controllers. If the resultant structure contains states in which more than one controllable transition exists, extra dynamic specification is involved. The four main steps of the method (process modelling, specification modelling, supervisory structure synthesis, procedural controller synthesis) are illustrated by realistic examples of chemical and other processes. There are 109 references, 65 figures and 49 tables. The book is intended for hybrid systems control software developers and process control engineers.