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

TL;DR

The paper tackles robotic planning under both quantifiable and unquantifiable uncertainty by modeling the problem as Markov Decision Processes with Set-Valued Transitions ($MDPSTs$) and specifying tasks with Linear Temporal Logic ($LTL$) objectives. It introduces a robust optimal synthesis framework that combines a product construction with a limit-deterministic Büchi automaton ($LDBA$), and a Winning Region ($WR$) to manage nondeterminism and unquantified uncertainty, all solved via a robust value iteration on a reduced submodel. A three-step method is presented: build the product $MDPST^{\times}$ with the $LDBA$, reduce to a reachability problem using the $WR$, and synthesize an optimal robust strategy from the resulting reachability. The approach demonstrates favorable scalability advantages over traditional $DRA$-based methods, validated by a hexagonal-grid mobile robot case study where the $LDBA$ representation reduces model size and computation time while maintaining robustness guarantees. This framework enables practical deployment of autonomous systems in environments with both stochastic and adversarial/unmodeled uncertainties, and paves the way for planning under temporal logic with cost constraints in future work.

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ü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.

Figures (5)

• Figure 1: Hexagonal world.
• Figure 2: Simulated trajectory of 2000 time steps for the LTL task $\varphi_{persistavoid}$, where the color bar denotes the time steps.
• Figure 3: The product MDPST $\mathcal{M}^\times$, where the sub-MDPST $\mathcal{M}_{sub}^\times$ (for the first iteration) is the part within the shaded box.
• Figure 4: The constructed product MDPST $\hat{\mathcal{M}}_{sub}^\times$.
• Figure 5: The product MDPST $\mathcal{M}_{sub}^\times$ for the second iteration.

Theorems & Definitions (15)

• Definition 1
• Definition 2: LDBA sickert2016limit
• Definition 3: MDPSTs
• Example 1: Hexagonal world
• Definition 4: Feasible distribution in MDPSTs
• Definition 5: Nature for MDPSTs yu2024trembling
• Definition 6: Robust strategy
• Definition 7: Optimal robust strategy
• Definition 8: Product MDPST
• Definition 9: EC for MDPs de1998formalbaier2008principles