What to Do When You Can’t Do It All: Temporal Logic Planning with Soft Temporal Logic Constraints
What to Do When You Can’t Do It All: Temporal Logic Planning with Soft Temporal Logic Constraints
复制标题
DOI：
10.1109/iros45743.2020.9341412
复制
发表时间：
2020-08
期刊：
影响因子：
--
通讯作者：
Hazhar Rahmani;J. O’Kane
中科院分区：
文献类型：
--
作者：
Hazhar Rahmani;J. O’Kane
在本文中，我们考虑一个时序逻辑规划问题，其目标是找到一个无限的轨迹，满足最优选择从一组软规格表示在线性时序逻辑（LTL），同时满足硬规格表示在LTL。我们以前的工作考虑了一个类似的问题，其中线性动态逻辑有限迹（LDLf），而不是LTL，用于表示软约束。在这项工作中，LDLf被用来对无限轨迹的有限前缀施加约束。通过使用LTL，人们不仅能够对轨迹的有限前缀施加约束，而且还能够在整个无限轨迹上设置“软”目标。我们的算法首先构造一个产品自动机，在其上的规划问题被减少到计算一个最小成本的套索。在所有这样的套索中，期望计算最短的套索。虽然我们证明了计算这样一个最短的套索是计算困难的，我们也引入了一个有效的贪婪的方法来合成短套索。我们提出了两个案例研究，描述了这种方法的实施，并报告我们的实验结果比较我们的贪婪算法与最佳基线。
In this paper, we consider a temporal logic planning problem in which the objective is to find an infinite trajectory that satisfies an optimal selection from a set of soft specifications expressed in linear temporal logic (LTL) while nevertheless satisfying a hard specification expressed in LTL. Our previous work considered a similar problem in which linear dynamic logic for finite traces (LDLf), rather than LTL, was used to express the soft constraints. In that work, LDLf was used to impose constraints on finite prefixes of the infinite trajectory. By using LTL, one is able not only to impose constraints on the finite prefixes of the trajectory, but also to set ‘soft’ goals across the entirety of the infinite trajectory. Our algorithm first constructs a product automaton, on which the planning problem is reduced to computing a lasso with minimum cost. Among all such lassos, it is desirable to compute a shortest one. Though we prove that computing such a shortest lasso is computationally hard, we also introduce an efficient greedy approach to synthesize short lassos nonetheless. We present two case studies describing an implementation of this approach, and report results of our experiment comparing our greedy algorithm with an optimal baseline.