線形時相論理仕様に基づく計画：定量化可能・不可能な不確実性への対処
Planning with Linear Temporal Logic Specifications: Handling Quantifiable and Unquantifiable Uncertainty
定量化可能・不可能な不確実性を統一的に扱うMDPST上で、LTL仕様を最適に満たすロボット計画手法を提案し、勝利領域の計算とロバスト価値反復で解く。
著者: Pian Yu, Yong Li, David Parker, Marta Kwiatkowska
分類: cs.RO, cs.FL
原文アブストラクト
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\"uchi 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.
