This paper presents an algorithmic framework for control synthesis of continuous dynamical systems subject to signal temporal logic (STL) specifications. We propose a novel algorithm to obtain a time-partitioned finite automaton from an STL specification, and introduce a multi-layered framework that utilizes this automaton to guide a sampling-based search tree both spatially and temporally. Our approach is able to synthesize a controller for nonlinear dynamics and polynomial predicate functions. We prove the correctness and probabilistic completeness of our algorithm, and illustrate the efficiency and efficacy of our framework on several case studies. Our results show an order of magnitude speedup over the state of the art.

翻译：本文为根据信号时间逻辑(STL)规格对连续动态系统进行控制合成提供了一个算法框架。我们提出了一个新的算法框架,以便从STL规格中获取一个有时间间隔的有限自动图,并引入一个多层框架,利用这个自动图在空间和时间上指导一个基于取样的搜索树。我们的方法可以合成一个控制器,用于非线性动态和多线性上游功能。我们证明了我们的算法的正确性和概率完整性,并展示了我们在若干案例研究中框架的效率和效力。我们的结果显示,在艺术状态上,数量在加速。