Value Functions for Temporal Logic: Optimal Policies and Safety Filters

Technische Samenvatting: Waardefuncties voor Temporele Logica: Optimale Beleidsplannen en Veiligheidsfilters

Probleemstelling
Hoewel Bellman-vergelijkingen voor basisbereik-, vermijd- en bereik-vermijd-problemen goed gevestigd zijn, wordt de relatie tussen waardeoptimaliteit en beleidsplanoptimaliteit subtiel in niet-gediskonteerde settings met een oneindige horizon, met name voor complexe specificaties in Temporele Logica (TL). Een kritieke pathologie ontstaat waarbij het gretig maximaliseren van de Q-functie beleidsplannen kan opleveren die de voltooiing van taken voor bereik-vermijd-problemen (equivalent aan Until-specificaties) onbepaald uitstellen, zelfs wanneer de waardefunctie zelf optimaal is. Dit gebeurt omdat de optimale actiesequentie voor oneindige trajecten fundamenteel niet-Markoviaans is; de optimale invoer moet mogelijk "schakelen" van het maximaliseren van de huidige waarde naar een constitutieve waarde in een decompositiegrafiek om resterende specificaties met een oneindige horizon te voldoen. Bestaande methoden, zoals state-augmentatie voor problemen met twee doelen, worstelen om te generaliseren naar complexe formules die geneste Until, Globally en Globally-Until-specificaties bevatten. Bovendien is er behoefte aan veiligheidsfilters die de voldoening van complexe TL-specificaties garanderen, die verder gaan dan eenvoudige vermijding of bereik-vermijdingstaken.

Methodologie
De auteurs stellen een kader voor dat waarde- en Q-functies generaliseert naar geschiedenissen van toestanden om de niet-Markoviaanse aard van het probleem te hanteren. De methodologie is gebaseerd op de algebraïsche decompositie van de waardefunctie voor TL in een grafiek van constitutieve waardefuncties.

1. Niet-Markoviaanse Waardefuncties: Het artikel definieert optimale waardefuncties $V^*$ en Q-functies $Q$ over geschiedenissen van toestanden $x_{0:t}$ in plaats van slechts over huidige toestanden. Dit stelt het beleidsplan in staat rekening te houden met de geschiedenis die nodig is om temporele beperkingen te voldoen.
2. Tijd-geaugmenteerde Systemen en Getuige-tijden: Om het uitstelprobleem bij Until ($U$)-specificaties aan te pakken, voeren de auteurs een tijd-geaugmenteerd systeem met een timer in. Ze definiëren een "optimale getuige-tijd" $\sigma^*$, wat het vroegste tijdstip is waarop een traject de optimale robustheidsscore bereikt. Dit maakt het mogelijk beleidsplannen te construeren die schakelen van een eindige-horizon gretige strategie (het maximaliseren van de Q-functie binnen de getuige-tijd) naar een suffix-beleidsplan dat de resterende subformules voldoet.
3. Compositional Beleidsconstructie: Het artikel construeert optimale beleidsplannen voor een specifiek fragment van TL-formules (Definitie 3), dat omvat:
   • Propositionele formules.
   • Until ($p U \phi$), Next ($X\phi$) en Globally ($Gp$) operatoren.
   • Globally-Until ($G(\bigvee p_i U r_i)$), dat Büchi-acceptatiecriteria codeert.
   • Disjuncties en propositionele conjuncties.
     De constructie gaat uit van het bestaan van optimale beleidsplannen voor subformules (Aanname 2) en combineert deze recursief. Voor Globally-Until bezoekt het beleidsplan iteratief elke Until-component in sequentie om oneindige bezoeken aan vereiste toestandssets te waarborgen.
4. Veiligheidsfiltering: De auteurs tonen aan dat de Q-functie kan dienen als veiligheidsfilter. Ze definiëren een falingsset waar de specificatie niet met een niet-negatieve robustheid kan worden voldaan. Er wordt een minimaal-restrictief interventieschema voorgesteld: als de actie van een nominaal beleidsplan een niet-negatieve Q-waarde oplevert (wat toekomstige voldoening aangeeft), wordt deze toegestaan; anders schakelt het systeem over naar de actie die de Q-functie maximaliseert. Onder specifieke aannames (bijvoorbeeld de afwezigheid van onbegrensde Until-operatoren) garandeert dit filter de voldoening van de specificatie.

Belangrijkste Bijdragen

1. Generalisatie van Waardefuncties: Het artikel generaliseert de optimale waardefunctie en Q-functie naar geschiedenissen van toestanden (Definitie 1) en definieert optimaliteit over geschiedenissen (Definitie 2), waarmee de niet-Markoviaanse aard van TL-problemen met een oneindige horizon wordt aangepakt.
2. Compositional Optimale Beleidsplannen: Voor een brede klasse van TL-formules (Definitie 3) construeren de auteurs compositional optimale beleidsplannen voor de bijbehorende robustheidsmetriek (Stellingen 1–8). Dit omvat het aanpakken van de uitstelpathologie in Until en Globally-Until-specificaties.
3. Minimaal-Restriktieve Veiligheidsfilters: Het werk toont aan dat de Q-functie over (potentieel sub-optimale) geschiedenissen een minimaal-restrictief veiligheidsfilter oplevert voor een nominaal beleidsplan (Stellingen 9, 10). Dit filter garandeert de voldoening van de specificatie terwijl het het voorgaande pad van het nominaal beleidsplan respecteert, mits de formule aan bepaalde structurele beperkingen voldoet.

Resultaten en Demonstraties
Het artikel valideert het voorgestelde kader via theoretische bewijzen en twee hardware/software-demonstraties:

• Twee-Agenten GridWorld: De auteurs lossen een 4-dimensionaal gezamenlijk toestand-actieprobleem op met een complexe specificatie die tijdgebonden bereik-, veiligheids- en levensvatbaarheidsbeperkingen omvat. Ze tonen aan dat het afgeleide optimale beleidsplan ($\pi_{spec}$) het systeem succesvol leidt om aan de specificatie te voldoen. Bovendien zorgt het filter, wanneer gebruikt voor "koffie"- en "thee"-nominaal beleidsplannen (die individueel falen om aan de gezamenlijke specificatie te voldoen), ervoor dat het gezamenlijke systeem de complexe taak voldoet, terwijl een standaard "alleen-veiligheid"-filter leidt tot deadlock en falen.
• Enige-Agent Drone: Met behulp van een Crazyflie-drone demonstreren de auteurs het beleidsplan in een navigatietaken met obstakels. Het voorgestelde TL-filter leidt de drone succesvol naar een werkterrein terwijl complexe temporele beperkingen worden voldaan (bijvoorbeeld het doorlopen van specifieke zones in een lus en het vermijden van muren). Daarentegen resulteert een ongefilterd nominaal beleidsplan of een filter dat alleen gebaseerd is op veiligheidsbeperkingen in dat de drone vastloopt of crasht.

Betekenis
Het artikel claimt een praktische aanpak te bieden om optimale beleidsplannen te genereren voor de waarde van een brede klasse van TL-formules door recente decompositieresultaten uit te breiden. De primaire betekenis ligt in het oplossen van de pathologie waarbij gretige Q-maximalisatie faalt voor taken met een oneindige horizon, en in het bieden van een mechanisme om veiligheidsfilters te synthetiseren die de voldoening van complexe taken garanderen, niet alleen veiligheid. Door het toepassingsgebied van oplosbare formules uit te breiden tot geneste Until en Globally-Until-specificaties, overbrugt dit werk de kloof tussen Hamilton-Jacobi-bereikbaarheid en Reinforcement Learning voor complexe, veiligheidskritieke temporele taken.