CSL Model Checking of Biochemical Networks with Interval Decision Diagrams

  • Martin Schwarick
  • Monika Heiner
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5688)


This paper presents an Interval Decision Diagram based approach to symbolic CSL model checking of Continuous Time Markov Chains which are derived from stochastic Petri nets. Matrix-vector and vector-matrix multiplication are the major tasks of exact analysis. We introduce a simple, but powerful algorithm which uses explicitly the Petri net structure and allows for parallelisation. We present results demonstrating the efficiency of our first prototype implementation when applied to biochemical network models, specifically with increasing token numbers. Our tool currently supports CSL model checking of time-bounded operators and the Next operator for ordinary stochastic Petri nets.


Model Check Rate Matrix Cache Data Continuous Time Markov Chain Biochemical Network 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [ASSB00]
    Aziz, A., Sanwal, K., Singhal, V., Brayton, R.: Model checking continuous time Markov chains. ACM Trans. on Computational Logic 1(1) (2000)Google Scholar
  2. [BHHK00]
    Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P.: Model checking Contiuous-Time Markov Chains by transient Analysis. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 358–372. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  3. [BL00]
    Barkai, N., Leibler, S.: Biological rhythms: Circadian clocks limited by noise. Nature 403, 267–268 (2000)PubMedGoogle Scholar
  4. [CDDS06]
    Cerotti, D., D’Aprile, D., Donatelli, S., Sproston, J.: Verifying stochastic well-formed nets with CSL model checking tools. In: Proc. ACSD 2006, pp. 143–152. IEEE Computer Society, Los Alamitos (2006)Google Scholar
  5. [CJMS06]
    Ciardo, G., Jones III, R.L., Miner, A.S., Siminiceanu, R.I.: Logic and stochastic modeling with smart. Perform. Eval. 63(6), 578–608 (2006)CrossRefGoogle Scholar
  6. [CSK+03]
    Cho, K.-H., Shin, S.-Y., Kim, H.-W., Wolkenhauer, O., McFerran, B., Kolch, W.: Mathematical modeling of the influence of RKIP on the ERK signaling pathway. In: Priami, C. (ed.) CMSB 2003. LNCS, vol. 2602, pp. 127–141. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  7. [CVOG05]
    Calder, M., Vyshemirsky, V., Orton, R., Gilbert, D.: Analysis of Signalling Pathways using the PRISM model checker. In: Proc. CMSB 2005, pp. 179–190. LFCS, Univ. of Edinburgh (2005)Google Scholar
  8. [GH06]
    Gilbert, D., Heiner, M.: From Petri nets to differential equations - an integrative approach for biochemical network analysis. In: Donatelli, S., Thiagarajan, P.S. (eds.) ICATPN 2006. LNCS, vol. 4024, pp. 181–200. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  9. [GHL07]
    Gilbert, D., Heiner, M., Lehrack, S.: A unifying framework for modelling and analysing biochemical pathways using Petri nets. In: Calder, M., Gilmore, S. (eds.) CMSB 2007. LNCS (LNBI), vol. 4695, pp. 200–216. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  10. [HDG10]
    Heiner, M., Donaldson, R., Gilbert, D.: Petri Nets for Systems Biology. In: Iyengar, M.S. (ed.) Symbolic Systems Biology: Theory and Methods, Jones and Bartlett Publishers, Inc. (in press, 2010)Google Scholar
  11. [HGD08]
    Heiner, M., Gilbert, D., Donaldson, R.: Petri nets for systems and synthetic biology. In: Bernardo, M., Degano, P., Zavattaro, G. (eds.) SFM 2008. LNCS, vol. 5016, pp. 215–264. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  12. [HRS08]
    Heiner, M., Richter, R., Schwarick, M.: Snoopy - a tool to design and animate/simulate graph-based formalisms. In: Proc. PNTAP 2008, associated to SIMUTools 2008. ACM digital library, New York (2008)Google Scholar
  13. [HST09]
    Heiner, M., Schwarick, M., Tovchigrechko, A.: DSSZ-MC - A Tool for Symbolic Analysis of Extended Petri Nets. In: Franceschinis, G., Wolf, K. (eds.) Petri Nets 2009. LNCS, vol. 5606, pp. 323–332. Springer, Heidelberg (2009)Google Scholar
  14. [JKO+08]
    Jansen, D.N., Katoen, J.-P., Oldenkamp, M., Stoelinga, M., Zapreev, I.: How fast and fat is your probabilistic model checker? In: Yorav, K. (ed.) HVC 2007. LNCS, vol. 4899, pp. 69–85. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  15. [KNP08]
    Kwiatkowska, M., Norman, G., Parker, D.: Using probabilistic model checking in systems biology. ACM SIGMETRICS Performance Evaluation Review 35(4), 14–21 (2008)CrossRefGoogle Scholar
  16. [LBS00]
    Levchenko, A., Bruck, J., Sternberg, P.W.: Scaffold proteins may biphasically affect the levels of mitogen-activated protein kinase signaling and reduce its threshold properties. Proc. Natl. Acad. Sci. USA 97(11), 5818–5823 (2000)CrossRefPubMedPubMedCentralGoogle Scholar
  17. [MC99]
    Miner, A.S., Ciardo, G.: Efficient Reachability Set Generation and Storage Using Decision Diagrams. In: Donatelli, S., Kleijn, J. (eds.) ICATPN 1999. LNCS, vol. 1639, pp. 6–25. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  18. [Noa99]
    Noack, A.: A ZBDD Package for Efficient Model Checking of Petri Nets (in German). Technical report, BTU Cottbus, Dep. of CS (1999)Google Scholar
  19. [Par02]
    Parker, D.: Implementation of Symbolic Model Checking for Probabilistic Systems. PhD thesis, University of Birmingham (2002)Google Scholar
  20. [PCS07]
    Peccoud, J., Courtney, T., Sanders, W.H.: Möbius: an integrated discrete-event modeling environment. Bioinformatics 23(24), 3412–3414 (2007)CrossRefPubMedGoogle Scholar
  21. [PNK06]
    Parker, D., Norman, G., Kwiatkowska, M.: PRISM 3.0.beta1 Users’ Guide (2006)Google Scholar
  22. [Sno08]
    Snoopy Website. A Tool to Design and Animate/Simulate Graphs. BTU Cottbus (2008),
  23. [Ste94]
    Stewart, W.J.: Introduction to the Numerical Solution of Markov Chains. Princeton Univ. Press, Princeton (1994)Google Scholar
  24. [Tov08]
    Tovchigrechko, A.: Model Checking Using Interval Decision Diagrams. PhD thesis, BTU Cottbus, Dep. of CS (2008)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Martin Schwarick
    • 1
  • Monika Heiner
    • 1
  1. 1.Department of Computer ScienceBrandenburg University of TechnologyCottbusGermany

Personalised recommendations