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 |
References:
| [1] | Baier, C.; Haverkort, B.; Hermanns, H.; Katoen, J.-P., Model checking continuous-time Markov chains by transient analysis, (Proc. CAV 2000. Proc. CAV 2000, LNCS, vol. 1855 (2000), Springer), 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, (Proceedings of the 27th ACM/IEEE Design Automation Conference. Proceedings of the 27th ACM/IEEE Design Automation Conference, ACM/IEEE (1990), IEEE Computer Society Press), 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, (Proceedings of the 5th Annual IEEE Symposium on Logic in Computer Science (1990), IEEE Computer Society Press), 1-33 · Zbl 0753.68066 |
| [6] | Calder, M.; Vyshemirsky, V.; Orton, R.; Gilbert, D., Analysis of signalling pathways using the PRISM model checker, (Proc. CMSB 2005. Proc. CMSB 2005, LFCS (2005), University of Edinburgh), 179-190 |
| [7] | Cerotti, D.; D’Aprile, D.; Donatelli, S.; Sproston, J., Verifying stochastic well-formed nets with CSL model checking tools, (Proc. ACSD 2006 (2006), IEEE Computer Society), 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, (CMSB 2003. CMSB 2003, LNCS, vol. 2602 (2003), Springer), 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.; 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, (Proceedings of the 23rd International Conference on Applications and Theory of Petri Nets. Proceedings of the 23rd International Conference on Applications and Theory of Petri Nets, LNCS, vol. 2360 (2002), Springer), 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, (Proc. ICATPN 2006. Proc. ICATPN 2006, LNCS, vol. 4024 (2006), Springer), 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.; 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, (Proc. CMSB 2007. Proc. CMSB 2007, LNCS/LNBI, vol. 4695 (2007), Springer), 200-216 |
| [17] | Heath, J.; Kwiatkowska, M.; Norman, G.; Parker, D.; Tymchyshyn, O., Probabilistic model checking of complex biological pathways, (Proc. CMSB 2006. Proc. CMSB 2006, LNBI, vol. 4210 (2006), Springer), 32-47 |
| [18] | Heiner, M.; Gilbert, D.; Donaldson, R., Petri nets in systems and synthetic biology, (SFM. SFM, LNCS, vol. 5016 (2008), Springer), 215-264 |
| [19] | Heiner, M.; Richter, R.; Schwarick, M., Snoopy — a tool to design and animate/simulate graph-based formalisms, (Proc. PNTAP 2008, Associated to SIMUTools 2008 (2008), ACM Digital Library) |
| [20] | Heiner, M.; Schwarick, M.; Tovchigrechko, A., DSSZ-MC — a tool for symbolic analysis of extended Petri nets, (Proc. Petri Nets 2009. Proc. Petri Nets 2009, LNCS, vol. 5606 (2009), Springer), 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.; 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.; 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, (Proceedings of the 30th ACM/IEEE Design Automation Conference (1993), ACM Press), 272-277 |
| [27] | Miner, A. S.; Ciardo, G., Efficient reachability set generation and storage using decision diagrams, (Proceedings of the 20th International Conference on Application and Theory of Petri Nets. Proceedings of the 20th International Conference on Application and Theory of Petri Nets, LNCS, vol. 1639 (1999), Springer), 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.; 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).; 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.; 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.; 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).; 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, (Proc. 15th German Workshop on Algorithms and Tools for Petri Nets, AWPN 2008. Proc. 15th German Workshop on Algorithms and Tools for Petri Nets, AWPN 2008, CEUR Workshop Proceedings, vol. 380 (September 2008), CEUR-WS.org), 43-48 |
| [36] | Schwarick, M.; Heiner, M., CSL model checking of biochemical networks with interval decision diagrams, (Proc. CMSB 2009. Proc. CMSB 2009, LNCS/LNBI, vol. 5688 (2009), Springer), 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; Snoopy Website. A tool to design and animate/simulate graphs. BTU Cottbus. http://www-dssz.informatik.tu-cottbus.de/software/snoopy.html |
| [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.; 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.; 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, (Design Automation Conference (1998)), 605-610 |
| [43] | Yoneda, T.; Hatori, H.; Takahara, A.; Minato, S., (BDDs vs. Zero-suppressed BDDs: For CTL Symbolic Model Checking of Petri Nets. BDDs vs. Zero-suppressed BDDs: For CTL Symbolic Model Checking of Petri Nets, LNCS, vol. 1166 (1996)), 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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
