Feasibility Restoration under Conflicting STL Specifications with Pareto-Optimal Refinement

This paper proposes a unified two-stage framework that restores feasibility for conflicting Signal Temporal Logic (STL) specifications by first applying minimal relaxation and then refining the solution through Pareto-optimal multi-objective optimization, thereby enabling interpretable decision-making and avoiding deadlocks in safety-critical applications like autonomous driving.

The Gist

Imagine you are driving a self-driving car. You have a set of strict rules written in a very precise language (like a computer's version of "Do not cross the line," "Stop for pedestrians," and "Yield to ambulances").

Usually, these rules work perfectly together. But sometimes, the real world gets messy. Imagine you are in a narrow alley:

1. An ambulance is screaming behind you, and you must move forward to let it pass.
2. A pedestrian suddenly steps out in front of you, and you must stop to avoid hitting them.
3. You are not allowed to cross the double yellow line or drive on the sidewalk.

In this impossible situation, the car's computer hits a wall. It tries to find a solution that satisfies all rules at once, realizes it's impossible, and panics. In the real world, this panic often looks like the car just freezing in place. It becomes a roadblock, which is dangerous for everyone.

This paper proposes a smarter way to handle these "impossible" moments. Think of it as a two-step emergency protocol for the car's brain.

Step 1: The "Minimum Damage" Fix

Instead of freezing, the car admits, "Okay, I can't follow every single rule perfectly right now."

It separates the rules into two piles:

• The Unbreakable Laws: (e.g., Don't drive off a cliff, don't drive into a wall). These are never broken.
• The Negotiable Rules: (e.g., "Don't cross the yellow line," "Yield to the ambulance"). These can be bent, but only a tiny bit.

The computer calculates the smallest possible bend needed to get the car moving again. It's like a tightrope walker who has to lean just a fraction of an inch to the left to avoid falling, rather than jumping off the rope entirely. This gets the car out of the "frozen" state and back on the road.

Step 2: The "Best of the Bad Options" Choice

Here is the clever part. Once the car is moving, there might be many different ways to bend those negotiable rules.

• Option A: Lean slightly left, go slow. (Safe for the pedestrian, but might get hit by the ambulance).
• Option B: Lean slightly right, speed up. (Safe for the ambulance, but scary for the pedestrian).
• Option C: Lean hard right, stop abruptly. (Safe for the pedestrian, but causes a rear-end collision).

Old systems might just pick one randomly or based on a rigid formula. This paper suggests looking at all these options and comparing them like a menu of trade-offs.

The authors use a mathematical tool (called a "Pareto Front") to create a list of "Smart Compromises."

• Imagine a menu where every dish is a different balance of risks.
• The system filters out the "bad deals" (options that are worse in every way than another option).
• It leaves you with a shortlist of "efficient compromises." For example: "If you want to save the pedestrian, you must accept a slightly higher risk to the ambulance. There is no magic option that saves everyone perfectly."

The Result: A Human-Like Decision Maker

By using this two-step process, the self-driving car doesn't just freeze when things get tough. Instead, it:

1. Unfreezes by making the tiniest necessary rule-bend.
2. Chooses the specific bend that offers the best overall safety outcome, rather than just the easiest one.

The Analogy:
Think of a parent trying to settle a fight between two kids who both want the last cookie.

• The Old Way (Freezing): The parent says, "I can't give it to either of you because that's unfair," and takes the cookie away. Everyone is unhappy, and the situation is stuck.
• The New Way (This Paper):
  1. Step 1: The parent says, "We can't give the whole cookie to one kid, but we can break it in half." (Restoring feasibility).
  2. Step 2: The parent looks at the broken pieces. "If I give the bigger piece to the kid who is crying, the other kid gets angry. If I give the bigger piece to the older kid, the younger one cries harder." The parent then picks the split that minimizes the total tears, explaining clearly: "I gave the bigger piece to the older one because it prevents a bigger meltdown, even though it's not perfect."

Why This Matters

In safety-critical situations (like autonomous driving), inaction is often the most dangerous action. This paper gives robots the ability to make "principled compromises." It allows them to say, "I know I'm breaking a small rule to save a life, and here is exactly why that was the best choice among the bad options." It turns a computer panic into a thoughtful, explainable decision.

Technical Summary

Here is a detailed technical summary of the paper "Feasibility Restoration under Conflicting STL Specifications with Pareto-Optimal Refinement."

1. Problem Statement

The paper addresses a critical failure mode in safety-critical autonomous systems (e.g., autonomous driving) where Signal Temporal Logic (STL) specifications become mutually conflicting in real-time.

• The Conflict: In complex environments, safety rules (e.g., "do not cross double yellow lines"), traffic regulations, and task objectives (e.g., "reach destination," "yield to ambulance") may simultaneously demand actions that are physically impossible to satisfy together.
• The Consequence: Traditional Model Predictive Control (MPC) constrained by strict STL formulas becomes infeasible. When this happens, standard controllers often default to conservative "freezing" behaviors (stopping completely), which can create new hazards (e.g., blocking an ambulance or causing rear-end collisions).
• The Gap: Existing methods either assume specifications are always satisfiable, use fixed priority ordering (lexicographic optimization) which prevents context-dependent tradeoffs, or lack a unified framework to systematically handle conflicts while making tradeoffs explicit.

2. Methodology

The authors propose a unified two-stage framework to resolve conflicts, restore feasibility, and refine decisions based on value-aware tradeoffs.

Stage 1: Minimal-Relaxation Feasibility Restoration

The first stage aims to recover a feasible control solution by minimally violating negotiable constraints while strictly enforcing non-negotiable safety constraints.

• Classification: STL specifications ($\Phi$) are partitioned into:
  • Non-negotiable ($\Phi_H$): Hard safety constraints (e.g., physical limits, drivable area) that must remain strict ($\rho \ge 0$).
  • Negotiable ($\Phi_S$): Rules and objectives that can be compromised (e.g., traffic rules, task completion).
• Optimization Formulation: The system introduces relaxation variables $\delta_\phi \ge 0$ for each negotiable formula. It solves an optimization problem to minimize the $L_1$-norm of these relaxations ($\|\delta\|_1$) subject to system dynamics and strict non-negotiable constraints.
  • Goal: Find the control sequence $u$ and minimal violation $\delta$ such that the MPC problem becomes feasible again.
  • Outcome: This prevents "freezing" by finding the "least-deviation" behavior, but the solution is not unique; multiple control sequences can achieve the same minimal relaxation level with different downstream consequences.

Stage 2: Counterfactual, Value-Aware Tradeoff Refinement

The second stage refines the feasible baseline by exploring the tradeoffs among competing objectives (e.g., risk to pedestrians vs. risk to the ego vehicle vs. rule violations).

• Multi-Objective Formulation: The problem is framed as minimizing a vector of consequence objectives $g(u, \delta)$ (e.g., collision probability, severity, vulnerability) subject to a relaxation budget.
• Pareto Approximation: Instead of collapsing objectives into a single weighted sum, the authors use the $\epsilon$-constraint method to approximate the Pareto front.
  • They solve a series of single-objective subproblems where all but one objective are bounded by $\epsilon$ values.
  • This generates a set of non-dominated solutions (Pareto set), representing distinct "counterfactual" outcomes (e.g., "If we violate the lane rule slightly more, we can significantly reduce rear-end collision risk").
• Decision Making: The controller selects a final action from the Pareto front based on scenario-specific preferences, ensuring the choice is interpretable and avoids strictly inferior (dominated) options.

3. Key Contributions

1. Infeasibility-Recovery Mechanism: A novel method based on minimal $L_1$-norm relaxation that restores MPC feasibility by relaxing only negotiable specifications, preventing conservative freezing behaviors.
2. Value-Aware Refinement: A framework that treats feasible conflict resolutions as counterfactual decisions. It explicitly maps the tradeoffs between risk and performance using Pareto optimization, allowing for systematic exploration of alternative actions.
3. Interpretable Decision-Making: By generating a Pareto front, the system provides a structured explanation for why a specific maneuver was chosen over others, highlighting the specific tradeoffs (e.g., increased rule violation vs. decreased collision risk) inherent in the decision.
4. Empirical Validation: Demonstration in autonomous driving scenarios showing that the method avoids deadlocks and selects safer, risk-aware maneuvers compared to minimal-relaxation-only approaches.

4. Experimental Results

The framework was tested in two autonomous driving scenarios using a kinematic bicycle model and MPC:

• Experiment 1: Intersection Conflict (Ambulance vs. Pedestrian):
  • Scenario: The ego vehicle must clear an intersection for an ambulance but faces a pedestrian crossing.
  • Result: Stage 1 (minimal relaxation) produced feasible but dominated solutions (e.g., high-speed maneuvers increasing collision severity or abrupt stops causing rear-end risks). Stage 2 identified a Pareto-optimal solution that balanced smooth deceleration with a gradual turn, minimizing overall risk without strictly increasing any single risk component.
• Experiment 2: Out-of-Control Rear Vehicle (Emergency Lane Borrowing):
  • Scenario: A vehicle approaches rapidly from behind, threatening a rear-end collision. The ego must decide whether to stay in the lane (violating safety) or borrow an emergency lane (violating traffic rules).
  • Result: Stage 1 minimized the magnitude of the rule violation (slight lane intrusion) but failed to sufficiently mitigate the rear-end risk. Stage 2 reallocated the relaxation budget, choosing to violate the "no emergency lane" rule more significantly to rapidly create separation, thereby drastically reducing collision risk. The Pareto front explicitly showed that this safer maneuver required a larger rule violation, making the tradeoff transparent.

5. Significance

This work bridges the gap between formal verification and practical control in safety-critical systems.

• Safety Criticality: It addresses the real-world issue of "deadlock" in autonomous vehicles (AVs), where conflicting rules cause vehicles to stop and become hazards.
• Beyond Binary Logic: It moves beyond binary satisfaction/violation by utilizing quantitative robustness semantics to manage partial violations intelligently.
• Explainability: By visualizing the Pareto front, the system offers a mechanism for counterfactual analysis, allowing operators or regulators to understand the specific tradeoffs made by the AI (e.g., "We chose to break the speed limit to avoid hitting a pedestrian").
• Future Impact: The framework provides a principled approach for deploying autonomous systems in unstructured, dynamic environments where perfect compliance with all rules is impossible, shifting the paradigm from "satisfy all" to "optimize the inevitable tradeoffs."