Under-approximating backward reachable sets by polytopes

Bai Xue; Zhikun She; Arvind Easwaran

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

Under-approximating backward reachable sets by polytopes

Bai Xue^*, Zhikun She, Arvind Easwaran

^*Corresponding author for this work

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

35 Citations (Scopus)

Abstract

Under-approximations are useful for falsification of safety properties for nonlinear (hybrid) systems by finding counter-examples. Polytopic under-approximations enable analysis of these properties using reasoning in the theory of linear arithmetic. Given a nonlinear system, a target region of the simply connected compact type and a time duration, we in this paper propose a method using boundary analysis to compute an under-approximation of the backward reachable set. The under-approximation is represented as a polytope. The polytope can be computed by solving linear program problems. We test our method on several examples and compare them with existing methods. The results show that our method is highly promising in under-approximating reachable sets. Furthermore, we explore some directions to improve the scalability of our method.

Original language	English
Title of host publication	Computer Aided Verification - 28th International Conference, CAV 2016, Proceedings
Editors	Azadeh Farzan, Swarat Chaudhuri
Publisher	Springer Verlag
Pages	457-476
Number of pages	20
ISBN (Print)	9783319415277
DOIs	https://doi.org/10.1007/978-3-319-41528-4_25
Publication status	Published - 2016
Externally published	Yes
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

Conference

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

Bibliographical note

Publisher Copyright:
© Springer International Publishing Switzerland 2016.

ASJC Scopus Subject Areas

Theoretical Computer Science
General Computer Science

Keywords

Backward reachable sets
Nonlinear systems
Polytopic under-approximations

Access to Document

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

Cite this

Xue, B., She, Z., & Easwaran, A. (2016). Under-approximating backward reachable sets by polytopes. In A. Farzan, & S. Chaudhuri (Eds.), Computer Aided Verification - 28th International Conference, CAV 2016, Proceedings (pp. 457-476). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 9779). Springer Verlag. https://doi.org/10.1007/978-3-319-41528-4_25

Xue, Bai ; She, Zhikun ; Easwaran, Arvind. / Under-approximating backward reachable sets by polytopes. Computer Aided Verification - 28th International Conference, CAV 2016, Proceedings. editor / Azadeh Farzan ; Swarat Chaudhuri. Springer Verlag, 2016. pp. 457-476 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{55e88ce6a7094e279dfa9f046a175b78,

title = "Under-approximating backward reachable sets by polytopes",

abstract = "Under-approximations are useful for falsification of safety properties for nonlinear (hybrid) systems by finding counter-examples. Polytopic under-approximations enable analysis of these properties using reasoning in the theory of linear arithmetic. Given a nonlinear system, a target region of the simply connected compact type and a time duration, we in this paper propose a method using boundary analysis to compute an under-approximation of the backward reachable set. The under-approximation is represented as a polytope. The polytope can be computed by solving linear program problems. We test our method on several examples and compare them with existing methods. The results show that our method is highly promising in under-approximating reachable sets. Furthermore, we explore some directions to improve the scalability of our method.",

keywords = "Backward reachable sets, Nonlinear systems, Polytopic under-approximations",

author = "Bai Xue and Zhikun She and Arvind Easwaran",

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_25",

language = "English",

isbn = "9783319415277",

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

publisher = "Springer Verlag",

pages = "457--476",

editor = "Azadeh Farzan and Swarat Chaudhuri",

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

address = "Germany",

}

Xue, B, She, Z & Easwaran, A 2016, Under-approximating backward reachable sets by polytopes. 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 Verlag, pp. 457-476, 28th International Conference on Computer Aided Verification, CAV 2016, Toronto, Canada, 7/17/16. https://doi.org/10.1007/978-3-319-41528-4_25

Under-approximating backward reachable sets by polytopes. / Xue, Bai; She, Zhikun; Easwaran, Arvind.
Computer Aided Verification - 28th International Conference, CAV 2016, Proceedings. ed. / Azadeh Farzan; Swarat Chaudhuri. Springer Verlag, 2016. p. 457-476 (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

TY - GEN

T1 - Under-approximating backward reachable sets by polytopes

AU - Xue, Bai

AU - She, Zhikun

AU - Easwaran, Arvind

N1 - Publisher Copyright: © Springer International Publishing Switzerland 2016.

PY - 2016

Y1 - 2016

N2 - Under-approximations are useful for falsification of safety properties for nonlinear (hybrid) systems by finding counter-examples. Polytopic under-approximations enable analysis of these properties using reasoning in the theory of linear arithmetic. Given a nonlinear system, a target region of the simply connected compact type and a time duration, we in this paper propose a method using boundary analysis to compute an under-approximation of the backward reachable set. The under-approximation is represented as a polytope. The polytope can be computed by solving linear program problems. We test our method on several examples and compare them with existing methods. The results show that our method is highly promising in under-approximating reachable sets. Furthermore, we explore some directions to improve the scalability of our method.

AB - Under-approximations are useful for falsification of safety properties for nonlinear (hybrid) systems by finding counter-examples. Polytopic under-approximations enable analysis of these properties using reasoning in the theory of linear arithmetic. Given a nonlinear system, a target region of the simply connected compact type and a time duration, we in this paper propose a method using boundary analysis to compute an under-approximation of the backward reachable set. The under-approximation is represented as a polytope. The polytope can be computed by solving linear program problems. We test our method on several examples and compare them with existing methods. The results show that our method is highly promising in under-approximating reachable sets. Furthermore, we explore some directions to improve the scalability of our method.

KW - Backward reachable sets

KW - Nonlinear systems

KW - Polytopic under-approximations

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

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

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

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

M3 - Conference contribution

AN - SCOPUS:84978852370

SN - 9783319415277

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

SP - 457

EP - 476

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

A2 - Farzan, Azadeh

A2 - Chaudhuri, Swarat

PB - Springer Verlag

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

Y2 - 17 July 2016 through 23 July 2016

ER -

Xue B, She Z, Easwaran A. Under-approximating backward reachable sets by polytopes. In Farzan A, Chaudhuri S, editors, Computer Aided Verification - 28th International Conference, CAV 2016, Proceedings. Springer Verlag. 2016. p. 457-476. (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_25

Under-approximating backward reachable sets by polytopes

Abstract

Publication series

Conference

Bibliographical note

ASJC Scopus Subject Areas

Keywords

Access to Document

Other files and links

Fingerprint

Cite this