Teaching LTL and ω-automata with Spot

Abstract

Spot is a mature, open-source C++/Python library and toolset for Linear Temporal Logic (LTL) and $\ddot{I}‰$-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 \emph{teaching} the connections between temporal logic formulas and the $\ddot{I}‰$-automata that give them their semantics.

Demonstration for TEAL'26