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.

翻译：本文研究非线性动力学系统混合控制器的自动综合问题，确保闭环系统满足任意的线性时序逻辑规范。此外，该规范可考虑由外部环境或系统自身触发的逻辑上下文切换。最终，我们旨在避免传统的暴力时间与空间离散化方法，以提升可扩展性。为实现这些目标，我们提出一种新颖的两层策略综合方法：下层生成的控制器提供不变集与吸引域，这些信息被上层逻辑层以抽象方式加以利用。为此，我们为上下层综合分别提供了新技术。该新方法能够以可扩展的方式，兼顾状态空间控制技术的计算能力与有限博弈求解处理复杂规范时的智能性。