论文标题
当您无法做到这一切时该怎么办：具有柔和时间逻辑约束的时间逻辑计划
What to Do When You Can't Do It All: Temporal Logic Planning with Soft Temporal Logic Constraints
论文作者
论文摘要
在本文中，我们考虑了一个时间逻辑计划问题，其中目标是找到一个无限轨迹，该轨迹满足了从线性时间逻辑（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.
