Published in Volume XXIII, Issue 1, 2013, pages 75-117, doi: 10.7561/SACS.2013.1.75
Authors: P. Drábik, A. Maggiolo-Schettini , P. Milazzo , G. Pardini
Abstract
Modular verification is a technique used to face the state explosion problem often encountered in the verification of properties of complex systems such as concurrent interactive systems. The modular approach is based on the observation that properties of interest often concern a rather small portion of the system. As a consequence, reduced models can be constructed which approximate the overall system behaviour thus allowing more efficient verification.
Biochemical pathways can be seen as complex concurrent interactive systems. Consequently, verification of their properties is often computationally very expensive and could take advantage of the modular approach.
In this paper we develop a modular verification framework for biochemical pathways. We view biochemical pathways as concurrent systems of reactions competing for molecular resources. A modular verification technique could be based on reduced models containing only reactions involving molecular resources of interest.
For a proper description of the system behaviour we argue that it is essential to consider a suitable notion of fairness, which is a well-established notion in concurrency theory but novel in the field of pathway modelling. The fairness notion we consider forbids starvation of reactions, namely it ensures that a reaction that is enabled infinitely often cannot always occur to the detriment of another infinitely often enabled reaction causing the latter to never occur.
We prove the correctness of the approach and demonstrate it on the model of the EGF receptor-induced MAP kinase cascade by Schoeberl et al.
Full Text (PDF)References
[1] Paul C. Attie and E. Allen Emerson. Synthesis of concurrent systems with many similar processes. ACM Transactions on Programming Languages and Systems, 20(1):51-115, 1998. http://dx.doi.org/10.1145/271510.271519 .
[2] Roberto Barbuti, Andrea Maggiolo-Schettini, Paolo Milazzo, and Angelo Troina. A calculus of looping sequences for modelling microbiological systems. Fundamenta Informaticae, 72(1-3):21-35, 2006 .
[3] Gilles Bernot and Fariza Tahi. Behaviour preservation of a biological regulatory network when embedded into a larger network. Fundamenta Informaticae, 91(3):463-485, 2009. http://dx.doi.org/10.3233/FI-2009-0052 .
[4] Chiara Bodei, Andrea Bracciali, and Davide Chiarugi. On deducing causality in metabolic networks. BMC Bioinformatics, 9(Suppl 4):S8, 2008. http://dx.doi.org/10.1186/1471-2105-9-S4-S8 .
[5] Jerry R. Burch, Edmund M. Clarke, Kenneth L. McMillan, David L. Dill, and L. J. Hwang. Symbolic model checking: 1020 states and beyond. Information and Computation, 98(2):142-170, 1992. http://dx.doi.org/10.1016/0890-5401(92)90017-A .
[6] Luca Cardelli. Brane calculi. In Vincent Danos and Vincent Schachter, editors, Computational Methods in Systems Biology, volume 3082 of Lecture Notes in Computer Science, pages 257-278. Springer Berlin Heidelberg, 2005. http://dx.doi.org/10.1007/978-3-540-25974-9_24 .
[7] Sagar Chaki, Edmund Clarke, Nishant Sinha, and Prasanna Thati. Automated assume-guarantee reasoning for simulation conformance. In Kousha Etessami and SriramK. Rajamani, editors, Computer Aided Verification, volume 3576 of Lecture Notes in Computer Science, pages 534-547. Springer Berlin Heidelberg, 2005. http://dx.doi.org/10.1007/11513988_51 .
[8] Claudine Chaouiya, Elisabeth Remy, and Denis Thieffry. Petri net modelling of biological regulatory networks. Journal of Discrete Algorithms, 6(2):165-177, 2008. http://dx.doi.org/10.1016/j.jda.2007.06.003 .
[9] Alessandro Cimatti, Edmund Clarke, Enrico Giunchiglia, Fausto Giunchiglia, Marco Pistore, Marco Roveri, Roberto Sebastiani, and Armando Tacchella. NuSMV version 2: An opensource tool for symbolic model checking. In Proc. International Conference on Computer-Aided Verification (CAV 2002), volume 2404 of Lecture Notes in Computer Science, pages 359-364, Copenhagen, Denmark, 2002. Springer Berlin Heidelberg. http://dx.doi.org/10.1007/3-540-45657-0_29 .
[10] Federica Ciocchetta and Jane Hillston. Bio-PEPA: A framework for the modelling and analysis of biological systems. Theoretical Computer Science, 410(33-34):3065-3084, 2009. http://dx.doi.org/10.1016/j.tcs.2009.02.037 .
[11] Edmund M. Clarke, Orna Grumberg, and David E. Long. Model checking and abstraction. ACM Transactions on Programming Languages and Systems, 16(5):1512-1542, 1994. http://dx.doi.org/10.1145/186025.186051 .
[12] Edmund M. Clarke, Orna Grumberg, and Doron Peled. Model Checking. MIT Press, 1999 .
[13] Vincent Danos, Jerome Feret, Walter Fontana, Russell Harmer, and Jean Krivine. Abstracting the differential semantics of rule-based models: exact and automated model reduction. In Logic in Computer Science (LICS), 2010 25th Annual IEEE Symposium on, pages 362-381. IEEE, 2010. http://dx.doi.org/10.1109/LICS.2010.44 .
[14] Vincent Danos and Cosimo Laneve. Formal molecular biology. Theoretical Computer Science, 325(1):69-110, 2004. http://dx.doi.org/10.1016/j.tcs.2004.03.065 .
[15] Maria I Davidich and Stefan Bornholdt. Boolean network model predicts cell cycle sequence of fission yeast. PLoS One, 3(2):e1672, 2008. http://dx.doi.org/10.1371/journal.pone.0001672 .
[16] Franck Delaplace, Hanna Klaudel, and Amandine Cartier-Michaud. Discrete causal model view of biological networks. In Proceedings of the 8th International Conference on Computational Methods in Systems Biology, CMSB ’10, pages 4-13, New York, NY, USA, 2010. ACM. http://dx.doi.org/10.1145/1839764.1839767 .
[17] Franck Delaplace, Hanna Klaudel, Tarek Melliti, and Sylvain Sene. Analysis of modular organisation of interaction networks based on asymptotic dynamics. In David Gilbert and Monika Heiner, editors, Computational Methods in Systems Biology, Lecture Notes in Computer Science, pages 148-165. Springer Berlin Heidelberg, 2012. http://dx.doi.org/10.1007/978-3-642-33636-2_10 .
[18] Peter Drabik, Andrea Maggiolo-Schettini, and Paolo Milazzo. Dynamic sync-programs for modular verification of biological systems. In 2nd Int. Workshop on Non-Classical Models of Automata and applications (NCMA’10), volume 263, Jena, Germany, 2010. Austrian Computer Society .
[19] Peter Drabik, Andrea Maggiolo-Schettini, and Paolo Milazzo. Modular verification of interactive systems with an application to biology .Electronic Notes in Theoretical Computer Science, 268:61-75, 2010. http://dx.doi.org/10.1016/j.entcs.2010.12.006 .
[20] Peter Drabik, Andrea Maggiolo-Schettini, and Paolo Milazzo. Modular verification of interactive systems with an application to biology. Scientific Annals of Computer Science, 21:39-72, 2011 .
[21] Peter Drabik, Andrea Maggiolo-Schettini, and Paolo Milazzo. On conditions for modular verification in systems of synchronising components. Fundamenta Informaticae, 120(3-4):259-274, 2012. http://dx.doi.org/10.3233/FI-2012-761 .
[22] Peter Drabik, Andrea Maggiolo-Schettini, and Paolo Milazzo. Towards modular verification of pathways: fairness and assumptions. In Gabriel Ciobanu, editor, Proceedings 6th Workshop on Membrane Computing and Biologically Inspired Process Calculi, Newcastle, UK, 8th September 2012, volume 100 of Electronic Proceedings in Theoretical Computer Science, pages 63-81. Open Publishing Association, 2012. http://dx.doi.org/10.4204/EPTCS.100.5 .
[23] E. Allen Emerson and Chin-Laung Lei. Modalities for model checking: branching time logic strikes back. Science of Computer Programming, 8(3):275-306, 1987. http://dx.doi.org/10.1016/0167-6423(87)90036-0 .
[24] Francois Fages, Sylvain Soliman, and Nathalie Chabrier-Rivier. Modelling and querying interaction networks in the biochemical abstract machine BIOCHAM. Journal of Biological Physics and Chemistry, 4(2):64-73, 2004. http://dx.doi.org/10.4024/2040402.jbpc.04.02 .
[25] Jerome Feret, Vincent Danos, Jean Krivine, Russ Harmer, and Walter Fontana. Internal coarse-graining of molecular systems. Proceedings of the National Academy of Sciences, 106(16):6453-6458, 2009. http://dx.doi.org/10.1073/pnas.0809908106 .
[26] Orna Grumberg and David E Long. Model checking and modular verification. ACM Transactions on Programming Languages and Systems (TOPLAS), 16(3):843-871, 1994. http://dx.doi.org/10.1145/177492.177725.
[27] John Heath, Marta Kwiatkowska, Gethin Norman, David Parker, and Oksana Tymchyshyn. Probabilistic model checking of complex biological pathways. Theoretical Computer Science, 391(3):239-257, 2008. http://dx.doi.org/10.1016/j.tcs.2007.11.013 .
[28] M. Hucka, A. Finney, H.M. Sauro, H. Bolouri, J.C. Doyle, H. Kitano, and the rest of the SBML Forum. The systems biology markup language (SBML): a medium for representation and exchange of biochemical network models. Bioinformatics, 19(4):524-531, 2003. http://dx.doi.org/10.1093/bioinformatics/btg015 .
[29] C. Li, M. Donizelli, N. Rodriguez, H. Dharuri, L. Endler, V. Chelliah, L. Li, E. He, A. Henry, M.I. Stefan, J.L. Snoep, M. Hucka, N. Le Novere, and C. Laibe. BioModels Database: An enhanced, curated and annotated resource for published quantitative kinetic models. BMC Systems Biology, 4:92, 2010. http://dx.doi.org/10.1186/1752-0509-4-92 .
[30] Andrea Maggiolo-Schettini, Paolo Milazzo, and Giovanni Pardini. Application of a semi-automatic algorithm for identification of molecular components in SBML models. In Proceedings of Wivace 2013, Italian Workshop on Artificial Life and Evolutionary Computation, (Milan, Italy, July 1-2, 2013), Electronic Proceedings in Theoretical Computer Science, 2013. To appear .
[31] Pedro T. Monteiro, Delphine Ropers, Radu Mateescu, Ana T. Freitas, and Hidde de Jong. Temporal logic patterns for querying dynamic models of cellular interaction networks. Bioinformatics, 24(16):i227-i233, 2008. http://dx.doi.org/10.1093/bioinformatics/btn275 .
[32] Aurelien Naldi, Elisabeth Remy, Denis Thieffry, and Claudine Chaouiya. Dynamically consistent reduction of logical regulatory graphs. Theoretical Computer Science, 412(21):2207-2218, 2011. http://dx.doi.org/10.1016/j.tcs.2010.10.021 .
[33] Giovanni Pardini, Paolo Milazzo, and Andrea Maggiolo-Schettini. An algorithm for the identification of components in biochemical pathways. In Proceedings of CS2Bio 2013, 4th International Workshop on Interactions between Computer Science and Biology, (Florence, Italy, June 6, 2013), Electronic Notes in Theoretical Computer Science, 2013. To appear .
[34] Amir Pnueli. The temporal semantics of concurrent programs. Theoretical Computer Science, 13(1):45-60, 1981. http://dx.doi.org/10.1016/0304-3975(81)90110-9 .
[35] Corrado Priami, Aviv Regev, Ehud Shapiro, and William Silverman. Application of a stochastic name-passing calculus to representation and simulation of molecular processes. Information Processing Letters, 80(1):25-31, 2001. http://dx.doi.org/10.1016/S0020-0190(01)00214-9 .
[36] Aviv Regev, Ekaterina M. Panina, William Silverman, Luca Cardelli, and Ehud Shapiro. Bioambients: an abstraction for biological compartments. Theoretical Computer Science, 325(1):141-167, 2004. http://dx.doi.org/10.1016/j.tcs.2004.03.061 .
[37] Birgit Schoeberl, Claudia Eichler-Jonsson, Ernst Dieter Gilles, and Gertraud Muller. Computational modeling of the dynamics of the MAP kinase cascade activated by surface and internalized EGF receptors. Nature Biotechnology, 20(4):370-375, 2002. http://dx.doi.org/10.1038/nbt0402-370.
Bibtex
@article{sacscuza:drábik2013mvoqpmwf,
title={Modular Verification of Qualitative Pathway Models with Fairness},
author={P. Drábik and A. Maggiolo-Schettini and P. Milazzo and G. Pardini},
journal={Scientific Annals of Computer Science},
volume={23},
number={1},
organization={``A.I. Cuza'' University, Iasi, Romania},
year={2013},
pages={75--117},
doi={10.7561/SACS.2013.1.75},
publisher={``A.I. Cuza'' University Press}
}