Local descent for temporal logic falsification of cyber-physical systems

Shakiba Yaghoubi; Georgios Fainekos

doi:10.1007/978-3-030-17910-6_2

Local descent for temporal logic falsification of cyber-physical systems

Shakiba Yaghoubi, Georgios Fainekos

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

1 Scopus citations

Abstract

One way to analyze Cyber-Physical Systems is by modeling them as hybrid automata. Since reachability analysis for hybrid nonlinear automata is a very challenging and computationally expensive problem, in practice, engineers try to solve the requirements falsification problem. In one method, the falsification problem is solved by minimizing a robustness metric induced by the requirements. This optimization problem is usually a non-convex non-smooth problem that requires heuristic and analytical guidance to be solved. In this paper, functional gradient descent for hybrid systems is utilized for locally decreasing the robustness metric. The local descent method is combined with Simulated Annealing as a global optimization method to search for unsafe behaviors.

Original language	English (US)
Title of host publication	Cyber Physical Systems. Design, Modeling, and Evaluation - 7th International Workshop, CyPhy 2017, Revised Selected Papers
Editors	Roger Chamberlain, Walid Taha, Martin Törngren
Publisher	Springer Verlag
Pages	11-26
Number of pages	16
ISBN (Print)	9783030179090
DOIs	https://doi.org/10.1007/978-3-030-17910-6_2
State	Published - 2019
Event	7th International Workshop on Design, Modeling, and Evaluation of Cyber Physical Systems, CyPhy 2017 - Seoul, Korea, Republic of Duration: Oct 15 2017 → Oct 20 2017

Publication series

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

Conference

Conference	7th International Workshop on Design, Modeling, and Evaluation of Cyber Physical Systems, CyPhy 2017
Country/Territory	Korea, Republic of
City	Seoul
Period	10/15/17 → 10/20/17

Keywords

Falsification
Hybrid systems
Optimization

ASJC Scopus subject areas

Theoretical Computer Science
General Computer Science

Access to Document

10.1007/978-3-030-17910-6_2

Cite this

Yaghoubi, S., & Fainekos, G. (2019). Local descent for temporal logic falsification of cyber-physical systems. In R. Chamberlain, W. Taha, & M. Törngren (Eds.), Cyber Physical Systems. Design, Modeling, and Evaluation - 7th International Workshop, CyPhy 2017, Revised Selected Papers (pp. 11-26). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11267 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-030-17910-6_2

Local descent for temporal logic falsification of cyber-physical systems. / Yaghoubi, Shakiba; Fainekos, Georgios.
Cyber Physical Systems. Design, Modeling, and Evaluation - 7th International Workshop, CyPhy 2017, Revised Selected Papers. ed. / Roger Chamberlain; Walid Taha; Martin Törngren. Springer Verlag, 2019. p. 11-26 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 11267 LNCS).

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

Yaghoubi, S & Fainekos, G 2019, Local descent for temporal logic falsification of cyber-physical systems. in R Chamberlain, W Taha & M Törngren (eds), Cyber Physical Systems. Design, Modeling, and Evaluation - 7th International Workshop, CyPhy 2017, Revised Selected Papers. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 11267 LNCS, Springer Verlag, pp. 11-26, 7th International Workshop on Design, Modeling, and Evaluation of Cyber Physical Systems, CyPhy 2017, Seoul, Korea, Republic of, 10/15/17. https://doi.org/10.1007/978-3-030-17910-6_2

Yaghoubi S, Fainekos G. Local descent for temporal logic falsification of cyber-physical systems. In Chamberlain R, Taha W, Törngren M, editors, Cyber Physical Systems. Design, Modeling, and Evaluation - 7th International Workshop, CyPhy 2017, Revised Selected Papers. Springer Verlag. 2019. p. 11-26. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-17910-6_2

Yaghoubi, Shakiba ; Fainekos, Georgios. / Local descent for temporal logic falsification of cyber-physical systems. Cyber Physical Systems. Design, Modeling, and Evaluation - 7th International Workshop, CyPhy 2017, Revised Selected Papers. editor / Roger Chamberlain ; Walid Taha ; Martin Törngren. Springer Verlag, 2019. pp. 11-26 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{d8e7588df86f42aba5e002c1852039da,

title = "Local descent for temporal logic falsification of cyber-physical systems",

abstract = "One way to analyze Cyber-Physical Systems is by modeling them as hybrid automata. Since reachability analysis for hybrid nonlinear automata is a very challenging and computationally expensive problem, in practice, engineers try to solve the requirements falsification problem. In one method, the falsification problem is solved by minimizing a robustness metric induced by the requirements. This optimization problem is usually a non-convex non-smooth problem that requires heuristic and analytical guidance to be solved. In this paper, functional gradient descent for hybrid systems is utilized for locally decreasing the robustness metric. The local descent method is combined with Simulated Annealing as a global optimization method to search for unsafe behaviors.",

keywords = "Falsification, Hybrid systems, Optimization",

author = "Shakiba Yaghoubi and Georgios Fainekos",

note = "Funding Information: Acknowledgments. This work was partially supported by the NSF awards CNS-1319560, CNS 1350420, IIP-1361926, and the NSF I/UCRC Center for Embedded Systems. Publisher Copyright: {\textcopyright} Springer Nature Switzerland AG 2019.; 7th International Workshop on Design, Modeling, and Evaluation of Cyber Physical Systems, CyPhy 2017 ; Conference date: 15-10-2017 Through 20-10-2017",

year = "2019",

doi = "10.1007/978-3-030-17910-6_2",

language = "English (US)",

isbn = "9783030179090",

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

publisher = "Springer Verlag",

pages = "11--26",

editor = "Roger Chamberlain and Walid Taha and Martin T{\"o}rngren",

booktitle = "Cyber Physical Systems. Design, Modeling, and Evaluation - 7th International Workshop, CyPhy 2017, Revised Selected Papers",

}

TY - GEN

T1 - Local descent for temporal logic falsification of cyber-physical systems

AU - Yaghoubi, Shakiba

AU - Fainekos, Georgios

N1 - Funding Information: Acknowledgments. This work was partially supported by the NSF awards CNS-1319560, CNS 1350420, IIP-1361926, and the NSF I/UCRC Center for Embedded Systems. Publisher Copyright: © Springer Nature Switzerland AG 2019.

PY - 2019

Y1 - 2019

N2 - One way to analyze Cyber-Physical Systems is by modeling them as hybrid automata. Since reachability analysis for hybrid nonlinear automata is a very challenging and computationally expensive problem, in practice, engineers try to solve the requirements falsification problem. In one method, the falsification problem is solved by minimizing a robustness metric induced by the requirements. This optimization problem is usually a non-convex non-smooth problem that requires heuristic and analytical guidance to be solved. In this paper, functional gradient descent for hybrid systems is utilized for locally decreasing the robustness metric. The local descent method is combined with Simulated Annealing as a global optimization method to search for unsafe behaviors.

AB - One way to analyze Cyber-Physical Systems is by modeling them as hybrid automata. Since reachability analysis for hybrid nonlinear automata is a very challenging and computationally expensive problem, in practice, engineers try to solve the requirements falsification problem. In one method, the falsification problem is solved by minimizing a robustness metric induced by the requirements. This optimization problem is usually a non-convex non-smooth problem that requires heuristic and analytical guidance to be solved. In this paper, functional gradient descent for hybrid systems is utilized for locally decreasing the robustness metric. The local descent method is combined with Simulated Annealing as a global optimization method to search for unsafe behaviors.

KW - Falsification

KW - Hybrid systems

KW - Optimization

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

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

U2 - 10.1007/978-3-030-17910-6_2

DO - 10.1007/978-3-030-17910-6_2

M3 - Conference contribution

AN - SCOPUS:85065019094

SN - 9783030179090

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

SP - 11

EP - 26

BT - Cyber Physical Systems. Design, Modeling, and Evaluation - 7th International Workshop, CyPhy 2017, Revised Selected Papers

A2 - Chamberlain, Roger

A2 - Taha, Walid

A2 - Törngren, Martin

PB - Springer Verlag

T2 - 7th International Workshop on Design, Modeling, and Evaluation of Cyber Physical Systems, CyPhy 2017

Y2 - 15 October 2017 through 20 October 2017

ER -

Local descent for temporal logic falsification of cyber-physical systems

Abstract

Publication series

Conference

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this