Planning with linear temporal logic specifications: handling quantifiable and unquantifiable uncertainty

Conference item

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 complicates the reduction of 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.

Authors: Yu, P; Parker, D; Li, Y; Kwiatkowska, M

• Publication status: Published
• Peer review status: Peer reviewed
• Publisher: IEEE
• Host title: 2025 IEEE International Conference on Robotics and Automation (ICRA)
• Pages: 3940-3946
• Publication date: 2025-09-02
• Acceptance date: 2025-01-27
• Event title: IEEE International Conference on Robotics and Automation (ICRA 2025)
• Event location: Atlanta, GA, USA
• Event website: https://2025.ieee-icra.org/
• Event start date: 2025-05-19
• Event end date: 2025-05-23
• DOI: 10.1109/ICRA55743.2025.11127333
• EISBN: 9798331541392
• ISBN: 9798331541408
• Language: English