(PN) new bdd/idd model checking tools
A new version of DSSZMC is available.
It 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).
Main 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 and forward traversals
# support of past-tense CTL operators
# support of Petri nets with extended arcs (read arcs, inhibitor arcs,
reset arcs)
The tools are available for windows, linux and mac.
For download and further details visit
http://www-dssz.informatik.tu-cottbus.de/software/software.html
Best regards
Martin Schwarick
———————————————–
Martin Schwarick
Brandenburg University of Technology at Cottbus
Computer Science Institute
= Data Structures and Software Dependability =
Postbox 10 13 44, 03013 Cottbus, Germany
http://www-dssz.informatik.tu-cottbus.de/
ms@informatik.tu-cottbus.de
———————————————–
—-
[[ Petri Nets World: ]]
[[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/ ]]
[[ Mailing list FAQ: ]]
[[ http://www.informatik.uni-hamburg.de/TGI/PetriNets/pnml/faq.html ]]
[[ Post messages/summary of replies: ]]
[[ petrinet@informatik.uni-hamburg.de ]]