Teaching LTL and {\omega}-automata with Spot

Resumen Técnico: La enseñanza de LTL y $\omega$-autómatas con Spot

Planteamiento del problema
La lógica temporal lineal (LTL) y los $\omega$-autómatas son fundamentales para la educación en métodos formales, particularmente en la verificación de programas y el model checking. Aunque los libros de texto proporcionan bases teóricas, una comprensión profunda requiere que los estudiantes experimenten con la traducción de fórmulas LTL a autómatas. Específicamente, los alumnos se benefician al observar cómo las variaciones en una fórmula afectan al autómata resultante, construyendo intuición sobre el determinismo, la complejidad de estados y la relación entre las estructuras sintácticas y las clases semánticas (por ejemplo, la jerarquía de Manna & Pnueli). Sin embargo, una enseñanza eficaz requiere herramientas accesibles que permitan la visualización inmediata, la comparación y la experimentación interactiva sin barreras de instalación complejas.

Metodología
El artículo presenta Spot, una madura biblioteca y conjunto de herramientas de C++/Python diseñada para la manipulación de LTL y $\omega$-autómatas, como una plataforma pedagógica. La metodología se centra en aprovechar las capacidades existentes de Spot para crear puntos de entrada de "cero instalación" para la educación. El enfoque utiliza tres interfaces principales:

1. Aplicación Web: Una aplicación de página única accesible mediante navegadores estándar (sin necesidad de instalación local) que sirve como interfaz interactiva para traducir fórmulas, estudiar propiedades y comparar lógicas.
2. Jupyter Notebooks: Una colección de cuadernos narrativos que combinan código Python, visualizaciones de autómatas inline (renderizadas mediante Graphviz) y texto explicativo. Estos permiten la exploración programática de comprobaciones de inclusión, contraejemplos y el recetado de etiquetas (relabeling) de estados.
3. Herramientas de Línea de Comandos: Un conjunto de utilidades para generar ejemplos aleatorios basados en criterios específicos para crear conjuntos de ejercicios.

Contribuciones Clave
El artículo detalla cómo las funciones existentes de Spot se han reestructurado y adaptado para el uso educativo:

• Visualización Interactiva y Traducción: La herramienta web permite a los usuarios introducir fórmulas LTL o PSL y generar inmediatamente $\omega$-autómatas con diversas condiciones de aceptación (Büchi generalizado, Rabin, Streett, Paridad, etc.). Soporta múltiples sintaxis y formatos (HOA, never claims, LBTT, etc.).
• Análisis Comparativo y Simplificación:
  • Comprobación de Equivalencia: La pestaña "compare" permite a los estudiantes introducir dos fórmulas y recibir palabras $\omega$ que las distingan si no son equivalentes, facilitando el descubrimiento de fórmulas equivalentes más simples.
  • Navegación por la Jerarquía: La pestaña "study" identifica la clase precisa de una fórmula dentro de la jerarquía temporal de Manna & Pnueli y la jerarquía sintáctica-futura. Resalta las discrepancias entre la clasificación sintáctica y las propiedades semánticas (por ejemplo, identificando cuándo una fórmula pertenece sintácticamente a una clase superior pero tiene un equivalente en una clase inferior).
  • Invarianza ante el Stutter (Stutter Invariance): La herramienta detecta la invarianza ante el stutter, una propiedad crítica para la reducción de orden parcial en el model checking. Si una fórmula no es invariante ante el stutter, la herramienta proporciona palabras contraejemplo específicas ($w$ y $w'$) que demuestran el fallo.
• Exploración Programática: La API de Python y los cuadernos de Jupyter permiten la demostración de conceptos avanzados, tales como comprobaciones de inclusión de lenguaje utilizando autómatas de Büchi no deterministas y el recetado de etiquetas de los estados de un autómata determinista con las fórmulas LTL que reconocen.
• Generación Automatizada de Ejercicios: Las herramientas de línea de comandos (randltl, ltlfilt) permiten a los instructores generar por fuerza bruta fórmulas aleatorias que satisfagan restricciones específicas (por ejemplo, fórmulas equivalentes a $a \mathbin{U} b$ sin usar el operador $X$, o fórmulas invariantes ante el stutter que contengan $X$).

Resultados
El artículo demuestra la aplicación práctica de estas herramientas a través de escenarios educativos específicos:

• Los estudiantes pueden verificar que $(a \mathbin{R} (a \mathbin{U} b)) \mathbin{W} b$ es equivalente a $a \mathbin{U} b$ comparando sus autómatas o utilizando la pestaña de comparación.
• La herramienta identifica con éxito que $a \mathbin{W} \mathbin{F}(b)$ es una propiedad de Obligación (Manna & Pnueli $\Delta_1$) a pesar de aparecer sintácticamente como $\Pi_2$, y confirma su equivalencia a $G(a) \lor \mathbin{F}(b)$.
• Los ejemplos de línea de comandos generan con éxito listas de fórmulas que cumplen criterios complejos, como encontrar 10 fórmulas equivalentes a $a \mathbin{U} b$ que excluyan operadores específicos, o encontrar fórmulas invariantes ante el stutter que, no obstante, contienen el operador $X$.

Significancia
El artículo sostiene que Spot proporciona una plataforma integral y accesible para la enseñanza de las conexiones entre las fórmulas de lógica temporal y sus autómatas semánticos. Al ofrecer interfaces basadas en la web, en cuadernos y en la línea de comandos, acomoda diversos entornos educativos, desde aulas que utilizan tabletas hasta investigadores que escriben código. La significancia radica en la capacidad de ir más allá de la teoría estática, permitiendo a los estudiantes "experimentar: variar una fórmula, ver cómo cambia el autómata resultante y construir intuición". Las herramientas se presentan como recursos listos para usar que no requieren instalación para los usuarios web y ofrecen entornos preconfigurados (vía spot-sandbox) para aquellos que no pueden instalar Python localmente, reduciendo así la barrera de entrada para la educación en métodos formales.