Teaching LTL and {\omega}-automata with Spot

Technisches Resümee: Lehre von LTL und $\omega$-Automaten mit Spot

Problemstellung
Lineare Temporallogik (LTL) und $\omega$-Automaten sind fundamentale Bestandteile der Ausbildung in den formalen Methoden, insbesondere in der Programmverifikation und dem Model Checking. Während Lehrbücher die theoretischen Grundlagen vermitteln, erfordert ein tiefes Verständnis oft, dass Studierende die Übersetzung von LTL-Formeln in Automaten experimentell nachvollziehen. Lernende profitieren davon, zu beobachten, wie Variationen einer Formel die resultierende Automatenstruktur beeinflussen, um eine Intuition bezüglich Determinismus, Zustandskomplexität und der Beziehung zwischen syntaktischen Strukturen und semantischen Klassen (z. B. der Manna- & Pnueli-Hierarchie) aufzubauen. Eine effektive Lehre erfordert jedoch zugängliche Werkzeuge, die eine sofortige Visualisierung, den Vergleich und interaktives Experimentieren ohne komplexe Installationsbarrieren ermöglichen.

Methodik
Das Paper präsentiert Spot, eine ausgereifte Open-Source C++/Python-Bibliothek und Toolset zur Manipulation von LTL und $\omega$-Automaten, als pädagogische Plattform. Die Methodik konzentriert sich darauf, die bestehenden Fähigkeiten von Spot zu nutzen, um „Zero-Install“-Einstiegspunkte für die Lehre zu schaffen. Der Ansatz nutzt drei primäre Schnittstellen:

1. Web-Applikation: Eine Single-Page-Application, die über Standardbrowser zugänglich ist (keine lokale Installation erforderlich) und als interaktive Schnittstelle zur Übersetzung von Formeln, zum Studium von Eigenschaften und zum Vergleich von Logiken dient.
2. Jupyter Notebooks: Eine Sammlung von narrativen Notebooks, die Python-Code, Inline-Automaten-Visualisierungen (gerendert via Graphviz) und erläuternden Text kombinieren. Diese ermöglichen die programmatische Exploration von Inklusionsprüfungen, Gegenbeispielen und State-Relabeling.
3. Kommandozeilen-Tools: Eine Suite von Utilities zur Generierung von Zufallsbeispielen basierend auf spezifischen Kriterien, um Übungssätze zu erstellen.

Zentrale Beiträge
Das Paper beschreibt, wie die bestehenden Funktionen von Spot für den pädagogischen Einsatz umfunktioniert und strukturiert wurden:

• Interaktive Visualisierung und Übersetzung: Das Web-Tool ermöglicht es Nutzern, LTL- oder PSL-Formeln einzugeben und unmittelbar $\omega$-Automaten mit verschiedenen Akzeptanzbedingungen (Generalized Büchi, Rabin, Streett, Parity, etc.) zu generieren. Es unterstützt mehrere Eingabesyntaxen und Formate (HOA, Never Claims, LBTT, etc.).
• Vergleichende Analyse und Vereinfachung:
  • Äquivalenzprüfung: Der „Compare“-Tab erlaubt es Studierenden, zwei Formeln einzugeben und distinktive $\omega$-Wörter zu erhalten, falls diese nicht äquivalent sind, was die Entdeckung einfacherer äquivalenter Formeln erleichtert.
  • Navigation in der Hierarchie: Der „Study“-Tab identifiziert die präzise Klasse einer Formel innerhalb der Manna-&-Pnueli-Temporallogik-Hierarchie sowie der syntaktisch-futuristischen Hierarchie. Er hebt Diskrepanzen zwischen der syntaktischen Klassifizierung und den semantischen Eigenschaften hervor (z. B. Identifizierung, wenn eine Formel syntaktisch einer höheren Klasse angehört, aber eine Äquivalenz in einer niedrigeren Klasse besitzt).
  • Stutter-Invarianz: Das Tool erkennt Stutter-Invarianz, eine kritische Eigenschaft für die Partial Order Reduction im Model Checking. Falls eine Formel nicht Stutter-invariant ist, liefert das Tool spezifische Gegenbeispiel-Wörter ($w$ und $w'$), die das Versagen demonstrieren.
• Programmatische Exploration: Die Python-API und die Jupyter Notebooks ermöglichen die Demonstration fortgeschrittener Konzepte, wie etwa die Prüfung der Sprachinklusion durch nicht-deterministische Büchi-Automaten und das Relabeling der Zustände deterministischer Automaten mit den von ihnen erkannten LTL-Formeln.
• Automatisierte Übungsgenerierung: Die Kommandozeilen-Tools (randltl, ltlfilt) ermöglichen es Dozenten, durch Brute-Force zufällige Formeln zu generieren, die spezifischen Constraints entsprechen (z. B. Formeln, die äquivalent zu $a \mathbin{U} b$ sind, aber den Operator $X$ ausschließen, oder Stutter-invariante Formeln, die $X$ enthalten).

Ergebnisse
Das Paper demonstriert die praktische Anwendung dieser Werkzeuge anhand spezifischer pädagogischer Szenarien:

• Studierende können verifizieren, dass $(a \mathbin{R} (a \mathbin{U} b)) \mathbin{W} b$ äquivalent zu $a \mathbin{U} b$ ist, indem sie die Automaten vergleichen oder den Vergleichs-Tab nutzen.
• Das Tool identifiziert erfolgreich, dass $a \mathbin{W} \mathbin{F}(b)$ eine Obligation-Eigenschaft (Manna & Pnueli $\Delta_1$) ist, obwohl sie syntaktisch als $\Pi_2$ erscheint, und bestätigt deren Äquivalenz zu $G(a) \lor \mathbin{F}(b)$.
• Die Kommandozeilen-Beispiele generieren erfolgreich Listen von Formeln, die komplexen Kriterien entsprechen, wie etwa das Finden von 10 Formeln, die äquivalent zu $a \mathbin{U} b$ sind und dabei bestimmte Operatoren ausschließen, oder das Finden von Stutter-invarianten Formeln, die dennoch den Operator $X$ enthalten.

Bedeutung
Das Paper behauptet, dass Spot eine umfassende, zugängliche Plattform bietet, um die Verbindungen zwischen temporallogischen Formeln und ihren semantischen Automaten zu lehren. Durch das Angebot von Web-, Notebook- und Kommandozeilen-Schnittstellen deckt es diverse Bildungsszenarien ab – vom Unterricht mit Tablets bis hin zu Forschern, die Code schreiben. Die Bedeutung liegt in der Möglichkeit, über die statische Theorie hinauszugehen und Studierenden zu erlauben, zu „experimentieren: variiere eine Formel, beobachte, wie sich der resultierende Automat ändert, und baue so eine Intuition auf“. Die Werkzeuge werden als einsatzbereite Ressourcen präsentiert, die für Web-Nutzer keine Installation erfordern und vorkonfigurierte Umgebungen (via spot-sandbox) für diejenigen bieten, die Python nicht lokal installieren können, wodurch die Eintrittsbarriere für die Ausbildung in den formalen Methoden gesenkt wird.