Local descent for temporal logic falsification of cyber-physical systems

Shakiba Yaghoubi, Georgios Fainekos

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 languageEnglish (US)
Title of host publicationCyber Physical Systems. Design, Modeling, and Evaluation - 7th International Workshop, CyPhy 2017, Revised Selected Papers
EditorsRoger Chamberlain, Walid Taha, Martin Törngren
PublisherSpringer Verlag
Pages11-26
Number of pages16
ISBN (Print)9783030179090
DOIs
StatePublished - Jan 1 2019
Event7th International Workshop on Design, Modeling, and Evaluation of Cyber Physical Systems, CyPhy 2017 - Seoul, Korea, Republic of
Duration: Oct 15 2017Oct 20 2017

Publication series

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

Conference

Conference7th International Workshop on Design, Modeling, and Evaluation of Cyber Physical Systems, CyPhy 2017
CountryKorea, Republic of
CitySeoul
Period10/15/1710/20/17

Fingerprint

Temporal logic
Global optimization
Temporal Logic
Simulated annealing
Descent
Hybrid systems
Engineers
Robustness
Hybrid Automata
Metric
Descent Method
Reachability Analysis
Gradient Descent
Requirements
Hybrid Systems
Simulated Annealing
Global Optimization
Guidance
Automata
Optimization Methods

Keywords

  • Falsification
  • Hybrid systems
  • Optimization

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

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 proceedingConference 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)). https://doi.org/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",
year = "2019",
month = "1",
day = "1",
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

PY - 2019/1/1

Y1 - 2019/1/1

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

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

ER -