Strategies in Sabotage Games: Temporal and Epistemic Perspectives

Probleemstelling

Sabotagegames zijn abstracte modellen waarin een speler (de "runner") probeert een doelvertex in een graaf te bereiken, terwijl een tegenstander (de "demon" of "blocker") in elke beurt een willekeurige rand uit de graaf verwijdert. Traditioneel worden deze games geanalyseerd met behulp van Sabotage Modal Logic (SML). Hoewel SML effectief is voor het karakteriseren van winnende strategieën in statische of stap-voor-stap scenario's, heeft het beperkingen:

1. Het mist een natuurlijke manier om temporele eigenschappen (zoals "levensvatbaarheid" of liveness) en complexe strategieën over tijd te modelleren.
2. Het is beperkt tot strikt beurtelings spelen en kan gelijktijdige bewegingen (concurrente games) niet goed behandelen.
3. Het houdt geen rekening met onvolledige informatie (epistemische aspecten) over de staat van het spel of de acties van de tegenstander.

Het doel van dit paper is een unificerend logisch raamwerk te bieden dat strategisch redeneren over tijd (via Alternating-time Temporal Logic, ATL) combineert met de structurele dynamiek van sabotagegames, inclusief onzekerheid.

Methodologie

De auteurs reconstrueren sabotagegames binnen het kader van Alternating-time Temporal Logic (ATL)* en zijn epistemische extensies (ATEL). De methodologische stappen zijn als volgt:

1. Definitie van Spelstructuren:
   De auteurs definiëren drie types sabotagegame-structuren op basis van een graaf $G=(V,E)$:

   • Strikt beurtelings (Turn-based, tb): Spelers wisselen beurtelings af. De staat wordt gekenmerkt door wie aan de beurt is.
   • Concurrent: Spelers kiezen gelijktijdig een rand. Als beide spelers dezelfde rand kiezen, wordt deze annulerend (geen effect).
   • Generiek (General): Een combinatie waarbij spelers kunnen kiezen om te bewegen of "skip" (niets doen) te kiezen, waardoor elke volgorde van bewegingen gesimuleerd kan worden.

2. Logische Formalisatie (ATL):*
   In plaats van alleen vertices te modelleren, modelleren de auteurs de volledige speltoestand (restant van randen + positie van de runner) als een toestand in een ATL*-model.

   • Ze gebruiken de strategische operator $\langle\langle C \rangle\rangle$ (coalitie $C$ heeft een strategie om $\phi$ af te dwingen).
   • Ze introduceren een geparametriseerde "until"-operator ($\psi U_i \phi$) uit metrische temporele logica om de "levensduur" (liveness) van de runner te kwantificeren (aantal beurten dat de runner actief blijft).

3. Epistemische Extensie (ATEL):
   De logica wordt uitgebreid met kennisoperatoren ($K_a$, $E_\Gamma$, $C_\Gamma$) om scenario's met onvolledige informatie te modelleren. Hierbij worden toegankelijkheidsrelaties ($\sim_i$) gedefinieerd die aangeven welke speltoestanden een agent niet van elkaar kan onderscheiden.

4. Analyse van Strategieën:
   De auteurs analyseren winnende strategieën voor zowel Reachability Sabotage Games (RSG) (doel: doelvertex bereiken) als Liveness Sabotage Games (LSG) (doel: zo lang mogelijk in leven blijven). Ze vergelijken deze resultaten met bestaande SML-formules.

Belangrijkste Bijdragen en Resultaten

1. Karakterisering van Winststrategieën in ATL*

• Reachability (RSG): De winnende strategie voor de runner in een beurtelings spel wordt uitgedrukt als $\langle\langle \{r\} \rangle\rangle \mathbf{F}g$ (de runner kan afdwingen dat $g$ uiteindelijk waar wordt).
  • Resultaat: In strikt beurtelings RSG's kan de runner bijna nooit winnen (tenzij de start- en doelvertex direct verbonden zijn), omdat de demon altijd de enige rand naar het doel kan verwijderen voordat de runner die kan nemen.
  • Concurrentie: Concurrente games beperken de runner verder; de demon kan de runner's beweging "annuleren" door dezelfde rand te kiezen.
• Liveness (LSG): Voor games waar de runner moet overleven gedurende $b$ beurten, wordt de formule $\langle\langle \{r\} \rangle\rangle \top \mathbf{U}_{2b} (\mathbf{X}\top)$ gebruikt. Dit betekent dat de runner een strategie heeft om het spel minimaal $2b$ stappen (beurten) te laten duren.

2. Dynamische Minimaal Snijpunt (Dynamic Min-Cut)

De auteurs verbinden sabotagegames met het grafentheoretische probleem van het minimale $s-t$ snijpunt (min-cut).

• Static vs. Dynamic: Een statische min-cut is het minimale aantal randen dat verwijderd moet worden om twee knopen te scheiden. In een dynamische sabotagegame kan de runner echter bewegen tussen de verwijderingen van de demon.
• Resultaat: De "dynamische min-cut" is het minimale aantal beurten dat de demon nodig heeft om de runner te blokkeren, rekening houdend met de runner's bewegingen. Dit getal is vaak hoger dan de statische min-cut omdat de runner uit een statische "val" kan ontsnappen. De auteurs tonen aan dat ATL* deze dynamische cut kan karakteriseren via formules zoals $\langle\langle \{d\} \rangle\rangle (\top \mathbf{U}_k (\langle\langle \emptyset \rangle\rangle \mathbf{G}\neg g))$.

3. Angelic Sabotage Games

Het paper introduceert een extensie waarbij een derde speler, de "angel", randen kan toevoegen (in plaats van alleen verwijderen). Dit maakt het mogelijk om games te modelleren waarin de connectiviteit van de graaf kan herstellen, wat leidt tot complexere, oneindige spelverlopen en eigenschappen zoals $\langle\langle C \rangle\rangle \mathbf{G}\mathbf{F}g$ (oneindig vaak het doel bereiken).

4. Epistemische Analyse (Onvolledige Informatie)

De auteurs tonen aan dat een speler een winnende strategie kan hebben zonder te weten dat ze die heeft.

• Voorbeeld: Als de runner niet weet of ze zich op knoop $u$ of $v$ bevindt (maar beide lijken qua uitgaande randen hetzelfde), kan ze een strategie hebben die werkt als ze op $u$ zit, maar falen als ze op $v$ zit.
• Formulering: In ATEL kan men onderscheid maken tussen $\langle\langle \{r\} \rangle\rangle \mathbf{F}g$ (er bestaat een strategie) en $K_r \langle\langle \{r\} \rangle\rangle \mathbf{F}g$ (de runner weet dat ze een strategie heeft). De auteurs tonen aan dat in scenario's met onvolledige informatie de tweede formule vaak niet waar is, zelfs als de eerste dat wel is.

Significantie en Toekomstperspectief

• Unificatie: Het paper biedt een krachtig raamwerk dat temporele logica (ATL*), speltheorie en grafentheorie verenigt. Het lost de beperkingen van SML op door concurrentie en complexe tijdsafhankelijke eigenschappen te kunnen modelleren.
• Toepassingsgebied: De aanpak is relevant voor het modelleren van dynamische netwerken (zoals vervoersnetwerken of communicatienetwerken) waar verbindingen kunnen falen of worden aangevallen, en waar agents onzekerheid hebben over de staat van het netwerk.
• Toekomstig werk: De auteurs zien potentie in het bestuderen van meerdere runners, gedistribueerde doelen, en het verder versterken van de link met algoritmische grafentheorie (bijv. dynamische max-flow/min-cut problemen). Ook wordt er gepleit voor verdere onderzoek naar strategieën met geheugen (memory-based strategies) in epistemische sabotagegames.

Kortom, dit paper transformeert sabotagegames van een puur statisch logisch probleem naar een dynamisch, strategisch en epistemisch model, wat nieuwe inzichten biedt in de complexiteit van interactieve systemen met veranderende structuren.