Teaching LTL and ω-automata with Spot

Alexandre Duret-Lutz

Teaching LTL and ω-automata with Spot

Logic in Computer Science 2026-07-07 v1 Formal Languages and Automata Theory

Authors: Alexandre Duret-Lutz

Abstract

Spot is a mature, open-source C++/Python library and toolset for Linear Temporal Logic (LTL) and $\omega$ -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 $\omega$ -automata that give them their semantics.

Cite

@article{arxiv.2607.05907,
  title  = {Teaching LTL and ω-automata with Spot},
  author = {Alexandre Duret-Lutz},
  journal= {arXiv preprint arXiv:2607.05907},
  year   = {2026}
}

Comments

Demonstration for TEAL'26