Feasibility Restoration under Conflicting STL Specifications with Pareto-Optimal Refinement

Dit artikel presenteert een tweestapsframework dat conflicterende Signal Temporal Logic-specificaties in veiligheidskritieke toepassingen, zoals autonoom rijden, oplost door eerst haalbaarheid te herstellen via minimale versoepeling en vervolgens een Pareto-optimale oplossing te vinden die interpreteerbare afwegingen tussen concurrerende doelen mogelijk maakt.

De kern

Stel je voor dat je een zelfrijdende auto bestuurt die een heel strikte set regels volgt, alsof het een robot is met een onbuigzame moraal. Deze regels zijn geschreven in een speciale taal (STL) die zegt: "Altijd stoppen bij een stopbord," "Nooit de gele lijn overschrijden" en "Altijd een veilige afstand houden."

Het probleem is dat het echte leven soms deze regels met elkaar in conflict brengt. Stel je voor: je staat in een smalle straat. Achter je komt een ambulance die razendsnel moet passeren. Voor je loopt plotseling een voetganger over de weg.

• Als je stopt voor de voetganger, blokkeer je de ambulance (en riskeer je een achteroprijd-ongeluk).
• Als je doorrijdt om de ambulance niet te blokkeren, riskeer je de voetganger aan te raken.

Een traditionele computer zou hier "in de war" raken. Omdat hij geen oplossing kan vinden die alle regels perfect volgt, doet hij het veiligste wat hij kan: bevriezen. Hij stopt en wacht, waardoor hij een obstakel wordt in een noodsituatie. Dit is gevaarlijk.

Dit artikel introduceert een slimme nieuwe manier om dit op te lossen, met een tweestapsplan dat de auto weer laat bewegen zonder gevaarlijk te worden.

Stap 1: De "Minimale Uitzondering" (Feasibility Restoration)

De eerste stap is als het oplossen van een knoop. De computer zegt: "Oké, we kunnen niet alles perfect doen. Laten we kijken welke regels we net iets kunnen opofferen om überhaupt een oplossing te vinden, zonder de levensgevaarlijke regels te breken."

• De strikte regels: "Blijf op de weg" en "Raak niemand aan" zijn heilig. Die mogen nooit worden overtreden.
• De onderhandelbare regels: "Rij niet over de gele lijn" of "Bereik je bestemming snel" zijn iets flexibeler.

De computer zoekt nu de kleinste mogelijke uitzondering. Misschien moet hij wel 10 centimeter over de gele lijn rijden om de ambulance door te laten, maar dat is beter dan helemaal stil te staan. Dit zorgt ervoor dat de auto niet meer "bevriest", maar weer beweegt.

Stap 2: De "Slimme Keuze" (Pareto-Optimal Refinement)

Nu de auto weer beweegt, is er vaak meer dan één manier om die kleine uitzondering te maken. Stel, de computer kan:

1. Een beetje hard remmen en iets naar links sturen.
2. Een beetje harder accelereren en iets naar rechts sturen.

Beide opties zijn "mogelijk" (ze breken de regels net iets, maar redden de situatie). Maar welke is het slimst?

Hier komt de tweede stap om de hoek kijken. In plaats van zomaar één keuze te maken, maakt de computer een lijst met de beste opties (een "Pareto-front"). Hij vergelijkt de gevolgen van elke optie als een weegschaal:

• Optie A: Risico op de voetganger is laag, maar risico op de ambulance is hoog.
• Optie B: Risico op de voetganger is iets hoger, maar risico op de ambulance is heel laag.

De computer toont deze opties aan de bestuurder (of het systeem) en zegt: "Kijk, als je Optie A kiest, red je de voetganger, maar riskeer je een botsing achteraan. Als je Optie B kiest, red je de ambulance, maar moet je de voetganger iets meer risico laten lopen."

De auto kiest dan de optie die de minste totale schade veroorzaakt, of de optie die het beste past bij de situatie, in plaats van willekeurig te kiezen.

De Analogie: De Chef-kok en de Ingrediënten

Je kunt dit vergelijken met een chef-kok die een gerecht moet maken, maar er ontbreekt een cruciaal ingrediënt (de regels zijn in conflict).

1. Stap 1 (De Reddingsactie): De chef zegt: "Ik kan dit gerecht niet perfect maken zoals het recept zegt. Maar ik kan wel een klein beetje zout weghalen en een beetje peper toevoegen om het eetbaar te houden." Hij zorgt ervoor dat het gerecht niet "onmogelijk" is.
2. Stap 2 (De Veredeling): Nu het gerecht eetbaar is, zijn er verschillende manieren om het te proeven. De chef proeft verschillende combinaties van peper en zout. Hij ziet: "Als ik meer peper doe, wordt het pittiger maar minder zout. Als ik minder peper doe, is het milder maar misschien saai." Hij kiest de combinatie die het beste smaakt (de veiligste en meest efficiënte route), in plaats van zomaar de eerste de beste optie te nemen.

Waarom is dit belangrijk?

Vroeger zouden robots in zo'n situatie "bevriezen" en de weg blokkeren, wat in het echt al gebeurd is (bijvoorbeeld met robotaxi's die ambulances blokkeren).

Met deze nieuwe methode:

• Geen bevriezen: De auto blijft bewegen.
• Slimme compromissen: De auto maakt bewuste keuzes over welke regel hij het minst breekt om het grootste gevaar te vermijden.
• Duidelijkheid: Het systeem kan uitleggen waarom hij een bepaalde keuze heeft gemaakt ("Ik heb de gele lijn iets overreden om de ambulance te redden, omdat dat veiliger was dan te wachten").

Kortom: Het maakt zelfrijdende auto's minder star en meer in staat om slimme, menselijke keuzes te maken in chaotische situaties, zonder hun veiligheidswaarden uit het oog te verliezen.

Technische samenvatting

Hier is een gedetailleerde technische samenvatting van het paper "Feasibility Restoration under Conflicting STL Specifications with Pareto-Optimal Refinement" in het Nederlands.

Titel: Herstel van Haalbaarheid onder Conflicterende STL-Specificaties met Pareto-Optimale Verfijning

Auteurs: Tianhao Wu en Yiwei Lyu
Context: Formele methoden, Robotica, Veiligheidskritieke autonome systemen, Autonomisch rijden.

---

1. Probleemstelling

Signal Temporal Logic (STL) is een krachtige formele taal voor het specificeren van ruimtelijk-temporele eisen in robotica, die vaak wordt geïntegreerd met Model Predictive Control (MPC) via kwantitatieve robustheidssemantiek. Een groot probleem in real-world toepassingen (zoals autonomisch rijden) is dat specificaties kunnen conflicteren.

• Het Conflict: Veiligheidsregels, verkeersvoorschriften en taakdoelen kunnen onverenigbaar zijn in specifieke situaties (bijv. een ambulance moet worden toegelaten, maar een voetganger moet worden beschermd, terwijl de rijbaan geblokkeerd is).
• Het Falen van Traditionele MPC: Wanneer STL-constraints niet gelijktijdig kunnen worden voldaan, wordt het optimalisatieprobleem onhaalbaar (infeasible). Traditionele controllers reageren hierop vaak met conservatief gedrag, zoals het "bevriezen" van de robot (stoppen en wachten).
• Gevolg: Dit leidt tot deadlocks en verhoogde risico's in veiligheidskritieke scenario's, zoals het blokkeren van een ambulance door een robotaxi. Er ontbreekt een kader dat systematisch omgaat met conflicten, de noodzakelijke compromissen expliciet maakt en vermijdt dat het systeem vastloopt.

2. Methodologie

De auteurs stellen een twee-staps framework voor om conflicterende STL-specificaties op te lossen binnen een MPC-structuur. Het systeem onderscheidt tussen niet-onderhandelbare specificaties (ΦH, bijv. fysische limieten, absolute veiligheid) en onderhandelbare specificaties (ΦS, bijv. verkeersregels, taakdoelen).

Fase 1: Herstel van Haalbaarheid via Minimale Relaxatie

Het doel is om de MPC opnieuw haalbaar te maken door de onderhandelbare constraints minimaal te verzwakken, terwijl de niet-onderhandelbare constraints strikt worden gehandhaafd.

• Mechanisme: Voor elke onderhandelbare formule $\phi \in \Phi_S$ wordt een relaxatievariabele $\delta_\phi \geq 0$ geïntroduceerd. De robustheidsconstraint wordt veranderd van $\rho_\phi \geq 0$ naar $\rho_\phi \geq -\delta_\phi$.
• Optimalisatie: Er wordt een probleem opgelost om de $L_1$-norm van de relaxatievector $\delta$ te minimaliseren:
  $$\min \|\delta\|_1$$
  onder de voorwaarden dat het systeem dynamisch haalbaar is en $\Phi_H$ strikt wordt gerespecteerd.
• Resultaat: Dit levert een minimale totale schending ($\Delta_{min}$) op die nodig is om een oplossing te vinden, waardoor "bevriezen" wordt voorkomen. Echter, er kunnen meerdere oplossingen zijn die dezelfde minimale schending hebben maar tot verschillende (en mogelijk onveilige) gedragingen leiden.

Fase 2: Pareto-Optimale Verfijning (Waarde-bewust)

Om de ambiguïteit van Fase 1 op te lossen en de beste compromisoplossing te vinden, wordt de gevonden haalbare basislijn verder verfijnd door afwegingen tussen verschillende doelen te analyseren.

• Doel: Het vinden van een set van Pareto-optimale oplossingen die niet-dominant zijn ten opzichte van elkaar. Dit omvat een vector van consequentiedoelen $g(u, \delta)$, zoals risico op botsing, comfort en taakvoltooiing.
• Risicometriek: Voor autonoom rijden wordt het risico berekend als het product van botsingskans, ernst en kwetsbaarheid van de betrokken agenten (voetgangers, voertuigen).
• Methode: De auteurs gebruiken de $\epsilon$-constraint methode. Hierbij wordt één doel geoptimaliseerd terwijl de andere doelen worden begrensd door drempelwaarden ($\epsilon$). Door deze drempels te variëren, wordt een benadering van de Pareto-front gegenereerd.
• Output: Een set van alternatieve, haalbare trajecten die verschillende afwegingen tonen tussen risico's en regelschendingen. De controller kan vervolgens een keuze maken op basis van scenario-specifieke voorkeuren zonder objecten te fixeren in vaste gewichten.

3. Belangrijkste Bijdragen

1. Herstelmechanisme: Een methode voor infeasibility-recovery gebaseerd op minimale $L_1$-norm relaxatie. Dit garandeert dat de MPC altijd een oplossing vindt (geen "freezing") door alleen de strikt noodzakelijke schendingen van onderhandelbare regels toe te staan.
2. Waarde-bewuste Verfijning: Een tweede fase die de gevonden oplossingen analyseert via Pareto-optimaliteit. Dit maakt systematische exploratie van trade-offs mogelijk en ondersteunt contrafactuele redenering (wat zou er gebeuren als we een andere keuze maakten?).
3. Validatie in Autonoom Rijden: Een case study die aantoont dat de methode deadlock voorkomt en interpreteerbare beslissingen neemt in complexe, conflicterende verkeerssituaties.

4. Resultaten (Case Studies)

De methode werd getest in twee autonome rij-scenario's:

• Scenario 1: Kruispuntconflict (Ambulance vs. Voetganger)

  • Situatie: Het voertuig moet een kruispunt verlaten om een ambulance niet te blokkeren, maar een voetganger stapt plotseling op.
  • Resultaat: Fase 1 (minimale relaxatie) leverde meerdere haalbare trajecten op, waaronder sommige die de voetganger ontweken maar de snelheid te hoog hielden (hoge botsingsernst), of die stopten maar de ambulance blokkeerden.
  • Fase 2: De Pareto-optimale selectie koos een traject met een geleidelijke linkse bocht en soepele vertraging. Dit balanceerde het risico voor de voetganger en de ambulance beter dan de "dominante" (inferieure) opties uit Fase 1.

• Scenario 2: Ongecontroleerd voertuig van achteren (Noodstrook)

  • Situatie: Een voertuig komt oncontroleerd van achteren; het autonome voertuig moet uitwijken, wat in strijd is met de regel "niet op de noodstrook rijden".
  • Resultaat: De minimale relaxatie (Fase 1) leidde tot een kleine uitwijking die de regels slechts licht schond, maar het risico op een achteraanrijding niet voldoende verlaagde.
  • Fase 2: De Pareto-geoptimaliseerde oplossing koos ervoor om de noodstrook meer te gebruiken (grotere regelschending) om sneller uit het gevaarzone te komen. Dit toont aan dat een grotere schending van een verkeersregel soms noodzakelijk is om het levensreddende risico te minimaliseren. De methode maakt deze trade-off expliciet.

5. Betekenis en Conclusie

Dit werk is significant omdat het een brug slaat tussen formele methoden en praktische, veilige autonomie in onzekere omgevingen.

• Van "Freezing" naar Actie: Het lost het probleem op waarbij robots vastlopen bij conflicterende regels.
• Interpreteerbaarheid: Door de Pareto-front te visualiseren, kunnen ontwikkelaars en toezichthouders zien waarom een bepaalde actie is gekozen en welke alternatieven zijn afgewezen (en waarom).
• Flexibiliteit: Het stelt systemen in staat om context-afhankelijke compromissen te sluiten in plaats van starre prioriteiten te hanteren.

De auteurs concluderen dat voor de veilige inzet van autonome systemen, het koppelen van haalbaarheids Herstel aan expliciete afwegingsstructuren (trade-offs) essentieel is. Toekomstig werk richt zich op het verbeteren van de rekentijd voor real-time toepassing en het uitbreiden naar multi-agent interacties.