Hybrid automata-based CEGAR for rectangular hybrid systems

Pavithra Prabhakar, Parasara Sridhar Duggirala, Sayan Mitra, Mahesh Viswanathan

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publicationVerification, Model Checking, and Abstract Interpretation - 14th International Conference, VMCAI 2013, Proceedings
PublisherSpringer-Verlag Berlin Heidelberg
Pages48-67
Number of pages20
ISBN (Print)9783642358722
DOIs
StatePublished - 2013
Event14th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2013 - Rome, Italy
Duration: Jan 20 2013Jan 22 2013

Publication series

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

Other

Other14th International Conference on Verification, Model Checking, and Abstract Interpretation, VMCAI 2013
CountryItaly
CityRome
Period1/20/131/22/13

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Hybrid automata-based CEGAR for rectangular hybrid systems'. Together they form a unique fingerprint.

Cite this