Teaching LTL and {\omega}-automata with Spot

Resumo Técnico: Ensinando LTL e $\omega$-autômatos com o Spot

Definição do Problema
A Lógica Temporal Linear (LTL) e os $\omega$-autômatos são fundamentais para o ensino de métodos formais, particularmente na verificação de programas e model checking. Embora os livros didáticos forneçam bases teóricas, a compreensão profunda muitas vezes exige que os alunos experimentem a tradução de fórmulas LTL em autômatos. Especificamente, os alunos beneficiam-se ao observar como variações em uma fórmula afetam o autômato resultante, construindo intuição sobre determinismo, complexidade de estados e a relação entre estruturas sintáticas e classes semânticas (ex: a hierarquia de Manna & Pnueli). No entanto, o ensino eficaz requer ferramentas acessíveis que permitam visualização imediata, comparação e experimentação interativa sem barreiras complexas de instalação.

Metodologia
O artigo apresenta o Spot, uma biblioteca e conjunto de ferramentas maduros em C++/Python projetados para manipulação de LTL e $\omega$-autômatos, como uma plataforma pedagógica. A metodologia foca em aproveitar as capacidades existentes do Spot para criar pontos de entrada de "instalação zero" para a educação. A abordagem utiliza três interfaces primárias:

1. Aplicação Web: Uma aplicação de página única acessível via navegadores padrão (sem necessidade de instalação local) que serve como uma interface interativa para traduzir fórmulas, estudar propriedades e comparar lógicas.
2. Jupyter Notebooks: Uma coleção de notebooks narrativos combinando código Python, visualizações de autômatos inline (renderizadas via Graphviz) e texto explicativo. Eles permitem a exploração programática de verificações de inclusão, contraexemplos e renomeação de rótulos (relabeling).
3. Ferramentas de Linha de Comando: Um conjunto de utilitários para gerar exemplos aleatórios baseados em critérios específicos para criar conjuntos de exercícios.

Principais Contribuições
O artigo detalha como os recursos existentes do Spot são reaproveitados e estruturados para uso educacional:

• Visualização Interativa e Tradução: A ferramenta web permite que os usuários insiram fórmulas LTL ou PSL e gerem imediatamente $\omega$-autômatos com várias condições de aceitação (Büchi Generalizado, Rabin, Streett, Paridade, etc.). Ela suporta múltiplas sintaxes e formatos de entrada (HOA, never claims, LBTT, etc.).
• Análise Comparativa e Simplificação:
  • Verificação de Equivalência: A aba "compare" permite que os alunos insiram duas fórmulas e recebam palavras-$\omega$ distintivas caso não sejam equivalentes, facilitando a descoberta de fórmulas equivalentes mais simples.
  • Navegação na Hierarquia: A aba "study" identifica a classe precisa de uma fórmula dentro da hierarquia temporal de Manna & Pnueli e da hierarquia sintático-futura. Ela destaca discrepâncias entre a classificação sintática e as propriedades semânticas (ex: identificando quando uma fórmula pertence sintaticamente a uma classe superior, mas possui um equivalente em uma classe inferior).
  • Invariância de Stutter: A ferramenta detecta invariância de stutter, uma propriedade crítica para redução de ordem parcial em model checking. Se uma fórmula não é invariante de stutter, a ferramenta fornece palavras de contraexemplo específicas ($w$ e $w'$) que demonstram a falha.
• Exploração Programática: A API Python e os notebooks Jupyter permitem a demonstração de conceitos avançados, como verificações de inclusão de linguagem usando autômatos de Büchi não-determinísticos e a renomeação de rótulos dos estados de autômatos determinísticos com as fórmulas LTL que eles reconhecem.
• Geração Automatizada de Exercícios: As ferramentas de linha de comando (randltl, ltlfilt) permitem que instrutores gerem, por força bruta, fórmulas aleatórias que satisfaçam critérios específicos (ex: fórmulas equivalentes a $a \mathbin{U} b$ sem usar o operador $X$, ou fórmulas invariantes de stutter que contêm o operador $X$).

Resultos
O artigo demonstra a aplicação prática dessas ferramentas através de cenários educacionais específicos:

• Alunos podem verificar que $(a \mathbin{R} (a \mathbin{U} b)) \mathbin{W} b$ é equivalente a $a \mathbin{U} b$ comparando seus autômatos ou usando a aba de comparação.
• A ferramenta identifica com sucesso que $a \mathbin{W} \mathbin{F}(b)$ é uma propriedade de Obrigação (Manna & Pnueli $\Delta_1$) apesar de parecer sintaticamente $\Pi_2$, e confirma sua equivalência a $G(a) \lor \mathbin{F}(b)$.
• Os exemplos de linha de comando geram com sucesso listas de fórmulas que atendem a critérios complexos, como encontrar 10 fórmulas equivalentes a $a \mathbin{U} b$ que excluam operadores específicos, ou encontrar fórmulas invariantes de stutter que, no entanto, contêm o operador $X$.

Significância
O artigo afirma que o Spot fornece uma plataforma abrangente e acessível para ensinar as conexões entre fórmulas de lógica temporal e seus autômatos semânticos. Ao oferecer interfaces baseadas em web, notebooks e linha de comando, ele acomoda diversos ambientes educacionais — desde salas de aula utilizando tablets até pesquisadores escrevendo código. A significância reside na capacidade de ir além da teoria estática, permitindo que os alunos "experimentem: variam uma fórmula, veem o autômato resultante mudar e constroem intuição". As ferramentas são apresentadas como recursos prontos para uso que não exigem instalação para usuários web e oferecem ambientes pré-configurados (via spot-sandbox) para aqueles que não podem instalar o Python localmente, reduzindo assim a barreira de entrada para o ensino de métodos formais.