D S S Z  - C S L  M O D E L   C H E C K E R  home page

latest update: March 26, 2009


general description
related papers
case studies
related software

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

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.


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

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

[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

C a s e   S t u d i e s

D o w n l o a d

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.

U s a g e

IDD-CSL is a command line tool. If the binary folder is in your PATH type:

iddcsl [options] [-j ilfile] netfile [cslfile]

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

 C o n t a c t 


. . .  t h e  e n d  . . .