data structures and software dependability

• home

• contact

• members

• teaching

• research

• publications

• software

• events

last updated: November 29, 2010, at 11:39 AM

• General Description
• Related Papers
• Related Tools
• Case Studies
• Download

General Description

IDD-MC is an Interval Decision Diagramm (IDD) based model checker for the Computation Tree Logic (CTL) and the Continuous Stochastic Logic (CSL). It does not make use of any kind of Kronecker based techniques or any kind of Multi Terminal Decision Diagrams. The development of IDD-MC was triggered by biochemically interpreted (stochastic) Petri net models which are characterized by a high boundedness degree.

Features

• no previous knowledge of the boundedness degree required
• efficient Interval Decision Diagram engine
• static variable ordering based on the Petri net structure
• efficient saturation-based state space construction

Qualitative analysis

• dead states
• reversibility
• liveness
• CTL model checking

Quantitative analysis

• multi-threaded CSL model checking
• steady state analysis using Jacobi, Gauss-Seidel or a Pseudo-Gauss-Seidel implementation
• support for Generalized stochastic Petri nets
• evaluation of reward structures

For detailed informations concerning data structures and algorithms see the related papers.

Related Papers

• M Schwarick: IDD-MC - a model checker for bounded stochastic Petri nets; Proc. 17th German Workshop on Algorithms and Tools for Petri Nets (AWPN 2010), volume 643 of CEUR Workshop Proceedings, CEUR-WS.org, pp. 80-87, October 2010.
• M Heiner, C Rohr, M Schwarick, S Streif: A Comparative Study of Stochastic Analysis Techniques; Proc. 8th International Conference on Computational Methods in Systems Biology (CMSB 2010), Trento, September 2010, ACM digital library 2010.
• M Schwarick, A Tovchigrechko: IDD-based model validation of biochemical networks ; Theoretical Computer Sience, doi:10.1016/j.tcs.2010.06.030, Juli 2010.
• M Schwarick, M Heiner: CSL model checking of biochemical networks with Interval Decision Diagrams, Proc. 7th International Conference on Computational Methods in Systems Biology (CMSB 2009), Bologna, September 2009, Springer LNCS/LNBI 5688, pp. 296-312.
• M Schwarick: Transient analysis of stochastic Petri nets with interval decision diagrams , Proc. 15th German Workshop on Algorithms and Tools for Petri Nets (AWPN 2008), volume 380 of CEUR Workshop Proceedings, CEUR-WS.org, pp. 43-48, September 2008.
• A Tovchigrechko: Efficient symbolic analysis of bounded Petri nets using interval decision disgrams (submitted version), BTU Cottbus, Ph. D. Thesis, October 2008
• S Lehrack: A Modelling and Simulation Tool for Stochastic Petri Nets Models of Biochemical Networks (in German) , Diploma Thesis ,2007
• A Tovchigrechko: Model Checking of Bounded Petri Nets Using Interval Diagrams, BTU Cottbus, Technical Report, 2004
• J Spranger: Symbolic LTL verification of Petri nets (in German), BTU Cottbus, Ph.D. Thesis, 2001
• A Noack: A ZBDD package for efficient model checking of Petri nets (in German), BTU Cottbus, Studienarbeit, 1999

Related Tools

• modelling tools
  • Snoopy
• other CSL model checker
  • PRISM - probabilistic symbolic model checker
  • MRMC - markov reward model checker

Case Studies

to appear

Download

IDD-MC is free for non-commercial use only. We provide the binaries for mac/os (linux and windows will follow) in the hope to be useful and with expectations of feedback.

• MAC (intel 10.5+)
• Linux (to appear)
• Windows (to appear)