Teaching LTL and {\omega}-automata with Spot

Technische Samenvatting: Het onderwijzen van LTL en $\omega$-automaten met Spot

Probleemstelling
Linear Temporal Logic (LTL) en $\omega$-automaten zijn fundamenteel voor het onderwijs in formele methoden, met name binnen programmareverificatie en model checking. Hoewel tekstboeken de theoretische fundamenten bieden, vereist een diepgaand begrip vaak dat studenten experimenteren met de vertaling van LTL-formules naar automaten. Leerlingen profiteren van het opbouwen van intuïtie door te observeren hoe variaties in een formule de resulterende automaat beïnvloeden, met name wat betreft determinisme, staatcomplexiteit en de relatie tussen syntactische structuren en semantische klassen (bijv. de Manna & Pnueli-hiërarchie). Effectief onderwijs vereist echter toegankelijke tools die directe visualisatie, vergelijking en interactief experimenteren mogelijk maken zonder complexe installatiebarrières.

Methodologie
Dit artikel presenteert Spot, een volwassen, open-source C++/Python-bibliotheek en toolset ontworpen voor de manipulatie van LTL en $\omega$-automaten, als een pedagogisch platform. De methodologie richt zich op het benutten van de bestaande capaciteiten van Spot om "zero-install" instappunten voor onderwijs te creëren. De aanpak maakt gebruik van drie primaire interfaces:

1. Webapplicatie: Een single-page applicatie die via standaard browsers toegankelijk is (geen lokale installatie vereist) en dient als een interactieve interface voor het vertalen van formules, het bestuderen van eigenschappen en het vergelijken van logica.
2. Jupyter Notebooks: Een collectie narratief gestuurde notebooks die Python-code, inline automaat-visualisaties (gerenderd via Graphviz) en verklarende tekst combineren. Deze maken programmatische exploratie mogelijk van inclusiecontroles, tegenvoorbeelden en het herlabelen van staten.
3. Command-Line Tools: Een suite van utilities voor het genereren van willekeurige voorbeelden op basis van specifieke criteria om oefensets te creëren.

Belangrijkste Bijdragen
Het artikel beschrijft hoe de bestaande functies van Spot worden hergebruikt en gestructureerd voor educatief gebruik:

• Interactieve Visualisatie en Vertaling: De webtool stelt gebruikers in staat om LTL- of PSL-formules in te voeren en direct $\omega$-automaten te genereren met diverse acceptatievoorwaarden (Generalized Büchi, Rabin, Streett, Parity, etc.). Het ondersteunt meerdere input-syntaxes en formaten (HOA, never claims, LBTT, etc.).
• Vergelijkende Analyse en Vereenvoudiging:
  • Equivalentiecontrole: Het "compare"-tabblad stelt studenten in staat om twee formules in te voeren en onderscheidende $\omega$-woorden te ontvangen als ze niet equivalent zijn, wat de ontdekking van eenvoudigere equivalente formules vergemakkelijkt.
  • Navigatie door de Hiërarchie: Het "study"-tabblad identificeert de exacte klasse van een formule binnen de Manna & Pnueli temporele hiërarchie en de syntactische-toekomst-hiërarchie. Het benadrukt discrepanties tussen syntactische classificatie en semantische eigenschappen (bijv. het identificeren wanneer een formule syntactisch tot een hogere klasse behoort, maar een equivalent heeft in een lagere klasse).
  • Stutter Invariance: De tool detecteert stutter-invariance, een cruciale eigenschap voor partitiële orde-reductie in model checking. Indien een formule niet stutter-invariant is, levert de tool specifieke tegenvoorbeeld-woorden ($w$ en $w'$) die het falen demonstreren.
• Programmatische Exploratie: De Python API en Jupyter notebooks maken demonstraties mogelijk van geavanceerde concepten, zoals taal-inclusiecontroles met niet-deterministische Büchi-automaten en het herlabelen van deterministische automaat-staten met de LTL-formules die zij herkennen.
• Geautomatiseerde Oefeningengeneratie: De command-line tools (randltl, ltlfilt) stellen instructeurs in staat om brute-force willekeurige formules te genereren die voldoen aan specifieke restricties (bijv. formules die equivalent zijn aan $a \mathbin{U} b$ zonder de $X$-operator te gebruiken, of stutter-invariante formules die de $X$-operator bevatten).

Resultaten
Het artikel demonstreert de praktische toepassing van deze tools door middel van specifieke educatieve scenario's:

• Studenten kunnen verifiëren dat $(a \mathbin{R} (a \mathbin{U} b)) \mathbin{W} b$ equivalent is aan $a \mathbin{U} b$ door hun automaten te vergelijken of de "compare"-tab te gebruiken.
• De tool identificeert succesvol dat $a \mathbin{W} \mathbin{F}(b)$ een Obligation property is (Manna & Pneli $\Delta_1$), ondanks dat het syntactisch als $\Pi_2$ verschijnt, en bevestigt de equivalentie met $G(a) \lor \mathbin{F}(b)$.
• De command-line voorbeelden genereren succesvol lijsten met formules die aan complexe criteria voldoen, zoals het vinden van 10 formules die equivalent zijn aan $a \mathbin{U} b$ die specifieke operatoren uitsluiten, of het vinden van stutter-invariante formules die desondanks de $X$-operator bevatten.

Betekenis
Het artikel stelt dat Spot een uitgebreid, toegankelijk platform biedt voor het onderwijzen van de verbanden tussen temporele logica-formules en hun semantische automaten. Door web-gebaseerde, notebook-gebaseerde en command-line interfaces aan te bieden, sluit het aan bij diverse onderwijsomgevingen—van klaslokalen met tablets tot onderzoekers die code schrijven. De betekenis ligt in de mogelijkheid om verder te gaan dan statische theorie, waardoor studenten kunnen "experimenteren: varieer een formule, zie hoe de resulterende automaat verandert, en bouw intuïtie op." De tools worden gepresenteerd als direct bruikbare bronnen die geen installatie vereisen voor webgebruikers en vooraf geconfigureerde omgevingen bieden (via spot-sandbox) voor degenen die geen Python lokaal kunnen installeren, waardoor de drempel voor het onderwijs in formele methoden wordt verlaagd.