Teaching LTL and {\omega}-automata with Spot

Sintesi Tecnica: Insegnare LTL e $\omega$-Automata con Spot

Problematica
La Logica Temporale Lineare (LTL) e gli $\omega$-automi sono fondamentali per l'educazione ai metodi formali, in particolare nella verifica di programmi e nel model checking. Sebbene i libri di testo forniscano le basi teoriche, una comprensione profonda richiede spesso che gli studenti sperimentino la traduzione di formule LTL in automi. Gli studenti beneficiano dell'osservazione di come le variazioni di una formula influenzino l'automa risultante, costruendo intuizione riguardo al determinismo, alla complessità degli stati e alla relazione tra strutture sintattiche e classi semantiche (ad esempio, la gerarchia di Manna & Pnueli). Tuttavia, un insegnamento efficace richiede strumenti accessibili che permettano la visualizzazione immediata, il confronto e la sperimentazione interattiva senza barriere di installazione complessa.

Metodologia
Il documento presenta Spot, una matura libreria e un set di strumenti open-source in C++/Python progettati per la manipolazione di LTL e $\omega$-automi, come piattaforma pedagogica. La metodologia si concentra sullo sfruttamento delle capacità esistenti di Spot per creare punti di accesso "zero-install" per l'istruzione. L'approccio utilizza tre interfacce primarie:

1. Applicazione Web: Una single-page application accessibile tramite browser standard (senza installazione locale) che funge da interfaccia interattiva per tradurre formule, studiare proprietà e confrontare logiche.
2. Jupyter Notebooks: Una collezione di notebook narrativi che combinano codice Python, visualizzazioni di automi inline (renderizzate tramite Graphviz) e testo esplicativo. Questi permettono l'esplorazione programmatica di controlli di inclusione, controesempi e ridenominazione degli stati (relabeling).
3. Strumenti da Riga di Comando: Una suite di utilità per generare esempi casuali basati su criteri specifici per creare set di esercizi.

Contributi Chiave
Il documento dettaglia come le funzionalità esistenti di Spot siano riutilizzate e strutturate per l'uso educativo:

• Visualizzazione Interattiva e Traduzione: Lo strumento web consente agli utenti di inserire formule LTL o PSL e generare immediatamente $\omega$-automi con varie condizioni di accettazione (Büchi generalizzati, Rabin, Streett, Parity, ecc.). Supporta molteplici sintassi di input e formati (HOA, never claims, LBTT, ecc.).
• Analisi Comparativa e Semplificazione:
  • Controllo di Equivalenza: La scheda "compare" permette agli studenti di inserire due formule e ricevere parole $\omega$ che le distinguono qualora non siano equivalenti, facilitando la scoperta di formule equivalenti più semplici.
  • Navigazione nella Gerarchia: La scheda "study" identifica la classe precisa di una formula all'interno della gerarchia temporale di Manna & Pnueli e della gerarchia sintattica-futura. Evidenzia le discrepanze tra classificazione sintattica e proprietà semantiche (ad esempio, identificando quando una formula appartiene sintatticamente a una classe superiore ma possiede un equivalente in una classe inferiore).
  • Invarianza rispetto allo Stuttering: Lo strumento rileva l'invarianza rispetto allo stuttering, una proprietà critica per la riduzione del ordine parziale nel model checking. Se una formula non è invariante rispetto allo stuttering, lo strumento fornisce parole controesempio specifiche ($w$ e $w'$) che dimostrano il fallimento.
• Esplorazione Programmatica: L'API Python e i Jupyter notebooks consentono la dimostrazione di concetti avanzati, come i controlli di inclusione del linguaggio utilizzando automi di Büchi non deterministici e la ridenominazione degli stati di un automa deterministico con le formule LTL che essi riconoscono.
• Generazione Automatica di Esercizi: Gli strumenti da riga di comando (randltl, ltlfilt) permettono agli istruttori di generare per forza bruta formule casuali che soddisfano vincoli specifici (ad esempio, formule equivalenti a $a \mathbin{U} b$ senza l'operatore $X$, o formule invarianti rispetto allo stuttering che contengono $X$).

Risultati
Il documento dimostra l'applicazione pratica di questi strumenti attraverso scenari educativi specifici:

• Gli studenti possono verificare che $(a \mathbin{R} (a \mathbin{U} b)) \mathbin{W} b$ è equivalente a $a \mathbin{U} b$ confrontando i loro automi o utilizzando la scheda di confronto.
• Lo strumento identifica con successo che $a \mathbin{W} \mathbin{F}(b)$ è una proprietà di Obbligo (Manna & Pnueli $\Delta_1$) nonostante appaia sintatticamente come $\Pi_2$, e conferma la sua equivalenza a $G(a) \lor \mathbin{F}(b)$.
• Gli esempi da riga di comando generano con successo liste di formule che soddisfano criteri complessi, come trovare 10 formule equivalenti a $a \mathbin{U} b$ che escludano operatori specifici, o trovare formule invarianti rispetto allo stuttering che contengono comunque l'operatore $X$.

Significatività
Il documento sostiene che Spot fornisca una piattaforma completa e accessibile per insegnare le connessioni tra formule di logica temporale e i loro automi semantici. Offrendo interfacce basate su web, notebook e riga di comando, esso si adatta a diversi contesti educativi — dal classico in aula fino ai ricercatori che scrivono codice. La significatività risiede nella capacità di andare oltre la teoria statica, permettendo agli studenti di "sperimentare: variare una formula, vedere come cambia l'automa risultante e costruire intuizione". Gli strumenti sono presentati come risorse pronte all'uso che non richiedono installazione per gli utenti web e offrono ambienti pre-configurati (tramite spot-sandbox) per chi non è in grado di installare Python localmente, abbassando così la barriera all'ingresso per l'educazione ai metodi formali.