An approach to the automatic synthesis of controllers with mixed qualitative/quantitative specifications.

Abstract

The world of systems and control guides more of our lives than most of us realize. Most of the products we rely on today are actually systems comprised of mechanical, electrical or electronic components. Engineering these complex systems is a challenge, as their ever growing complexity has made the analysis and the design of such systems an ambitious task. This urged the need to explore new methods to mitigate the complexity and to create simplified models. The answer to these new challenges? \textit{Abstractions}. An abstraction of the the continuous dynamics is a \textit{symbolic model}, where each ``symbol'' corresponds to an ``aggregate'' of states in the continuous model. Symbolic models enable the \textit{correct-by-design} synthesis of controllers and the synthesis of controllers for classes of specifications that traditionally have not been considered in the context of continuous control systems. These include \textit{qualitative} specifications formalized using temporal logics, such as \acf{LTL}. Besides addressing qualitative specifications, we are also interested in synthesizing controllers with \textit{quantitative} specifications, in order to solve optimal control problems. To date, the use of symbolic models for solving optimal control problems, is not well explored. This MSc Thesis presents a new approach towards solving problems of optimal control. Without loss of generality, such control problems are considered as path-planning problems on finite graphs, for which we provide two shortest path algorithms; one deterministic \acf{SDSP} algorithm and one non-deterministic \acs{SDSP} algorithm, in order to solve problems with quantitative specifications in both deterministic and non-deterministic systems. The fact that certain classes of qualitative specifications result in the synthesis of (maximally-permissive) controllers, enables us to use the \acs{SDSP} algorithms to also enforce quantitative specifications. This, however, is not the only path towards our goal of synthesizing controllers with mixed qualitative-quantitative specifications; it is possible to use the \acs{SDSP} algorithms directly to synthesize controllers for the same classes of specifications. Finally, we implement the algorithms as an extension to the \texttt{MATLAB} toolbox \texttt{Pessoa}, using Binary Decision Diagrams (BDDs) as our main data structure.