×

zbMATH — the first resource for mathematics

IDD-based model validation of biochemical networks. (English) Zbl 1216.68197
Summary: This paper presents efficient techniques for the qualitative and quantitative analysis of biochemical networks, which are modeled by means of qualitative and stochastic Petri nets, respectively. The analysis includes standard Petri net properties as well as model checking of the computation tree logic and the continuous stochastic logic. Efficiency is achieved by using interval decision diagrams to alleviate the well-known problem of state space explosion, and by applying operations exploiting the Petri structure and the principle of locality. All presented techniques are implemented in our tool IDD-MC which is available on our website.
MSC:
68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
03B44 Temporal logic
68Q60 Specification and verification (program logics, model checking, etc.)
92C42 Systems biology, networks
Software:
SMART_; DSSZ-MC; SNOOPY; ZBDD
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Baier, C.; Haverkort, B.; Hermanns, H.; Katoen, J.-P., Model checking continuous-time Markov chains by transient analysis, (), 358-372 · Zbl 0974.68017
[2] Baldan, P.; Cocco, N.; Marin, A.; Simeoni, M., Petri nets for modelling metabolic pathways: a survey, J. natural comput., (2010) · Zbl 1206.68209
[3] Brace, K.S.; Rudell, R.L.; Bryant, R.E., Efficient implementation of a BDD package, (), 40-45
[4] Bryant, R.E., Graph-based algorithms for Boolean function manipulation, IEEE transactions on computers, C-35, 8, 677-691, (1986) · Zbl 0593.94022
[5] Burch, J.; Clarke, B.; Mcmillan, K.; Dill, D.; Hwang, L., Symbolic model checking: 10^{20} states and beyond, (), 1-33 · Zbl 0753.68066
[6] Calder, M.; Vyshemirsky, V.; Orton, R.; Gilbert, D., Analysis of signalling pathways using the PRISM model checker, (), 179-190
[7] Cerotti, D.; D’Aprile, D.; Donatelli, S.; Sproston, J., Verifying stochastic well-formed nets with CSL model checking tools, (), 143-152
[8] 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, (), 127-141 · Zbl 1112.92315
[9] G. Ciardo, R.L. Jones, A.S. Miner, R.I. Siminiceanu, SMART: stochastic model analyzer for reliability and timing, in: Tools of Aachen 2001, International MultiConference on Measurement, Modelling and Evaluation of Computer-Communication Systems, 2001, pp. 29-34.
[10] Clarke, E.M.; Emerson, E.A.; Sistla, A.P., Automatic verification of finite state concurrent systems using temporal logic specifications, ACM trans. program. lang. syst., 8, 2, 244-263, (1986) · Zbl 0591.68027
[11] Clarke, E.M.; Grumberg, O.; Peled, D., Model checking, (2001), MIT Press
[12] Couvreur, J.-M.; Encrenaz, E.; Paviot-Adet, E.; Poitrenaud, D.; Wacrenier, P.-A., Data decision diagrams for Petri net analysis, (), 1-101 · Zbl 1047.68555
[13] Fujita, M.; McGeer, P.C.; Yang, J.C.-Y., Multi-terminal binary decision diagrams: an efficient datastructure for matrix representation, Form. methods syst. des., 10, 2-3, 149-169, (1997)
[14] Gilbert, D.; Heiner, M., From Petri nets to differential equations — an integrative approach for biochemical network analysis, (), 181-200 · Zbl 1234.68298
[15] D. Gilbert, M. Heiner, S. Lehrack, A unifying framework for modelling and analysing biochemical pathways using Petri nets. TR I-02, CS Dep., BTU Cottbus, 2007.
[16] Gilbert, D.; Heiner, M.; Lehrack, S., A unifying framework for modelling and analysing biochemical pathways using Petri nets, (), 200-216
[17] Heath, J.; Kwiatkowska, M.; Norman, G.; Parker, D.; Tymchyshyn, O., Probabilistic model checking of complex biological pathways, (), 32-47
[18] Heiner, M.; Gilbert, D.; Donaldson, R., Petri nets in systems and synthetic biology, (), 215-264
[19] Heiner, M.; Richter, R.; Schwarick, M., Snoopy — a tool to design and animate/simulate graph-based formalisms, ()
[20] Heiner, M.; Schwarick, M.; Tovchigrechko, A., DSSZ-MC — a tool for symbolic analysis of extended Petri nets, (), 323-332
[21] Huang, C.; Ferrell, J., Ultrasensitivity in the mitogen-activated protein kinase cascade, Proc. natl. acad. sci., 93, 10078-10083, (1996)
[22] T. Kam, State Minimization of Finite State Machines Using Implicit Techniques. Ph.D. Thesis, University of California at Berkeley, 1995.
[23] K. Lautenbach, H. Ridder, A completion of the S-invariance technique by means of fixed point algorithms. Technical Report 10-95, Universität Koblenz-Landau, 1995.
[24] 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)
[25] Manna, Z.; Pnueli, A., The temporal logic of reactive and concurrent systems — specification, (1992), Springer
[26] Minato, S., Zero-suppressed BDDs for set manipulation in combinatorial problems, (), 272-277
[27] Miner, A.S.; Ciardo, G., Efficient reachability set generation and storage using decision diagrams, (), 6-25
[28] J. Møller, J. Lichtenberg, Difference decision diagrams, Master’s thesis, Department of Information Technology, Technical University of Denmark, Building 344, DK-2800 Lyngby, Denmark, 1998.
[29] A. Noack, A ZBDD package for efficient model checking of Petri nets. Technical report, BTU Cottbus, Dep. of CS, 1999 (in German).
[30] D. Parker, Implementation of symbolic model checking for probabilistic systems. Ph.D. Thesis, University of Birmingham, 2002.
[31] D. Parker, G. Norman, M. Kwiatkowska, PRISM 3.0.beta1 Users’ Guide, 2006.
[32] Priese, L.; Wimmel, H., Theoretical informatics — Petri nets, (2003), Springer, (in German) · Zbl 1137.68452
[33] H. Ridder, Analysis of Petri net models with decision diagrams. Ph.D. Thesis, Universität Koblenz-Landau, 1997 (in German).
[34] Rohr, C.; Marwan, W.; Heiner, M., Snoopy — a unifying Petri net framework to investigate biomolecular networks, Bioinformatics, 26, 7, 974-975, (2010)
[35] Schwarick, M., Transient analysis of stochastic Petri nets with interval decision diagrams, (), 43-48
[36] Schwarick, M.; Heiner, M., CSL model checking of biochemical networks with interval decision diagrams, (), 296-312
[37] Snoopy Website. A tool to design and animate/simulate graphs. BTU Cottbus. http://www-dssz.informatik.tu-cottbus.de/software/snoopy.html, 2008.
[38] Stewart, W.J., Introduction to the numerical solution of Markov chains, (1994), Princeton University Press · Zbl 0821.65099
[39] K. Strehl, L. Thiele, Symbolic model checking using interval diagram techniques. Technical report, Computer Engineering and Networks Lab (TIK), Swiss Federal Institute of Technology (ETH) Zurich, 1998.
[40] Tarjan, R., Depth-first search and linear graph algorithms, SIAM J. comput., 1, 2, 146-160, (1972) · Zbl 0251.05107
[41] A. Tovchigrechko, Model checking using interval decision diagrams. Ph.D. Thesis, BTU Cottbus, Dep. of CS, 2008.
[42] Xie, A.; Beerel, P.A., Efficient state classification of finite state Markov chains, (), 605-610
[43] Yoneda, T.; Hatori, H.; Takahara, A.; Minato, S., (), 435-449
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.