Source-linked AI summary
Safety-aware Model Predictive Path Integral Control with Signal Temporal Logic
Yiqi Zhao, Taekyung Kim, Hideki Okamoto, Bardh Hoxha, Jyotirmoy V. Deshmukh, Lars Lindemann, Georgios Fainekos
TL;DR
Safety-aware motion planning needs to handle time-critical missions with complex STL specifications while maintaining safety. The paper integrates discrete-time STL-to-CBF encoding with MPPI in a sampling-based receding-horizon planner. Across Mars Rover case studies and a quadcopter simulation, the method demonstrates high safety and computational efficiency.
Problem
General STL satisfaction remains unresolved in MPPI, while online mixed-integer approaches can be computationally expensive.
Method
The method constructs time-varying CBFs for discrete-time STL formulas, incorporates them into MPPI weighting, and projects violating rollouts toward the CBF zero-superlevel set.
Results
100% empirical STL satisfaction was achieved in the evaluated Mars Rover trials, with computational efficiency demonstrated across diverse costs and environments.
Takeaways & Limitations
The framework combines sampling-based receding-horizon planning with CBF-informed constraints for STL specifications and customized cost functions.
Abstract
from arXiv · showhide
Safety-aware motion planning remains a challenge in robotics, especially when missions are time-critical and are under complex specifications. In this paper, we propose safety-aware-stl-mppi, a computationally efficient sampling-based receding-horizon planning framework designed to promote satisfaction of constraints expressed in Signal Temporal Logic (STL). Our approach encodes discrete-time STL formulas into candidate time-varying control barrier functions (CBF), which are integrated into a model predictive path integral (MPPI) controller. Our method inherits the benefits of low computational cost from an efficiently parallelizable sampling based planner and utilizes CBF for constraints expressed in STL. We compare against several MPPI baselines using four artificial Mars Rover planning case studies with a diverse environment and cost setups, where we show our method consistently achieving high safety and efficiency. We show a quadcopter planning experiment with NVIDIA Isaac Lab.
I. INTRODUCTION
STL provides a formal language for real-time spatio-temporal requirements, but satisfying general STL formulas in MPPI remains unresolved. The paper proposes safety-aware-stl-mppi, which combines discrete-time time-varying CBFs with MPPI to promote STL satisfaction while retaining customized costs and sampling-based efficiency.
- STL expresses rich real-time spatio-temporal safety and mission requirements for planning.
- General STL satisfaction remains unresolved in MPPI, despite MPPI’s parallelizability and optimality guarantees.
- Safety-aware-stl-mppi incorporates STL specifications as CBF-informed constraints while minimizing a user-defined cost function.
- The method adapts time-varying CBF encoding for discrete-time STL formulas and projects rollouts toward the associated satisfaction constraints.
- Unlike approaches that use STL as the cost, the framework addresses STL satisfaction while allowing cost functions customized independently of STL constraints.
III. PROBLEM FORMULATION
The problem formulation seeks a feedback controller that satisfies a user-defined STL specification while optimizing receding-horizon control objectives. At each time step, the controller repeatedly solves an open-loop optimal control problem and executes the resulting control in closed loop.
- The system evolves under dynamics f with state x_t, bounded input u_t, planning horizon H, and user-defined stage and terminal costs.
- At each current time, the controller seeks an optimal sequence of control inputs by solving an open-loop optimal control problem.
- After solving the optimal control problem, the controller executes the selected input and increments time before solving again.
- Receding-horizon control can produce trajectories robust against system disturbances.
- The resulting closed-loop trajectory is required to satisfy the user-defined STL specification.
IV. SAFETY-AWARE-STL-MPPI
The method encodes discrete-time STL formulas as time-varying CBFs and integrates them into MPPI through a safety filter. Under exact CBF enforcement, the construction provides forward invariance and implies STL satisfaction, while the algorithm retains approximation and feasibility limitations.
- Method: safety-aware-stl-mppi incorporates time-varying CBFs into MPPI to promote satisfaction of STL constraints during receding-horizon control.The method adapts STL CBF encoding to discrete time and applies a lightweight projection toward the CBF zero-superlevel set.
- Guarantees: Enforcing the exact CBF constraint keeps the state in every time-varying safe set and implies satisfaction of the encoded STL formula.Forward invariance follows from the input condition, while Theorem 2 connects the valid CBF construction to STL satisfaction.
- Assumptions and limitations: The STL-to-CBF construction does not necessarily ensure that the candidate safe sets remain nonempty at every time.The paper therefore assumes nonempty admissible control sets and notes additional requirements for first-order CBFs and order reduction.
- CBF encoding: The encoded CBF aggregates temporal subformula functions with a smooth minimum and deletes terms after their associated temporal intervals expire.This time-varying deletion strategy removes functions sharing a switching time simultaneously.
- Assumptions and limitations: Theorem 2 does not directly establish STL satisfaction for Algorithm 1 because the algorithm uses a first-order approximation instead of the exact CBF constraint.The paper also notes that the constructed CBF may not be valid in the example considered.
B. Model Predictive Path Integral
MPPI samples control perturbations, evaluates their rollouts, and forms a weighted control sequence. The safety-aware variant augments rollout costs with CBF violations and projects the weighted rollout through an approximate safety filter, whose guarantees depend on assumptions and approximation quality.
- Sampling and rollouts: MPPI samples K control perturbation sequences from a zero-centered Gaussian distribution and generates corresponding rollouts from nominal controls.Each perturbation sequence has dimension R^m × H and is added to the nominal control sequence.
- Safety-aware weighting: The safety-augmented rollout cost incorporates CBF constraint violations alongside the ordinary MPPI performance cost.The violation penalty uses a tunable hyperparameter η, while the resulting sample costs determine the rollout weights.
- Safety filtering: The weighted rollout is not guaranteed to satisfy the CBF constraint, so the method applies a subsequent safety filter based on an approximate quadratic program.The paper proposes a closed-form solution when U = R^m using a first-order Taylor expansion.
- Closed-loop execution: The closed-loop procedure repeatedly uses the filtered control, advances the dynamics, and replans with MPPI over a receding horizon.The approach assumes the approximated admissible set remains nonempty along the closed-loop trajectory.
- Safety filtering: The safety-filter derivation guarantees safety when the cost is zero and U = R^m, but the discrete-time optimization is generally nonconvex.The standard first-order optimizer is not generally run to convergence in real time, and convergence would not guarantee an optimal solution.
C. Solving the CBF Constraint with Approximation
The method approximates the CBF constraint with a first-order affine condition, then solves the resulting projection problem efficiently within the closed-loop MPPI procedure. The implementation assumes feasible projected controls, while approximation error means perfect safety is not theoretically guaranteed.
- Constraint approximation: A first-order Taylor expansion around the current state approximates the CBF constraint with a condition affine in the control input.
- Closed-loop procedure: The method consistently uses the same action-perturbation cost across baselines for consistency with the original MPPI formulation and fair comparison.
- Projection: The approximation is formulated as a standard quadratic program for efficiently projecting the MPPI weighted rollout toward CBF-feasible controls.The QP has a closed-form solution when the admissible control set is unconstrained.
- Closed-loop procedure: The controller uses the QP or its closed-form solution to update sampled controls, warm-starts with the new weighted rollout, and executes the first control.
- Assumptions and limitation: The closed-loop procedure assumes the approximated CBF-feasible action set is nonempty and the CBF constraint normal is nonzero where projection is applied.Because of approximation error, perfect safety is not guaranteed theoretically; optional robustification is discussed in the appendix.
V. EVALUATION
The evaluation combines four artificial Mars rover path-planning studies with a photorealistic quadcopter inspection simulation. Rover experiments compare safety-aware-stl-mppi with four baseline models on safety and computational cost.
- The evaluation uses four artificial Mars rover path-planning case studies and a photorealistic quadcopter simulation in NVIDIA Isaac Lab.
- The rover studies compare safety-aware-stl-mppi against four state-of-the-art baseline models.
- The evaluation discusses the proposed method's safety and low computation cost across the rover experiments.
A. Mars Rover Case Studies
The Mars rover evaluation tests four case studies spanning different dynamics, goals, environments, and STL safety specifications, with and without actuation limits. Across the evaluated trials, all methods satisfy actuation limits, while safety-aware-stl-mppi achieves 100% empirical STL satisfaction and efficient computation.
- Study design: Four Mars rover cases vary the dynamics, goals, and STL safety specifications, and are evaluated both with and without actuation limits.
- Study design: The STL missions combine persistent obstacle avoidance with timed reach requirements, including returning before battery depletion and reaching specified regions.
- Case-specific stress test: Case C uses an potentially unreachable goal, requiring the rover to obey its safety constraint even when it cannot approach the goal closely.
- Metrics and results: 100% Actuation Limit Satisfaction Rate is achieved by every method across all cases.ALSR measures the percentage of trajectories satisfying actuation limits at all times.
- Metrics and results: 100% empirical STL satisfaction is achieved by safety-aware-stl-mppi in the evaluated trials, alongside computational efficiency under diverse costs and environments.
- Baseline comparison: Vanilla MPPI is efficient but frequently violates safety constraints, while reach-avoid MPPI does not generalize to complex STL tasks with tight timing constraints.
- Baseline comparison: Robustness- and penalty-based MPPI methods incur high computation costs from long-horizon rollouts and do not provide safety guarantees.
B. Quadcopter Simulation
The quadcopter experiment evaluates safety-aware-stl-mppi in an artificial Isaac Lab factory, where it plans and tracks trajectories under STL safety constraints. Across 50 trials, tracked trajectories satisfied the safety specification, while planning incurred a recorded average time of 15.21 seconds.
- Environment and task: The Isaac Lab factory contains seven obstacles, and the Crazyflie must navigate near (0, 0, 1)^T without colliding with obstacles or the ground.The obstacles are modeled with infinite-cylinder bounding volumes, and the quadcopter uses double-integrator dynamics with bounded actuation.
- Environment and task: The STL specification requires obstacle and ground clearance throughout 0–5 seconds and proximity to the goal at 5 seconds.The specification combines signed-distance safety conditions, a height constraint p_z − 0.3 ≥ 0, and a terminal goal-region condition.
- Planning results: 50 trials used safety-aware-stl-mppi for trajectory planning, with example successful waypoints and sampled rollouts shown in Figure 3.The planning samples used K := 100 rollouts, with weighted rollouts distinguished from the other sampled trajectories.
- Planning results: 15.21 seconds was the average planning time across the 50 trials, and all executions satisfied the actuation limit during planning.The implementation treats actuation as within limit using a tolerance ϵ := 10^-5 to address floating-point issues.
- Tracking results: 100% of tracked trajectories satisfied the safety specification during position updates through Isaac Sim API calls.The tracking stage followed the planned waypoints after the planning stage.
VI. CONCLUSION
The paper proposes safety-aware-stl-mppi for STL-constrained receding-horizon planning and evaluates it in Mars Rover case studies and a quadcopter simulation. These studies demonstrate high safety and efficiency outcomes, while future work targets multi-agent tasks and uncertain dynamics.
- Conclusion: The method integrates a time-varying control barrier function into a receding-horizon sampling-based planner for STL safety specifications.The paper evaluates this approach through Mars Rover case studies and a quadcopter simulation.
- Conclusion: The case studies and quadcopter simulation demonstrate high safety and efficiency outcomes for safety-aware-stl-mppi.The conclusion reports these outcomes without specifying a single aggregate metric.
- Future work: Future work will extend the results to multi-agent tasks and dynamics with uncertainty.
VIII. APPENDIX
The appendix proves forward-invariance and STL-satisfaction properties for the constructed barrier functions, then derives a closed-form projection for a single affine constraint. The proof handles STL temporal operators through barrier composition and induction.
- Barrier invariance: Forward invariance follows by induction when x_0 ∈ C_0 and each input satisfies the barrier condition u_t ∈ S(x_t,t).The update preserves h(x_t,t) ≥ 0 and therefore keeps the next state in C_{t+1}.
- STL satisfaction: The STL proof uses smooth-minimum barrier composition to show nonnegative constituent barriers and satisfaction of atomic, globally, eventually, until, and conjunction formulas.The argument proceeds by induction on the structure of the STL formula.
- Closed-form projection: For an already safe affine action, the projection leaves the action unchanged because its objective cost is zero.This is the case a^T v^+ ≤ b.
- Closed-form projection: When a^T v^+ > b, KKT conditions place the optimum on the constraint boundary and yield a multiplier proportional to (a^T v^+ − b)/∥a∥^2.The feasible region is affine and the objective is strictly convex, making the KKT conditions sufficient and necessary.
- Closed-form projection: The two cases combine into the closed-form projection ˆv_s = v^+ − a max(0, a^T v^+ − b)/∥a∥^2.
D. Theorem 3
Theorem 3 provides a robustified barrier constraint using a Lipschitz-gradient bound and a bound on one-step state displacement. The resulting robustified algorithm subtracts this margin from the nominal barrier bound, but computing it can be difficult and more time consuming.
- Theorem assumptions: If ∇h_ϕ(·,τ+1) is L_{x,τ}-Lipschitz and one-step displacement is bounded by Δ_x, increasing the right-hand side by ϵ_{x,τ} yields a subset of the original feasibility region.The theorem assumes the Lipschitz condition holds on a set containing every relevant state-transition segment.
- Robustification: The robustified algorithm replaces b_cbf(x(t),τ) with b_cbf(x(t),τ) − ϵ_{x,τ} in the planning procedure.This modification is derived from Theorem 3.
- Computing the bound: Computing L_{x,τ} is generally nontrivial, so the paper suggests a heuristic sampling-based estimate.
- Computing the bound: For control-affine dynamics with boxed input constraints, Δ_x can be computed by maximizing the transition norm over the vertices of the input box.Convexity shows that the maximum over the box occurs at a vertex.
- Trade-offs: The robustification is conservative and more time consuming than safety-aware-stl-mppi because it requires computing ϵ_{x,τ}.