Spot

Library for omega automata manipulation and model checking

Spot is a library for LTL, omega-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 omega-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, etc.
• 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.