Skip to main navigation Skip to search Skip to main content

Language-based abstraction refinement for hybrid system verification

  • Felix Klaedtke*
  • , Stefan Ratschan
  • , Zhikun She
  • *Corresponding author for this work
  • Swiss Federal Institute of Technology Zurich
  • Czech Academy of Sciences
  • Max Planck Institute for Informatics

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

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.

Original languageEnglish
Title of host publicationVerification, Model Checking, and Abstract Interpretation, - 8th International Conference, VMCAI 2007, Proceedings
PublisherSpringer Verlag
Pages151-166
Number of pages16
ISBN (Print)3540697357, 9783540697350
DOIs
StatePublished - 2007
Externally publishedYes
Event8th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2007 - Nice, France
Duration: 14 Jan 200716 Jan 2007

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume4349 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference8th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2007
Country/TerritoryFrance
CityNice
Period14/01/0716/01/07

Fingerprint

Dive into the research topics of 'Language-based abstraction refinement for hybrid system verification'. Together they form a unique fingerprint.

Cite this