论文标题
最佳概率运动计划和潜在的不可行的LTL约束
Optimal Probabilistic Motion Planning with Potential Infeasible LTL Constraints
论文作者
论文摘要
本文研究了最佳运动计划,但应运动和环境不确定性。通过将系统建模为标有马尔可夫决策过程(PL-MDP)的概率,控制目标是合成有限的记忆策略,在该策略下,代理在其下满足了具有期望满意度的线性时间性时间逻辑(LTL)的复杂高级任务。特别是,考虑了满足无限范围任务的轨迹的成本优化,并分析了降低预期平均成本与最大化任务满意度的可能性之间的权衡。 LTL公式不使用传统的Rabin Automata,而是将其转换为具有可及性可接受条件和紧凑的图形结构的极限确定性BüchiAutomata(LDBA)。这项工作的新颖性在于考虑LTL规格可能是不可行的情况并在PL-MDP和LDBA之间开发松弛的产品MDP的情况。轻松的产品MDP允许代理商在任务不完全可行并量化修订后的计划的违反测量时修改其运动计划。然后提出多目标优化问题,以共同考虑任务满意度的概率,对原始任务约束的违规以及策略执行的实施成本。可以通过耦合线性程序来解决该法式问题。据我们所知,这项工作首先弥合了潜在的不可行的LTL规范的概率计划修订与计划前缀的最佳控制综合和无限层上轨迹后缀的最佳控制综合。提供实验结果以证明所提出的框架的有效性。
This paper studies optimal motion planning subject to motion and environment uncertainties. By modeling the system as a probabilistic labeled Markov decision process (PL-MDP), the control objective is to synthesize a finite-memory policy, under which the agent satisfies complex high-level tasks expressed as linear temporal logic (LTL) with desired satisfaction probability. In particular, the cost optimization of the trajectory that satisfies infinite horizon tasks is considered, and the trade-off between reducing the expected mean cost and maximizing the probability of task satisfaction is analyzed. Instead of using traditional Rabin automata, the LTL formulas are converted to limit-deterministic Büchi automata (LDBA) with a reachability acceptance condition and a compact graph structure. The novelty of this work lies in considering the cases where LTL specifications can be potentially infeasible and developing a relaxed product MDP between PL-MDP and LDBA. The relaxed product MDP allows the agent to revise its motion plan whenever the task is not fully feasible and quantify the revised plan's violation measurement. A multi-objective optimization problem is then formulated to jointly consider the probability of task satisfaction, the violation with respect to original task constraints, and the implementation cost of the policy execution. The formulated problem can be solved via coupled linear programs. To the best of our knowledge, this work first bridges the gap between probabilistic planning revision of potential infeasible LTL specifications and optimal control synthesis of both plan prefix and plan suffix of the trajectory over the infinite horizons. Experimental results are provided to demonstrate the effectiveness of the proposed framework.