D S S Z M O D E L C H E C K I NG T O O L S home page

latest update: Jun 19, 2008

Index:

general description
related papers
case studies
download
related software
contact

G e n e r a l D e s c r i p t i o n

DSSZ-MC contains tools for the symbolic analysis of bounded Petri nets for standard properties and CTL model checking. They are based on an efficient implementation of Zero-suppressed Binary Decision Diagrams (zbdd-mc) and Interval Decision Diagrams (idd-mc).

Features

no previous knowledge of the boundedness degree required (idd-mc)
efficient saturation-based reachability analysis
dead state analysis with trace generation
analysis of strongly connected components (liveness, reversibility)
efficient CTL model checking based on limited backward reachability analysis
support of Petri nets with extended arcs (read arcs, inhibitor arcs, reset arcs)

In Preparation

specification of sets of inital states by means of interval logic expressions
the option --initial-file in the current release is just a dummy
efficient CTL model checking based on forward traversals
support of past-tense CTL operators

For detailed informations concerning data structures and algorithms see the related papers. The tools read Petri nets in the Abstract Petri Net Notation (APNN) only.

R e l a t e d P a p e r s

[1] F. Bause; P. Kemper; P. Kritzinger: Abstract Petri Net Notation , 1994

[2] A. Noack: A ZBDD package for efficient model checking of Petri nets (in German), BTU Cottbus, Studienarbeit, 1999

[3] J. Spranger: Symbolic LTL verification of Petri nets (in German), BTU Cottbus, Ph.D. Thesis, 2001

[4] A. Tovchigrechko: Model Checking of Bounded Petri Nets Using Interval Diagrams, BTU Cottbus, Technical Report, 2004

[5] A. Tovchigrechko: Efficient symbolic analysis of bounded Petri nets using interval decision disgrams (submitted version), BTU Cottbus, Ph. D. Thesis, October 2008

C a s e S t u d i e s

mitogen-activated protein kinase kaskade (MAPK)
D Gilbert, M Heiner, S Lehrack:
A Unifying Framework for Modelling and Analysing Biochemical Pathways Using Petri Nets.
Springer LNCS/LNBI 4695, pp. 200-216, 2007.
M Heiner, D Gilbert, R Donaldson:
Petri Nets for Systems and Synthetic Biology;
Springer LNCS 5016, pp. 215-264, 2008.

D o w n l o a d

DSSZ-MC is free for non-commercial use only. We provide the binaries for windows, mac and linux in the hope to be useful and with expectations of feedback.

windows
mac
linux 32bit
linux 64bit
Graphical User Interface written in Java.
- Extract the file dsszmc_gui.tgz by typing tar -xzvf dsszmc_gui.tgz and change to the directory dsszmc_gui. The subdirectory modelchecker contains the binaries for all supported platforms
- After starting the GUI by typing java -jar gui_gen_v1.jar a tool description (e.g. modelchecker/linux32/iddmc_linux.xml)must be loaded.
- When the needed options have been specified, the tool can be started by pushing the "Execute Command" button.
examples

former verions of our BDD based model checkers

R e l a t e d S o f t w a r e

Snoopy - our hierarchical Petri net editor. It can be used to create the Petri net models in the APNN format.
Charlie - our Petri net analysator is going to provide a gui interface to set all the various model checkers' options, upcoming soon.

C o n t a c t

dsszmc(at)informatik(dot)tu-cottbus(dot)de