Feasibility Restoration under Conflicting STL Specifications with Pareto-Optimal Refinement

TL;DR

This paper introduces a two-stage framework for restoring feasibility in control systems with conflicting STL specifications, using Pareto-optimal refinement to balance safety, task objectives, and constraints in autonomous driving.

Contribution

It proposes a novel approach combining minimal relaxation and Pareto front approximation to handle conflicting STL specifications in safety-critical control tasks.

Findings

Avoids deadlock under conflicting STL specifications

Enables interpretable decision-making in safety-critical scenarios

Balances multiple objectives through Pareto-optimal refinement

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.