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. © Springer-Verlag Berlin Heidelberg 2007.
Cite
CITATION STYLE
Klaedtke, F., Ratschan, S., & She, Z. (2007). Language-based abstraction refinement for hybrid system verification. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4349 LNCS, pp. 151–166). Springer Verlag. https://doi.org/10.1007/978-3-540-69738-1_11
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
