Bild mit Unilogo
homeicon university sucheicon search siteicon sitemap kontakticon contact impressicon legal notice
unilogo University of Stuttgart 
SZS | Contact | People | Teaching | Research | Publications | Tools | Institute | Department | Links
Institute of Formal Methods in Computer Science

QQ - An LTL Model-Checker for Petri Nets
 

Overview

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 Model-Checking Kit.

Installation

  1. Download the source code and unpack the archive.
  2. Typing make should suffice to compile the checker.
  3. The model-checker makes use of the Spin tool to convert LTL formulas into Büchi automata.
    The spin executable needs to be in some directory that is listed in your PATH variable.
  4. You can get a list of command-line options by calling qq without any arguments.

Contact

Questions can be directed to Frank Wallner or Stefan Schwoon.

Changes

  • 19.03.2001: Initial release of the tool.
  • 27.11.2003: Tool page moved to Stuttgart.

 
last change 02.12.2003 (mailto ss) |  © University of Stuttgart | legal notice