On the Optimality of Uncertain MDP Abstractions

Titel: Over de Optimaliteit van Onzekere MDP-Abstrakties

Auteurs: Ibón Gracia en Morteza Lahijanian

1. Probleemstelling

Het paper adresseert het probleem van het automatisch synthetiseren van controllers voor niet-lineaire, stochastische systemen (zoals cyber-fysieke systemen) die onderhevig zijn aan onzekerheid. Het doel is om een controller te vinden die voldoet aan complexe temporale logica-specificaties (uitgedrukt in LTLf - Linear Temporal Logic over finite traces), zoals veiligheidseisen en doelbereiking, met formele waarborgen.

De huidige aanpak gebruikt Abstraktie-gebaseerde methoden, waarbij het continue systeem wordt gemodelleerd als een Uncertain Markov Decision Process (UMDP). Hoewel deze methoden geldige onder- en bovengrenzen voor de waarschijnlijkheid van het voldoen aan specificaties kunnen geven, ontbreekt er vaak een garantie op asymptotische optimaliteit.

• Het kernprobleem: Het verfijnen van de discretisatie (het kleiner maken van de ruimtelijke cellen) leidt niet altijd tot strakkere grenzen of betere controllers. In sommige gevallen kunnen de grenzen zelfs verslechteren.
• De vraag: Onder welke voorwaarden garanderen UMDP-abstraktie-methoden dat ze convergeren naar de ware optimale oplossing (asymptotische optimaliteit) en dat het algoritme in eindige tijd stopt met een $\epsilon$-optimale controller (compleetheid)?

2. Methodologie

De auteurs presenteren een abstraktie-verfijningsframework dat de volgende stappen omvat:

1. Systeemmodel: Een discrete-tijd stochastisch systeem $x_{t+1} = f(x_t, u_t, w_t)$ met niet-lineaire dynamica en onbekende verstoringen.
2. Abstraktie: Het continue toestandsruimte wordt gepartitioneerd in een eindig aantal regio's. Op basis hiervan wordt een UMDP geconstrueerd. De overgangskansen in de UMDP worden niet als vaste waarden gegeven, maar als onzekerheidssets (ambiguity sets) die alle mogelijke overgangskansen van het oorspronkelijke systeem omvatten.
3. Robuuste Dynamische Programmering (RDP): Op het geabstraheerde UMDP wordt RDP toegepast om een strategie (controller) en onder- ($p_{\eta}$) en bovengrenzen ($\bar{p}_{\eta}$) voor de vervullingswaarschijnlijkheid te berekenen.
4. Iteratief Verfijnen: Als de gap tussen de onder- en bovengrens groter is dan een vooraf gedefinieerde tolerantie $\epsilon$, wordt de partitie verfijnd (kleinere cellen) en wordt het proces herhaald.

De theoretische kern:
De auteurs introduceren een cruciale maatstaf: de Ambiguity Diameter ($\phi$). Dit is de maximale Wasserstein-afstand tussen de kansverdelingen binnen de onzekerheidssets van het UMDP.
Ze stellen een voldoende voorwaarde op, genaamd "Vanishing Ambiguity" (verdwijnende ambiguïteit):
$$\lim_{\eta \to 0} \phi(\text{Abs}(S, \eta)) = 0$$
Waarbij $\eta$ de grootte van de partitie is. Als deze voorwaarde geldt, garandeert het dat de abstraktie convergeert naar de ware dynamiek naarmate de discretisatie fijner wordt.

3. Belangrijkste Bijdragen

1. Voldoende Voorwaarde voor Asymptotische Optimaliteit:
   De auteurs leiden een theoretische voorwaarde af ("vanishing ambiguity") die garandeert dat een abstraktie-procedure asymptotisch optimaal is. Dit betekent dat naarmate de partitie oneindig fijn wordt, de berekende waarden convergeren naar de werkelijke optimale vervullingswaarschijnlijkheid.

2. Vergelijking van Abstraktie-klassen (SMDP vs. IMDP):

   • Set-valued MDP (SMDP): De auteurs tonen aan dat SMDP-abstrakties (die gebruikmaken van bereiksets om de onzekerheid te modelleren) voldoen aan de "vanishing ambiguity" voorwaarde. Zij zijn dus asymptotisch optimaal.
   • Interval MDP (IMDP): Ze bewijzen dat de populaire IMDP-aanpak (die overgangskansen beperkt tot intervallen) niet noodzakelijkerwijs aan deze voorwaarde voldoet, zelfs niet bij zeer fijne discretisatie. IMDP kan leiden tot "triviale" grenzen (bijv. [0, 1]) die niet verbeteren bij verfijning.

3. Compleetheid van het Algoritme:
   Ze bewijzen dat als de abstraktie-procedure asymptotisch optimaal is, het verfijningsalgoritme (Algorithm 1) in eindige tijd stopt en een $\epsilon$-optimale controller levert voor elke LTLf-specificatie.

4. Efficiëntie-optimalisatie:
   Ze presenteren een variant van de SMDP-abstraktie waarbij alleen de veilige toestandsruimte ($X_{safe}$) wordt gepartitioneerd, terwijl de onveilige regio als één enkele "val" wordt behandeld. Dit vermindert de rekencomplexiteit zonder de optimaliteit te verliezen.

4. Resultaten en Empirische Validatie

De theorie werd gevalideerd via twee case studies:

• 1D Temperatuurregeling:

  • Doel: Temperatuur regelen naar een doelinterval binnen 20 stappen, terwijl de veiligheidsgrenzen worden gehandhaafd.
  • Resultaat: De SMDP-aanpak convergeerde snel (binnen 8 iteraties) naar een nauwkeurige grens (fout < 2%). De IMDP-aanpak vertoonde geen verbetering bij verfijning; de gap tussen onder- en bovengrens bleef groot.

• 2D Niet-lineaire Karretje-model:

  • Doel: Een complex LTLf-schets (veilig blijven, water vermijden of drogen, opladen bereiken).
  • Resultaat: De SMDP-methoden leverden zinvolle, strakke waarschijnlijkheidsborders en verbeterden bij verfijning. De IMDP-methoden leverden vaak vacuüm grenzen (bijna [0, 1]) over grote delen van de toestandsruimte, wat betekent dat ze geen bruikbare informatie gaven over de waarschijnlijkheid van succes, zelfs niet bij fijne discretisatie.

5. Betekenis en Conclusie

Dit paper legt de theoretische basis voor het vertrouwen in abstraktie-gebaseerde controller-synthese voor complexe systemen.

• Praktische impact: Het identificeert dat niet alle UMDP-abstrakties gelijk zijn. Het gebruik van IMDP (vaak gebruikt vanwege eenvoud) kan leiden tot algoritmes die nooit convergeren naar een bruikbare oplossing voor niet-lineaire systemen. SMDP wordt aanbevolen als de methode die wel garandeert dat verfijning leidt tot betere resultaten.
• Theoretische bijdrage: Het paper lost een fundamentele vraag op: "Wanneer garanderen abstraktie-methoden optimaliteit?" Door de "vanishing ambiguity" voorwaarde te definiëren, biedt het een richtsnoer voor het ontwerpen van toekomstige abstraktie-algoritmen.
• Toekomstperspectief: Het werk maakt het mogelijk om formele garanties te geven voor het inzetten van autonome systemen in veiligheidskritieke omgevingen, waarbij men zeker weet dat een fijnere discretisatie de betrouwbaarheid van de controller verbetert in plaats van verslechtert.

Kortom, het paper waarschuwt voor de valkuilen van interval-gebaseerde abstrakties bij niet-lineaire dynamica en biedt Set-valued MDPs als een wiskundig onderbouwde, asymptotisch optimale alternatief.