Witnesses for Fixpoint Games on Lattices

Probleemstelling

In de concurrentietheorie worden veel concepten (zoals bisimilariteit, gedragsmetrieken voor probabilistische systemen en terminatiekansen in Markov-ketens) gekarakteriseerd als de kleinste vaste punt ($\mu$) van een monotonische functie op een volledige tralies (lattice).

• Het is vaak eenvoudig om een bovengrens te bewijzen voor een vaste punt: men hoeft alleen een pre-vaste punt te vinden dat onder de bovengrens ligt.
• Het is echter veel moeilijker om een ondergrens te bewijzen (of te tonen dat een gegeven bovengrens niet geldt). Bijvoorbeeld: bewijzen dat twee toestanden niet bisimulair zijn, of dat de afstand tussen twee toestanden strikt groter is dan een bepaalde waarde.
• Bestaande methoden, zoals onderscheidende formules (distinguishing formulas) in de Hennessy-Milner logica, bestaan wel, maar hun constructie is vaak specifiek voor het geval en niet generiek. Er ontbreekt een uniforme, tralietheoretische benadering om deze "witnesses" (getuigen) systematisch af te leiden uit strategieën in speltheoretische modellen.

Methodologie

De auteurs ontwikkelen een algemeen raamwerk dat tralietheorie, Galois-verbindingen en fixpoint-spellen combineert.

1. Tralies en Galois-verbindingen:

   • Er wordt een onderscheid gemaakt tussen een "logische wereld" ($L$) en een "gedragswereld" ($B$).
   • Deze werelden worden verbonden via een Galois-verbinding $(\alpha \dashv \gamma)$, waarbij $\alpha: L \to B$ en $\gamma: B \to L$.
   • De functie $\alpha$ vertaalt de kleinste vaste punt van de logische functie ($\mu_{log}$) naar de kleinste vaste punt van de gedragsfunctie ($\mu_{beh}$), d.w.z. $\alpha(\mu_{log}) = \mu_{beh}$.

2. Fixpoint-spellen:

   • Er worden twee soorten spellen geïntroduceerd om de relatie tussen een element en de vaste punt te testen:
     • Primaal spel: De speler $\exists$ (aanvaller) probeert te bewijzen dat een element $b$ strikt onder de vaste punt ligt ($b \ll \mu_{beh}$). De speler $\forall$ (verdediger) probeert dit te weerleggen.
     • Dual spel: Hier wordt de orde omgekeerd. De speler $\forall$ (aanvaller) probeert te bewijzen dat de vaste punt niet onder een element ligt ($\mu_{beh} \not\sqsubseteq b$).
   • Deze spellen worden gedefinieerd op continue (voor primaal) en co-continue (voor dual) tralies, gebruikmakend van de "way-below" ($\ll$) en "way-above" ($\triangleright\triangleright$) relaties.

3. Witnesses en Strategieën:

   • Een witness is een element in de logische tralies $L$ dat fungeert als een onderscheidende formule.
   • De kern van de methode is de transformatie tussen:
     • Een witness in $L$ $\leftrightarrow$ Een winnende strategie in het spel op $B$.
   • De auteurs definiëren hulpfuncties om strategieën in het logische spel om te zetten in strategieën in het gedrags spel en vice versa.

Kernbijdragen

1. Universele Definitie van Witnesses:
   De auteurs definiëren "primaal" en "dual" witnesses formeel. Een primaal witness $a \in L$ voor een element $b \in B$ voldoet aan $a \ll \mu_{log}$ en $b \ll \alpha(a)$. Een dual witness voldoet aan $a \ll \mu_{log}$ en $\alpha(a) \not\sqsubseteq b$.

2. Equivalentie tussen Strategieën en Witnesses:
   Er wordt bewezen dat het bestaan van een witness equivalent is aan het bestaan van een finitaire winnende strategie voor de aanvaller in het respectievelijke spel.

   • Als de aanvaller een strategie heeft om te winnen, kan deze strategie worden omgezet in een constructieve witness (een formule).
   • Omgekeerd kan een witness worden gebruikt om een strategie te construeren.

3. Constructieve Algoritmen:
   Het artikel biedt generieke algoritmen voor:

   • Het afleiden van een strategie uit een gegeven witness.
   • Het inductief construeren van een witness uit een gegeven strategie (via de hulpfuncties $W_p$ en $W_d$).
   • Deze constructies garanderen dat de "graad" (degree) van de witness afneemt, wat zorgt voor terminatie van het constructieproces.

4. Instantiaties in Bestaande en Nieuwe Contexten:
   Het raamwerk wordt succesvol toegepast op:

   • Bisimilariteit: Herleidt het concept van onderscheidende formules (Hennessy-Milner) tot een tralietheoretische constructie.
   • Gedragsmetrieken (Probabilistische Systemen): Toont aan hoe formules kunnen worden geconstrueerd die bewijzen dat de afstand tussen toestanden boven een bepaalde drempel ligt (gebaseerd op de Kantorovich-afstand).
   • Terminatiekansen in Markov-ketens (Nieuw): Dit is een nieuwe case study. Het artikel toont aan hoe men witnesses kan construeren (in de vorm van bomen) die een ondergrens certificeren voor de waarschijnlijkheid dat een Markov-keten terminateert.

Resultaten

• Existentie en Constructie: Er wordt bewezen dat voor continue tralies en geschikte basissets (zoals singletons of co-singletons), het bestaan van een witness equivalent is aan het bestaan van een finitaire strategie.
• Finitaire Strategieën: De auteurs tonen aan dat onder bepaalde voorwaarden (zoals continuïteit van de functies) de winnende strategieën "finitair" zijn. Dit betekent dat ze gebaseerd zijn op eindige verzamelingen van basis-elementen, wat cruciaal is voor praktische implementatie en begrijpelijkheid.
• Dualiteit: De paper illustreert dat er twee complementaire perspectieven zijn (primaal en dual) die elk hun eigen type witness en strategie genereren, afhankelijk van of men een ondergrens wil bewijzen of een bovengrens wil ontkrachten.

Betekenis en Impact

• Generalisatie: Het werk generaliseert het concept van onderscheidende formules van specifieke logische systemen naar een abstracte tralietheoretische setting. Dit maakt het toepasbaar op een breed scala aan systemen, inclusief die met kwantitatieve aspecten (zoals waarschijnlijkheid en metrieken).
• Verklarende AI (Explainability): De geconstrueerde witnesses fungeren als "verklaringen" voor waarom twee toestanden niet equivalent zijn of waarom een bepaalde eigenschap niet geldt. In plaats van alleen te zeggen "ze zijn niet bisimulair", levert het systeem een concrete formule of boom op die de reden toont.
• Nieuwe Toepassingen: De toepassing op terminatiekansen in Markov-ketens opent nieuwe wegen voor het verifiëren van probabilistische systemen, waar eerdere methoden beperkt waren.
• Verbinding met Speltheorie: Het artikel legt een sterke brug tussen de abstracte theorie van vaste punten en de praktische implementatie via spelstrategieën, wat nuttig is voor het ontwikkelen van model-checking tools.

Kortom, dit artikel biedt een robuust theoretisch fundament voor het genereren van bewijzen (witnesses) voor negatieve eigenschappen in systemen die via vaste punten worden gemodelleerd, met een duidelijke route van abstracte tralietheorie naar concrete constructieve algoritmen.