Spot: a platform for LTL and ω-automata manipulation

Spot is a C++17 library for LTL, ω-automata manipulation and model checking. It 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.