Advertisement

Language-Based Abstraction Refinement for Hybrid System Verification

  • Felix Klaedtke
  • Stefan Ratschan
  • Zhikun She
Part of the Lecture Notes in Computer Science book series (LNCS, 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.

Keywords

Model Check Hybrid System Transition System Abstract State Regular Language 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 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)CrossRefGoogle Scholar
  2. 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. 3.
    Brihaye, T., Michaux, C.: On the expressiveness and decidability of o-minimal hybrid systems. J. Complexity 21(4), 447–478 (2005)zbMATHCrossRefMathSciNetGoogle Scholar
  4. 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. 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)zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    Clarke, E., et al.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752–794 (2003)CrossRefMathSciNetGoogle Scholar
  7. 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. 8.
    Davis, E.: Constraint propagation with interval labels. Artif. Intell. 32(3), 281–331 (1987)zbMATHCrossRefGoogle Scholar
  9. 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)CrossRefGoogle Scholar
  10. 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. 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. 12.
    Henzinger, T.A., et al.: What’s decidable about hybrid automata. J. Comput. System Sci. 57, 94–124 (1998)zbMATHCrossRefMathSciNetGoogle Scholar
  13. 13.
    Klarlund, N., Møller, A., Schwartzbach, M.I.: MONA implementation secrets. Internat. J. Found. Comput. Sci. 13(4), 571–586 (2002)zbMATHCrossRefMathSciNetGoogle Scholar
  14. 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)CrossRefGoogle Scholar
  15. 15.
    Ratschan, S.: RSolver. http://rsolver.sourceforge.net. Software package
  16. 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)CrossRefGoogle Scholar
  17. 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. 18.
    Ratschan, S., She, Z.: HSolver, http://hsolver.sourceforge.net. Software package
  19. 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. 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)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2007

Authors and Affiliations

  • Felix Klaedtke
    • 1
  • Stefan Ratschan
    • 2
  • Zhikun She
    • 3
  1. 1.ETH Zurich, Computer Science Department, ZurichSwitzerland
  2. 2.Institute of Computer Science, Czech Academy of Sciences, PragueCzech Republic
  3. 3.Max-Planck-Institut für Informatik, SaarbrückenGermany

Personalised recommendations