Automatic reachability analysis for nonlinear hybrid models with C2E2

Chuchu Fan, Bolun Qi, Sayan Mitra, Mahesh Viswanathan, Parasara Sridhar Duggirala

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


C2E2 is a bounded reachability analysis tool for nonlinear dynamical systems and hybrid automaton models. Previously it required users to annotate each system of differential equations of the hybrid automaton with discrepancy functions, and since these annotations are difficult to get for general nonlinear differential equations, the tool had limited usability. This version of C2E2 is improved in several ways, the most prominent among which is the elimination of the need for userprovided discrepancy functions. It automatically computes piece-wise (or local) discrepancy functions around the reachable parts of the state space using symbolically computed Jacobian matrix and eigenvalue perturbation bounds. The special cases of linear and constant rate differential equations are handled with more efficient algorithm. In this paper, we discuss these and other new features that make the new C2E2 a usable tool for bounded reachability analysis of hybrid systems.

Original languageEnglish (US)
Title of host publicationComputer Aided Verification - 28th International Conference, CAV 2016, Proceedings
EditorsAzadeh Farzan, Swarat Chaudhuri
Number of pages8
ISBN (Print)9783319415277
StatePublished - 2016
Event28th International Conference on Computer Aided Verification, CAV 2016 - Toronto, Canada
Duration: Jul 17 2016Jul 23 2016

Publication series

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


Other28th International Conference on Computer Aided Verification, CAV 2016

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Automatic reachability analysis for nonlinear hybrid models with C2E2'. Together they form a unique fingerprint.

Cite this