Modelling and Analysing Qualitative Biological Models using Rewriting Logic

• Autorzy: Alhumaidan A. , Steggles J.

Identyfikatory

DOI

10.3233/FI-2017-1529

• Języki publikacji: EN

Abstrakty

EN

Qualitative logical modelling techniques play an important role in biology and are seen as crucial for developing scalable methods for modelling and synthesizing biological systems. While a range of interesting work has been done in this area there still exists challenging issues that need to be addressed for the practical application of these modelling techniques. In this paper we present an algebraic framework for exploring these issues by developing techniques for modelling and analysing qualitative biological models using Rewriting Logic (RL). The aim here is to develop a universal formal framework which is able to integrate models expressed in different formalisms (e.g. Boolean networks, Petri Nets and process algebra) and provide a basis for new work in this area (e.g. merging models based on different formalisms; compositional model construction and analysis; and tools for synthetic biology). We take as our starting point Multi-valued networks (MVNs), a simple yet expressive qualitative state based modelling approach widely used in biology. We develop a semantic translation from MVNs to a corresponding RL model and formally show that this translation is correct. We consider both the asynchronous and synchronous update semantics, and investigate the use of rewriting strategies to enable synchronisation to be modelled. We illustrate the RL framework developed and the potential RL analysis possible by presenting two detailed case studies.

Słowa kluczowe

EN

genetic regulatory networks; multi-valued networks; qualitative modelling; rewriting logic

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2017
• Tom: Vol. 153, nr 1/2
• Strony: 1--28
• Opis fizyczny: Bibliogr. 38 poz., rys., tab.

Twórcy

autor

Alhumaidan A.

• School of Computing Science, University of Newcastle, U. K

autor

Steggles J.

• School of Computing Science, University of Newcastle, U. K

Bibliografia

• [1] Bartocci E, and Lió P. Computational modeling, formal analysis and tools for systems biology. PLOS Computational Biology, 2016;12(1):e1004591. doi:10.1371/ journal.pcbi.1004591.
• [2] Rudell R, and Sangiovanni-Vincentelli A. Multiple-Valued Minimization for PLA Optimization. IEEE Transactions on Computer-Aided Design, CAD-6, 1987;6(5):727–750. doi:10.1109/TCAD.1987.1270318.
• [3] Thomas R, and D’Ari R. Biological Feedback, CRC Press, 1990. ISBN 9780849367663 - CAT# 6766.
• [4] Chaouiya C, Remy E, and Thieffry D. Petri Net Modelling of Biological Regulatory Networks. Journal of Discrete Algorithms, 2008;6(2):165–177. URL http://doi.org/10.1016/j.jda.2007.06.003.
• [5] Banks R, and Steggles LJ. A High-Level Petri Net Framework for Multi-Valued Genetic Regulatory Networks. Journal of Integrative Bioinformatics, 2007;4(3):60. URL https://doi.org/10.2390/biecoll-jib-2007-60.
• [6] Kauffman SA. Metabolic stability and epigenesis in randomly constructed genetic nets. Journal of Theoretical Biology, 1969;22(3):437–467. URL https://doi.org/10.1016/0022-5193(69)90015-0.
• [7] Wuensch A. Basins of Attraction in Network Dynamics: A Conceptual Framework for Biomolecular Networks, In: G.Schlosser and G.P.Wagner (Eds), Modularity in Development and Evolution, pages 288-311, Chicago University Press, 2002.
• [8] Harvey I, and Bossomaier T. Time Out of Joint: Attractors in Asynchronous Random Boolean Networks.In: P. Husbands and I. Harvey (eds.), Proc. of ECAL97, pages 67–75, MIT Press 1997.
• [9] Meseguer J. Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science, 1992;96(1):73–155. URL https://doi.org/10.1016/0304-3975(92)90182-F.
• [10] Martí-Oliet N, and Meseguer J. Rewriting logic as a logical and semantic framework. In: D.M.Gabbay and F.Guenthner (eds), Handbook of Philosophical Logic (Second Edition), Vol. 9, pages 1–87, Kluwer Academic Publishers, 2002. doi:10.1007/978-94-017-0464-9_1.
• [11] Ciobanu G, Koutny M, and Steggles LJ. Strategy based semantics for mobility with time and access permissions. Formal Aspects of Computing, 2015;27(3):525–549. doi:10.1007/s00165-014-0324-9.
• [12] Stehr M-O, Meseguer J, and Ölveczky PC. Rewriting Logic As a Unifying Framework for Petri Nets. In: H. Ehrig, et al. (eds), Unifying Petri Nets: Advances in Petri Nets, LNCS 2128, pages 250–303, Springer Verlag, 2001. doi:10.1007/3-540-45541-8_9.
• [13] Steggles LJ. Rewriting Logic and Elan: Prototyping Tools for Petri Nets with Time. Applications and Theory of Petri Nets 2001, LNCS 2075, pages 363-381, Springer Verlag, 2001. doi:10.1007/3-540-45740-2_21.
• [14] Eker S, Knapp M, Laderoute K, Lincoln P, Meseguer J, Sonmez K. Pathway Logic: Executable models of biological networks. In: F. Gadducci, U. Montanari (eds.), Proc. of WRLA 2002, Electronic Notes in Theoretical Computer Science, 2004;71:144–161. URL https://doi.org/10.1016/S1571-0661(05)82533-2.
• [15] Nigam V, Donaldson R, Knapp M, McCarthy T, and Talcott C. Inferring Executable Models from Formalized Experimental Evidence. In: Computational Methods in Systems Biology 9308, pages 90–103, Springer Verlag, 2015. doi:10.1007/978-3-319-23401-4_9.
• [16] Clavel M et al. Maude: Specification and Programming in Rewriting Logic. Theoretical Computer Science, 2002;285(2):187–243. URL https://doi.org/10.1016/S0304-3975(01)00359-0.
• [17] Borovanský P, Kirchner C, Kirchner H, Moreau P-E, and Ringeissen C. An overview of ELAN. In: C. Kirchner and H. Kirchner (eds), Proc. of WRLA ’98, Electronic Notes in Theoretical Computer Science, 15, 1998. URL https://doi.org/10.1016/S1571-0661(05)82552-6.
• [18] Balland E, Brauner P, Kopetz R, Moreau P-E, and Reilles A. Tom: Piggybacking rewriting on java. In: RTA’07, LNCS 4533, pages 36–47, Springer Verlag, 2007. doi:10.1007/978-3-540-73449-9_5.
• [19] Eker S, Martí-Oliet N, Meseguer J, Verdejo A. Deduction, Strategies, and Rewriting. Proc. of STRATEGIES 2006, Electronic Notes in Theoretical Computer Science, 2007;174(11):3–25. URL https://doi.org/10.1016/j.entcs.2006.03.017.
• [20] Sen AK, and Liu W. Dynamic analysis of genetic control and regulation of amino acid synthesis: The tryptophan operon in Escherichia coli. Biotechnology and Bioengineering, 1990;35(2):185–194. doi:10.1002/bit.260350209.
• [21] Santillán M, and Mackey MC. Dynamic regulation of the tryptophan operon: A modeling study and comparison with experimental data. PNAS, 2001;98(4): 1364–1369. doi:10.1073/pnas.98.4.1364.
• [22] Simão E, Remy E, Thieffry D, and Chaouiya C. Qualitative modelling of regulated metabolic pathways: application to the tryptophan biosynthesis in E. Coli. Bioinformatics, 2005;21:190–196. doi:10.1093/bioinformatics/bti1130.
• [23] Thieffry D, and Thomas R. Dynamical behaviour of biological regulatory networks - II. Immunity control in bacteriophage lambda. Bulletin of Mathematical Biology, 1995;57:277–295. doi:10.1007/BF02460619.
• [24] Pathway Logic, http://pl.csl.sri.com/. Accessed: 30/12/2016.
• [25] Eker S, Meseguer J, Sridharanarayanan A. The Maude LTL Model Checker. In: F. Gadducci, U. Montanari (eds.), Proc. of WRLA 2002, Electronic Notes in Theoretical Computer Science, 2004;71:162–187. URL https://doi.org/10.1016/S1571-0661(05)82534-4.
• [26] M.Clavel et al. Maude Manual (Version 2.7) http://maude.lcc.uma.es/manual/maude-manual.html. Accessed April 2016.
• [27] Schaub M, Henzinger T, and Fisher J. Qualitative networks: A symbolic approach to analyze biological signaling networks. BMC Systems Biology, 2007;1:4. doi:10.1186/1752-0509-1-4.
• [28] Mishchenko A, and Brayton R. Simplification of non-deterministic multi-valued networks. In: ICCAD ’02: Proc. of the 2002 IEEE/ACM Int. Conference on Computer-aided design, pages 557–562, 2002. doi:10.1109/ICCAD.2002.1167587.
• [29] Oppenheim AB, Kobiler O, Stavans J, Court DL, and Adhya SL. Switches in bacteriophage λ development. Annual Review of Genetics, 2005;39:4470–4475. doi:10.1146/annurev.genet.39.073003.113656.
• [30] Thomas R. Boolean formalization of genetic control circuits. Journal of Theoretical Biology, 1990; 42:563–585.
• [31] Kauffman SA. The origins of order: Self-organization and selection in evolution. Oxford University Press, New York, January 1993. ISBN-13: 978-0195079517.
• [32] Tournier L, and Chaves M. Uncovering operational interactions in genetic networks using asynchronous Boolean dynamics. Journal of Theoretical Biology, 2009;260:196–209. doi:10.1016/j.jtbi.2009.06.006.
• [33] Saadatpour A, Albert I, and Albert R. Attractor analysis of asynchronous Boolean models of signal transduction networks. Journal of Theoretical Biology, 2010;266(4):641–656. URL http://doi.org/10.1016/j.jtbi.2010.07.022.
• [34] MVSIS Group. UC Berkeley: https://embedded.eecs.berkeley.edu/mvsis/. Accessed:30/12/2016.
• [35] Manna Z, and Pnueli A. The Temporal Logic of Reactive and Concurrent Systems – Specification. Springer, 1992. ISBN-0-387-97664-7.
• [36] Steggles LJ, Banks R, Shaw O, and Wipat A. Qualitatively modelling and analysing genetic regulatory networks: a Petri net approach. Bioinformatics, 2006;23(3):336-343. URL https://doi.org/10.1093/bioinformatics/btl596.
• [37] Chaouiya C, Naldi A, and Thieffry D. Logical Modelling of Gene Regulatory Networks with GINsim. Methods in molecular biology (Clifton, N.J.), 2012;804:463-79. doi:10.1007/978-1-61779-361-5_23.
• [38] Meseguer J, and Montanari U. Petri nets are monoids. Information and Computation, 1990;88(2): 105–155. URL https://doi.org/10.1016/0890-5401(90)90013-8.