Parameter Synthesis in Nonlinear Dynamical Systems: Application to Systems Biology

  • Alexandre Donzé
  • Gilles Clermont
  • Axel Legay
  • Christopher J. Langmead
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5541)


The dynamics of biological processes are often modeled as systems of nonlinear ordinary differential equations (ODE). An important feature of nonlinear ODEs is that seemingly minor changes in initial conditions or parameters can lead to radically different behaviors. This is problematic because in general it is never possible to know/measure the precise state of any biological system due to measurement errors. The parameter synthesis problem is to identify sets of parameters (including initial conditions) for which a given system of nonlinear ODEs does not reach a given set of undesirable states. We present an efficient algorithm for solving this problem that combines sensitivity analysis with an efficient search over initial conditions. It scales to high-dimensional models and is exact if the given model is affine. We demonstrate our method on a model of the acute inflammatory response to bacterial infection, and identify initial conditions consistent with 3 biologically relevant outcomes.


Verification Nonlinear Dynamical Systems Uncertainty Systems Biology Acute Illness 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoretical Computer Science 138(1), 3–34 (1995)CrossRefGoogle Scholar
  2. 2.
    Alur, R., Henzinger, T., Lafferriere, G., Pappas, G.: Discrete abstractions of hybrid systems, vol. 88(7), pp. 971–984. IEEE, Los Alamitos (2000)Google Scholar
  3. 3.
    An, G.: Agent based computer simulation and sirs: building a gap between basic science and clinical trials. Shock 16, 266–273 (2001)CrossRefPubMedGoogle Scholar
  4. 4.
    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)CrossRefGoogle Scholar
  5. 5.
    Asarin, E., Dang, T., Girard, A.: Hybridization methods for verification of non-linear systems. In: ECC-CDC 2005 joint conference: Conference on Decision and Control CDC and European Control Conference ECC (2005)Google Scholar
  6. 6.
    Batt, G., Belta, C., Weiss, R.: 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)CrossRefGoogle Scholar
  7. 7.
    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, pp. 323–338. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  8. 8.
    Batt, G., Ropers, D., de Jong, H., Geiselmann, J., Mateescu, R., Page, M., Schneider, D.: Analysis and verification of qualitative models of genetic regulatory networks: A model-checking approach. In: IJCAI, pp. 370–375 (2005)Google Scholar
  9. 9.
    Cinquemani, E., Milias-Argeitis, A., Lygeros, J.: Identification of genetic regulatory networks: A stochastic hybrid approach. In: IFAC World Congress (2008)Google Scholar
  10. 10.
    Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)Google Scholar
  11. 11.
    Donzé, A., Krogh, B., Rajhans, A.: Parameter synthesis for hybrid systems with an application to simulink models. In: Proceedings of the 12th International Conference on Hybrid Systems: Computation and Control (HSCC 2009). LNCS. Springer, Heidelberg (2009)Google Scholar
  12. 12.
    Donzé, A.: Trajectory-Based Verification and Controller Synthesys for Continuous and Hybrid Systems. PhD thesis, University Joseph Fourier (June 2007)Google Scholar
  13. 13.
    Donzé, A., Maler, O.: Systematic simulation using sensitivity analysis. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 174–189. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  14. 14.
    Drulhe, S., Ferrari-Trecate, G., de Jong, H., Viari, A.: Reconstruction of switching thresholds in piecewise-affine models of genetic regulatory networks. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 184–199. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  15. 15.
    Fainekos, G.E., Pappas, G.J.: Robust sampling for MITL specifications. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 147–162. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  16. 16.
    Fargot, E., Gouze, J.-L.: How to control a biological switch: a mathematical framework for the control of piecewise affine models of gene networks. Technical report, INRIA Sophia Antipolis (2006)Google Scholar
  17. 17.
    Frehse, G., Jha, S.K., Krogh, B.H.: A counterexample-guided approach to parameter synthesis for linear hybrid automata. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 187–200. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  18. 18.
    Ghosh, R., Tomlin, C.: Symbolic reachable set computation of piecewise affine hybrid automata and its application to biological modelling: Delta-notch signalling. System Biology (2004)Google Scholar
  19. 19.
    Henzinger, T.A., Horowitz, B., Majumdar, R., Wong-Toi, H.: Beyond hytech: Hybrid systems analysis using interval numerical methods. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 130–144. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  20. 20.
    Kumar, R.: The Dynamics of Acute Inflammation. PhD thesis, University of Pittsburgh (2004)Google Scholar
  21. 21.
    Mitchell, I., Tomlin, C.: Level set methods for computation in hybrid systems. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 310–323. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  22. 22.
    Mitchell, I.M., Tomlin, C.J.: Overapproximating reachable sets by hamilton-jacobi projections. J. Symbolic Computation 19, 1–3 (2002)Google Scholar
  23. 23.
    Platzer, A., Clarke, E.M.: The image computation problem in hybrid systems model checking. In: Bemporad, A., Bicchi, A., Buttazzo, G. (eds.) HSCC 2007. LNCS, vol. 4416, pp. 473–486. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  24. 24.
    Pnueli, A.: The temporal logic of programs. In: Proc. 18th Annual Symposium on Foundations of Computer Science (FOCS), pp. 46–57 (1977)Google Scholar
  25. 25.
    Polidori, D., Trimmer, J.: Bringing advanced therapies to marker faster: a role for bio-simulation? Diabetes’ Voice 48(2), 28–30 (2003)Google Scholar
  26. 26.
    Reynolds, A., Rubin, J., Clermont, G., Day, J., Vodovotz, Y., Ermentrout, B.: A reduced mathematical model of the acute inflammatory response: I. derivation of model and analysis of anti-inflammation. J. Theor. Biol. 242(1), 220–236 (2006)CrossRefPubMedGoogle Scholar
  27. 27.
    Serban, R., Hindmarsh, A.C.: Cvodes: the sensitivity-enabled ode solver in sundials. In: Proceedings of IDETC/CIE 2005, Long Beach, CA (September 2005)Google Scholar
  28. 28.
    Stursberg, O., Krogh, B.H.: Efficient representation and computation of reachable sets for hybrid systems. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 482–497. Springer, Heidelberg (2003)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Alexandre Donzé
    • 1
  • Gilles Clermont
    • 2
  • Axel Legay
    • 1
  • Christopher J. Langmead
    • 1
    • 3
  1. 1.Computer Science DepartmentCarnegie Mellon UniversityPittsburghUSA
  2. 2.Department of Critical Care MedicineUniversity of PittsburghPittsburghUSA
  3. 3.Lane Center for Computational BiologyCarnegie Mellon UniversityPittsburghUSA

Personalised recommendations