Abstract
The lack of precise numerical information for the values of biological parameters severely limits the development and analysis of models of genetic regulatory networks. To deal with this problem, we propose a method for the analysis of genetic regulatory networks with parameter uncertainty. We consider models based on piecewise-multiaffine differential equations, dynamical properties expressed in temporal logic, and intervals for the values of uncertain parameters. The problem is then either to guarantee that the system satisfies the expected properties for every possible parameter value - the corresponding parameter set is then called valid - or to find valid subsets of a given parameter set. The proposed method uses discrete abstractions and model checking, and allows for efficient search of the parameter space. This approach has been implemented in a tool for robust verification of gene networks (RoVerGeNe) and applied to the tuning of a synthetic network build in E. coli.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Kitano, H.: Systems biology: A brief overview. Science 295(5560), 1662–1664 (2002)
Andrianantoandro, E., et al.: Synthetic biology: New engineering rules for an emerging discipline. Mol. Syst. Biol. (2006)
Szallasi, Z., Stelling, J., Periwal, V. (eds.): System Modeling in Cellular Biology: From Concepts to Nuts and Bolts. MIT Press, Cambridge (2006)
de Jong, H., Ropers, D.: Qualitative approaches to the analysis of genetic regulatory networks. In: Szallasi, Z., Stelling, J., Periwal, V. (eds.) System Modeling in Cellular Biology: From Concepts to Nuts and Bolts, pp. 125–148. MIT Press, Cambridge (2006)
Belta, C., Habets, L.C.G.J.M.: Controlling a class of nonlinear systems on rectangles. IEEE Trans. Aut. Control 51(11), 1749–1759 (2006)
Alur, R., et al.: Discrete abstractions of hybrid systems. Proc. IEEE 88(7), 971–984 (2000)
Clarke, E.M., Grumberg, O., Peled, D.A.: Model Checking. MIT Press, Cambridge (1999)
Batt, G., Belta, C.: Model checking genetic regulatory networks with applications to synthetic biology. CISE Tech. Rep. 2006-IR-0030, Boston University (2006)
de Jong, H., et al.: Qualitative simulation of genetic regulatory networks using piecewise-linear models. Bull. Math. Biol. 66(2), 301–340 (2004)
Abate, A., Tiwari, A.: Box invariance of hybrid and switched systems. In: Proc. ADHS’06 (2006)
Belta, C., Habets, L.C.G.J.M., Kumar, V.: Control of multi-affine systems on rectangles with applications to hybrid biomolecular networks. In: Proc. CDC’02 (2002)
Mestl, T., Plahte, E., Omholt, S.: A mathematical framework for describing and analysing gene regulatory networks. J. Theor. Biol. 176, 291–300 (1995)
Glass, L., Kauffman, S.: The logical analysis of continuous non-linear biochemical control networks. J. Theor. Biol. 39(1), 103–129 (1973)
Kloetzer, M., Belta, C.: Reachability analysis of multi-affine systems. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 348–362. Springer, Heidelberg (2006)
Alur, R., Dang, T., Ivancic, F.: Progress on reachability analysis of hybrid systems using predicate abstraction. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 4–19. Springer, Heidelberg (2003)
Koutsoukos, X., Antsaklis, P.J.: Safety and reachability of piecewise linear hybrid dynamical systems based on discrete abstractions. J. Discrete Event Dynamic Systems 13(3), 203–243 (2003)
Batt, G., et al.: Validation of qualitative models of genetic regulatory networks by model checking: Analysis of the nutritional stress response in E. coli. Bioinformatics 21(Suppl. 1), i19–i28 (2005)
Batt, G., Belta, C., Weiss, R.: Model checking liveness properties of genetic regulatory networks. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, Springer, Heidelberg (2007)
Hooshangi, S., Thiberge, S., Weiss, R.: Ultrasensitivity and noise propagation in a synthetic transcriptional cascade. Proc. Natl. Acad. Sci. USA 102(10), 3581–3586 (2005)
Annichini, A., Asarin, E., Bouajjani, A.: Symbolic techniques for parametric reasoning about counter and clock systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 419–434. Springer, Heidelberg (2000)
Wang, F.: Symbolic parametric safety analysis of linear hybrid systems with BDD-like data-structures. IEEE Trans. Softw. Eng. 31(1), 38–51 (2005)
Henzinger, T., Ho, P.-H., Wong-Toi, H.: HYTECH: A model checker for hybrid systems. Software Tools Technology Transfer 1(1-2), 110–122 (1997)
Ghosh, R., Tomlin, C.J.: Symbolic reachable set computation of piecewise affine hybrid automata and its application to biological modelling: Delta-Notch protein signalling. IEE Proc. Syst. Biol. 1(1), 170–183 (2004)
Lin, H., Antsaklis, P.J.: Robust regulation of polytopic uncertain linear hybrid systems with networked control system applications. In: Antsaklis, P., Liu, D. (eds.) Stability and Control of Dynamical Systems Applications, Birkhäuser, Basel (2003)
Antoniotti, M., et al.: Taming the complexity of biochemical models through bisimulation and collapsing: Theory and practice. Theor. Comput. Sci. 325(1), 45–67 (2004)
Calzone, L., et al.: Machine learning biochemical networks from temporal logic properties. In: Priami, C., Plotkin, G. (eds.) Transactions on Computational Systems Biology VI. LNCS (LNBI), vol. 4220, pp. 68–94. Springer, Heidelberg (2006)
Bernot, G., et al.: Application of formal methods to biological regulatory networks: Extending Thomas’ asynchronous logical approach with temporal logic. J. Theor. Biol. 229(3), 339–347 (2004)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer Berlin Heidelberg
About this paper
Cite this paper
Batt, G., Belta, C., Weiss, R. (2007). Model Checking Genetic Regulatory Networks with Parameter Uncertainty. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds) Hybrid Systems: Computation and Control. HSCC 2007. Lecture Notes in Computer Science, vol 4416. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71493-4_8
Download citation
DOI: https://doi.org/10.1007/978-3-540-71493-4_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71492-7
Online ISBN: 978-3-540-71493-4
eBook Packages: Computer ScienceComputer Science (R0)