Automatic reachability analysis for nonlinear hybrid models with C2E2

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

doi:10.1007/978-3-319-41528-4_29

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 proceeding › Conference contribution

Abstract

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 language	English (US)
Title of host publication	Computer Aided Verification - 28th International Conference, CAV 2016, Proceedings
Editors	Azadeh Farzan, Swarat Chaudhuri
Publisher	Springer
Pages	531-538
Number of pages	8
ISBN (Print)	9783319415277
DOIs	https://doi.org/10.1007/978-3-319-41528-4_29
State	Published - 2016
Event	28th International Conference on Computer Aided Verification, CAV 2016 - Toronto, Canada Duration: Jul 17 2016 → Jul 23 2016

Publication series

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

Other

Other	28th International Conference on Computer Aided Verification, CAV 2016
Country/Territory	Canada
City	Toronto
Period	7/17/16 → 7/23/16

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Online availability

10.1007/978-3-319-41528-4_29

Library availability

Discover UIUC Full Text

Cite this

Fan, C., Qi, B., Mitra, S., Viswanathan, M., & Duggirala, P. S. (2016). Automatic reachability analysis for nonlinear hybrid models with C2E2. In A. Farzan, & S. Chaudhuri (Eds.), Computer Aided Verification - 28th International Conference, CAV 2016, Proceedings (pp. 531-538). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9779). Springer. https://doi.org/10.1007/978-3-319-41528-4_29

Automatic reachability analysis for nonlinear hybrid models with C2E2. / Fan, Chuchu; Qi, Bolun; Mitra, Sayan et al.
Computer Aided Verification - 28th International Conference, CAV 2016, Proceedings. ed. / Azadeh Farzan; Swarat Chaudhuri. Springer, 2016. p. 531-538 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9779).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Fan, C, Qi, B, Mitra, S , Viswanathan, M & Duggirala, PS 2016, Automatic reachability analysis for nonlinear hybrid models with C2E2. in A Farzan & S Chaudhuri (eds), Computer Aided Verification - 28th International Conference, CAV 2016, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 9779, Springer, pp. 531-538, 28th International Conference on Computer Aided Verification, CAV 2016, Toronto, Canada, 7/17/16. https://doi.org/10.1007/978-3-319-41528-4_29

Fan C, Qi B, Mitra S , Viswanathan M, Duggirala PS. Automatic reachability analysis for nonlinear hybrid models with C2E2. In Farzan A, Chaudhuri S, editors, Computer Aided Verification - 28th International Conference, CAV 2016, Proceedings. Springer. 2016. p. 531-538. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-319-41528-4_29

Fan, Chuchu ; Qi, Bolun ; Mitra, Sayan et al. / Automatic reachability analysis for nonlinear hybrid models with C2E2. Computer Aided Verification - 28th International Conference, CAV 2016, Proceedings. editor / Azadeh Farzan ; Swarat Chaudhuri. Springer, 2016. pp. 531-538 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{bc72e26b125c43f9b65f23a7f0afbebf,

title = "Automatic reachability analysis for nonlinear hybrid models with C2E2",

abstract = "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.",

author = "Chuchu Fan and Bolun Qi and Sayan Mitra and Mahesh Viswanathan and Duggirala, {Parasara Sridhar}",

note = "Publisher Copyright: {\textcopyright} Springer International Publishing Switzerland 2016.; 28th International Conference on Computer Aided Verification, CAV 2016 ; Conference date: 17-07-2016 Through 23-07-2016",

year = "2016",

doi = "10.1007/978-3-319-41528-4_29",

language = "English (US)",

isbn = "9783319415277",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer",

pages = "531--538",

editor = "Azadeh Farzan and Swarat Chaudhuri",

booktitle = "Computer Aided Verification - 28th International Conference, CAV 2016, Proceedings",

address = "Germany",

}

TY - GEN

T1 - Automatic reachability analysis for nonlinear hybrid models with C2E2

AU - Fan, Chuchu

AU - Qi, Bolun

AU - Mitra, Sayan

AU - Viswanathan, Mahesh

AU - Duggirala, Parasara Sridhar

PY - 2016

Y1 - 2016

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84978903969&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84978903969&partnerID=8YFLogxK

U2 - 10.1007/978-3-319-41528-4_29

DO - 10.1007/978-3-319-41528-4_29

M3 - Conference contribution

AN - SCOPUS:84978903969

SN - 9783319415277

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 531

EP - 538

BT - Computer Aided Verification - 28th International Conference, CAV 2016, Proceedings

A2 - Farzan, Azadeh

A2 - Chaudhuri, Swarat

PB - Springer

T2 - 28th International Conference on Computer Aided Verification, CAV 2016

Y2 - 17 July 2016 through 23 July 2016

ER -

Automatic reachability analysis for nonlinear hybrid models with C2E2

Abstract

Publication series

Other

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this