Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A*-based Temporal Logic Path Planning with User Preferences on Relaxed Task Satisfaction

Disha Kamale, Xi Yu, Cristian-Ioan Vasile

TL;DR

The paper tackles planning for syntactically co-safe Linear Temporal Logic (scLTL) tasks in large robotic environments when full task satisfaction is infeasible. It introduces an $A^*$-based framework that uses automata-based representations of the TL goals and user relaxation preferences, implemented via a Weighted Finite State Edit System and a relaxed specification automaton, while avoiding explicit product construction. A specially designed heuristic guides the search by estimating progress toward relaxed satisfaction, yielding substantial reductions in node explorations and memory use with near-optimal trajectory costs. The approach scales to city-scale graphs (e.g., NYC road network) and provides empirical bounds on suboptimality, making it practically impactful for real-time, large-scale robotic planning under user-defined relaxations.

Abstract

In this work, we consider the problem of planning for temporal logic tasks in large robot environments. When full task compliance is unattainable, we aim to achieve the best possible task satisfaction by integrating user preferences for relaxation into the planning process. Utilizing the automata-based representations for temporal logic goals and user preferences, we propose an A*-based planning framework. This approach effectively tackles large-scale problems while generating near-optimal high-level trajectories. To facilitate this, we propose a simple, efficient heuristic that allows for planning over large robot environments in a fraction of time and search memory as compared to uninformed search algorithms. We present extensive case studies to demonstrate the scalability, runtime analysis as well as empirical bounds on the suboptimality of the proposed heuristic.

A*-based Temporal Logic Path Planning with User Preferences on Relaxed Task Satisfaction

TL;DR

The paper tackles planning for syntactically co-safe Linear Temporal Logic (scLTL) tasks in large robotic environments when full task satisfaction is infeasible. It introduces an -based framework that uses automata-based representations of the TL goals and user relaxation preferences, implemented via a Weighted Finite State Edit System and a relaxed specification automaton, while avoiding explicit product construction. A specially designed heuristic guides the search by estimating progress toward relaxed satisfaction, yielding substantial reductions in node explorations and memory use with near-optimal trajectory costs. The approach scales to city-scale graphs (e.g., NYC road network) and provides empirical bounds on suboptimality, making it practically impactful for real-time, large-scale robotic planning under user-defined relaxations.

Abstract

In this work, we consider the problem of planning for temporal logic tasks in large robot environments. When full task compliance is unattainable, we aim to achieve the best possible task satisfaction by integrating user preferences for relaxation into the planning process. Utilizing the automata-based representations for temporal logic goals and user preferences, we propose an A*-based planning framework. This approach effectively tackles large-scale problems while generating near-optimal high-level trajectories. To facilitate this, we propose a simple, efficient heuristic that allows for planning over large robot environments in a fraction of time and search memory as compared to uninformed search algorithms. We present extensive case studies to demonstrate the scalability, runtime analysis as well as empirical bounds on the suboptimality of the proposed heuristic.

Paper Structure

This paper contains 17 sections, 1 theorem, 4 equations, 6 figures, 1 table, 1 algorithm.

Table of Contents

  1. Introduction
  2. Problem Setup
  3. Robot and Environment Model
  4. Temporal Logic Specification
  5. User preferences for relaxation
  6. Problem definition
  7. Approach
  8. Automata models for temporal logic
  9. Relaxed Specification Product Automaton
  10. Heuristic-based for TL planning with relaxation
  11. Heuristic discussion
  12. Case studies
  13. Functionality
  14. Large Scale Robot Environments
  15. Runtime analysis
  16. ...and 2 more sections

Key Result

Lemma III.1

The solution given by the proposed search algorithm always satisfies the specification. i.e., $\mathbf{\Tilde{o}}^{relax} = h(\tilde{\mathbf{x}}) \models \phi$.

Figures (6)

  • Figure 1: Runtime, memory, and precomputation time for $h=0, h_{info}$ and proposed heuristic $h$.
  • Figure 2: Trajectories obtained using baseline and the proposed heuristic. Nodes with atomic propositions of interest are shown in yellow.
  • Figure 3: Empirical determination of the scaling factor
  • Figure 4: Trajectories with relaxation obtained using baseline and the proposed heuristic. The green circles indicate satisfaction of a minimally relaxed subspecification. The red circle denotes a sub-optimal relaxation.
  • Figure 5: a) Effect of randomized AP assignment, b) Effect of varying $\mathcal{T}$ size
  • ...and 1 more figures

Theorems & Definitions (9)

  • Definition II.1: Transition System
  • Definition II.2: User Relaxation Preference
  • Example II.1
  • Definition III.1: Deterministic Finite State Automaton
  • Definition III.2: Weighted Finite State Edit System
  • Example III.1: Continuation of Example \ref{['ex:spec']}
  • Definition III.3: Relaxed Specification Automaton
  • Lemma III.1: correctness
  • proof