Motion Planning with Temporal Logic Specifications

Overview

As robotics applications expand into autonomous driving, search-and-rescue, manipulation, and medicine, motion planning must go beyond simple collision avoidance and reachability. Tasks now require formal specifications of coverage, sequencing, and temporal ordering — e.g., “inspect areas A, B, C in order” or “never enter zone D until zone E is cleared.” This seminar work surveys how temporal logics are used to formalize these higher-level task specifications and integrate them into motion planning for robotic systems with complex, nonlinear dynamics.

Challenge

Integrated task and motion planning requires reasoning over a hybrid discrete/continuous space: discrete task-level decisions (which regions to visit, in what order) coupled with continuous trajectory generation (collision-free, dynamically-feasible motions). Standard motion planning algorithms like PRM and RRT are designed for reachability — they have no built-in mechanism for enforcing temporal task constraints. The key challenge is bridging formal verification methods from model checking with sampling-based motion planners that operate in high-dimensional state spaces.

Temporal Logics for Task Specification

The paper reviews three families of temporal logics and their trade-offs for motion planning:

• LTL (Linear Temporal Logic) — Models time as a sequence of states extending infinitely into the future. Supports operators like “eventually” (F), “always” (G), “next” (X), and “until” (U). Well-suited for motion planning since trajectories are linear-time in nature. Can express coverage (F p1 ∧ … ∧ F pn), sequencing, and temporal ordering. However, LTL cannot express existential path properties (“there exists a path where…”).
• CTL (Computation Tree Logic) — Models time as a branching tree with path quantifiers (for-all A, exists E). Can express properties LTL cannot, such as “there exists a future where the robot stays idle.” However, CTL cannot freely alternate between temporal and path quantifiers.
• CTL* — Combines the expressive power of both LTL and CTL by dropping the constraint that every temporal operator must be paired with a path quantifier. More expressive but computationally much more expensive for model checking, so LTL and CTL remain dominant in practice.

Approaches to Integration

Controller Synthesis from Temporal Logic

This approach obtains discrete abstractions of the system by decomposing continuous state space into polytopes, defines propositions over these regions, and uses model checking to compute a discrete path (sequence of regions) satisfying the temporal specification. Controllers must then generate collision-free, dynamically-feasible motions between regions. Best suited for lower-dimensional systems where polytope decomposition is tractable.

Sampling-Based Methods with Temporal Logics

For high-dimensional systems with nonlinear dynamics, the paper reviews multi-layered approaches that couple discrete planning with sampling-based motion planning:

• Incremental Model Checking (Karaman & Frazzoli) — Extends RRT into a Rapidly-exploring Random Graph (RRG) that constructs a Kripke structure incrementally. At each iteration, the structure is checked against the specification using Tarski-Knaster iteration. The resulting trajectory satisfies the given temporal logic formula.
• Online/Offline Planning (Vasile et al.) — Addresses reactivity to environmental changes. A sparse global Kripke structure is built offline for global LTL goals (translated to Buchi automata), while a local RRT-based planner handles online requests and newly sensed obstacles. The local planner checks paths against specifications and reconnects to the global plan.
• Multi-Layered Synergistic Planning (Bhatia et al.) — Separates planning into a discrete layer (automaton from temporal logic + workspace decomposition) and a continuous layer (sampling-based trajectory generation). The layers exchange feedback iteratively: the discrete plan guides continuous search, and infeasibility in the continuous layer refines the discrete plan.

Extensions of Temporal Logics

The survey covers four categories of extensions addressing limitations of standard temporal logics:

Time Constraints

• MTL (Metric Temporal Logic) — Extends LTL with time-bounded temporal operators (e.g., “reach goal within 10 seconds”). Used with timed automata models.
• MITL (Metric Interval Temporal Logic) — MTL fragment requiring interval constraints instead of singletons. Combined with timed automata and UPPAAL model checker for path generation.
• STL (Signal Temporal Logic) — Extends MTL with numerical predicates over real-valued variables, enabling reasoning about hybrid systems with both discrete and continuous dynamics. Handles noise and approximations but has high computational complexity for high-dimensional nonlinear systems.

Probabilistic Quantification

• PCTL (Probabilistic Computation Tree Logic) — Extends CTL with probability bounds over path quantifiers (e.g., “at least 98% probability the robot inspects area A”). Used with Markov Decision Processes to handle probabilistic robot actions and uncertain environments.

Quantitative Semantics

• TLTL (Truncated Linear Temporal Logic) — Replaces binary satisfaction with a continuous robustness degree indicating how far a signal is from satisfying or violating a specification. Used as reward functions for reinforcement learning, with faster convergence than heuristic rewards.

Spatio-Temporal Logics

• SSTL (Signal Spatio-Temporal Logic) — Extends STL with spatial operators (somewhere, everywhere, surround) for distributed and networked systems like robotic teams or smart grids.
• STREL (Spatio-Temporal Reach and Escape Logic) — Generalizes SSTL with reach and escape operators, supporting dynamic/mobile networks in addition to static spatial models.

Key Takeaways

1. LTL and its extensions are the most commonly used temporal logics for motion planning due to their natural fit with linear-time trajectory planning and relative computational tractability.
2. Sampling-based methods (RRG, multi-layered planners) are the primary approach for high-dimensional systems, as polytope decomposition becomes intractable in high dimensions.
3. Temporal logics with time constraints (MTL, STL) are necessary for real-time systems like autonomous driving, but their computational cost remains a significant barrier.
4. Open challenges include scaling to highly dynamic environments, handling high-dimensional nonlinear dynamics with timing constraints, and extending beyond known or partially known environments.

Tools & Technologies

• Temporal Logics (LTL, CTL, CTL*, STL, MTL) — Formal specification of task-level goals with varying expressiveness
• Model Checking (Buchi Automata, Tarski-Knaster, UPPAAL) — Verification of temporal specifications against system models
• Sampling-Based Motion Planning (RRT, RRG, PRM) — Trajectory generation in high-dimensional continuous spaces
• CommonRoad — Benchmark scenarios for autonomous driving motion planning