Hierarchical Decomposition of LTL Synthesis Problem for Nonlinear Control Systems
Hierarchical Decomposition of LTL Synthesis Problem for Nonlinear Control Systems
复制标题
DOI：
10.1109/tac.2019.2902643
复制
发表时间：
2017-12
影响因子：
6.8
通讯作者：
Pierre-Jean Meyer;Dimos V. Dimarogonas
中科院分区：
文献类型：
--
作者：
Pierre-Jean Meyer;Dimos V. Dimarogonas
研究了线性时间逻辑公式下连续非线性动力系统的控制综合问题。提出的解决方案是对控制问题进行自顶向下的分层分解，涉及问题的三个抽象层，从最粗到最细迭代求解。LTL规划首先在一个仅描述LTL公式中涉及的感兴趣区域的小型转换系统上求解。对于结果接受路径中满足LTL公式的每一对连续感兴趣的区域，然后在划分的工作空间中构造一个离散计划来连接这两个区域，同时避免不安全区域。最后，采用抽象细化的方法合成了一个控制器，使动力系统遵循每个离散规划。第二个主要贡献，用于第三抽象层，是一种新的基于单调性的方法来过逼近任何连续可微系统的有限时间可达集。最后，以扰动独轮车移动机器人的运动规划问题为例进行了仿真验证。
This paper deals with the control synthesis problem for a continuous nonlinear dynamical system under a linear temporal logic (LTL) formula. The proposed solution is a top-down hierarchical decomposition of the control problem involving three abstraction layers of the problem, iteratively solved from the coarsest to the finest. The LTL planning is first solved on a small transition system only describing the regions of interest involved in the LTL formula. For each pair of consecutive regions of interest in the resulting accepting path satisfying the LTL formula, a discrete plan is then constructed in the partitioned workspace to connect these two regions while avoiding unsafe regions. Finally, an abstraction refinement approach is applied to synthesize a controller for the dynamical system to follow each discrete plan. The second main contribution, used in the third abstraction layer, is a new monotonicity-based method to overapproximate the finite-time reachable set of any continuously differentiable system. The proposed framework is demonstrated in simulation for a motion planning problem of a mobile robot modeled as a disturbed unicycle.