QQ can check LTL properties of safe, deadlock-free Petri nets.
The tool was created by Frank Wallner. The tool can also be used
to synchronise a Petri net with a Büchi automaton.
QQ is one of the checkers supported by the
- Download the source code and unpack the archive.
make should suffice to compile the checker.
- The model-checker makes use of the
tool to convert LTL formulas into Büchi automata.
executable needs to be in some directory that is listed in your
- You can get a list of command-line options by calling
without any arguments.
Questions can be directed to
or Stefan Schwoon.
- 19.03.2001: Initial release of the tool.
- 27.11.2003: Tool page moved to Stuttgart.