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

1. Problemstellung

Die automatische Synthese reaktiver Systeme zielt darauf ab, Strategien für Systeme zu konstruieren, die mit ihrer Umgebung interagieren. Derzeitige Ansätze leiden oft unter der sogenannten Zustandsraum-Explosion (State Space Explosion).

• Komplexität: Die Übersetzung von Spezifikationen in Linearer Temporaler Logik (LTL) in deterministische Wortautomaten (als Spielgraphen) führt zu einer Zustandsanzahl, die doppelt exponentiell in der Länge der Spezifikation ist. Selbst für LTL-Subklassen wie GR(1) bleibt die Komplexität hoch, wenn komplexe Muster wie Zählungen involviert sind.
• Spezifisches Defizit: Viele praktische Anwendungen erfordern Verhaltensmuster, die durch Zählbedingungen (Counting Constraints) beschrieben werden (z. B. „Das System muss Aktion $a$ mindestens $k$-mal in $l$ Zügen ausführen"). Bisherige effiziente Synthese-Algorithmen (wie GR(1)) können solche Bedingungen oft nicht direkt oder effizient handhaben, da die direkte Kodierung des gesamten Gedächtnisses (History) für diese Bedingungen den Zustandsraum massiv aufbläht.
• Herausforderung: Es fehlt an heuristisch effizienten Methoden, um diese Zählbedingungen in die Synthese zu integrieren, ohne den gesamten Spielgraphen sofort in seiner maximalen Größe zu konstruieren.

2. Methodik: Inkrementelle Synthese mit Fenster-Zählbedingungen

Die Autoren schlagen einen inkrementellen Synthese-Ansatz vor, der die Monotonie-Eigenschaft von Zählbedingungen ausnutzt, um den Zustandsraum schrittweise zu verfeinern.

A. Fenster-Zählbedingungen (Window Counting Constraints)

Die Methode basiert auf Bedingungen der Form:

• $CC_{min}$: „Spieler EGO führt Aktion $a$ mindestens $k$-mal in $l$ eigenen Zügen aus."
• $CC_{max}$: „Spieler EGO führt Aktion $a$ höchstens $k$-mal in $l$ eigenen Zügen aus."
  Diese Bedingungen werden als „Fenster" betrachtet, die über den Spielverlauf gleiten.

B. Das Prinzip der Monotonie und Inkrementierung

Der Kern der Methode liegt in der Beobachtung, dass die Erfüllbarkeit von Bedingungen monoton ist:

• Wenn eine Strategie eine Bedingung $CC_{min}(k, l-1)$ erfüllt, erfüllt sie automatisch auch $CC_{min}(k, l)$.
• Umgekehrt ist die Existenz einer Strategie für eine restriktivere Bedingung (kleineres $l$ bei $CC_{min}$) eine notwendige Bedingung für die weniger restriktive Version.

Der Algorithmus läuft wie folgt ab:

1. Initialisierung: Statt die volle Länge $l$ der Zählbedingungen zu verwenden, startet der Algorithmus mit einer minimalen Länge (z. B. $l' = k$). Dies erzeugt einen sehr kleinen Spielgraphen (Situation Graph).
2. Synthese-Schritt: Es wird eine Gewinnstrategie für den aktuellen, kleinen Graphen berechnet.
3. Analyse und Pruning:
   • Wenn eine Gewinnstrategie gefunden wird, werden die Gewinnregionen (Winning Regions) dieser Iteration gespeichert.
   • Aufgrund der Monotonie-Eigenschaft gilt: Zustände, die in einer früheren Iteration (mit kürzeren Fenstern) als gewinnend identifiziert wurden, bleiben auch in späteren Iterationen (mit längeren Fenstern) gewinnend.
   • Diese Information wird genutzt, um den Graphen der nächsten Iteration zu reduzieren: Teile des Graphen, die bereits als gewinnend bekannt sind, müssen nicht weiter expandiert werden; sie werden direkt in einen „Gewinn-Senken"-Zustand (Winning Sink) umgeleitet.
4. Iteration: Die Länge der Fenster ($l$) wird schrittweise erhöht, bis die ursprüngliche Spezifikation erreicht ist. In jedem Schritt wird nur der Teil des Graphen konstruiert, der nicht bereits durch vorherige Ergebnisse abgedeckt ist.

C. Situation Graphs (Situationsgraphen)

Um das Gedächtnis für die Zählbedingungen effizient zu kodieren, wird ein Situation Graph verwendet. Ein Zustand (Situation) besteht aus:

• Dem aktuellen Zustand des ursprünglichen Spielgraphen.
• Einem History-Teil, der nur die für die Zählbedingungen relevanten Informationen speichert (z. B. ob die Aktion in den letzten $l$ Zügen ausgeführt wurde).
  Dieser Graph wird inkrementell aufgebaut und durch die gewonnenen Informationen aus vorherigen Schritten „beschnitten".

D. Behandlung von $CC_{max}$

Für Bedingungen vom Typ „höchstens $k$" ($CC_{max}$) wird eine Transformation in eine äquivalente „mindestens"-Bedingung ($CC_{min}$) für die komplementäre Aktion vorgeschlagen, um die Inkrementierung einheitlich handhaben zu können.

3. Wichtige Beiträge

1. Neues Synthese-Framework: Einführung eines inkrementellen Ansatzes speziell für reaktive Systeme mit Fenster-Zählbedingungen, der die direkte Konstruktion des vollständigen, riesigen Automaten vermeidet.
2. Erweiterung der Spielklassen: Im Gegensatz zum Vorgängerwerk (GandALF 2024), das nur Sicherheits-Spiele behandelte, erweitert dieses Paper die Methode auf Erreichbarkeits-, Büchi-, Co-Büchi- und Paritätsspiele.
3. Flexibilität bei Constraints: Die Methode erlaubt das gleichzeitige Inkrementieren sowohl von „mindestens"- als auch von „höchstens"-Bedingungen innerhalb desselben Synthese-Prozesses.
4. Theoretische Fundierung: Formale Definition von Spielen mit Zählbedingungen, Situation Graphs und Beweise für die Korrektheit der Monotonie-Ausnutzung (Theorem 3.1, Lemma 3.2).
5. Implementierung und Evaluation: Eine vollständige Implementierung in Python und eine detaillierte experimentelle Auswertung.

4. Ergebnisse

Die Autoren führten Experimente an künstlich generierten Gitter-Spielen (Grid Games) durch, die Szenarien wie die Navigation eines Roboters auf einer Fabrikhalle simulieren.

• Vergleich: Der inkrementelle Ansatz (sequentiell und Round-Robin) wurde mit einer direkten Synthese (ohne Inkrementierung, also Konstruktion des vollen Graphen) verglichen.
• Performance-Gewinn:
  • In fast allen getesteten Fällen (außer einem) reduzierte der inkrementelle Ansatz den Speicherbedarf und die Rechenzeit drastisch.
  • Beispiel: In Experiment 2 benötigte die direkte Synthese über 6.000 Sekunden und fast 6 Millionen Zustände. Der inkrementelle Ansatz (Round-Robin) benötigte nur 3 Sekunden und ca. 9.700 Zustände.
  • Selbst wenn der inkrementelle Ansatz mehr Speicher für die Zwischenergebnisse (Gewinnregionen) benötigt, ist dieser Speicherbedarf um Größenordnungen geringer als der des vollen Graphen.
• Grenzen: In Fällen, in denen eine Gewinnstrategie nur bei voller Fensterlänge existiert und vorherige Iterationen leer bleiben, kann der inkrementelle Ansatz einen leichten Overhead haben, ist aber nie katastrophal schlechter als die direkte Methode.

5. Bedeutung und Ausblick

Bedeutung:
Dieser Ansatz bietet einen vielversprechenden Weg, die Synthese reaktiver Systeme für Anwendungen mit komplexen Zählanforderungen (z. B. Robotik, autonome Fahrzeuge, industrielle Automatisierung) praktikabel zu machen. Er umgeht die Notwendigkeit, die theoretische Komplexitätsklasse des Problems zu ändern, und nutzt stattdessen heuristische Optimierungen, um die praktische Effizienz massiv zu steigern.

Zukünftige Arbeiten (Future Work):
Die Autoren skizzieren fünf Richtungen für zukünftige Forschung:

1. Kooperative Spiele: Erweiterung von Nullsummen-Spielen auf kooperative Szenarien, wo die Umgebung (ALTER) auch ihre eigenen Zählbedingungen erfüllen muss, ohne vom System in eine Verletzung gezwungen zu werden.
2. Erweiterung der Constraints: Identifikation weiterer Spezifikationsmuster mit Monotonie-Eigenschaften (z. B. zeitliche Abhängigkeiten).
3. Symbolische Synthese: Transformation des expliziten Ansatzes in einen symbolischen Algorithmus (z. B. mittels BDDs oder Antichains), um noch größere Systeme zu handhaben.
4. On-the-Fly-Synthese: Kombination mit Algorithmen, die den Graphen dynamisch während der Suche erweitern.
5. Symmetrische Synthese: Anwendung auf Systeme von Systemen (z. B. Roboter-Schwärme), bei denen identische Agenten dieselbe Strategie verwenden.

Zusammenfassend demonstriert das Paper, dass die Ausnutzung struktureller Eigenschaften von Spezifikationen (hier: Monotonie bei Zählbedingungen) ein effektives Mittel ist, um die Hürde der Zustandsraum-Explosion in der reaktiven Synthese zu überwinden.