Advertisement

Computing Reachable States for Nonlinear Biological Models

  • Thao Dang
  • Colas Le Guernic
  • Oded Maler
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5688)

Abstract

In this paper we describe reachability computation for continuous and hybrid systems and its potential contribution to the process of building and debugging biological models. We then develop a novel algorithm for computing reachable states for nonlinear systems and report experimental results obtained using a prototype implementation. We believe these results constitute a promising contribution to the analysis of complex models of biological systems.

Keywords

Nonlinear System Hybrid System Reachable State Hybrid Automaton Reachability Analysis 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Althoff, M., Stursberg, O., Buss, M.: Reachability Analysis of Nonlinear Systems with Uncertain Parameters using Conservative Linearization. In: CDC 2008 (2008)Google Scholar
  2. 2.
    Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The Algorithmic Analysis of Hybrid Systems. Theoretical Computer Science 138, 3–34 (1995)CrossRefGoogle Scholar
  3. 3.
    Alur, R., Dang, T., Ivancic, F.: Counterexample-guided Predicate Abstraction of Hybrid Systems. Theoretical Computer Science 354, 250–271 (2006)CrossRefGoogle Scholar
  4. 4.
    Asarin, E., Bournez, O., Dang, T., Maler, O.: Approximate Reachability Analysis of Piecewise Linear Dynamical Systems. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 21–31. Springer, Heidelberg (2000)Google Scholar
  5. 5.
    Asarin, E., Dang, T.: Abstraction by Projection and Application to Multi-affine Systems. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 32–47. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  6. 6.
    Asarin, E., Dang, T., Girard, A.: Hybridization Methods for the Analysis of Nonlinear Systems. Acta Informatica 43, 451–476 (2007)CrossRefGoogle Scholar
  7. 7.
    Aubin, J.-P., Cellina, A.: Differential Inclusions. Springer, Heidelberg (1984)CrossRefGoogle Scholar
  8. 8.
    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
  9. 9.
    Ben Salah, R., Bozga, M., Maler, O.: On Interleaving in Timed Automata. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol. 4137, pp. 465–476. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  10. 10.
    Botchkarev, O., Tripakis, S.: Verification of hybrid systems with linear differential inclusions using ellipsoidal approximations. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 73–88. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  11. 11.
    Chutinan, A., Krogh, B.H.: Verification of polyhedral-invariant hybrid automata using polygonal flow pipe approximations. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol. 1569, pp. 76–90. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  12. 12.
    Chutinan, A., Krogh, B.H.: Computational Techniques for Hybrid System Verification. IEEE Trans. on Automatic Control 48, 64–75 (2003)CrossRefGoogle Scholar
  13. 13.
    Dang, T.: Verification and Synthesis of Hybrid Systems, PhD thesis, Institut National Polytechnique de Grenoble, Laboratoire Verimag (2000)Google Scholar
  14. 14.
    Dang, T.: Approximate Reachability Computation for Polynomial Systems. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 138–152. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  15. 15.
    Dang, T., Maler, O.: Reachability Analysis via Face Lifting. In: Henzinger, T.A., Sastry, S.S. (eds.) HSCC 1998. LNCS, vol. 1386, pp. 96–109. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  16. 16.
    Donze, A., Clermont, G., Legay, A., Langmead, C.J.: Parameter Synthesis in Nonlinear Dynamical Systems: Application to Systems Biology. In: RECOMB 2009, pp. 155–169 (2009)Google Scholar
  17. 17.
    Frehse, G.: PHAVer: Algorithmic Verification of Hybrid Systems Past HyTech. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 258–273. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  18. 18.
    Han, Z., Krogh, B.H.: Reachability Analysis of Nonlinear Systems using Trajec- tory Piecewise Linearized Models. In: American Control Conference, pp. 1505–1510 (2006)Google Scholar
  19. 19.
    Halasz, A., Kumar, V., Imielinski, M., Belta, C., Sokolsky, O., Pathak, S.: Analysis of Lactose Metabolism in E.coli using Reachability Analysis of Hybrid Systems. IEE Proceedings - Systems Biology 21, 130–148 (2007)CrossRefGoogle Scholar
  20. 20.
    Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: Algorithmic Analysis of Nonlinear Hybrid Systems. IEEE Trans. on Automatic Control 43, 540–554 (1998)CrossRefGoogle Scholar
  21. 21.
    de Jong, H., Page, M., Hernandez, C., Geiselmann, J.: Qualitative Simulation of Genetic Regulatory Networks: Method and Application. In: IJCAI 2001, pp. 67–73 (2001)Google Scholar
  22. 22.
    Gillespie, D.T.: Stochastic Simulation of Chemical Kinetics. Annual Review of Physical Chemistry 58, 35–55 (2007)CrossRefPubMedGoogle Scholar
  23. 23.
    Girard, A.: Reachability of Uncertain Linear Systems using Zonotopes. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 291–305. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  24. 24.
    Girard, A., Le Guernic, C., Maler, O.: Efficient Computation of Reachable Sets of Linear Time-invariant Systems with Inputs. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 257–271. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  25. 25.
    Greenstreet, M.R.: Verifying Safety Properties of Differential Equations. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol. 1102, pp. 277–287. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  26. 26.
    Greenstreet, M.R., Mitchell, I.: Reachability Analysis Using Polygonal Projections. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol. 1569, pp. 103–116. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  27. 27.
    Le Guernic, C.: Calcul efficace de l’ensemble atteignable des systémes linaires avec incertitudes, Master’s thesis, Université Paris 7 (2005)Google Scholar
  28. 28.
    Hirsch, M., Smale, S.: Differential Equations, Dynamical Systems and Linear Algebra. Academic Press, London (1974)Google Scholar
  29. 29.
    Jaulin, L., Kieffer, M., Didrit, O., Walter, E.: Applied Interval Analysis. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  30. 30.
    de Jong, H., Page, M., Hernandez, C., Geiselmann, J.: Qualitative Simulation of Genetic Regulatory Networks: Method and Application. In: IJCAI 2001, pp. 67–73 (2001)Google Scholar
  31. 31.
    Klipp, E., Herwig, R., Kowald, A., Wierling, C., Lehrach, H.: Systems Biology in Practice: Concepts, Implementation and Application. Wiley, Chichester (2005)CrossRefGoogle Scholar
  32. 32.
    Kurzhanskiy, A., Varaiya, P.: Ellipsoidal Techniques for Reachability Analysis of Discrete-time Linear Systems. IEEE Trans. Automatic Control 52, 26–38 (2007)CrossRefGoogle Scholar
  33. 33.
    Kurzhanski, A., Varaiya, P.: Ellipsoidal tehcniques for reachability analysis. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, p. 202. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  34. 34.
    Maler, O.: A Unified Approach for Studying Discrete and Continuous Dynamical Systems. In: CDC 1998, pp. 2083–2088 (1998)Google Scholar
  35. 35.
    Maler, O.: Control from Computer Science. Ann. Rev. in Control 26, 175–187 (2002)CrossRefGoogle Scholar
  36. 36.
    Maler, O., Batt, G.: Approximating Continuous Systems by Timed Automata. In: Fisher, J. (ed.) FMSB 2008. LNCS (LNBI), vol. 5054, pp. 77–89. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  37. 37.
    Mitchell, I., Tomlin, C.J.: 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
  38. 38.
    Sastry, S.: Nonlinear systems. Analysis, Stability and Control. Springer, Heidelberg (1999)Google Scholar
  39. 39.
    Schrijver, A.: Theory of Linear and Integer Programming. Wiley, Chichester (1986)Google Scholar
  40. 40.
    Thomas, R., D’Ari, R.: Biological Feedback. CRC Press, Boca Raton (1990)Google Scholar
  41. 41.
    Varaiya, P.: Reach Set computation using Optimal Control. In: KIT Workshop, pp. 377–383. Verimag, Grenoble (1998)Google Scholar
  42. 42.
    Zeigler, G.M.: Lectures on Polytpoes. Springer, Heidelberg (1995)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Thao Dang
    • 1
  • Colas Le Guernic
    • 1
  • Oded Maler
    • 1
  1. 1.CNRS-VERIMAGGieresFrance

Personalised recommendations