Skip to main content
SpringerLink
Log in

Reachability Analysis of Polynomial Systems Using Linear Programming Relaxations

  • Conference paper
Automated Technology for Verification and Analysis (ATVA 2012)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 7561))

Abstract

In this paper we propose a new method for reachability analysis of the class of discrete-time polynomial dynamical systems. Our work is based on the approach combining the use of template polyhedra and optimization [25, 7]. These problems are non-convex and are therefore generally difficult to solve exactly. Using the Bernstein form of polynomials, we define a set of equivalent problems which can be relaxed to linear programs. Unlike using affine lower-bound functions in [7], in this work we use piecewise affine lower-bound functions, which allows us to obtain more accurate approximations. In addition, we show that these bounds can be improved by increasing artificially the degree of the polynomials. This new method allows us to compute more accurately guaranteed over-approximations of the reachable sets of discrete-time polynomial dynamical systems. We also show different ways to choose suitable polyhedral templates. Finally, we show the merits of our approach on several examples.

This work was supported by the Agence Nationale de la Recherche (VEDECY project - ANR 2009 SEGI 015 01).

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Asarin, E., Dang, T., Girard, A.: Hybridization methods for the analysis of nonlinear systems. Acta Informatica 43(7), 451–476 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  2. Bernstein, S.: Collected Works, vol. 1. USSR Academy of Sciences (1952)

    Google Scholar 

  3. Bernstein, S.: Collected Works, vol. 2. USSR Academy of Sciences (1954)

    Google Scholar 

  4. 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)

    Chapter  Google Scholar 

  5. Dang, T., Le Guernic, C., Maler, O.: Computing Reachable States for Nonlinear Biological Models. In: Degano, P., Gorrieri, R. (eds.) CMSB 2009. LNCS, vol. 5688, pp. 126–141. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  6. Dang, T., Maler, O., Testylier, R.: Accurate hybridization of nonlinear systems. In: HSCC 2010, pp. 11–20 (2010)

    Google Scholar 

  7. Dang, T., Salinas, D.: Image Computation for Polynomial Dynamical Systems Using the Bernstein Expansion. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 219–232. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  8. FitzHugh, R.: Impulses and physiological states in theoretical models of nerve membrane. Biophysical J. 1, 445–466 (1961)

    Article  Google Scholar 

  9. Frehse, G., Le Guernic, C., Donzé, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: Scalable Verification of Hybrid Systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379–395. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  10. 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)

    Chapter  Google Scholar 

  11. Halasz, A., Kumar, V., Imielinski, M., Belta, C., Sokolsky, O., Pathak, S., Rubin, H.: Analysis of lactose metabolism in e.coli using reachability analysis of hybrid systems. IET Systems Biology 1(2), 130–148 (2007)

    Article  Google Scholar 

  12. Han, Z., Krogh, B.H.: Reachability Analysis of Large-Scale Affine Systems Using Low-Dimensional Polytopes. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 287–301. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  13. Horst, R., Tuy, H.: Global optimazation: Deterministic approaches, 2nd edn. Springer (1993)

    Google Scholar 

  14. Jaulin, L., Kieffer, M., Didrit, O., Walter, E.: Applied Interval Analysis. Springer (2001)

    Google Scholar 

  15. Kaynama, S., Oishi, M., Mitchell, I., Dumont, G.A.: The continual reachability set and its computation using maximal reachability techniques. In: CDC (2011)

    Google Scholar 

  16. 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)

    Chapter  Google Scholar 

  17. Lasserre, J.B.: Global optimization with polynomials and the problem of moments. SIAM Journal of Optimization 11(3), 796–817 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  18. Le Guernic, C., Girard, A.: Reachability Analysis of Hybrid Systems Using Support Functions. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 540–554. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  19. Lin, Q., Rokne, J.G.: Interval approxiamtions of higher order to the ranges of functions. Computers Math 31, 101–109 (1996)

    MathSciNet  MATH  Google Scholar 

  20. Martin, R., Shou, H., Voiculescu, I., Bowyer, A., Wang, G.: Comparison of interval methods for plotting algebraic curves. Computer Aided Geometric Design (19), 553–587 (2002)

    Google Scholar 

  21. 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)

    Chapter  Google Scholar 

  22. Nedialkov, N.S., Jackson, K.R., Corliss, G.F.: Validated solutions of initial value problems for ordinary differential equations. Applied Mathematics and Computation (105), 21–68 (1999)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  24. Prajna, S., Jadbabaie, A., Pappas, G.J.: A framework for worst-case and stochastic safety verification using barrier certificates. IEEE Transactions on Automatic Control 52(8), 1415–1429 (2007)

    Article  MathSciNet  Google Scholar 

  25. Sankaranarayanan, S., Dang, T., Ivančić, F.: Symbolic Model Checking of Hybrid Systems Using Template Polyhedra. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 188–202. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  26. Sherali, H.D., Tuncbilek, C.H.: A global optimization algorithm for polynomial programming using a reformulation-linearization technique. Journal of Global Optimization 2, 101–112 (1991)

    Article  MathSciNet  Google Scholar 

  27. Sherali, H.D., Tuncbilek, C.H.: New reformulation-linearization/convexification relaxations for univariate and multivariate polynomial programming problems. Operation Research Letters 21, 1–9 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  28. Tiwari, A., Khanna, G.: Nonlinear Systems: Approximating Reach Sets. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 600–614. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  29. Yordanov, B., Belta, C.: Cdc. In: A Formal Verification Approach to the Design of Synthetic Gene Networks (2011)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Verimag, Université de Grenoble, France

    Romain Testylier & Thao Dang

  2. Laboratoire Jean Kuntzmann, Université de Grenoble, France

    Mohamed Amin Ben Sassi & Antoine Girard

Authors
  1. Mohamed Amin Ben Sassi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Romain Testylier
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Thao Dang
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Antoine Girard
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Indian Institute of Technology, Computer Science and Engineering, Dept. of Computer Science and Engineering, IIT Bombay, Powai, 400076, Mumbai, Maharashtra, India

    Supratik Chakraborty

  2. Chennai Mathematical Institute, H1, SIPCOT IT Park, Kelambakkam, 603103, Siruseri, Tamil Nadu, India

    Madhavan Mukund

Rights and permissions

Reprints and permissions

Copyright information

© 2012 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Ben Sassi, M.A., Testylier, R., Dang, T., Girard, A. (2012). Reachability Analysis of Polynomial Systems Using Linear Programming Relaxations. In: Chakraborty, S., Mukund, M. (eds) Automated Technology for Verification and Analysis. ATVA 2012. Lecture Notes in Computer Science, vol 7561. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33386-6_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-33386-6_12

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-33385-9

  • Online ISBN: 978-3-642-33386-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation