Skip to main content
SpringerLink
Log in

Hybrid automata-based CEGAR for rectangular hybrid systems

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

Abstract

In this paper, we present a counterexample guided abstraction refinement (CEGAR) framework for systems modelled as rectangular hybrid automata. The main difference, between our approach and previous proposals for CEGAR for hybrid automata, is that we consider the abstractions to be hybrid automata as well, as opposed to finite state systems. We show that the CEGAR scheme is semi-complete for the class of rectangular hybrid automata and complete for the subclass of initialized rectangular automata. We have implemented the CEGAR based algorithm in a tool called Hare, that makes calls to HyTech to analyze the abstract models and validate the counterexamples. The experimental evaluations demonstrate the merits of the approach.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10
Fig. 11

Similar content being viewed by others

References

  1. Clarke EM, Grumberg O, Jha S, Lu Y, Veith H (2000) Counterexample-guided abstraction refinement. In: Proceedings of the 12th international conference on computer aided verification, vol 1855 of Lecture Notes in Computer Science. pp 154–169

  2. Ball T, Rajamani S (2000) Bebop: a symbolic model checker for Boolean programs. In: Proceedings of the 7th international SPIN, pp 113–130

  3. Corbett J, Dwyer M, Hatcliff J, Laubach S, Robby C. Pasareanu, Zheng H (2000) Bandera: extracting finite-state models from Java source code. In: Proceedings of ICSE. pp 439–448

  4. Henzinger TA, Jhala R, Majumdar R, Sutre G (2002) Lazy Abstraction. In: Proceedings of 29th ACM symposium on principles of programming languages (POPL’02). pp 58–70

  5. Holzmann G, Smith M (2000) Automating software feature verification. Bell Labs Tech J 5(2):72–87

    Article  Google Scholar 

  6. Alur R, Dang T, Ivancic F (2003) Counter-example guided predicate abstraction of hybrid systems. In: Proceedings of TACAS 2003. pp 208–223

  7. Clarke EM, Fehnker A, Han Z, Krogh B, Ouaknine J, Stursberg O, Theobald M (2003) Abstraction and counterexample-guided refinement in model checking of hybrid systems. JFCS 14(4):583–604

    MATH  MathSciNet  Google Scholar 

  8. Clarke E.M., Fehnker A, Han Z, Krogh B, Ouaknine J, Stursberg O, Theobald M (2003) Verification of hybrid systems based on counterexmple-guided abstraction refinement. In: Proceedings of TACAS. pp 192–207

  9. Dierks H, Kupferschmid S, Larsen KG (2007) Automatic Abstraction refinement for timed automata. In: Proceedings of FORMATS. pp 114–129

  10. Fehnker A, Clarke EM, Jha S, Krogh B (2005) Refining abstractions of hybrid systems using counterexample fragments. In: Proceedings of HSCC 2005. pp 242–257

  11. Segelken M (2007) Abstraction and Counterexample-guided construction of omega-automata for model checking of step-discrete linear hybrid models. In: Proceedings of CAV. pp 433–448

  12. Sorea M (2004) Lazy approximation for dense real-time systems. In: Proceedings of FORMATS/FTRFTS. pp 363–378

  13. Ratschan S, She Z (2007) Safety verification of hybrid systems by constraint propagation based abstraction refinement. ACM Trans Embed Comput Syst 6(1):8

  14. Graf S, Saidi H (1997) Construction of abstact state graphs with PVS. In: Proceedings of CAV, pp 72–83

  15. Jha SK, Krogh BH, Weimer JE, Clarke EM (2007) Reachability for linear hybrid automata using iterative relaxation abstraction. In: Proceedings of HSCC 2007, pp 287–300

  16. Henzinger TA (1996) The theory of hybrid automata. In: LICS, pp 278–292

  17. Hybrid abstraction refinement engine (HARE) (2013). In: http://publish.illinois.edu/hare-tool/

  18. Henzinger TA, Ho P-H, Howard W-T (1997) Hytech: a model checker for hybrid systems. In: Proceedings of CAV. pp 460–483

  19. Frehse G (2005) Phaver: algorithmic verification of hybrid systems past hytech. In: Proceedings of HSCC. pp 258–273

  20. Frehse G, Le Guernic C, Donzé A, Cotton S, Ray R, Lebeltel O, Ripado R, Girard A, Dang T, Maler O (2011) SpaceEx: scalable verification of hybrid systems. In Proceedings of CAV

  21. Asarin E, Dang T, Maler O (2002) The d/dt tool for verification of hybrid system

  22. Prabhakar P, Duggirala PS, Mitra S, Viswanathan M (2013) Hybrid automata-based cegar for rectangular hybrid systems. In: Proceedings of VMCAI. pp 48–67

  23. Doyen L, Henzinger TA, Raskin J-F (2005) Automatic rectangular refinement of affine hybrid systems. In: Proceedings of FORMATS05, vol 3829 in LNCS. pp 144–161

  24. Henzinger TA, Kopke PW, Puri A, Varaiya P (1995) What’s decidable about hybrid automata? In: Proceedings of STOC. pp 373–382

  25. Alur Rajeev, Courcoubetis Costas, Halbwachs Nicolas, Henzinger Thomas A, Ho P-H, Nicollin Xavier, Olivero Alfredo, Sifakis Joseph, Yovine Sergio (1995) The algorithmic analysis of hybrid systems. TCS 138(1):3–34

    Article  MATH  Google Scholar 

  26. Fehnker A, Ivancic F (2004) Benchmarks for hybrid systems verification. pp 326–341

  27. Munoz CA, Dowek G, Carreo V (2004) Modeling and verification of an air traffic concept of operations. In: ISSTA, pp 175–182

  28. Dutertre B, Sorea M (2004) Timed systems in SAL. Technical report, Computer Science Laboratory

Download references

Author information

Authors and Affiliations

  1. IMDEA Software Institute, Pozuelo de Alarcon, Madrid, Spain

    Pavithra Prabhakar

  2. University of Illinois at Urbana-Champaign, Champaign, USA

    Parasara Sridhar Duggirala, Sayan Mitra & Mahesh Viswanathan

Authors
  1. Pavithra Prabhakar
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Parasara Sridhar Duggirala
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Sayan Mitra
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Mahesh Viswanathan
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Pavithra Prabhakar.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Prabhakar, P., Duggirala, P.S., Mitra, S. et al. Hybrid automata-based CEGAR for rectangular hybrid systems. Form Methods Syst Des 46, 105–134 (2015). https://doi.org/10.1007/s10703-015-0225-4

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10703-015-0225-4

Keywords

Search

Navigation