Skip to main content
SpringerLink
Log in

Language-Based Abstraction Refinement for Hybrid System Verification

  • Conference paper
Verification, Model Checking, and Abstract Interpretation (VMCAI 2007)

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

Abstract

The standard counterexample-guided abstraction-refinement (cegar) approach uses finite transition systems as abstractions of concrete systems. We present an approach to represent and refine abstractions of infinite-state systems that uses regular languages instead of finite transition systems. The advantage of using languages over transition systems is that we can store more fine-grained information in the abstraction and thus reduce the number of abstract states. Based on this language-based approach for cegar, we present new abstraction-refinement algorithms for hybrid system verification. Moreover, we evaluate our approach by verifying various non-linear hybrid systems.

This work was partly supported by the German Research Foundation (DFG) and the Swiss National Science Foundation (SNF).

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alur, R., Dang, T., Ivančić, F.: Predicate abstraction for reachability analysis of hybrid systems. ACM Trans. Embedded Comput. Syst. 5(1), 152–199 (2006)

    Article  Google Scholar 

  2. Asarin, E., Schneider, G., Yovine, S.: On the decidability of the reachability problem for planar differential inclusions. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 89–104. Springer, Heidelberg (2001)

    Google Scholar 

  3. Brihaye, T., Michaux, C.: On the expressiveness and decidability of o-minimal hybrid systems. J. Complexity 21(4), 447–478 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  4. Brihaye, T., et al.: On o-minimal hybrid systems. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 219–233. Springer, Heidelberg (2004)

    Google Scholar 

  5. Clarke, E., et al.: Abstraction and counterexample-guided refinement in model checking of hybrid systems. Internat. J. Found. Comput. Sci. 14(4), 583–604 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  6. Clarke, E., et al.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752–794 (2003)

    Article  MathSciNet  Google Scholar 

  7. Dams, D.: Comparing abstraction refinement algorithms. In: Proc. of 2nd Workshop on Software Model Checking (SoftMC’03), Electr. Notes Theor. Comput. Sci. 89(3), 405–416 (2003)

    Google Scholar 

  8. Davis, E.: Constraint propagation with interval labels. Artif. Intell. 32(3), 281–331 (1987)

    Article  MATH  Google Scholar 

  9. Doyen, L., Henzinger, T.A., Raskin, J.-F.: Automatic rectangular refinement of affine hybrid systems. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 144–161. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  10. Fehnker, A., et al.: 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)

    Google Scholar 

  11. Fränzle, M.: Analysis of hybrid systems: An ounce of realism can save an infinity of states. In: Flum, J., Rodríguez-Artalejo, M. (eds.) CSL 1999. LNCS, vol. 1683, pp. 126–140. Springer, Heidelberg (1999)

    Google Scholar 

  12. Henzinger, T.A., et al.: What’s decidable about hybrid automata. J. Comput. System Sci. 57, 94–124 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  13. Klarlund, N., Møller, A., Schwartzbach, M.I.: MONA implementation secrets. Internat. J. Found. Comput. Sci. 13(4), 571–586 (2002)

    Article  MATH  MathSciNet  Google Scholar 

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

  15. Ratschan, S.: RSolver. http://rsolver.sourceforge.net . Software package

  16. Ratschan, S.: Continuous first-order constraint satisfaction. In: Calmet, J., et al. (eds.) AISC 2002 and Calculemus 2002. LNCS (LNAI), vol. 2385, pp. 181–195. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  17. Ratschan, S., She, Z.: Safety verification of hybrid systems by constraint propagation based abstraction refinement. ACM Trans. Embedded Comput. Syst. (to appear)

    Google Scholar 

  18. Ratschan, S., She, Z.: HSolver, http://hsolver.sourceforge.net . Software package

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

    Google Scholar 

  20. Ratschan, S., She, Z.: Constraints for continuous reachability in the verification of hybrid systems. In: Calmet, J., Ida, T., Wang, D. (eds.) AISC 2006. LNCS (LNAI), vol. 4120, pp. 196–210. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. ETH Zurich, Computer Science Department, Zurich, Switzerland

    Felix Klaedtke

  2. Institute of Computer Science, Czech Academy of Sciences, Prague, Czech Republic

    Stefan Ratschan

  3. Max-Planck-Institut für Informatik, Saarbrücken, Germany

    Zhikun She

Authors
  1. Felix Klaedtke
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Stefan Ratschan
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Zhikun She
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Byron Cook Andreas Podelski

Rights and permissions

Reprints and permissions

Copyright information

© 2007 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Klaedtke, F., Ratschan, S., She, Z. (2007). Language-Based Abstraction Refinement for Hybrid System Verification. In: Cook, B., Podelski, A. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2007. Lecture Notes in Computer Science, vol 4349. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-69738-1_11

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-69738-1_11

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-69735-0

  • Online ISBN: 978-3-540-69738-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation