Hybrid automata-based CEGAR for rectangular hybrid systems

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

Research output: Contribution to journalArticlepeer-review


In this paper, we present a counterexample guided abstraction refinement (CEGAR) framework 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, as opposed to finite state systems. 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. The experimental evaluations demonstrate the merits of the approach.

Original languageEnglish (US)
Pages (from-to)105-134
Number of pages30
JournalFormal Methods in System Design
Issue number2
StatePublished - Apr 1 2015


  • Abstraction refinement
  • Counter-example guided abstraction refinement
  • Hybrid system
  • Rectangular hybrid automata
  • Safety verification

ASJC Scopus subject areas

  • Software
  • Theoretical Computer Science
  • Hardware and Architecture


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

Cite this