Parsimonious, simulation based verification of linear systems

Parasara Sridhar Duggirala; Mahesh Viswanathan

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

Parsimonious, simulation based verification of linear systems

Parasara Sridhar Duggirala, Mahesh Viswanathan

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

Abstract

We present a technique to verify safety properties of linear systems (possibly time varying) using very few simulations. For a linear system of dimension n, our technique needs n + 1 simulation runs. This is in contrast to current simulation based approaches, where the number of simulations either depends upon the number of vertices in the convex polyhedral initial set, or on the proximity of the unsafe set to the set of reachable states. At its core, our algorithm exploits the superposition principle of linear systems. Our algorithm computes both an over and an under approximation of the set of reachable states.

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	477-494
Number of pages	18
ISBN (Print)	9783319415277
DOIs	https://doi.org/10.1007/978-3-319-41528-4_26
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
Computer Science(all)

Online availability

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

Library availability

Discover UIUC Full Text

Cite this

Duggirala, P. S., & Viswanathan, M. (2016). Parsimonious, simulation based verification of linear systems. In A. Farzan, & S. Chaudhuri (Eds.), Computer Aided Verification - 28th International Conference, CAV 2016, Proceedings (pp. 477-494). (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_26

Parsimonious, simulation based verification of linear systems. / Duggirala, Parasara Sridhar; Viswanathan, Mahesh.

Computer Aided Verification - 28th International Conference, CAV 2016, Proceedings. ed. / Azadeh Farzan; Swarat Chaudhuri. Springer, 2016. p. 477-494 (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

Duggirala, PS & Viswanathan, M 2016, Parsimonious, simulation based verification of linear systems. 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. 477-494, 28th International Conference on Computer Aided Verification, CAV 2016, Toronto, Canada, 7/17/16. https://doi.org/10.1007/978-3-319-41528-4_26

Duggirala PS, Viswanathan M. Parsimonious, simulation based verification of linear systems. In Farzan A, Chaudhuri S, editors, Computer Aided Verification - 28th International Conference, CAV 2016, Proceedings. Springer. 2016. p. 477-494. (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_26

Duggirala, Parasara Sridhar ; Viswanathan, Mahesh. / Parsimonious, simulation based verification of linear systems. Computer Aided Verification - 28th International Conference, CAV 2016, Proceedings. editor / Azadeh Farzan ; Swarat Chaudhuri. Springer, 2016. pp. 477-494 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{7b046bb6cfb44e73aeb62a3d69b1262f,

title = "Parsimonious, simulation based verification of linear systems",

abstract = "We present a technique to verify safety properties of linear systems (possibly time varying) using very few simulations. For a linear system of dimension n, our technique needs n + 1 simulation runs. This is in contrast to current simulation based approaches, where the number of simulations either depends upon the number of vertices in the convex polyhedral initial set, or on the proximity of the unsafe set to the set of reachable states. At its core, our algorithm exploits the superposition principle of linear systems. Our algorithm computes both an over and an under approximation of the set of reachable states.",

author = "Duggirala, {Parasara Sridhar} and Mahesh Viswanathan",

year = "2016",

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

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 = "477--494",

editor = "Azadeh Farzan and Swarat Chaudhuri",

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

address = "Germany",

note = "28th International Conference on Computer Aided Verification, CAV 2016 ; Conference date: 17-07-2016 Through 23-07-2016",

}

TY - GEN

T1 - Parsimonious, simulation based verification of linear systems

AU - Duggirala, Parasara Sridhar

AU - Viswanathan, Mahesh

PY - 2016

Y1 - 2016

N2 - We present a technique to verify safety properties of linear systems (possibly time varying) using very few simulations. For a linear system of dimension n, our technique needs n + 1 simulation runs. This is in contrast to current simulation based approaches, where the number of simulations either depends upon the number of vertices in the convex polyhedral initial set, or on the proximity of the unsafe set to the set of reachable states. At its core, our algorithm exploits the superposition principle of linear systems. Our algorithm computes both an over and an under approximation of the set of reachable states.

AB - We present a technique to verify safety properties of linear systems (possibly time varying) using very few simulations. For a linear system of dimension n, our technique needs n + 1 simulation runs. This is in contrast to current simulation based approaches, where the number of simulations either depends upon the number of vertices in the convex polyhedral initial set, or on the proximity of the unsafe set to the set of reachable states. At its core, our algorithm exploits the superposition principle of linear systems. Our algorithm computes both an over and an under approximation of the set of reachable states.

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

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

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

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

M3 - Conference contribution

AN - SCOPUS:84978906037

SN - 9783319415277

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

SP - 477

EP - 494

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 -

Parsimonious, simulation based verification of linear systems

Abstract

Publication series

Other

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this