Planning with Linear Temporal Logic Specifications: Handling Quantifiable and Unquantifiable Uncertainty

TL;DR

This paper presents a novel framework for robotic planning under both quantifiable and unquantifiable uncertainty using MDPSTs and LTL specifications, introducing new algorithms for strategy synthesis and validation through a case study.

Contribution

It introduces a unified modeling framework with MDPSTs and a new solution technique leveraging LDBAs for efficient robust strategy synthesis under LTL constraints.

Findings

Efficient algorithms for computing Winning Regions in MDPSTs.

Successful validation through a mobile robot case study.

Promising efficiency improvements over existing methods.

Abstract

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.