Teaching LTL and ω-Automata with Spot

Jul 16, 2026

Upload by Miles

Spot is an open-source C++/Python library for working with Linear Temporal Logic (LTL) and ω-automata, used as a research and verification backend. Its visualization and Python interface support instruction on how temporal logic formulas map to ω-automata semantics. The demo provides two zero-install entry points: a web app for entering LTL/PSL formulas, visualizing automata, exploring simplifications, and checking equivalence/implication, and Jupyter notebooks for interactive experimentation and assignment creation. Spot command-line tools can generate random exercises.

LanguageEnglish

CategoryTechnology

FormatPDF

Pages8

Reading Time20 min

LTL and Spot

Spot in a nutshell

The Online LTL Toolset

Web application overview

Classroom activities

arXiv :2607 .05907v 1 [ cs .LO] 7 Jul 2026 Teaching LTL and ω-Automata with Spot Alexandre Duret-Lutz \# EPITA Research Laboratory (LRE), Paris, France ~~ Abstract ~~ Spot is a mature, open-source C++/Python library and toolset for Linear Temporal Logic (LTL) and ω-automata manipulation. While Spot is routinely used as a research and verification back-end, its rich visualization capabilities and Python interface also make it an attractive platform for teaching the connections between temporal logic formulas and the ω-automata that give them their semantics. This demonstration showcases two complementary, zero-install entry points into Spot that are suitable for educational settings: 1. a web application that lets students type LTL or PSL formulas and immediately see the resulting automaton, explore formula simplifications, compare formula equivalence/implication, and navigate Manna & Pnueli’s temporal hierarchy. 2. Jupyter notebooks that combine narrative explanations, live Python code, and inline automaton drawings, enabling students to experiment interactively and instructors to build assignments around concrete, executable examples. Additionally, we can discuss the use of the command-line tools of Spot to generate random examples suitable for preparing a series of exercises. 2012 ACM Subject Classification Theory of computation → Logic and verification; Theory of computation → Formal languages and automata theory; Applied computing → Education Keywords and phrases linear temporal logic, ω-automata, interactive tool, Jupyter notebooks, education Digital Object Identifier 10.4230/LIPIcs... Category Demo Supplementary Material Online tool: [https://spot.lre.epita.fr/app/](https://spot.lre.epita.fr/app/) Interactive notebooks: [https://spot.lre.epita.fr/tut.html](https://spot.lre.epita.fr/tut.html) Source code: [https://gitlab.lre.epita.fr/spot/spot](https://gitlab.lre.epita.fr/spot/spot) 1 LTL and Spot Linear Temporal Logic (LTL) [18] and ω-automata are cornerstones of formal methods education. LTL appears in virtually every graduate course on program verification, and the translation of an LTL formula into a Büchi automaton is an important step to better understand the logic and its many applications, like model checking [19] or reactive synthesis [17] . Several textbooks present the theoretical foundations [e.g. 5, 6], but understanding deepens considerably when students can experiment: vary a formula, see the resulting automaton change, and build intuition about which formulas yield small deterministic automata and which do not. Spot in a nutshell. Spot [8, 9] is an open-source library (GPL v3) for the manipulation of LTL formulas and ω-automata. It supports: LTL and a subset of PSL [1], with multiple input syntaxes; ω-automata with arbitrary (Emerson–Lei) acceptance conditions, in five standard formats (HOA [4], never claims, LBTT, DSTAR, PGsolver); a comprehensive set of formula and automaton algorithms: simplification, equivalence and implication testing, checking stutter-invariance [16], translation to automata (generalized Büchi, Rabin, Streett, parity, . . . ), simulation-based reduction [3] and SAT-based minimization [2], and more. recent support for LTLf (LTL over finite traces) and DFA represented using multi-terminal binary decision diagrams [10] . © Alexandre Duret-Lutz; licensed under Creative Commons License CC-BY 4.0 Leibniz International Proceedings in Informatics Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl Publishing, Germany XX:2 Teaching LTL and ω-Automata with Spot Figure 1 Spot’s online LTL toolset [9] . Beyond the C++ library, Spot exposes all algorithms through command-line tools and Python bindings, and generates automaton pictures rendered via Graphviz. 2 The Online LTL Toolset Spot’s online LTL toolset, available at [https://spot.lre.epita.fr/app/](https://spot.lre.epita.fr/app/), is a single-page web application that

FAQs

What teaching resources does Spot provide for learning LTL and ω-automata?

Spot offers two zero-install entry points: a web application where students type LTL/PSL formulas and immediately see the resulting ω-automaton, and Jupyter notebooks that combine narrative explanations, executable Python code, and inline automaton drawings.

What can students do in the Spot online LTL toolset?

Students can translate formulas into ω-automata with different acceptance conditions, inspect formula characteristics, compare two formulas and obtain distinguishing ω-words when they exist, and simplify formulas using the dedicated simplification tab.

How can Spot support assignments and exercise preparation for instructors?

Instructors can use the Jupyter notebooks to build interactive assignments with concrete examples, and can use Spot’s command-line tools to generate random examples suitable for preparing a sequence of exercises.

Jul 16, 2026

Upload by Miles