Symbolic approaches for the control of non linear systems

In the field of automation, the use of mathematical models that are as faithful as possible (non-linear, with constraints on states and commands, with disturbances, etc.) generally increases reliability and confidence in the results obtained from the analysis of these models. Unfortunately, this complexity of the models makes the controller synthesis stage all the more difficult, if not sometimes impossible. On the other hand, although there is an extensive bibliography considering classical control objectives of continuous automation such as stability, these methods are not the most suitable for dealing with other types of specifications such as safety, achievability, or the rich range of properties that can be described by automata or temporal logic formulas found in the fields of computer science and robotics.

The symbolic approaches presented in this article aim to tackle the intersection of these two points. These approaches are based on three successive steps:

• abstraction of the continuous dynamic system into a discrete symbolic model described by a dynamic system with a finite number of states and commands;

• controller synthesis in the discrete domain ;

• the concretization of the symbolic controller for its application to the original continuous system.

In contrast to predictive control methods, all three steps are carried out offline, and the online application of the realized controller is carried out via a simple mapping table.

These approaches based on symbolic abstraction have a number of advantages. The first is that they can handle a very wide range of complex nonlinear dynamic systems (with disturbances, uncertainties, state or control constraints) in a completely automatic way, since controller synthesis in the discrete domain is independent of the form and complexity of continuous dynamics. They also make it possible to address a new range of more varied and complex specifications than those traditionally considered in continuous automatics, such as temporal logic formulas. On the other hand, the algorithms used for synthesis in the discrete domain come from the fields of formal methods and model checking, and enable formal guarantees of specification satisfaction to be obtained even after the controller has been concretized to the continuous domain; the controller is thus certified as "correct by construction". Finally, since the first stage of symbolic abstraction relies on methods based on over-approximations of all the system's real behaviours, the overall approach is endowed with a certain intrinsic robustness, in addition to taking into account model perturbations and uncertainties. On the other hand, the...