Reactive sampling-based path planning with temporal logic specifications
Reactive sampling-based path planning with temporal logic specifications
复制标题
DOI：
10.1177/0278364920918919
复制
发表时间：
2020-06-04
影响因子：
9.2
通讯作者：
Belta, Calin
中科院分区：
文献类型：
--
作者：
Vasile, Cristian Ioan;Li, Xiao;Belta, Calin
我们开发了一种基于采样的运动规划算法，该算法结合了长期时间逻辑目标和短期反应需求。任务规范有两个部分：(1)作为一组发生在已知环境区域的静态服务请求的线性时间逻辑（LTL）公式给出的全局规范，以及(2)需要为一组动态请求提供服务的本地规范，这些请求在执行期间可以在本地感知。提出的计算框架包括两个主要部分：(a)基于离线采样的算法，用于构建包含满足LTL公式的路径的全局过渡系统；(b)一种基于在线采样的算法来生成满足局部请求的路径，同时确保不影响全局规范的满意度。离线算法有四个主要特点。首先，它是增量的，从某种意义上说，在每次迭代中寻找令人满意的路径的过程只与该迭代中生成的新样本的数量有关。其次，底层图是稀疏的，这意味着整个方法的复杂性很低。第三，它在概率上是完整的。第四，在一些温和的假设下，它具有可能的最佳复杂性界限。在线算法利用LTL监控和潜在功能的思想，确保在服务本地感知请求的同时满足全局规范。最后给出了实例和实验，说明了该框架的有效性和性能。
We develop a sampling-based motion planning algorithm that combines long-term temporal logic goals with short-term reactive requirements. The mission specification has two parts: (1) a global specification given as a linear temporal logic (LTL) formula over a set of static service requests that occur at the regions of a known environment, and (2) a local specification that requires servicing a set of dynamic requests that can be sensed locally during the execution. The proposed computational framework consists of two main ingredients: (a) an off-line sampling-based algorithm for the construction of a global transition system that contains a path satisfying the LTL formula; and (b) an on-line sampling-based algorithm to generate paths that service the local requests, while making sure that the satisfaction of the global specification is not affected. The off-line algorithm has four main features. First, it is incremental, in the sense that the procedure for finding a satisfying path at each iteration scales only with the number of new samples generated at that iteration. Second, the underlying graph is sparse, which implies low complexity for the overall method. Third, it is probabilistically complete. Fourth, under some mild assumptions, it has the best possible complexity bound. The on-line algorithm leverages ideas from LTL monitoring and potential functions to ensure progress towards the satisfaction of the global specification while servicing locally sensed requests. Examples and experimental trials illustrating the usefulness and the performance of the framework are included.