Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Feasibility Restoration under Conflicting STL Specifications with Pareto-Optimal Refinement

Tianhao Wu, Yiwei Lyu

TL;DR

This paper proposes a unified two-stage framework that first restores feasibility via minimal relaxation, then refine the feasible solution by formulating it as a value-aware multi-objective optimization problem, approximate the Pareto front of the multi-objective optimization.

Abstract

Signal Temporal Logic (STL) is expressive formal language that specifies spatio-temporal requirements in robotics. Its quantitative robustness semantics can be easily integrated with optimization-based control frameworks. However, STL specifications may become conflicting in real-world applications, where safety rules, traffic regulations, and task objectives can be cannot be satisfied together. In these situations, traditional STL-constrained Model Predictive Control (MPC) becomes infeasible and default to conservative behaviors such as freezing, which can largely increase risks in safety-critical scenarios. In this paper, we proposes a unified two-stage framework that first restores feasibility via minimal relaxation, then refine the feasible solution by formulating it as a value-aware multi-objective optimization problem. Using $\varepsilon$-constraint method, we approximate the Pareto front of the multi-objective optimization, which allows analysis of tradeoffs among competing objectives and counterfactual analysis of alternative actions. We demonstrate that the proposed approach avoids deadlock under conflicting STL specifications and enables interpretable decision-making in safety-critical applications by conducting a case study in autonomous driving.

Feasibility Restoration under Conflicting STL Specifications with Pareto-Optimal Refinement

TL;DR

This paper proposes a unified two-stage framework that first restores feasibility via minimal relaxation, then refine the feasible solution by formulating it as a value-aware multi-objective optimization problem, approximate the Pareto front of the multi-objective optimization.

Abstract

Signal Temporal Logic (STL) is expressive formal language that specifies spatio-temporal requirements in robotics. Its quantitative robustness semantics can be easily integrated with optimization-based control frameworks. However, STL specifications may become conflicting in real-world applications, where safety rules, traffic regulations, and task objectives can be cannot be satisfied together. In these situations, traditional STL-constrained Model Predictive Control (MPC) becomes infeasible and default to conservative behaviors such as freezing, which can largely increase risks in safety-critical scenarios. In this paper, we proposes a unified two-stage framework that first restores feasibility via minimal relaxation, then refine the feasible solution by formulating it as a value-aware multi-objective optimization problem. Using -constraint method, we approximate the Pareto front of the multi-objective optimization, which allows analysis of tradeoffs among competing objectives and counterfactual analysis of alternative actions. We demonstrate that the proposed approach avoids deadlock under conflicting STL specifications and enables interpretable decision-making in safety-critical applications by conducting a case study in autonomous driving.
Paper Structure (18 sections, 24 equations, 4 figures, 1 algorithm)

This paper contains 18 sections, 24 equations, 4 figures, 1 algorithm.

Table of Contents

  1. Introduction
  2. Preliminaries on Signal Temporal Logic (STL)
  3. Syntax
  4. Semantics
  5. Methodology
  6. Problem Formulation
  7. Minimal-Relaxation Feasibility Restoration
  8. Counterfactual, Value-Aware Tradeoff Refinement
  9. Autonomous-driving: dynamics and consequence objectives
  10. Organizing counterfactual tradeoffs by nondominance
  11. Experiments
  12. Exp1: Intersection conflict between emergency passage and pedestrian right-of-way
  13. Problem setup
  14. Results and discussion
  15. Exp2: Out-of-control rear vehicle and emergency-lane borrowing
  16. ...and 3 more sections

Figures (4)

  • Figure 1: Ego-vehicle trajectory outcomes under competing STL rules. (a)-(c) illustrate feasible but dominated solutions. (d) shows the selected nondominated (Pareto-optimal) solution, which achieves a principled compromise among the risk objectives under the same observed scene.
  • Figure 2: Stage-1 versus Stage-2 behavior in the same driving context. (e) shows the Stage-1 minimal-relaxation solution that restores feasibility with the smallest combined STL violation. (f) shows a Stage-2 Pareto-optimal refinement that reallocates the admissible violation budget to improve risk objectives
  • Figure 3: Control sequences corresponding to Fig. 2.
  • Figure 4: Relaxation allocations across negotiable STL specifications, where d1, d2, d3 corresponds to the relaxation level of $\varphi_{\text{no emergency lane}}$, $\varphi_{\text{cyclist safe}}$ and $\varphi_{\text{rear vehicle safe}}$. $d_{min}$ indicates the minimal total relaxation to restore feasibility