Optimal temporal logic planning with cascading soft constraints

Optimal temporal logic planning with cascading soft constraints
复制标题

DOI:
10.1109/iros40897.2019.8968261
复制
发表时间:
2019-11
期刊:
2019 IEEE/RSJ International Conference on Intelligent Robots and Systems (IROS)
影响因子:
--
通讯作者:
Hazhar Rahmani;J. O’Kane
Hazhar Rahmani;J. O’Kane
中科院分区:
其他
文献类型:
--
作者:
Hazhar Rahmani;J. O’Kane

文献摘要

被引文献

相似文献

在本文中,我们讨论了时间逻辑规划问题,给出了机器人任务的硬规范和对实现任务的计划的软偏好。特别地,我们考虑了这样一个问题,它的输入是一个转换系统、一个指定机器人任务的线性时序逻辑(LTL)公式,以及一个用有限迹上的线性动态逻辑(LDLf)表示的公式的有序序列,该公式序列指定了用户应该如何完成任务的偏好。规划者的目标是在这个过渡系统上合成一个无限的轨迹,该轨迹最符合用户对该轨迹的有限前缀的偏好,同时仍然满足总体目标。我们描述了这个问题的一个算法,它根据输入构造一个乘积自动机--实际上是一种特殊的状态加权Büchi自动机--在这个自动机上综合一个最优轨迹。这个综合问题可以通过归结为顶点赋权图中的极小极大路问题来解决,该问题可以通过计算图中最短路径的标准算法的变体来解决,或者通过顶点赋权图上的所有对瓶颈路问题的算法来解决。我们通过一些案例研究展示了该方法的适用性,并给出了一个实现的计算结果。
In this paper, we address the problem of temporal logic planning given both hard specifications of the robot’s mission and soft preferences on the plans that achieve the mission. In particular, we consider a problem whose inputs are a transition system, a linear temporal logic (LTL) formula specifying the robot’s mission, and an ordered sequence of formulas expressed in linear dynamic logic over finite traces (LDLf) specifying the user’s preferences for how the mission should be completed. The planner’s objective is to synthesize, on this transition system, an infinite trajectory that best fits the user’s preferences over finite prefixes of that trajectory while nonetheless satisfying the overall objective. We describe an algorithm for this problem that constructs, from the inputs, a product automaton —which is, in fact, a special kind of state-weighted Büchi automaton— over which an optimal trajectory is synthesized. This synthesis problem is solved via reduction to the minimax path problem in vertex weighted graphs, which can be solved by variants of the standard algorithms for computing shortest paths in a graph or by algorithms for the all-pairs bottleneck paths problem on vertex-weighted graphs. We show the applicability of the approach via some case studies, for which we present results computed by an implementation.