用统一框架处理机器人规划中的可量化与不可量化不确定性
Planning with Linear Temporal Logic Specifications: Handling Quantifiable and Unquantifiable Uncertainty
- 基于带集合转移的马尔可夫决策过程建模不确定环境
- 提出新算法实现线性时序逻辑任务的最优鲁棒策略合成
- 适合研究智能机器人自主决策与形式化验证的学者
本文研究在可量化和不可量化不确定性并存条件下，机器人系统的规划问题。目标是使机器人能够最优地完成由线性时序逻辑（LTL）公式描述的高层任务。为在统一建模框架中刻画两类不确定性，我们采用带集合转移的马尔可夫决策过程（MDPST）。针对具有LTL规范的MDPST，提出一种新的最优鲁棒策略合成方法。为提升效率，利用极限确定性巴乌奇自动机（LDBA）表示LTL，以利用其高效的构造特性。为应对MDPST固有的非确定性带来的挑战——该挑战使得将LTL规划问题转化为可达性问题变得困难——我们引入了适用于MDPST的获胜区域（WR）概念，并提出在MDPST与LDBA乘积图上计算WR的算法。最后，调用鲁棒值迭代算法求解可达性问题。通过在六边形世界中移动机器人的案例研究验证了方法的有效性，展示了显著的效率提升。
原文摘要 · Abstract (English)
This work studies the planning problem for robotic systems under both quantifiable and unquantifiable uncertainty. The objective is to enable the robotic systems to optimally fulfill high-level tasks specified by Linear Temporal Logic (LTL) formulas. To capture both types of uncertainty in a unified modelling framework, we utilise Markov Decision Processes with Set-valued Transitions (MDPSTs). We introduce a novel solution technique for the optimal robust strategy synthesis of MDPSTs with LTL specifications. To improve efficiency, our work leverages limit-deterministic Büchi automata (LDBAs) as the automaton representation for LTL to take advantage of their efficient constructions. To tackle the inherent nondeterminism in MDPSTs, which presents a significant challenge for reducing the LTL planning problem to a reachability problem, we introduce the concept of a Winning Region (WR) for MDPSTs. Additionally, we propose an algorithm for computing the WR over the product of the MDPST and the LDBA. Finally, a robust value iteration algorithm is invoked to solve the reachability problem. We validate the effectiveness of our approach through a case study involving a mobile robot operating in the hexagonal world, demonstrating promising efficiency gains.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。