Context-triggered Abstraction-based Control Design

We consider the problem of automatically synthesizing a hybrid controller fornon-linear dynamical systems which ensures that the closed-loop fulfills anarbitrary \emph{Linear Temporal Logic} specification. Moreover, thespecification may take into account logical context switches induced by anexternal environment or the system itself. Finally, we want to avoid classicalbrute-force time- and space-discretization for scalability. We achieve thesegoals by a novel two-layer strategy synthesis approach, where the controllergenerated 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 toachieve this, we provide new techniques for both the upper- and lower-levelsynthesis. Our new methodology allows to leverage both the computing power of statespace control techniques and the intelligence of finite game solving forcomplex specifications, in a scalable way.