A Probabilistic Model for Molecular Systems

• Autorzy: Barbuti R. , Cataudella S. , Maggiolo-Schettini A. , Milazzo P. , Troina A.
• Języki publikacji: EN

Abstrakty

EN

We introduce a model for molecular reactions based on probabilistic rewriting rules. We give a probabilistic algorithm for rule applications as a semantics for the model, and we show how a probabilistic transition system can be derived from it. We use the algorithm in the development of an interpreter for the model, which we use to simulate the evolution of molecular systems. In particular, we show the results of the simulation of a real example of enzymatic activity. Moreover, we apply the probabilistic model checker PRISM to the transition system derived by the model of this example, and we show the results of model checking of some illustrative properties.

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2005
• Tom: Vol. 67, nr 1-3
• Strony: 13--27
• Opis fizyczny: Bibliogr. 24 poz., wykr.

Twórcy

autor

Barbuti R.

• Dipartimento di Informatica, Universit`a di Pisa Largo B. Pontecorvo 3, 56127 - Pisa, Italy

autor

Cataudella S.

• Dipartimento di Informatica, Universit`a di Pisa Largo B. Pontecorvo 3, 56127 - Pisa, Italy

autor

Maggiolo-Schettini A.

• Dipartimento di Informatica, Universit`a di Pisa Largo B. Pontecorvo 3, 56127 - Pisa, Italy

autor

Milazzo P.

• Dipartimento di Informatica, Universit`a di Pisa Largo B. Pontecorvo 3, 56127 - Pisa, Italy

autor

Troina A.

• Dipartimento di Informatica, Universit`a di Pisa Largo B. Pontecorvo 3, 56127 - Pisa, Italy

Bibliografia

• [1] R. Alur, C. Belta, F. Ivancic, V. Kumar, M. Mintz, G. Pappas, H. Rubin, and J. Schug. Hybrid Systems : Computation and Control, volume 2034 of LNCS, chapter HybridModeling and Simulation of Biomolecular Networks, pages 19–32. Springer, 2001.
• [2] C. Baier and M. Kwiatowska. Model checking for a probabilistic branching time logic with fairness. Distributed Computing, 11(3):125–155, 1998.
• [3] Christel Baier, Boudewijn R. Haverkort, Holger Hermanns, and Joost-Pieter Katoen. Model checking continuous-timemarkov chains by transient analysis. In Proc. of CAV, volume 1885 of LNCS, pages 358–372. Springer, 2000.
• [4] A. Bianco and L. de Alfaro. Model checking of probabilistic and nondeterministic systems. In Proc. of Int. Conference on Foundation of Software Technologies and Theoretical Computer Science, volume 1026 of LNCS, pages 499–513. Springer, 1995.
• [5] L. Cardelli. Bioware languages. In Computer Systems. Theory, Technology and Applications. Papers for Roger Needham, pages 59–66. Springer, 2003.
• [6] N. Chabrier and F. Fages. Symbolic model checking of biochemical networks. In Comp. Methods in Systems Biology (CMSB), volume 2602 of LNCS, pages 149–162. Springer, 2003.
• [7] N. Chabrier-Rivier, F. Fages, and S. Soliman. The biochemical abstract machine biocham. In Comp.Methods in Systems Biology (CMSB) 2004, LNCS. Springer, to appear.
• [8] M. Curti, P. Degano, C. Priami, and C.T. Baldari. Modelling biochemical pathways through enhanced 􀀀 π–calculus. Theoretical Computer Science, 325(1):111–140, 2004.
• [9] Vincent Danos and Cosimo Laneve. Formal molecular biology. Theoretical Computer Science, 325(1):69–110, 2004.
• [10] S. Geman and M. Johnson. Probabilistic grammars and their applications. International Encyclopedia of the Social & Behavioral Sciences, pages 12075–12082, Elsevier, 2002.
• [11] D. Gillespie. Exact stochastic simulation of coupled chemical reactions. Journal of Physical Chemistry, 81:2340–2361, 1977.
• [12] H. Hansson and B. Jonsson. A logic for reasoning about time and probability. Formal Aspects of Computing, 6(5):512–535, 1994.
• [13] D. Harel. A grand challenge: Full reactive modeling of a multi-cellular animal. Bulletin of the EATCS , European Association for Theoretical Computer Science, 81:226–235, 2003.
• [14] N. Kam, D. Harel, H. Kugler, R. Marelly, A. Pnueli, E.J.A. Hubbard, and M.J. Stern. Formal modeling of c. elegans development: A scenario-based approach. In Comp. Methods in Systems Biology (CMSB), volume 2602 of LNCS, pages 4–20. Springer, 2003.
• [15] M. Kwiatkowska. Model checking for probability and time: From theory to practice. In Proc. of LICS’03, pages 351–360. IEEE CS Press, 2003.
• [16] I. Marini, L. Bucchioni, P. Borella, A. Del Corso, and U. Mura. Sorbitol dehydrogenase from bovine lens: Purification and properties. Archives of Biochemistry and Biophysics, 340:383–391, 1997.
• [17] H. Matsuno, A. Doi, M. Nagasaki, and S. Miyano. Hybrid petri net representation of gene regulatory networ. In Pacific Symposium on Biocomputing, volume 5, pages 341–352,World Scientific Press, 2000.
• [18] M. Nagasaki, S. Miyano, S. Onami, and H. Kitano. Bio-calculus: Its concept and molecular interaction. Genome Informatics, 10:133–143, 1999.
• [19] L. Popova-Zeugmann, M. Heiner, and I. Koch. Modelling and analysis of biochemical networks with time petri nets. In 13th Int. Workshop on Concurrency Specification and Programming (CS&P’04), number 170 in Informatik–Berichte, pages 136–143. Humboldt–Universitaet, 2004.
• [20] C. Priami, A. Regev, E.Y. Shapiro, and W. Silverman. Application of a stochastic name-passing calculus to representation and simulation of molecular processes. Information Processing Letters, 80:25–31, 2001.
• [21] PRISM Model Checker. web site, 2004. http://www.cs.bham.ac.uk/˜dxp/prism.
• [22] A. Regev. Computational Systems Biology: a Calculus for Biomolecular Knowledge. PhD thesis, Tel Aviv University, 2002.
• [23] A. Regev, W. Silverman, and E.Y. Shapiro. Representation and simulation of biochemical processes using the pi-calculus process algebra. In Pacific Symposium on Biocomputing, pages 459–470, World Scientific Press, 2001.
• [24] SICStus prolog. web site, 2004. http://www.sics.se/sicstus/.