Datensatz

Zusammenfassung

We consider the problem of automatically synthesizing a hybrid controller for
non-linear dynamical systems which ensures that the closed-loop fulfills an
arbitrary \emph{Linear Temporal Logic} specification. Moreover, the
specification may take into account logical context switches induced by an
external environment or the system itself. Finally, we want to avoid classical
brute-force time- and space-discretization for scalability. We achieve these
goals by a novel two-layer strategy synthesis approach, where the controller
generated in the lower layer provides invariant sets and basins of attraction,
which are exploited at the upper logical layer in an abstract way. In order to
achieve this, we provide new techniques for both the upper- and lower-level
synthesis.
Our new methodology allows to leverage both the computing power of state
space control techniques and the intelligence of finite game solving for
complex specifications, in a scalable way.