1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
|
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.
|
