Skip to main content
SpringerLink
Log in

Safe Over- and Under-Approximation of Reachable Sets for Autonomous Dynamical Systems

  • Conference paper
  • First Online:
Formal Modeling and Analysis of Timed Systems (FORMATS 2018)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11022))

Abstract

We present a method based on the Hamilton-Jacobi framework that is able to compute over- and under-approximations of reachable sets for autonomous dynamical systems beyond polynomial dynamics. The method does not resort to user-supplied candidate polynomials, but rather relies on an expansion of the evolution function whose convergence in compact state space is guaranteed. Over- and under-approximations of the reachable state space up to any designated precision can consequently be obtained based on truncations of that expansion. As the truncations used in computing over- and under-approximations as well as their associated error bounds agree, double-sided enclosures of the true reach-set can be computed in a single sweep. We demonstrate the precision of the enclosures thus obtained by comparison of benchmark results to related simulations.

This work was partially supported by the National Natural Science Foundation of China under Grants 11371047, 11422111.

M. Li—The author was supported by the China Scholarship Council for 1 year study at Carl von Ossietzky University of Oldenburg.

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 EPUB and 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

References

  1. Althoff, M.: Reachability analysis of nonlinear systems using conservative polynomialization and non-convex sets. In: Belta, C., Ivancic, F. (eds.) Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, HSCC 2013, Philadelphia, PA, USA, 8–11 April 2013, pp. 173–182. ACM (2013)

    Google Scholar 

  2. Althoff, M., Stursberg, O., Buss, M.: Reachability analysis of nonlinear systems with uncertain parameters using conservative linearization. In: Proceedings of the 47th IEEE Conference on Decision and Control, CDC 2008, Cancún, México, 9–11 December 2008, pp. 4042–4048. IEEE (2008)

    Google Scholar 

  3. Anai, H., Weispfenning, V.: Reach set computations using real quantifier elimination. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 63–76. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-45351-2_9

    Chapter  Google Scholar 

  4. Chen, X., Ábrahám, E., Sankaranarayanan, S.: Taylor model flowpipe construction for non-linear hybrid systems. In: Proceedings of the 33rd IEEE Real-Time Systems Symposium, RTSS 2012, San Juan, PR, USA, 4–7 December 2012, pp. 183–192. IEEE Computer Society (2012)

    Google Scholar 

  5. Chen, X., Sankaranarayanan, S., Ábrahám, E.: Under-approximate flowpipes for non-linear continuous systems. In: Formal Methods in Computer-Aided Design, FMCAD 2014, Lausanne, Switzerland, 21–24 October 2014, pp. 59–66. IEEE (2014)

    Google Scholar 

  6. Dreossi, T., Dang, T., Piazza, C.: Parallelotope bundles for polynomial reachability. In: Abate, A., Fainekos, G.E. (eds.) Proceedings of the 19th International Conference on Hybrid Systems: Computation and Control, HSCC 2016, Vienna, Austria, 12–14 April 2016, pp. 297–306. ACM (2016)

    Google Scholar 

  7. Duggirala, P.S., Mitra, S., Viswanathan, M.: Verification of annotated models from executions. In: Proceedings of the International Conference on Embedded Software, EMSOFT 2013, Montreal, QC, Canada, 29 September–4 October 2013, pp. 26:1–26:10. IEEE (2013)

    Google Scholar 

  8. Eggers, A., Ramdani, N., Nedialkov, N., Fränzle, M.: Improving SAT modulo ODE for hybrid systems analysis by combining different enclosure methods. In: Barthe, G., Pardo, A., Schneider, G. (eds.) SEFM 2011. LNCS, vol. 7041, pp. 172–187. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-24690-6_13

    Chapter  MATH  Google Scholar 

  9. Fan, C., Qi, B., Mitra, S., Viswanathan, M., Duggirala, P.S.: Automatic reachability analysis for nonlinear hybrid models with C2E2. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 531–538. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41528-4_29

    Chapter  Google Scholar 

  10. Frehse, G., Bogomolov, S., Greitschus, M., Strump, T., Podelski, A.: Eliminating spurious transitions in reachability with support functions. In: Girard, A., Sankaranarayanan, S. (eds.) Proceedings of the 18th International Conference on Hybrid Systems: Computation and Control, HSCC 2015, Seattle, WA, USA, 14–16 April 2015, pp. 149–158. ACM (2015)

    Google Scholar 

  11. Frehse, G., et al.: SpaceEx: scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379–395. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_30

    Chapter  Google Scholar 

  12. Frehse, G., Kateja, R., Le Guernic, C.: Flowpipe approximation and clustering in space-time. In: Proceedings of the 16th International Conference on Hybrid Systems: Computation and Control, HSCC 2013, pp. 203–212. ACM, New York (2013)

    Google Scholar 

  13. 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). https://doi.org/10.1007/11730637_21

    Chapter  MATH  Google Scholar 

  14. Girard, A., Pappas, G.J.: Verification using simulation. In: Hespanha, J.P., Tiwari, A. (eds.) HSCC 2006. LNCS, vol. 3927, pp. 272–286. Springer, Heidelberg (2006). https://doi.org/10.1007/11730637_22

    Chapter  Google Scholar 

  15. Goubault, E., Mullier, O., Putot, S., Kieffer, M.: Inner approximated reachability analysis. In: Fränzle, M., Lygeros, J. (eds.) 17th International Conference on Hybrid Systems: Computation and Control (part of CPS Week), HSCC 2014, Berlin, Germany, 15–17 April 2014, pp. 163–172. ACM (2014)

    Google Scholar 

  16. 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). https://doi.org/10.1007/978-3-642-02658-4_40

    Chapter  Google Scholar 

  17. Hamadeh, A.O., Goncalves, J.M.: Reachability analysis of continuous-time piecewise affine systems. Automatica 44(12), 3189–3194 (2008)

    Article  MathSciNet  Google Scholar 

  18. Huang, Z., Mitra, S.: Computing bounded reach sets from sampled simulation traces. In: Dang, T., Mitchell, I.M. (eds.) Hybrid Systems: Computation and Control (part of CPS Week 2012), HSCC 2012, Beijing, China, 17–19 April 2012, pp. 291–294. ACM (2012)

    Google Scholar 

  19. Isidori, A., Byrnes, C.I.: Output regulation of nonlinear systems. IEEE Trans. Autom. Control 35(2), 131–140 (1990)

    Article  MathSciNet  Google Scholar 

  20. Jones, D.R.: Direct global optimization algorithm. In: Floudas, C.A., Pardalos, P.M. (eds.) Encyclopedia of Optimization, 2nd edn, pp. 725–735. Springer, Boston (2009). https://doi.org/10.1007/978-0-387-74759-0

    Chapter  Google Scholar 

  21. Korda, M., Henrion, D., Jones, C.N.: Inner approximations of the region of attraction for polynomial dynamical systems. In: Tarbouriech, S., Krstic, M. (eds.) 9th IFAC Symposium on Nonlinear Control Systems, NOLCOS 2013, Toulouse, France, 4–6 September 2013, pp. 534–539. International Federation of Automatic Control (2013)

    Google Scholar 

  22. Kurzhanski, A.B., Varaiya, P.: On ellipsoidal techniques for reachability analysis. Part II: internal approximations box-valued constraints. Optim. Methods Softw. 17(2), 207–237 (2002)

    Article  MathSciNet  Google Scholar 

  23. Lal, R., Prabhakar, P.: Bounded error flowpipe computation of parameterized linear systems. In: Girault, A., Guan, N. (eds.) 2015 International Conference on Embedded Software, EMSOFT 2015, Amsterdam, Netherlands, 4–9 October 2015, pp. 237–246. IEEE (2015)

    Google Scholar 

  24. Lhommeau, M., Jaulin, L., Hardouin, L.: Inner and outer approximation of capture basin using interval analysis. In: Zaytoon, J., Ferrier, J., Andrade-Cetto, J., Filipe, J. (eds.) Proceedings of the Fourth International Conference on Informatics in Control, Automation and Robotics, Signal Processing, Systems Modeling and Control, ICINCO 2007, Angers, France, 9–12 May 2007, pp. 5–9. INSTICC Press (2007)

    Google Scholar 

  25. Maidens, J.N., Kaynama, S., Mitchell, I.M., Oishi, M.M.K., Dumont, G.A.: Lagrangian methods for approximating the viability kernel in high-dimensional systems. Automatica 49(7), 2017–2029 (2013)

    Article  MathSciNet  Google Scholar 

  26. Mitchell, I.M.: The flexible, extensible and efficient toolbox of level set methods. J. Sci. Comput. 35(2), 300–329 (2008)

    Article  MathSciNet  Google Scholar 

  27. Mitsch, S., Ghorbal, K., Vogelbacher, D., Platzer, A.: Formal verification of obstacle avoidance and navigation of ground robots. CoRR, abs/1605.00604 (2016)

    Google Scholar 

  28. Nghiem, T., Sankaranarayanan, S., Fainekos, G.E., Ivancic, F., Gupta, A., Pappas, G.J.: Monte-carlo techniques for falsification of temporal properties of non-linear hybrid systems. In: Johansson, K.H., Yi, W. (eds.) Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2010, Stockholm, Sweden, 12–15 April 2010, pp. 211–220. ACM (2010)

    Google Scholar 

  29. Plaku, E., Kavraki, L.E., Vardi, M.Y.: Hybrid systems: from verification to falsification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 463–476. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-73368-3_48

    Chapter  MATH  Google Scholar 

  30. Prabhakar, P., Duggirala, P.S., Mitra, S., Viswanathan, M.: Hybrid automata-based CEGAR for rectangular hybrid systems. Formal Methods Syst. Des. 46(2), 105–134 (2015)

    Article  Google Scholar 

  31. Prajna, S., Jadbabaie, A.: Safety verification of hybrid systems using barrier certificates. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 477–492. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-24743-2_32

    Chapter  MATH  Google Scholar 

  32. Ratschan, S., She, Z.: Safety verification of hybrid systems by constraint propagation-based abstraction refinement. ACM Trans. Embedded Comput. Syst. 6(1), 1–23 (2007). Article No. 8

    Google Scholar 

  33. Sankaranarayanan, S.: Automatic abstraction of non-linear systems using change of bases transformations. In: Caccamo, M., Frazzoli, E., Grosu, R. (eds.) Proceedings of the 14th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2011, Chicago, IL, USA, 12–14 April 2011, pp. 143–152. ACM (2011)

    Google Scholar 

  34. 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). https://doi.org/10.1007/978-3-540-24743-2_40

    Chapter  MATH  Google Scholar 

  35. Wang, T.C., Lall, S., West, M.: Polynomial level-set method for polynomial system reachable set estimation. IEEE Trans. Autom. Control 58(10), 2508–2521 (2013)

    Article  MathSciNet  Google Scholar 

  36. Xue, B., Fränzle, M., Zhan, N.: Under-approximating reach sets for polynomial continuous systems. In: Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (Part of CPS Week), HSCC 2018, pp. 51–60. ACM, New York (2018)

    Google Scholar 

  37. Xue, B., She, Z., Easwaran, A.: Under-approximating backward reachable sets by polytopes. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 457–476. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41528-4_25

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. School of Mathematics and Systems Science, Beihang University, Beijing, China

    Meilun Li & Zhikun She

  2. Department of Computing Science, Carl von Ossietzky Universität Oldenburg, Oldenburg, Germany

    Peter N. Mosaad & Martin Fränzle

  3. State Key Laboratory of Computer Science, Institute of Software, CAS, Beijing, China

    Bai Xue

Authors
  1. Meilun Li
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Peter N. Mosaad
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Martin Fränzle
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Zhikun She
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Bai Xue
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Zhikun She .

Editor information

Editors and Affiliations

  1. Institute of Software, Chinese Academy of Sciences, Beijing, China

    David N. Jansen

  2. Kansas State University, Manhattan, Kansas, USA

    Pavithra Prabhakar

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Li, M., Mosaad, P.N., Fränzle, M., She, Z., Xue, B. (2018). Safe Over- and Under-Approximation of Reachable Sets for Autonomous Dynamical Systems. In: Jansen, D., Prabhakar, P. (eds) Formal Modeling and Analysis of Timed Systems. FORMATS 2018. Lecture Notes in Computer Science(), vol 11022. Springer, Cham. https://doi.org/10.1007/978-3-030-00151-3_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-00151-3_15

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-00150-6

  • Online ISBN: 978-3-030-00151-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation