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.

Official link

https://spot.lre.epita.fr/