论文标题
实时时间逻辑的自动轨迹合成
Automatic Trajectory Synthesis for Real-Time Temporal Logic
论文作者
论文摘要
许多安全 - 关键系统必须以保证的安全性和正确性来实现高级任务规格。通过时间逻辑规范的控制器合成，最近取得了最新的进展。但是，现有的方法仅限于相对较短和简单的规格。此外，现有方法要么考虑对状态空间的事先离散化，只处理时间逻辑的凸片段，或者未经证明是完整的。我们提出了一种可扩展的，可证明的完整算法，该算法合成连续轨迹以满足非convex \ gls*{rtl}规格。我们将离散的任务计划和持续的运动计划分开，并且利用高效的布尔可满足性（SAT）和\ gls*{lp}求解器，以找到可动态可行的轨迹，这些轨迹满足了高维系统的非convex \ gls*{rtl}规格。所提出的设计算法被证明是声音和完整的，模拟结果证明了我们的方法的可伸缩性。
Many safety-critical systems must achieve high-level task specifications with guaranteed safety and correctness. Much recent progress towards this goal has been made through controller synthesis from temporal logic specifications. Existing approaches, however, have been limited to relatively short and simple specifications. Furthermore, existing methods either consider some prior discretization of the state-space, deal only with a convex fragment of temporal logic, or are not provably complete. We propose a scalable, provably complete algorithm that synthesizes continuous trajectories to satisfy non-convex \gls*{rtl} specifications. We separate discrete task planning and continuous motion planning on-the-fly and harness highly efficient boolean satisfiability (SAT) and \gls*{lp} solvers to find dynamically feasible trajectories that satisfy non-convex \gls*{rtl} specifications for high dimensional systems. The proposed design algorithms are proven sound and complete, and simulation results demonstrate our approach's scalability.
