Skip to main content
SpringerLink
Log in

Abstractions of Hybrid Systems for Verification

  • Conference paper
Informatics in Control Automation and Robotics

Part of the book series: Lecture Notes in Electrical Engineering ((LNEE,volume 85))

  • 866 Accesses

Abstract

Safety verification for hybrid systems is a very important issue but also a very complex one. The abstraction is a mean to simplify it by shifting from global considerations to local ones. The aim of this paper is to present an overview of techniques of abstraction of hybrid systems that are commonly used for safety analysis. Reachability approaches related to abstraction for verification are briefly presented.

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 169.00
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 219.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info
Hardcover Book
USD 219.99
Price excludes VAT (USA)
  • Durable hardcover 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. Guéguen, H., Zaytoon, J.: On the formal verification of hybrid systems. Control Engineering Practice 12, 1253–1268 (2004)

    Article  Google Scholar 

  2. Guéguen, H., Lefebvre, M., Zaytoon, J., Nasri, O.: Safety verification and reachability analysis for hybrid systems. Annual Reviews in Control 33, 25–36 (2009)

    Article  Google Scholar 

  3. Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T., Ho, P., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoretical Computer Science 138, 3–34 (1995)

    Article  MathSciNet  MATH  Google Scholar 

  4. Henzinger, T.A., Ho, P., Wong-Toi, H.: Algorithmic analysis of nonlinear hybrid systems. IEEE Trans. on Automatic Control 43, 540–554 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  5. Lefebvre, M., Guéguen, H.: Hybrid abstractions of affine systems. NonLinear Analysis: Theory and Methods 65, 1150–1167 (2006)

    Article  MATH  Google Scholar 

  6. Nasri, O., Lefebvre, M., Gueguen, H.: Abstraction based reachability computation for affine systems with bounded input. In: CDC Conference on Decision and Control, pp. 2609–2613. IEEE, Los Alamitos (2006)

    Google Scholar 

  7. Alur, R., Henzinger, T., Laferriere, G., Pappas, J.: Discrete abstractions of hybrid systems. Proceedings of IEEE 88, 971–984 (2000)

    Article  Google Scholar 

  8. Chutinan, A., Krogh, B.: Computation techniques for hybrid systems verification. IEEE Trans. on Automatic Control 48, 64–75 (2003)

    Article  MathSciNet  Google Scholar 

  9. Chutinan, A., Krogh, B.: Verification of infinite-state dynamic systems using approximate quotient transition systems. IEEE Trans. on Automatic Control 46, 1401–1410 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  10. Tabuada, P., Pappas, G., Lima, P.: Composing abstractions of hybrid systems. In: Tomlin, C.J., Greenstreet, M.R. (eds.) HSCC 2002. LNCS, vol. 2289, pp. 436–450. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  11. Alur, R., Ivancic, F., Dang, T.: Progress on reachability analysis of hybrid systems using predicate abstraction. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 4–19. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  12. Fehnker, A., Clarke, E., Jha, S., Krogh, B.: Refining abstractions of hybrid systems using counterexample fragments. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 242–257. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  13. 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 

  14. Alur, R., Dang, T., Ivancic, F.: Reachability analysis of hybrid systems via predicate abstraction. In: Tomlin, C.J., Greenstreet, M.R. (eds.) HSCC 2002. LNCS, vol. 2289, pp. 35–48. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  15. Ratschan, S., She, Z.: Safety verification of hybrid systems by constraint propagation based abstraction refinement. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 573–589. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  16. Blouin, S., Guay, M., Rudie, K.: Discrete abstractions for two dimensional nearly integrable continuous systems. In: Engel, S., Guéguen, H., Zaytoon, J. (eds.) ADHS 2003: IFAC Conference on Analysis and Design of Hybrid Systems, Saint-Malo, France, pp. 343–348. Elsevier, Amsterdam (2003)

    Google Scholar 

  17. 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 

  18. Tiwari, A.: Approximate reachability for linear systems. In: Maler, O., Pnueli, A. (eds.) HSCC 2003. LNCS, vol. 2623, pp. 514–525. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  19. Rodriguez-Carbonell, E., Tiwari, A.: Generating polynomial invariance for hybrid systems. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 590–605. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  20. Prajna, S., Jadbabaie, A., Pappas, G.: A framework for worst-cas and stochastic safety verification using barrier certificates. IEEE Transactions on Automatic control 52, 1415–1428 (2007)

    Article  MathSciNet  Google Scholar 

  21. Yazarel, H., Pappas, G.: Geometric programming relaxations for linear systems reachability. In: American Control Conference, pp. 553–559 (2004)

    Google Scholar 

  22. Yazarel, H., Prajna, S., Pappas, G.J.: Sos for safety. In: 43rd IEEE CDC, pp. 461–466 (2004)

    Google Scholar 

  23. Lohner, R.: Enclosing the solutions of ordinary initial and boundary value problems. In: Computer Arithmethic: Scientific Computation and Programming Languages. Wiley-Teubner Series in Computer Science, pp. 255–286 (1987)

    Google Scholar 

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

    Chapter  Google Scholar 

  25. Asarin, E., Dang, T., Frehse, G., Girard, A., Guernic, C.L., Maler, O.: Recent progress in continuous and hybrid reachability analysis. In: CACSD 2006, Munich, Germany (2006)

    Google Scholar 

  26. Hickey, T., Wittenberg, D.: Rigourous modelling of hybrid systems using interval arithmetic constraints. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 402–416. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  27. 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 

  28. Kurzhanski, A., Variya, P.: Ellipsoïdal techniques for reachability analysis. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 202–214. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

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

    Article  MathSciNet  MATH  Google Scholar 

  30. Kühn, W.: Zonotope dynamics in numerical quality control. In: Hege, H.C., Polthier, K. (eds.) Mathematical Visualization, pp. 125–134. Springer, Heidelberg (1998)

    Google Scholar 

  31. Bagnara, R., Ricci, E., Zaffanella, E., Hill, P.: Possibly not closed convex polyhedra and the parma polyhedra library. In: Hermenegildo, M., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 213–229. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

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

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. SUPELEC / IETR, Rennes, France

    Hervé Guéguen

  2. Université de Reims Champagne Ardenne / CRESTIC, Reims, France

    Janan Zaytoon

Authors
  1. Hervé Guéguen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Janan Zaytoon
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institut de Robòtica i Informàtica Industrial, Consejo Superior de Investigaciones Científicas / Universidad Politècnica de Catalunya , Llorens i Artigas, 4-6 Edifici U, 08028, Barcelona, Spain

    Juan Andrade Cetto

  2. Polytechnic Institute of Setúbal / INSTICC , 2910-595, Setubal, Portugal

    Joaquim Filipe

  3. Institut des Sciences et Techniques de l’Ingénieur d’Angers (ISTIA), Labo. d’Ingénierie des Systémes Automatisés (LISA) , 62 avenue Notre Dame du Lac, 49000, Angers, France

    Jean-Louis Ferrier

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Guéguen, H., Zaytoon, J. (2011). Abstractions of Hybrid Systems for Verification. In: Cetto, J.A., Filipe, J., Ferrier, JL. (eds) Informatics in Control Automation and Robotics. Lecture Notes in Electrical Engineering, vol 85. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-19730-7_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-19730-7_2

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-19729-1

  • Online ISBN: 978-3-642-19730-7

  • eBook Packages: EngineeringEngineering (R0)

Publish with us

Policies and ethics

Search

Navigation