23 lines
1.3 KiB
Plaintext
23 lines
1.3 KiB
Plaintext
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.
|