Probably Approximate Safety Verification of Hybrid Dynamical Systems

Bai Xue; Martin Fränzle; Hengjun Zhao; Naijun Zhan; Arvind Easwaran

doi:10.1007/978-3-030-32409-4_15

Probably Approximate Safety Verification of Hybrid Dynamical Systems

Bai Xue^*, Martin Fränzle, Hengjun Zhao, Naijun Zhan, Arvind Easwaran

^*Corresponding author for this work

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

7 Citations (Scopus)

Abstract

In this paper we present a method based on linear programming that facilitates reliable safety verification of hybrid dynamical systems subject to perturbation inputs over the infinite time horizon. The verification algorithm applies the probably approximately correct (PAC) learning framework and consequently can be regarded as statistically formal verification in the sense that it provides formal safety guarantees expressed using error probabilities and confidences. The safety of hybrid systems in this framework is verified via the computation of so-called PAC barrier certificates, which can be computed by solving a linear programming problem. Based on scenario approaches, the linear program is constructed by a family of independent and identically distributed state samples. In this way we can conduct verification of hybrid dynamical systems that existing methods are not capable of dealing with. Some preliminary experiments demonstrate the performance of our approach.

Original language	English
Title of host publication	Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Proceedings
Editors	Yamine Ait-Ameur, Shengchao Qin
Publisher	Springer
Pages	236-252
Number of pages	17
ISBN (Print)	9783030324087
DOIs	https://doi.org/10.1007/978-3-030-32409-4_15
Publication status	Published - 2019
Externally published	Yes
Event	21st International Conference on Formal Engineering Methods, ICFEM 2019 - Shenzhen, China Duration: Nov 5 2019 → Nov 9 2019

Publication series

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

Conference

Conference	21st International Conference on Formal Engineering Methods, ICFEM 2019
Country/Territory	China
City	Shenzhen
Period	11/5/19 → 11/9/19

Bibliographical note

Publisher Copyright:
© 2019, Springer Nature Switzerland AG.

ASJC Scopus Subject Areas

Theoretical Computer Science
General Computer Science

Keywords

Hybrid systems
Linear program
Probably approximately safe

Access to Document

10.1007/978-3-030-32409-4_15

Cite this

Xue, B., Fränzle, M., Zhao, H., Zhan, N., & Easwaran, A. (2019). Probably Approximate Safety Verification of Hybrid Dynamical Systems. In Y. Ait-Ameur, & S. Qin (Eds.), Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Proceedings (pp. 236-252). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11852 LNCS). Springer. https://doi.org/10.1007/978-3-030-32409-4_15

Xue, Bai ; Fränzle, Martin ; Zhao, Hengjun et al. / Probably Approximate Safety Verification of Hybrid Dynamical Systems. Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Proceedings. editor / Yamine Ait-Ameur ; Shengchao Qin. Springer, 2019. pp. 236-252 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{824d9dfec0964781a9b4604f4bd54c7f,

title = "Probably Approximate Safety Verification of Hybrid Dynamical Systems",

abstract = "In this paper we present a method based on linear programming that facilitates reliable safety verification of hybrid dynamical systems subject to perturbation inputs over the infinite time horizon. The verification algorithm applies the probably approximately correct (PAC) learning framework and consequently can be regarded as statistically formal verification in the sense that it provides formal safety guarantees expressed using error probabilities and confidences. The safety of hybrid systems in this framework is verified via the computation of so-called PAC barrier certificates, which can be computed by solving a linear programming problem. Based on scenario approaches, the linear program is constructed by a family of independent and identically distributed state samples. In this way we can conduct verification of hybrid dynamical systems that existing methods are not capable of dealing with. Some preliminary experiments demonstrate the performance of our approach.",

keywords = "Hybrid systems, Linear program, Probably approximately safe",

author = "Bai Xue and Martin Fr{\"a}nzle and Hengjun Zhao and Naijun Zhan and Arvind Easwaran",

note = "Publisher Copyright: {\textcopyright} 2019, Springer Nature Switzerland AG.; 21st International Conference on Formal Engineering Methods, ICFEM 2019 ; Conference date: 05-11-2019 Through 09-11-2019",

year = "2019",

doi = "10.1007/978-3-030-32409-4_15",

language = "English",

isbn = "9783030324087",

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

publisher = " Springer",

pages = "236--252",

editor = "Yamine Ait-Ameur and Shengchao Qin",

booktitle = "Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Proceedings",

}

Xue, B, Fränzle, M, Zhao, H, Zhan, N & Easwaran, A 2019, Probably Approximate Safety Verification of Hybrid Dynamical Systems. in Y Ait-Ameur & S Qin (eds), Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11852 LNCS, Springer, pp. 236-252, 21st International Conference on Formal Engineering Methods, ICFEM 2019, Shenzhen, China, 11/5/19. https://doi.org/10.1007/978-3-030-32409-4_15

Probably Approximate Safety Verification of Hybrid Dynamical Systems. / Xue, Bai; Fränzle, Martin; Zhao, Hengjun et al.
Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Proceedings. ed. / Yamine Ait-Ameur; Shengchao Qin. Springer, 2019. p. 236-252 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11852 LNCS).

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

TY - GEN

T1 - Probably Approximate Safety Verification of Hybrid Dynamical Systems

AU - Xue, Bai

AU - Fränzle, Martin

AU - Zhao, Hengjun

AU - Zhan, Naijun

AU - Easwaran, Arvind

PY - 2019

Y1 - 2019

N2 - In this paper we present a method based on linear programming that facilitates reliable safety verification of hybrid dynamical systems subject to perturbation inputs over the infinite time horizon. The verification algorithm applies the probably approximately correct (PAC) learning framework and consequently can be regarded as statistically formal verification in the sense that it provides formal safety guarantees expressed using error probabilities and confidences. The safety of hybrid systems in this framework is verified via the computation of so-called PAC barrier certificates, which can be computed by solving a linear programming problem. Based on scenario approaches, the linear program is constructed by a family of independent and identically distributed state samples. In this way we can conduct verification of hybrid dynamical systems that existing methods are not capable of dealing with. Some preliminary experiments demonstrate the performance of our approach.

AB - In this paper we present a method based on linear programming that facilitates reliable safety verification of hybrid dynamical systems subject to perturbation inputs over the infinite time horizon. The verification algorithm applies the probably approximately correct (PAC) learning framework and consequently can be regarded as statistically formal verification in the sense that it provides formal safety guarantees expressed using error probabilities and confidences. The safety of hybrid systems in this framework is verified via the computation of so-called PAC barrier certificates, which can be computed by solving a linear programming problem. Based on scenario approaches, the linear program is constructed by a family of independent and identically distributed state samples. In this way we can conduct verification of hybrid dynamical systems that existing methods are not capable of dealing with. Some preliminary experiments demonstrate the performance of our approach.

KW - Hybrid systems

KW - Linear program

KW - Probably approximately safe

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

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

U2 - 10.1007/978-3-030-32409-4_15

DO - 10.1007/978-3-030-32409-4_15

M3 - Conference contribution

AN - SCOPUS:85076153787

SN - 9783030324087

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

SP - 236

EP - 252

BT - Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Proceedings

A2 - Ait-Ameur, Yamine

A2 - Qin, Shengchao

PB - Springer

T2 - 21st International Conference on Formal Engineering Methods, ICFEM 2019

Y2 - 5 November 2019 through 9 November 2019

ER -

Xue B, Fränzle M, Zhao H, Zhan N, Easwaran A. Probably Approximate Safety Verification of Hybrid Dynamical Systems. In Ait-Ameur Y, Qin S, editors, Formal Methods and Software Engineering - 21st International Conference on Formal Engineering Methods, ICFEM 2019, Proceedings. Springer. 2019. p. 236-252. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-32409-4_15

Probably Approximate Safety Verification of Hybrid Dynamical Systems

Abstract

Publication series

Conference

Bibliographical note

ASJC Scopus Subject Areas

Keywords

Access to Document

Other files and links

Fingerprint

Cite this