Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Safe Planning through Incremental Decomposition of Signal Temporal Logic Specifications

Parv Kapoor, Eunsuk Kang, Romulo Meira-Goes

TL;DR

This paper addresses the computational bottleneck of planning from complex, deeply nested STL specifications in robotic planning. It introduces STLInc, a decomposition-based approach that reformulates an STL formula as two constraint sets—reachability and invariance—augmented by a flattening step that introduces symbolic time variables, followed by symbolic time resolution and incremental scheduling of atomic tasks. The method yields correct-by-construction plans that satisfy the original specification and demonstrates superior performance for long-horizon, deeply nested tasks on linear and nonlinear dynamics compared to state-of-the-art MILP encodings. The approach is planner-agnostic and dynamics-agnostic, enabling runtime planning under tight computational budgets and often improving robustness in challenging planning scenarios.

Abstract

Trajectory planning is a critical process that enables autonomous systems to safely navigate complex environments. Signal temporal logic (STL) specifications are an effective way to encode complex temporally extended objectives for trajectory planning in cyber-physical systems (CPS). However, planning from these specifications using existing techniques scale exponentially with the number of nested operators and the horizon of specification. Additionally, performance is exacerbated at runtime due to limited computational budgets and compounding modeling errors. Decomposing a complex specification into smaller subtasks and incrementally planning for them can remedy these issues. In this work, we present a way to decompose STL requirements temporally to improve planning efficiency and performance. The key insight in our work is to encode all specifications as a set of reachability and invariance constraints and scheduling these constraints sequentially at runtime. Our proposed technique outperforms the state-of-the-art trajectory synthesis techniques for both linear and non linear dynamical systems.

Safe Planning through Incremental Decomposition of Signal Temporal Logic Specifications

TL;DR

This paper addresses the computational bottleneck of planning from complex, deeply nested STL specifications in robotic planning. It introduces STLInc, a decomposition-based approach that reformulates an STL formula as two constraint sets—reachability and invariance—augmented by a flattening step that introduces symbolic time variables, followed by symbolic time resolution and incremental scheduling of atomic tasks. The method yields correct-by-construction plans that satisfy the original specification and demonstrates superior performance for long-horizon, deeply nested tasks on linear and nonlinear dynamics compared to state-of-the-art MILP encodings. The approach is planner-agnostic and dynamics-agnostic, enabling runtime planning under tight computational budgets and often improving robustness in challenging planning scenarios.

Abstract

Trajectory planning is a critical process that enables autonomous systems to safely navigate complex environments. Signal temporal logic (STL) specifications are an effective way to encode complex temporally extended objectives for trajectory planning in cyber-physical systems (CPS). However, planning from these specifications using existing techniques scale exponentially with the number of nested operators and the horizon of specification. Additionally, performance is exacerbated at runtime due to limited computational budgets and compounding modeling errors. Decomposing a complex specification into smaller subtasks and incrementally planning for them can remedy these issues. In this work, we present a way to decompose STL requirements temporally to improve planning efficiency and performance. The key insight in our work is to encode all specifications as a set of reachability and invariance constraints and scheduling these constraints sequentially at runtime. Our proposed technique outperforms the state-of-the-art trajectory synthesis techniques for both linear and non linear dynamical systems.
Paper Structure (8 sections, 7 equations, 2 figures)

This paper contains 8 sections, 7 equations, 2 figures.

Table of Contents

  1. Introduction
  2. Motivation
  3. Preliminaries
  4. Approach
  5. Basic Concepts and Definitions
  6. STL fragment
  7. Task constraints
  8. Flattening

Figures (2)

  • Figure 1: Left: An STL specification $\phi$ with multiple nested temporal operators and a possible decomposition into subtasks. Right: A sample trajectory that satisfies $\phi$ in a planar environment.
  • Figure 2: Overview of the StlInc approach

Theorems & Definitions (5)

  • definition thmcounterdefinition
  • definition thmcounterdefinition
  • definition thmcounterdefinition: Reachability set
  • definition thmcounterdefinition: Invariance set
  • definition thmcounterdefinition: Time variable intervals