Reachability Analysis of Hybrid Systems Using Support Functions

  • Colas Le Guernic
  • Antoine Girard
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5643)


This paper deals with conservative reachability analysis of a class of hybrid systems with continuous dynamics described by linear differential inclusions, convex invariants and guards, and linear reset maps. We present an approach for computing over-approximations of the set of reachable states. It is based on the notion of support function and thus it allows us to consider invariants, guards and constraints on continuous inputs and initial states defined by arbitrary compact convex sets. We show how the properties of support functions make it possible to derive an effective algorithm for approximate reachability analysis of hybrid systems. We use our approach on some examples including the navigation benchmark for hybrid systems verification.


Hybrid System Support Function Hybrid Automaton Reachability Analysis Continuous Dynamic 
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.


  1. 1.
    Chutinan, A., Krogh, B.: 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
  2. 2.
    Asarin, E., Dang, T., Maler, O., Bournez, O.: Approximate reachability analysis of piecewise-linear dynamical systems. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 20–31. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  3. 3.
    Kurzhanski, A., 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)CrossRefGoogle Scholar
  4. 4.
    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
  5. 5.
    Stursberg, O., Krogh, B.: 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
  6. 6.
    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
  7. 7.
    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
  8. 8.
    Varaiya, P.: Reach set computation using optimal control. In: Proc. KIT Workshop on Verification of Hybrid Systems, Grenoble (1998)Google Scholar
  9. 9.
    Le Guernic, C., Girard, A.: Reachability analysis of linear systems using support functions. Nonlinear Analysis: Hybrid Systems (2009) (to appear)Google Scholar
  10. 10.
    Fehnker, A., Ivancic, F.: Benchmarks for hybrid systems verification. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 326–341. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  11. 11.
    Bertsekas, D., Nedic, A., Ozdaglar, A.: Convex analysis and optimization. Athena Scientific (2003)Google Scholar
  12. 12.
    Boyd, S., Vandenberghe, L.: Convex optimization. Cambridge University Press, Cambridge (2004)CrossRefzbMATHGoogle Scholar
  13. 13.
    Rockafellar, R., Wets, R.: Variational analysis. Springer, Heidelberg (1998)CrossRefzbMATHGoogle Scholar
  14. 14.
    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)CrossRefGoogle Scholar
  15. 15.
    Kiefer, J.: Sequential minimax search for a maximum. Proceedings of the American Mathematical Society 4, 502–506 (1953)MathSciNetCrossRefzbMATHGoogle Scholar
  16. 16.
    Frehse, G.: PHAVer: algorithmic verification of hybrid systems past HyTech. Int. J. on Software Tools for Technology Transfer 10(3), 263–279 (2008)MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Colas Le Guernic
    • 1
  • Antoine Girard
    • 2
  1. 1.Verimag, Université de GrenobleFrance
  2. 2.Laboratoire Jean KuntzmannUniversité de GrenobleFrance

Personalised recommendations