Time-Robust Path Planning with Piece-Wise Linear Trajectory for Signal Temporal Logic Specifications

TL;DR

This work studies time-robust path planning for synthesizing robots' trajectories that adhere to spatial-temporal specifications expressed in Sig-nal Temporal Logic (STL), and proposes quantitative semantics for PWL signals according to the recursive syntax of STL and proves their soundness.

Abstract

Real-world scenarios are characterized by timing uncertainties, e.g., delays, and disturbances. Algorithms with temporal robustness are crucial in guaranteeing the successful execution of tasks and missions in such scenarios. We study time-robust path planning for synthesizing robots' trajectories that adhere to spatial-temporal specifications expressed in Signal Temporal Logic (STL). In contrast to prior approaches that rely on {discretize}d trajectories with fixed time steps, we leverage Piece-Wise Linear (PWL) signals for the synthesis. PWL signals represent a trajectory through a sequence of time-stamped waypoints. This allows us to encode the STL formula into a Mixed-Integer Linear Program (MILP) with fewer variables. This reduction is more pronounced for specifications with a long planning horizon. To that end, we define time-robustness for PWL signals. Subsequently, we propose quantitative semantics for PWL signals according to the recursive syntax of STL and prove their soundness. We then propose an encoding strategy to transform our semantics into a MILP. Our simulations showcase the soundness and the performance of our algorithm.

Figures (2)

• Figure 1: Examples of atomic predicates and its negation with PWL segment. The grey area denotes the original polygon $\mathcal{P}$. The shrunk/bloated polygons by $\epsilon$ distant margin are the inner/outer dotted lines respectively. The black lines denote the segment is "inside" the shrunk region ($z_2$) or "outside" the bloated region ($z_1$). The red segments $z_3, z_4$ are neither "inside" nor "outside" $\mathcal{P}$.
• Figure 2: Experiment results of four scenarios with different complexity. In each figure, the blue dots are the synthesized waypoints. The PWL signal is the blue piecewise-linear connecting the waypoints. The $XY$ plane consists of the reach (green/dark blue)-avoid (red/yellow) regions. The $Z$ axis denotes the synthesized time-stamp in seconds. The starting and ending positions are the declared markers as shown in the figures' legends.

Theorems & Definitions (11)

• Definition 1: STL Syntax
• Definition 2: Qualitative Semantics of STL formulas
• Definition 3: Waypoint
• Definition 4: Linear Waypoint Segment
• Definition 5: PWL Trajectory
• Example 1
• Definition 6: Time Robustness STL for PWL Signal
• Theorem 1: Soundness
• proof
• Remark 1: Feasibility