Abstract
Pathway Logic (PL) is an approach to modeling and analysis of biological processes based on rewriting logic. This tutorial describes the use of PL to model signal transduction processes. It begins with a general discussion of Symbolic Systems Biology, followed by some background on rewriting logic and signal transduction. The representation and analysis of a small model Ras and Raf activation is presented in some detail. This is followed by discussion of a curated model of early signaling events in response to Epidermal Growth Factor stimulation.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
References
Apolzan, R.: Rapid prototyping applications of formal reasoning tools to biological cellular signalling networks (2005), http://mcs.une.edu.au/~iop/Data/Papers/
Calder, M., Vyshemirsky, V., Gilbert, D., Orton, R.: Analysis of signalling pathways using the PRISM model checker. In: Plotkin, G. (ed.) Proceedings of the Third International Conference on Computational Methods in System Biology (2005)
Calzone, L., Chabrier-Rivier, N., Fages, F., Gentils, L., Soliman, S.: Machine learning bio-molecular interactions from temporal logic properties. In: Plotkin, G. (ed.) Proceedings of the Third International Conference on Computational Methods in System Biology (2005)
Cardelli, L.: Abstract machines of systems biology. In: Priami, C., Merelli, E., Gonzalez, P., Omicini, A. (eds.) Transactions on Computational Systems Biology III. LNCS (LNBI), vol. 3737, pp. 145–168. Springer, Heidelberg (2005)
Chabrier-Rivier, N., Chiaverini, M., Danos, V., Fages, F., Schächter, V.: Modeling and querying biomolecular interaction networks. Theoretical Computer Science 351(1), 24–44 (2004)
Chaouiya, C.: Petri net modelling of biological networks. Briefings in Bioinformatics 8, 210–219 (2007)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Mart́-Oliet, N., Meseguer, J., Talcott, C.: All About Maude: A High-Performance Logical Framework. Springer, Heidelberg (2007)
Damm, W., Harel, D.: Breathing life into message sequence charts. Formal Methods in System Design 19(1) (2001)
Edwards, J.S., Covert, M., Palsson, B.O.: Metabolic modelling of microbes: The flux-balance approach. Environmental Microbiology 4(3), 133–140 (2002)
Efroni, S., Harel, D., Cohen, I.R.: Towards rigorous comprehension of biological complexity: Modeling, execution and visualization of thymic t-cell maturation. Genome Research, Special issue on Systems Biology (in press, 2003)
Eker, S., Knapp, M., Laderoute, K., Lincoln, P., Meseguer, J., Sonmez, K.: Pathway Logic: Symbolic analysis of biological signaling. In: Proceedings of the Pacific Symposium on Biocomputing, pp. 400–412 (January 2002)
Eker, S., Knapp, M., Laderoute, K., Lincoln, P., Talcott, C.: Pathway Logic: Executable models of biological networks. In: Fourth International Workshop on Rewriting Logic and Its Applications. Electronic Notes in Theoretical Computer Science, vol. 71, Elsevier, Amsterdam (2002)
Pearson, G., et al.: Mitogen-activated protein (MAP) kinase pathways: regulation and physiological functions. Endocr. Rev, 153–183 (2001)
Fages, F., Soliman, S., Chabrier-Rivier, N.: Modelling and querying interaction networks in the biochemical abstract machine BIOCHAM. Journal of Biological Physics and Chemistry 4(2), 64–73 (2004)
Fisher, J., Henzinger, T.A.: Executable cell biology. Nature Biotechnology 25(11) (2007)
Genrich, H., Küffner, R., Voss, K.: Executable Petri net models for the analysis of metabolic pathways. Software Tools for Technology Transfer 3 (2001)
Ghosh, R., Tiwari, A., Tomlin, C.: Automated symbolic reachability analysis with application to delta-notch signaling automata. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 233–248. Springer, Heidelberg (2003)
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)
Goss, P.J., Peccoud, J.: Quantitative modeling of stochastic systems in molecular biology using stochastic Petri nets. Proceedings of the National Academy of Science 95, 6750–6755 (1998)
Harel, D.: Statecharts: A visual formalism for complex systems. Science of Computer Programming 8, 231–274 (1987)
Henzinger, T.A.: The theory of hybrid automata. In: 11th IEEE Symposium on Logic in Computer Science, pp. 278–292 (1996)
Hofestädt, R.: A Petri net application to model metabolic processes. Systems Analysis Modelling Simulation 16, 113–122 (1994)
Kam, N., Cohen, I.R., Harel, D.: The immune system as a reactive system: Modeling t cell activation with statecharts. In: Visual Languages and Formal Methods (VLFM 2001), pp. 15–22 (2001)
Kam, N., Harel, D., Kugler, H., Marelly, R., Pnueli, A., Hubbard, J., Stern, M.: Formal modeling of C.elegans development: A scenario-based approach. In: Priami, C. (ed.) CMSB 2003. LNCS, vol. 2602, pp. 4–20. Springer, Heidelberg (2003)
Kolch, W.: Meaningful relationships: The regulation of the Ras/Raf/MEK/ERK pathway by protein interactions. Biochem J. 351, 289–305 (2000)
Küffner, R., Zimmer, R., Lengauer, T.: Pathway analysis in metabolic databases via differential metabolic display (DMD). Bioinformatics 16, 825–836 (2000)
Kyriakis, J.M., Avruch, J.: Mammalian mitogen-activated protein kinase signal transduction pathways activated by stress and inflammation. Physiol. Rev. 81, 807–869 (2001)
Cardelli, L.: Brane calculi interactions of biological membranes. In: Danos, V., Schachter, V. (eds.) CMSB 2004. LNCS (LNBI), vol. 3082, Springer, Heidelberg (2005)
Li, C., Ge, Q.W., Nakata, M., Matsuno, H., Miyano, S.: Modelling and simulation of signal transductions in an apoptosis pathway by using timed petri nets. Journal of Bioscience 32, 113–127 (2007)
Lincoln, P., Tiwari, A.: Symbolic systems biology: Hybrid modeling and analysis of biological networks. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 660–672. Springer, Heidelberg (2004)
LoLA: Low Level Petri net Analyzer (2004), http://www.informatik.hu-berlin.de/~kschmidt/lola.html
Matsuno, H., Doi, A., Nagasaki, M., Miyano, S.: Hybrid Petri net representation of gene regulatory network. In: Pacific Symposium on Biocomputing, vol. 5, pp. 341–352 (2000)
Meseguer, J.: Conditional Rewriting Logic as a unified model of concurrency. Theoretical Computer Science 96(1), 73–155 (1992)
Milner, R.: Communication and Concurrency. Prentice-Hall, Englewood Cliffs (1989)
Milner, R.: Communicating and Mobile Systems: The pi-Calculus. Cambridge University Press, Cambridge (1999)
Nielson, F., Nielson, H.R., Priami, C., Rosa, D.: Control flow analysis for bioambients. In: BioConcur (2003)
Päun, G.: Membrane Computing. An Introduction. Springer, Heidelberg (2002)
Peterson, J.L.: Petri Nets: Properties, analysis, and applications. Prentice-Hall, Englewood Cliffs (1981)
Petri, C.A.: Introduction to general net theory. In: Brauer, W. (ed.) Net Theory and Applications. LNCS, vol. 84, pp. 1–19. Springer, Heidelberg (1980)
Priami, C., Regev, A., Shapiro, E., Silverman, W.: Application of a stochastic name-passing calculus to representation and simulation of molecular processes. Information Processing Letters 80, 25–31 (2001)
Prez-Jimnez, M.J., Romero-Campero, F.J.: Modelling EGFR signalling cascade using continuous membrane systems (simulation). In: Plotkin, G. (ed.) Proceedings of the Third International Conference on Computational Methods in System Biology (2005)
Reddy, V.N., Liebmann, M.N., Mavrovouniotis, M.L.: Qualitative analysis of biochemical reaction systems. Computational Biological Medicine 26, 9–24 (1996)
Regev, A., Panina, E., Silverman, W., Cardelli, L., Shaprio, E.: Bioambients: An abstraction for biological compartments (2004)
Regev, A., Silverman, W., Shapiro, E.: Representation and simulation of biochemical processes using the pi-calculus process algebra. In: Pacific Symposium on Biocomputing, vol. 6, pp. 459–470. World Scientific Press, Singapore (2001)
Schmidt, K.: LoLA: A Low Level Analyser. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol. 1825, pp. 465–474. Springer, Heidelberg (2000)
Seger, R., Krebs, E.G.: The mapk signaling cascade. FASEB J. 9(9), 726–735 (1995)
Shankar, N.: Symbolic analysis of transition systems. In: Proceedings of the International Workshop on Abstract State Machines, Theory and Applications, pp. 287–302. Springer, Heidelberg (2000)
Stehr, M.-O.: A rewriting semantics for algebraic nets. In: Girault, C., Valk, R. (eds.) Petri Nets for System Engineering – A Guide to Modelling, Verification, and Applications, Springer, Heidelberg (2000)
Talcott, C., Eker, S., Knapp, M., Lincoln, P., Laderoute, K.: Pathway logic modeling of protein functional domains in signal transduction. In: Proceedings of the Pacific Symposium on Biocomputing (January 2004)
Talcott, C.: Formal executable models of cell signaling primitives. In: Margaria, T., Philippou, A., Steffen, B. (eds.) 2nd International Symposium On Leveraging Applications of Formal Methods, Verification and Validation ISOLA06, pp. 303–307 (2006)
Talcott, C.: Symbolic modeling of signal transduction in pathway logic. In: Perrone, L.F., Wieland, F.P., Liu, J., Lawson, B.G., Nicol, D.M., Fujimoto, R.M. (eds.) 2006 Winter Simulation Conference, pp. 1656–1665 (2006)
Talcott, C., Dill, D.L.: Multiple representations of biological processes. Transactions on Computational Systems Biology (2006)
Tiwari, A.: Abstractions for hybrid systems. Formal Methods in Systems Design 32(1), 57–83 (2008)
Tiwari, A., Talcott, C., Knapp, M., Lincoln, P., Laderoute, K.: Analyzing pathways using sat-based approaches. In: Anai, H., Horimoto, K., Kutsia, T. (eds.) Ab 2007. LNCS, vol. 4545, pp. 155–169. Springer, Heidelberg (2007)
Zevedei-Oancea, I., Schuster, S.: Topological analysis of metabolic networks based on Petri net theory. In: Silico Biology, vol. 3, p. 29 (2003)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Talcott, C. (2008). Pathway Logic. In: Bernardo, M., Degano, P., Zavattaro, G. (eds) Formal Methods for Computational Systems Biology. SFM 2008. Lecture Notes in Computer Science, vol 5016. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-68894-5_2
Download citation
DOI: https://doi.org/10.1007/978-3-540-68894-5_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-68892-1
Online ISBN: 978-3-540-68894-5
eBook Packages: Computer ScienceComputer Science (R0)