Advertisement

Reachability Analysis of Hybrid Systems Using Symbolic Orthogonal Projections

  • Willem Hagemann
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8559)

Abstract

This paper deals with reachability analysis of hybrid systems with continuous dynamics described by linear differential inclusions and arbitrary linear maps for discrete updates. The invariants, guards, and sets of reachable states are given as convex polyhedra. Our reachability algorithm is based on a novel representation class for convex polyhedra, the symbolic orthogonal projections (sops), on which various geometric operations, including convex hulls, Minkowski sums, linear maps, and intersections, can be performed efficiently and exactly. The capability to represent intersections of convex polyhedra exactly is superior to support function-based approaches like the LGG-algorithm (Le Guernic and Girard [21]).

Accompanied by some simple examples, we address the problem of the monotonic growth of the exact representation and propose a combination of our reachability algorithm with the LGG-algorithm. This results in an efficient method of better accuracy than the LGG-algorithm and its productive implementation in SpaceEx [13].

Keywords

Convex Hull Hybrid System Support Function Reachable State Implicit Equality 
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.

References

  1. 1.
    Althoff, M., Krogh, B.H.: Avoiding geometric intersection operations in reachability analysis of hybrid systems. In: Proceedings of the 15th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2012, pp. 45–54. ACM, New York (2012)Google Scholar
  2. 2.
    Asarin, E., Dang, T., Girard, A.: Reachability analysis of nonlinear systems using conservative approximation. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 20–35. Springer, Heidelberg (2003)Google Scholar
  3. 3.
    Asarin, E., Dang, T., Girard, A.: Hybridization methods for the analysis of nonlinear systems. Acta Informatica 43(7), 451–476 (2007)CrossRefzbMATHMathSciNetGoogle Scholar
  4. 4.
    Asarin, E., Dang, T., Maler, O.: The d/dt tool for verification of hybrid systems. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 365–370. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  5. 5.
    Bournez, O., Maler, O., Pnueli, A.: Orthogonal polyhedra: Representation and computation. In: Vaandrager, F.W., van Schuppen, J.H. (eds.) HSCC 1999. LNCS, vol. 1569, pp. 46–60. Springer, Heidelberg (1999)Google Scholar
  6. 6.
    Chen, X., Ábrahám, E., Sankaranarayanan, S.: Flow*: An analyzer for non-linear hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 258–263. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  7. 7.
    Chutinan, A., Krogh, B.: Computational techniques for hybrid system verification. IEEE Transactions on Automatic Control 48(1), 64–75 (2003)CrossRefMathSciNetGoogle Scholar
  8. 8.
    Chutinan, A., Krogh, B.H.: Computing polyhedral approximations to flow pipes for dynamic systems. In: Proceedings of the 37th IEEE Conference on Decision and Control, 1998, vol. 2, pp. 2089–2094 (December 1998)Google Scholar
  9. 9.
    Damm, W., Dierks, H., Disch, S., Hagemann, W., Pigorsch, F., Scholl, C., Waldmann, U., Wirtz, B.: Exact and fully symbolic verification of linear hybrid automata with large discrete state spaces. Science of Computer Programming 77(10-11), 1122–1150 (2012), aVoCS 2009Google Scholar
  10. 10.
    Damm, W., Hagemann, W., Möhlmann, E., Rakow, A.: Component based design of hybrid systems: A case study on concurrency and coupling. Reports of SFB/TR 14 AVACS 95, SFB/TR 14 AVACS (2014), http://www.avacs.org, ISSN: 1860-9821
  11. 11.
    Damm, W., Möhlmann, E., Rakow, A.: Component based design of hybrid systems: A case study on concurrency and coupling. In: Proceedings of the 17th International Conference on Hybrid Systems: Computation and Control, HSCC 2014, pp. 145–150. ACM, New York (2014)Google Scholar
  12. 12.
    Dang, T., Maler, O., Testylier, R.: Accurate hybridization of nonlinear systems. In: Proceedings of the 13th ACM International Conference on Hybrid Systems: Computation and Control, HSCC 2010, pp. 11–20. ACM, New York (2010)Google Scholar
  13. 13.
    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)CrossRefGoogle Scholar
  14. 14.
    Fukuda, K.: Lecture: Polyhedral computation, spring 2011 (2011), http://stat.ethz.ch/ifor/teaching/lectures/poly_comp_ss11/lecture_notes
  15. 15.
    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)Google Scholar
  16. 16.
    Girard, A., Le Guernic, C.: Zonotope/hyperplane intersection for hybrid systems reachability analysis. In: Egerstedt, M., Mishra, B. (eds.) HSCC 2008. LNCS, vol. 4981, pp. 215–228. Springer, Heidelberg (2008)Google Scholar
  17. 17.
    Hagemann, W.: Reachability analysis of hybrid systems using symbolic orthogonal projections. Reports of SFB/TR 14 AVACS 98, SFB/TR 14 AVACS (2014), http://www.avacs.org, ISSN: 1860-9821
  18. 18.
    Henzinger, T.A., Ho, P.H., Wong-Toi, H.: Hytech: Amodel checker for hybrid systems. International Journal on Software Tools for Technology Transfer 1(1-2), 110–122 (1997)CrossRefzbMATHGoogle Scholar
  19. 19.
    Kurzhanski, A.B., Varaiya, P.: Ellipsoidal techniques for reachability analysis. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 202–214. Springer, Heidelberg (2000)Google Scholar
  20. 20.
    Le Guernic, C.: Reachability analysis of hybrid systems with linear continuous dynamics. Ph.D. thesis, Université Grenoble 1 - Joseph Fourier (2009)Google Scholar
  21. 21.
    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)CrossRefGoogle Scholar
  22. 22.
    Prabhakar, P., Viswanathan, M.: A dynamic algorithm for approximate flow computations. In: Proceedings of the 14th International Conference on Hybrid Systems: Computation and Control, HSCC 2011, pp. 133–142. ACM, New York (2011)Google Scholar
  23. 23.
    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)CrossRefGoogle Scholar
  24. 24.
    Schrijver, A.: Theory of Linear and Integer Programming. John Wiley & Sons, Chichester (1986)zbMATHGoogle Scholar
  25. 25.
    Tiwary, H.R.: On the hardness of computing intersection, union and Minkowski sum of polytopes. Discrete & Computational Geometry 40(3), 469–479 (2008)CrossRefzbMATHMathSciNetGoogle Scholar
  26. 26.
    Ziegler, G.M.: Lectures on polytopes, vol. 152. Springer (1995)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Willem Hagemann
    • 1
  1. 1.Carl von Ossietzky Universität OldenburgOldenburgGermany

Personalised recommendations