An Update to the Level Set Theorems in Hamilton-Jacobi Reachability Analysis

Technische Samenvatting: Een update van de Level Set-stellingen in Hamilton-Jacobi Reachability Analyse

Probleemstelling
Hamilton-Jacobi Reachability (HJR) is een gevestigd kader voor het synthetiseren van controllers voor veiligheidskritische nietlineaire systemen onder onzekerheid, die doorgaans worden geformuleerd als differentiële spellen. Het proces omvat het omzetten van een kwalitatieve controleopdracht (bijv. het vermijden van obstakels of het bereiken van een doel) in een "spel van graad", waarbij de bijbehorende Hamilton-Jacobi (HJ) partiële differentiaalvergelijking wordt opgelost om een waardefunctie te verkrijgen, en vervolgens wordt de interpretatie van deze waardefunctie gebruikt om de verzameling veilige of onveilige initiële toestanden te definiëren. Deze laatste stap steunt op "Level Set-stellingen".

De auteurs stellen vast dat de bestaande literatuur technische fouten en ambiguïteiten bevat met betrekking tot deze stellingen, specifiek wat betreft de voorwaarden waaronder de level sets van de waardefunctie correct overeenkomen met de winnende verzamelingen van het spel. Deze problemen hebben gezorgd voor verwarring in de gemeenschap, met name met betrekking tot de interpretatie van toestanden die zich precies op de nul-level set van de waardefunctie bevinden. Het artikel stelt dat eerdere formuleringen vaak noodzakelijke topologische en convexiteitsveronderstellingen over het hoofd zien, wat leidt tot incorrecte karakterisaties van veiligheids- en bereikbaarheidsverzamelingen.

Methodologie
Het artikel hanteert een rigoureuze wiskundige benadering geworteld in de differentiële speltheorie en topologie. De auteurs:

1. Formaliseren de spelopzet: Ze definiëren een eindig-horizontaal differeentieel spel met een controller-speler en een adversariële verstoringsspeler. De systeemdynamica wordt beheerst door $\dot{x} = f(x, a, b)$, waarbij $a$ en $b$ respectievelijk controle- en verstoringssignalen zijn. De verstoringsspeler maakt gebruik van niet-anticiperende strategieën.
2. Stellen aannames vast: De analyse steunt op vijf aannames:
   • Standaard continuïteit en compactheid van dynamica en controleverzamelingen (Aannames 1-3).
   • Convexiteit van de verstoringsdynamica: Voor elke toestand en controle moet de verzameling mogelijke dynamica-vectoren geïnduceerd door de verstoringsverzameling $B$ convex zijn (Aanname 4).
   • Geslotenheid van faalmodi: De verzameling van faaltrajecten $F(t)$ moet gesloten zijn in de ruimte van continue trajecten (Aanname 5).
3. Leiden een algemene stelling af: Ze bewijzen een gegeneraliseerde Level Set-stelling (Stelling 1) die de waardefunctie $v(x,t)$ koppelt aan de veilige ($L(t)$) en onveilige ($G(t)$) verzamelingen. De stelling stelt dat $L(t) = \{x \mid v(x,t) > 0\}$ en $G(t) = \{x \mid v(x,t) \leq 0\}$, mits de functionaal $J$ die de faalmodi definieert continu en begrensd is.
4. Construeren tegenvoorbeelden: Om de noodzaak van de nieuwe aannames aan te tonen, construeren de auteurs twee specifieke tegenvoorbeelden:
   • Gebrek aan convexiteit: Een obstakelvermijdingsspel waarbij de verstoringsverzameling $B$ niet-convex is (discrete punten). Ze laten zien dat zonder Aanname 4, een toestand op de nul-level set ($v=0$) mogelijk niet tot de onveilige verzameling behoort, wat de standaardinterpretaties tegenspreekt.
   • Gesloten doelverzamelingen: Een doelbereikingsspel waarbij de doelverzameling gesloten is in plaats van open. Ze demonstreren dat zonder Aanname 5 (die impliceert dat doelen open moeten zijn), een toestand op de nul-level set mogelijk niet tot de veilige verzameling behoort, wat eveneens de standaardinterpretaties tegenspreekt.
5. Bewijstechnieken: De bewijzen maken gebruik van Filippovs Lemma om de existentie van meetbare verstoringssignalen vast te stellen, en topologische argumenten waarbij de compactheid van trajectverzamelingen en niet-anticiperende verstoringsplannen (met behulp van de Stelling van Tychonoff en lexicografische ordening) worden gebruikt om de hoofdstelling te bewijzen.

Belangrijkste Bijdragen

1. Correctie van technische fouten: Het artikel identificeert en corrigeert technische gebreken in eerdere Level Set-stellingen in de literatuur, waarbij specifiek wordt gewezen op de omissie van de convexiteitsconditie op de dynamica (Aanname 4) en de vereiste voor gesloten faalverzamelingen (Aanname 5).
2. Algemene Level Set-stelling: De auteurs bieden een verenigde, beknopte stelling die toepasbaar is op alle relevante eindig-horizontale spellen in HJR, waarbij de strikte ongelijkheid voor de veilige verzameling ($v > 0$) en de niet-strikte ongelijkheid voor de onveilige verzameling ($v \leq 0$) wordt verduidelijkt.
3. Verheldering van de ambiguïteit van de nul-level set: Door middel van tegenvoorbeelden legt het artikel uit waarom punten op de nul-level set van de waardefunctie ambigu zijn wanneer de standaard aannames worden geschonden. In dergelijke gevallen kan de uitkomst van het spel (winst/verlies) voor deze specifieke punten niet uitsluitend bepaald worden door de waardefunctie nul te zijn; de controller kan winnen voor sommige punten op de grens terwijl de verstoring wint voor andere punten.
4. Topologische Rigor: Het werk overbrugt de kloof tussen HJR en de topologische argumenten die worden gebruikt in de viability theory en semi-permeabele barrières, waardoor een robuustere theoretische basis wordt geboden voor de interpretatie van waardefuncties.

Resultaten
Het primaire resultaat is Stelling 1, die de veilige en onveilige verzamelingen rigoureus definieert op basis van de waardefunctie onder de gespecificeerde aannames. Het artikel demonstreert dat:

• Als de verstoringsdynamica niet convex is (bijv. discrete verstoringsverzamelingen), de standaardinterpretatie dat $v(x,t) \leq 0$ impliceert dat de toestand onveilig is, faalt voor punten op de grens.
• Als de doelverzameling gesloten is (wat Aanname 5 schendt, die open doelen vereist in bereikbaarheidsspelen), de standaardinterpretatie dat $v(x,t) > 0$ impliceert dat de toestand veilig is, faalt voor punten op de grens.
• Onder de gecorrigeerde aannames biedt de waardefunctie een precieze karakterisering van de winnende verzamelingen, waarbij de verstoringsspeler een "instantane voorsprong" heeft die de splitsing tussen strikte en niet-strikte ongelijkheid noodzakelijk maakt.

Betekenis
De auteurs stellen dat hoewel deze technische kwesties mogelijk geen directe impact hebben op praktijkgebruikers die vertrouwen op bestaande softwaretools, hun theoretische oplossing "interessant en genuanceerd" is. Het artikel beoogt de verwarring in de gemeenschap weg te nemen die is veroorzaakt door eerdere technische fouten. Door een gecorrigeerde algemene stelling te bieden en de oorsprong van discrepanties via tegenvoorbeelden uit te leggen, zorgt het werk ervoor dat de theoretische fundamenten van Hamilton-Jacobi Reachability solide zijn. Dit is bijzonder relevant voor onderzoekers die learning-based HJR-methoden ontwikkelen of het kader uitbreiden naar complexe, gelaagde taken, omdat het de exacte voorwaarden verheldert die nodig zijn om de waardefunctie correct te gebruiken voor het certificeren van veiligheid en liveness.