general description
related papers
case studies
download
usage
related software
contact
IDD-CSL is a prototype implementation for an Interval Decision Diagramm (IDD) based model checker for 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-CSL was triggered by biochomically interpreted stochastic Petri net models (See case studies) which are characterized by a high boundedness degree.
At the current stage of development IDD-CSL is just a proof of concept which
supports only the timed operators F,G,U and the X-operator. Furthermore it offers steady state analysis using the Jacobi method.
[1] M. Schwarick: Transient analysis of stochastic Petri nets with interval decision diagrams , AWPN Workshop, 2008
[2] S. Lehrack: A Modelling and Simulation Tool for Stochastic Petri Nets Models of Biochemical Networks (in German) , Diploma Thesis ,2007
[3] F. Bause; P. Kemper; P. Kritzinger: Abstract Petri Net Notation , 1994
[4] A. Noack: A ZBDD package for efficient model checking of Petri nets (in German), BTU Cottbus, Studienarbeit, 1999
[5] J. Spranger: Symbolic LTL verification of Petri nets (in German), BTU Cottbus, Ph.D. Thesis, 2001
[6] A. Tovchigrechko: Model Checking of Bounded Petri Nets Using Interval Diagrams, BTU Cottbus, Technical Report, 2004
[7] A. Tovchigrechko: Efficient symbolic analysis of bounded Petri nets using interval decision disgrams (submitted version), BTU Cottbus, Ph. D. Thesis, October 2008
[8] 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.
[9] M. Heiner; D. Gilbert; R Donaldson:
Petri Nets for
Systems and Synthetic Biology;
Springer LNCS 5016, pp. 215-264, 2008.
IDD-CSL is free for non-commercial use only. We provide the binaries for linux (windows and mac/os will follow) in the hope to be useful and with expectations of feedback.
netfile
must be a valid model description in the APNN formatcslfile
must be a file containing a csl formula conform to this CSL-grammar-j ilfile
steady state analysis using the Jacobi method
ilfile must be a file containing an interval logic expression conform to this IL-grammar
the various model checker's options
initial marking will be multiplied with the given value (to define comfortable different levels)
specify the mass constant when using biolevel interpretation semantics
specify the cache layer
the root level is 0, the terminal nodes are on layer |P|, where P is the set of places in the stochastic Petri net
valid cache layers are between 0 and |P-1|
default is |P|/2 - |P|/10
specify the nummer of threads performing concurrently one matrix-vector multiplication
if set, result vectors will be printed
ms(at)informatik(dot)tu-cottbus(dot)de