The Automata and Applications team develops Spot, a free and open-source platform for working with ω-automata and temporal logic formulas. Spot is primarily a C++17 library designed around the automata-theoretic approach to model checking and reactive synthesis. It comes with both command-line tools and Python bindings to make its algorithms accessible in different contexts, including interactive environments such as IPython or Jupyter.
Spot has the following notable features:
- Support for LTL (several syntaxes supported) and a subset of the linear fragment of PSL.
- Support for ω-automata with arbitrary acceptance condition.
- Support for transition-based acceptance (state-based acceptance is supported by a reduction to transition-based acceptance).
- The automaton parser can read a stream of automata written in any of four syntaxes (HOA, never claims, LBTT, DSTAR).
- Several algorithms for formula manipulation including: simplifying formulas, testing implication or equivalence, testing stutter-invariance, removing some operators by rewriting, translation to automata, testing membership to the temporal hierarchy of Manna & Pnueli…
- Several algorithms for automata manipulation including: product, emptiness checks, simulation-based reductions, minimization of weak-DBA, removal of useless SCCs, acceptance-condition transformations, determinization, SAT-based minimization of deterministic automata, Alternating Cycle Decomposition, etc.
- Support for Safety and parity games.
- Applications to reactive synthesis and model checking.
- In addition to the C++ interface, most of its algorithms are usable via command-line tools, and via Python bindings.
- One command-line tool, called ltlcross, is a rewrite of LBTT, but with support for PSL and automata with arbitrary acceptance conditions. It can be used to test tools that translate LTL into ω-automata, or benchmark them. A similar tool, autcross, checks tools that transform automata.