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

Index:

general description
related papers
case studies
download
usage
related software
contact

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.

Features

• no previous knowledge of the boundedness degree required
• efficient saturation-based state space construction inherited from DSSZ-MC
• efficient multi-threaded CSL model checking
• steady state analysis

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

• mitogen-activated protein kinase kaskade (MAPK):
  

  [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.

D o w n l o a d

• linux32
• linux64
• windows in preparation
• mac/os in preparation
• benchmarks

U s a g e

• netfile

  must be a valid model description in the APNN format
• Currently ordinary stochastic Petri nets are supported only.
• The creation of suitable APNN files can be done by help of our tool Snoopy.
• IDD-CSL supports three kind of rate functions which can be defined within Snoopy's stochastic Petri net class:
• biomass action
• biolevel interpretation
• arbitrary arithmetic functions
  

• cslfile

  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

  • -q natural_number

    initial marking will be multiplied with the given value (to define comfortable different levels)

  • -m real_number

    specify the mass constant when using biolevel interpretation semantics

  • -l natural_number

    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

  • -t natural_number

    specify the nummer of threads performing concurrently one matrix-vector multiplication

  • -V

    if set, result vectors will be printed

• rate functions
  
  1. biomass action semantics (tokens represent molecules)
     h_t=c_t \prod_{p\in ^\bullet t} m(p)
     example: levchenko_bma.apnn
  2. biolevel interpretaion semantics ( tokens represent a level of concentration)
     h_t=(c_m)^{^\bullet t-1}\cdot c_t\cdot N \prod_{p\in ^\bullet t} \frac{m(p)}{N} = c_t \cdot (\frac{c_m}{N})^{(|^\bullet t|-1)} \prod_{p\in ^\bullet t} m(p)
     example: levchenko_bli.apnn
     
  3. arithmetic functions
     can contain the operators +,-,*,/ and all pre-places of the related transition
     levchenkoN4_bli_exp.apnn
     
  • ^\bullet t denotes the set of pre-places of transition t
  • m(p) is the number of tokens on place p
  • N is the number of the highest level and corresponds to the boundedness degree of the net
  • c_m is the mass constant and must be defined either in the APNN file with a singe entry \\mass{c_m} or with the option -m
  • The quotient \frac{c_m}{N},which is called the scaling factor, will be computed after the state space generation automatically
  
  For further details see [2].
  
• an example call:
  iddcsl -t2 -l11 levchenko_bma.apnn F[1-1]RafP2.csl

 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 

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

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