Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Formal Techniques for Safety-Critical Systems

FTSCS 2013: Formal Techniques for Safety-Critical Systems pp 88–106Cite as

Counterexample Generation for Hybrid Automata

  • Conference paper
  • First Online:

Part of the book series: Communications in Computer and Information Science ((CCIS,volume 419))

Abstract

The last decade brought us a whole range of over-approximative algorithms for the reachability analysis of hybrid automata, a widely used modeling language for systems with combined discrete-continuous behavior. Besides theoretical results, there are also some tools available for proving safety in the continuous time domain. However, if a given set of critical states is found to be reachable, these tools do not provide counterexamples for models beyond timed automata.

This paper investigates the question whether and how available tools can be used to generate counterexamples, even if this functionality is not directly supported. Using the tools SpaceEx and Flow*, we discuss possibilities to solve our task with and without modifying the tools’ source code, report on the effort and the efficiency of implementation, and propose a simulation-based approach for the validation of the resulting (possibly spurious) counterexamples.

The original publication is available at http://www.springerlink.com.

This work is supported by the DFG research training group AlgoSyn and the DFG research project HyPro.

This is a preview of subscription content, 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

Learn about institutional subscriptions

References

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

    Article  MATH  Google Scholar 

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

    Google Scholar 

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

    Google Scholar 

  4. Stursberg, O., Krogh, B.H.: 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)

    Google Scholar 

  5. Chutinan, A., Krogh, B.H.: Computing polyhedral approximations to flow pipes for dynamic systems. In: Proceedings of CDC’98, vol. 2, pp. 2089–2094. IEEE Press (1998)

    Google Scholar 

  6. Henzinger, T.A., Ho, P., Wong-Toi, H.: HyTech: a model checker for hybrid systems. Softw. Tools Technol. Transfer 1, 110–122 (1997)

    Article  MATH  Google Scholar 

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

    Google Scholar 

  8. Kvasnica, M., Grieder, P., Baotić, M.: Multi-parametric toolbox (MPT). http://control.ee.ethz.ch/~mpt/ (2004)

  9. Chen, X., Ábrahám, E.: Choice of directions for the approximation of reachable sets for hybrid systems. In: Moreno-Díaz, R., Pichler, F., Quesada-Arencibia, A. (eds.) EUROCAST 2011, Part I. LNCS, vol. 6927, pp. 535–542. Springer, Heidelberg (2012)

    Google Scholar 

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

    Chapter  Google Scholar 

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

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

  13. Kurzhanski, A.B., Varaiya, P.: On ellipsoidal techniques for reachability analysis. Optim. Meth. Softw. 17, 177–237 (2000)

    Article  MathSciNet  Google Scholar 

  14. Le Guernic, C.: Reachability analysis of hybrid systems with linear continuous dynamics. Ph.D. thesis, Université Joseph Fourier (2009)

    Google Scholar 

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

    Google Scholar 

  16. Chen, X., Ábrahám, E., Sankaranarayanan, S.: Taylor model flowpipe construction for non-linear hybrid systems. In: Proceedings of RTSS’12, pp. 183–192. IEEE Computer Society (2012)

    Google Scholar 

  17. Collins, P., Bresolin, D., Geretti, L., Villa, T.: Computing the evolution of hybrid systems using rigorous function calculus. In: Proceedings of ADHS’12, IFAC-PapersOnLine (2012)

    Google Scholar 

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

    Google Scholar 

  19. Asarin, E., Dang, T., Maler, O.: The \({\bf {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)

    Google Scholar 

  20. Girard, A., Pappas, G.J.: Approximation metrics for discrete and continuous systems. IEEE Trans. Autom. Control 52, 782–798 (2007)

    Article  MathSciNet  Google Scholar 

  21. Kurzhanskiy, A., Varaiya, P.: Ellipsoidal toolbox. Technical report, EECS, UC Berkeley (2006)

    Google Scholar 

  22. Balluchi, A., Casagrande, A., Collins, P., Ferrari, A., Villa, T., Sangiovanni-Vincentelli, A.L.: Ariadne: A framework for reachability analysis of hybrid automata. In: Proceedings of MTNS’06 (2006)

    Google Scholar 

  23. Prabhakar, P., Duggirala, P.S., Mitra, S., Viswanathan, M.: Hybrid automata-based CEGAR for rectangular hybrid systems. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 48–67. Springer, Heidelberg (2013)

    Google Scholar 

  24. Duggirala, P.S., Mitra, S.: Abstraction refinement for stability. In: Proceedings of ICCPS’11, pp. 22–31. IEEE (2011)

    Google Scholar 

  25. Fehnker, A., Ivančić, F.: Benchmarks for hybrid systems verification. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 326–341. Springer, Heidelberg (2004)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. RWTH Aachen University, Aachen, Germany

    Johanna Nellen, Erika Ábrahám & Xin Chen

  2. Maastricht University, Maastricht, The Netherlands

    Pieter Collins

Authors
  1. Johanna Nellen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Erika Ábrahám
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Xin Chen
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Pieter Collins
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Erika Ábrahám .

Editor information

Editors and Affiliations

  1. AIST, Research Institute for Secure Systems, Amagasaki, Japan

    Cyrille Artho

  2. University of Oslo Department of Informatics, Oslo, Norway

    Peter Csaba Ölveczky

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Nellen, J., Ábrahám, E., Chen, X., Collins, P. (2014). Counterexample Generation for Hybrid Automata. In: Artho, C., Ölveczky, P. (eds) Formal Techniques for Safety-Critical Systems. FTSCS 2013. Communications in Computer and Information Science, vol 419. Springer, Cham. https://doi.org/10.1007/978-3-319-05416-2_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-05416-2_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-05415-5

  • Online ISBN: 978-3-319-05416-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation