Towards the Usage of Window Counting Constraints in the Synthesis of Reactive Systems to Reduce State Space Explosion

Probleemstelling

De synthese van reactieve systemen (het automatisch construeren van strategieën voor systemen die interageren met hun omgeving) lijdt onder het probleem van explosie van de toestandsruimte (state space explosion).

• Complexiteit: Het vertalen van een specificatie in Linear Temporal Logic (LTL) naar een deterministische automaat voor strategievorming heeft een complexiteit van dubbel exponentieel ($2^{2^n}$) ten opzichte van de lengte van de specificatie.
• Beperkingen: Bestaande heuristieken, zoals het beperken tot de GR(1)-subclass van LTL, lossen dit niet volledig op, omdat veel praktische specificaties (zoals die met tel- of telling-patronen) buiten deze klasse vallen.
• Specifiek doel: Het artikel richt zich op het synthetiseren van systemen met window counting constraints (venster-telconstraints). Deze constraints eisen dat een speler een bepaalde actie $k$ keer uitvoert binnen een venster van $l$ eigen zetten (bijv. "een robot moet zijn batterij opladen in ten minste 2 van de laatste 10 zetten"). Het direct modelleren van deze constraints vereist vaak een enorme hoeveelheid geheugen om de geschiedenis van de laatste $l$ zetten bij te houden.

Methodologie

De auteurs stellen een incrementele synthese-aanpak voor die gebruikmaakt van de monotonie-eigenschap van telconstraints om de grootte van de te construeren automaat te beperken.

1. Venster-telconstraints (Window Counting Constraints):

   • De constraints worden gedefinieerd als $CC_{min}(p, a, k, l)$ (minimaal $k$ keer in $l$ zetten) of $CC_{max}(p, a, k, l)$ (maximaal $k$ keer in $l$ zetten).
   • De methode gaat uit van een nulsom-spel (zero-sum game) waarbij de omgeving (ALTER) rationeel is: deze zal haar eigen constraints niet schenden, tenzij ze er geen keuze in hebben.

2. Incrementele Strategie:

   • In plaats van direct de volledige constraints (met de uiteindelijke, vaak grote waarden voor $l$) te modelleren, start het algoritme met een subgroep van constraints met korte vensters (kleine $l$).
   • Monotonie: Als een winnende strategie bestaat voor een korter venster (bijv. $l-1$), dan geldt deze strategie ook voor een langer venster ($l$) voor $CC_{max}$-constraints. Voor $CC_{min}$-constraints geldt het omgekeerde: als een strategie voldoet aan een korter venster, voldoet deze automatisch aan een langer venster.
   • Iteratief proces:
     1. Start met minimale constraint-lengtes.
     2. Construeer een situatiegrafiek (situation graph). Dit is een expansie van de spelgrafiek waarbij toestanden worden verrijkt met de relevante geschiedenis (telwaarden) om de constraints te controleren.
     3. Bereken de winnende regio voor deze vereenvoudigde graaf.
     4. Pruning (Versnoeiing): Gebruik de kennis uit de vorige iteratie. Als een situatie een uitbreiding is van een situatie die al bekend is als "winnend" in een eerdere iteratie, hoeven de opvolgers van deze situatie niet meer te worden geconstrueerd; ze worden direct gemarkeerd als winnend.
     5. Verhoog de lengte van de constraints ($l$) en herhaal het proces totdat de volledige specificatie is bereikt of geen winnende strategie meer mogelijk is.

3. Situatiegrafieken en Zinken (Sinks):

   • Om de synthese-algoritmen voor standaard speltypen (veiligheid, bereikbaarheid, B"uchi, etc.) te kunnen toepassen, worden de situatiegrafieken aangepast met twee speciale "zinken" (sinks):
     • Winnende zink (W): Wordt bereikt als een situatie een uitbreiding is van een eerdere winnende regio.
     • Verliezende zink (L): Wordt bereikt als een constraint wordt geschonden.
   • Dit zorgt ervoor dat de graaf geen dodelopen (deadlocks) heeft en dat standaard synthese-algoritmen direct toepasbaar zijn.

4. Transformatie van Constraints:

   • Om de monotonie consistent te houden, worden $CC_{max}$-constraints (maximaal $k$ keer) tijdelijk vertaald naar $CC_{min}$-constraints (minimaal $l-k$ keer voor de tegengestelde actie) zodat de incrementele lengte-verhoging uniform kan worden toegepast.

Belangrijkste Bijdragen

• Incrementele Benadering voor Telconstraints: Een nieuw algoritme dat de synthese van reactieve systemen met telconstraints aanpakt door de constraint-lengte stapsgewijs te verhogen in plaats van alles in één keer te modelleren.
• Uitbreiding van Speltypen: In tegenstelling tot eerdere werk (dat zich beperkte tot veiligheidsspellen), ondersteunt deze methode nu ook bereikbaarheid, B"uchi, co-B"uchi en pariteitsspellen.
• Flexibiliteit in Constraints: De methode ondersteunt nu zowel "minimaal $k$ keer" als "maximaal $k$ keer" constraints binnen dezelfde synthese-procedure, wat in eerdere versies beperkt was.
• Situatiegrafiek-concept: Een formele definitie van situatiegrafieken die geschiedenis alleen opslaan waar nodig voor de constraints, gecombineerd met een mechanisme om winnende regio's uit eerdere iteraties te hergebruiken om de graaf te verkleinen.

Resultaten

De auteurs hebben een implementatie in Python ontwikkeld en experimenten uitgevoerd op gegenereerde spelgrafieken (gebaseerd op rooster-spellen voor robots).

• Vergelijking: De incrementele methode (met sequentiële en round-robin strategieën voor het verhogen van $l$) werd vergeleken met directe synthese (volledige constraint-lengte vanaf het begin).
• Prestaties:
  • In de meeste experimenten (bijv. Experiment 1, 2, 4, 5, 6, 7) resulteerde de incrementele methode in een significante reductie van zowel de rekentijd als het aantal toestanden in de laatste graaf.
  • Voorbeeld: In Experiment 2 daalde de rekentijd van 6102 seconden (direct) naar 3 seconden (incrementeel) en het aantal toestanden van ~6 miljoen naar ~9.700.
  • Geheugenbesparing: Hoewel de incrementele methode geheugen moet bijhouden voor de winnende regio's van eerdere stappen, is dit set van toestanden heuristisch veel kleiner dan de volledige situatiegrafiek die nodig zou zijn voor de volledige constraints.
• Uitzondering: In sommige gevallen (zoals Experiment 3) was er geen winnende strategie, en leverde de incrementele methode slechts een kleine overhead op zonder grote winst, omdat de volledige constraint-lengte nodig was om te concluderen dat er geen oplossing is.

Betekenis en Toekomstperspectief

• Praktische Toepasbaarheid: De methode biedt een haalbare weg om complexe specificaties met telconstraints te synthetiseren zonder dat de toestandsruimte onbeheersbaar groot wordt. Dit is cruciaal voor toepassingen zoals robotica en geautomatiseerde fabrieken.
• Heuristische Efficiëntie: Hoewel de methodologische complexiteitsklasse van het synthese-probleem niet verandert (het blijft exponentieel/dubbel exponentieel), biedt de aanpak een krachtige heuristiek om de praktische uitvoerbaarheid te verbeteren.
• Toekomstig Werk: De auteurs schetsen vijf richtingen voor verdere ontwikkeling:
  1. Uitbreiden naar coöperatieve spellen (in plaats van strikt nulsom), waarbij de omgeving ook kan verliezen als ze haar constraints schendt.
  2. Identificeren van nieuwe specificatiepatronen met vergelijkbare monotonie-eigenschappen.
  3. Overgang naar symbolische synthese (in plaats van expliciete toestandsrepresentatie) voor nog grotere schaalbaarheid.
  4. Combineren met on-the-fly synthese-algoritmen.
  5. Toepassing op systemen van systemen (symmetrische synthese), zoals een vloot van identieke robots die dezelfde strategie volgen.

Kortom, dit artikel introduceert een innovatieve, iteratieve techniek die de "state space explosion" bij reactieve synthese met telconstraints effectief aanpakt door slim gebruik te maken van eerdere berekeningen en de wiskundige eigenschappen van de constraints.