zbMATH — the first resource for mathematics

Hybrid automata-based CEGAR for rectangular hybrid systems. (English) Zbl 1426.68175
Giacobazzi, Roberto (ed.) et al., Verification, model checking, and abstract interpretation. 14th international conference, VMCAI 2013, Rome, Italy, January 20–22, 2013. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 7737, 48-67 (2013).
Summary: In this paper we present a framework for carrying out counterexample guided abstraction-refinement (CEGAR) 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. 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. Our experiments demonstrate the usefulness of the approach.
For the entire collection see [Zbl 1298.68027].

68Q60 Specification and verification (program logics, model checking, etc.)
68Q45 Formal languages and automata
Full Text: DOI