Abstract
Recent studies have demonstrated the possibility to build genetic regulatory networks that confer a desired behavior to a living organism. However, the design of these networks is difficult, notably because of uncertainties on parameter values. In previous work, we proposed an approach to analyze genetic regulatory networks with parameter uncertainties. In this approach, the models are based on piecewise-multiaffine (PMA) differential equations, the specifications are expressed in temporal logic, and uncertain parameters are given by intervals. Abstractions are used to obtain finite discrete representations of the dynamics of the system, amenable to model checking. However, the abstraction process creates spurious behaviors along which time does not progress, called time-converging behaviors. Consequently, the verification of liveness properties, expressing that something will eventually happen, and implicitly assuming progress of time, often fails. In this work, we extend our previous approach to enforce progress of time. More precisely, we define transient regions as subsets of the state space left in finite time by every solution trajectory, show how they can be used to rule out time-converging behaviors, and provide sufficient conditions for their identification in PMA systems. This approach is implemented in RoVerGeNe and applied to the analysis of a network built in the bacterium E. coli.
Chapter PDF
References
Andrianantoandro, E., et al.: Synthetic biology: New engineering rules for an emerging discipline. Mol. Syst. Biol. (2006)
Batt, G., Belta, C.: Model checking genetic regulatory networks with applications to synthetic biology. CISE Tech. Rep. 2006-IR-0030, Boston University (2006)
Belta, C., Weiss, R., Batt, G.: Model Checking Genetic Regulatory Networks with Parameter Uncertainty. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 61–75. Springer, Heidelberg (2007)
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)
Alpern, B., Schneider, F.B.: Recognizing safety and liveness. Distrib. Comput. 2(3), 117–126 (1986)
Henzinger, T.A., et al.: Symbolic model checking for real-time systems. Inform. and Comput. 111, 193–244 (1994)
Tripakis, S., Yovine, S.: Analysis of timed systems using time-abstracting bisimulations. Formal Methods System Design 18(1), 25–68 (2001)
Wang, F., Huang, G.D., Yu, F.: TCTL inevitability analysis of dense-time systems: From theory to engineering. IEEE Trans. Softw. Eng., in press (2006)
Habets, L.C.G.J.M., Collins, P.J., van Schuppen, J.H.: Reachability and control synthesis for piecewise-affine hybrid systems on simplices. IEEE Trans. Aut. Control 51(6), 938–948 (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)
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)
de Jong, H., et al.: Qualitative simulation of genetic regulatory networks using piecewise-linear models. Bull. Math. Biol. 66(2), 301–340 (2004)
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.A.: The logical analysis of continuous non-linear biochemical control networks. J. Theor. Biol. 39(1), 103–129 (1973)
Lygeros, J., et al.: Dynamical properties of hybrid automata. IEEE Trans. Aut. Control 48(1), 2–17 (2003)
Bouajjani, A., et al.: Analysis of fair parametric extended automata. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, pp. 335–355. Springer, Heidelberg (2001)
Dams, D., Gerth, R., Grumberg, O.: A heuristic for the automatic generation of ranking functions. In: Proc. WAVe’00, pp. 1–8 (2000)
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)
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)
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)
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)
Eker, S., et al.: Pathway logic: Executable models of biological networks. In: Gadducci, F., Montanari, U. (eds.) Proc. WRLA’02. ENTCS, vol. 71, Elsevier, Amsterdam (2002)
Bengtsson, J., et al.: New generation of uppaal. In: Proc. STTT’98 (1998)
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 Liveness Properties of Genetic Regulatory Networks. In: Grumberg, O., Huth, M. (eds) Tools and Algorithms for the Construction and Analysis of Systems. TACAS 2007. Lecture Notes in Computer Science, vol 4424. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-71209-1_25
Download citation
DOI: https://doi.org/10.1007/978-3-540-71209-1_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-71208-4
Online ISBN: 978-3-540-71209-1
eBook Packages: Computer ScienceComputer Science (R0)