Active sampling-based binary verification of dynamical systems

John F. Quindlen, Ufuk Topcu, Girish Chowdhary, Jonathan P. How

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

Abstract

Nonlinear, adaptive, or otherwise complex control techniques are increasingly relied upon to ensure the safety of systems operating in uncertain environments. However, the nonlinearity of the resulting closed-loop system complicates verification that the system does in fact satisfy those requirements at all possible operating conditions. While ana- lytical proof-based techniques and finite abstractions can be used to provably verify the closed-loop system’s response at different operating conditions, they often produce con- servative approximations due to restrictive assumptions and are dificult to construct in many applications. In contrast, popular statistical verification techniques relax the restric- tions and instead rely upon simulations to construct statistical or probabilistic guarantees. This work presents a data-driven statistical verification procedure that instead constructs statistical learning models from simulated training data to separate the set of possible perturbations into “safe” and “unsafe” subsets. Binary evaluations of closed-loop system requirement satisfaction at various realizations of the uncertainties are obtained through temporal logic robustness metrics, which are then used to construct predictive models of requirement satisfaction over the full set of possible uncertainties. As the accuracy of these predictive statistical models is inherently coupled to the quality of the training data, an active learning algorithm selects additional sample points in order to maximize the expected change in the data-driven model and thus, indirectly, minimize the prediction er- ror. Various case studies demonstrate the closed-loop verification procedure and highlight improvements in prediction error over both existing analytical and statistical verification techniques.

Original languageEnglish (US)
Title of host publicationAIAA Guidance, Navigation, and Control
PublisherAmerican Institute of Aeronautics and Astronautics Inc, AIAA
Edition210039
ISBN (Print)9781624105265
DOIs
StatePublished - Jan 1 2018
EventAIAA Guidance, Navigation, and Control Conference, 2018 - Kissimmee, United States
Duration: Jan 8 2018Jan 12 2018

Publication series

NameAIAA Guidance, Navigation, and Control Conference, 2018
Number210039

Other

OtherAIAA Guidance, Navigation, and Control Conference, 2018
CountryUnited States
CityKissimmee
Period1/8/181/12/18

Fingerprint

Dynamical systems
Sampling
Closed loop systems
Temporal logic
Learning algorithms
Uncertainty

ASJC Scopus subject areas

  • Aerospace Engineering
  • Control and Systems Engineering
  • Electrical and Electronic Engineering

Cite this

Quindlen, J. F., Topcu, U., Chowdhary, G., & How, J. P. (2018). Active sampling-based binary verification of dynamical systems. In AIAA Guidance, Navigation, and Control (210039 ed.). (AIAA Guidance, Navigation, and Control Conference, 2018; No. 210039). American Institute of Aeronautics and Astronautics Inc, AIAA. https://doi.org/10.2514/6.2018-1107

Active sampling-based binary verification of dynamical systems. / Quindlen, John F.; Topcu, Ufuk; Chowdhary, Girish; How, Jonathan P.

AIAA Guidance, Navigation, and Control. 210039. ed. American Institute of Aeronautics and Astronautics Inc, AIAA, 2018. (AIAA Guidance, Navigation, and Control Conference, 2018; No. 210039).

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

Quindlen, JF, Topcu, U, Chowdhary, G & How, JP 2018, Active sampling-based binary verification of dynamical systems. in AIAA Guidance, Navigation, and Control. 210039 edn, AIAA Guidance, Navigation, and Control Conference, 2018, no. 210039, American Institute of Aeronautics and Astronautics Inc, AIAA, AIAA Guidance, Navigation, and Control Conference, 2018, Kissimmee, United States, 1/8/18. https://doi.org/10.2514/6.2018-1107
Quindlen JF, Topcu U, Chowdhary G, How JP. Active sampling-based binary verification of dynamical systems. In AIAA Guidance, Navigation, and Control. 210039 ed. American Institute of Aeronautics and Astronautics Inc, AIAA. 2018. (AIAA Guidance, Navigation, and Control Conference, 2018; 210039). https://doi.org/10.2514/6.2018-1107
Quindlen, John F. ; Topcu, Ufuk ; Chowdhary, Girish ; How, Jonathan P. / Active sampling-based binary verification of dynamical systems. AIAA Guidance, Navigation, and Control. 210039. ed. American Institute of Aeronautics and Astronautics Inc, AIAA, 2018. (AIAA Guidance, Navigation, and Control Conference, 2018; 210039).
@inproceedings{f909dce43e74416abb591d23a096fa5d,
title = "Active sampling-based binary verification of dynamical systems",
abstract = "Nonlinear, adaptive, or otherwise complex control techniques are increasingly relied upon to ensure the safety of systems operating in uncertain environments. However, the nonlinearity of the resulting closed-loop system complicates verification that the system does in fact satisfy those requirements at all possible operating conditions. While ana- lytical proof-based techniques and finite abstractions can be used to provably verify the closed-loop system’s response at different operating conditions, they often produce con- servative approximations due to restrictive assumptions and are dificult to construct in many applications. In contrast, popular statistical verification techniques relax the restric- tions and instead rely upon simulations to construct statistical or probabilistic guarantees. This work presents a data-driven statistical verification procedure that instead constructs statistical learning models from simulated training data to separate the set of possible perturbations into “safe” and “unsafe” subsets. Binary evaluations of closed-loop system requirement satisfaction at various realizations of the uncertainties are obtained through temporal logic robustness metrics, which are then used to construct predictive models of requirement satisfaction over the full set of possible uncertainties. As the accuracy of these predictive statistical models is inherently coupled to the quality of the training data, an active learning algorithm selects additional sample points in order to maximize the expected change in the data-driven model and thus, indirectly, minimize the prediction er- ror. Various case studies demonstrate the closed-loop verification procedure and highlight improvements in prediction error over both existing analytical and statistical verification techniques.",
author = "Quindlen, {John F.} and Ufuk Topcu and Girish Chowdhary and How, {Jonathan P.}",
year = "2018",
month = "1",
day = "1",
doi = "10.2514/6.2018-1107",
language = "English (US)",
isbn = "9781624105265",
series = "AIAA Guidance, Navigation, and Control Conference, 2018",
publisher = "American Institute of Aeronautics and Astronautics Inc, AIAA",
number = "210039",
booktitle = "AIAA Guidance, Navigation, and Control",
edition = "210039",

}

TY - GEN

T1 - Active sampling-based binary verification of dynamical systems

AU - Quindlen, John F.

AU - Topcu, Ufuk

AU - Chowdhary, Girish

AU - How, Jonathan P.

PY - 2018/1/1

Y1 - 2018/1/1

N2 - Nonlinear, adaptive, or otherwise complex control techniques are increasingly relied upon to ensure the safety of systems operating in uncertain environments. However, the nonlinearity of the resulting closed-loop system complicates verification that the system does in fact satisfy those requirements at all possible operating conditions. While ana- lytical proof-based techniques and finite abstractions can be used to provably verify the closed-loop system’s response at different operating conditions, they often produce con- servative approximations due to restrictive assumptions and are dificult to construct in many applications. In contrast, popular statistical verification techniques relax the restric- tions and instead rely upon simulations to construct statistical or probabilistic guarantees. This work presents a data-driven statistical verification procedure that instead constructs statistical learning models from simulated training data to separate the set of possible perturbations into “safe” and “unsafe” subsets. Binary evaluations of closed-loop system requirement satisfaction at various realizations of the uncertainties are obtained through temporal logic robustness metrics, which are then used to construct predictive models of requirement satisfaction over the full set of possible uncertainties. As the accuracy of these predictive statistical models is inherently coupled to the quality of the training data, an active learning algorithm selects additional sample points in order to maximize the expected change in the data-driven model and thus, indirectly, minimize the prediction er- ror. Various case studies demonstrate the closed-loop verification procedure and highlight improvements in prediction error over both existing analytical and statistical verification techniques.

AB - Nonlinear, adaptive, or otherwise complex control techniques are increasingly relied upon to ensure the safety of systems operating in uncertain environments. However, the nonlinearity of the resulting closed-loop system complicates verification that the system does in fact satisfy those requirements at all possible operating conditions. While ana- lytical proof-based techniques and finite abstractions can be used to provably verify the closed-loop system’s response at different operating conditions, they often produce con- servative approximations due to restrictive assumptions and are dificult to construct in many applications. In contrast, popular statistical verification techniques relax the restric- tions and instead rely upon simulations to construct statistical or probabilistic guarantees. This work presents a data-driven statistical verification procedure that instead constructs statistical learning models from simulated training data to separate the set of possible perturbations into “safe” and “unsafe” subsets. Binary evaluations of closed-loop system requirement satisfaction at various realizations of the uncertainties are obtained through temporal logic robustness metrics, which are then used to construct predictive models of requirement satisfaction over the full set of possible uncertainties. As the accuracy of these predictive statistical models is inherently coupled to the quality of the training data, an active learning algorithm selects additional sample points in order to maximize the expected change in the data-driven model and thus, indirectly, minimize the prediction er- ror. Various case studies demonstrate the closed-loop verification procedure and highlight improvements in prediction error over both existing analytical and statistical verification techniques.

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

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

U2 - 10.2514/6.2018-1107

DO - 10.2514/6.2018-1107

M3 - Conference contribution

AN - SCOPUS:85044572982

SN - 9781624105265

T3 - AIAA Guidance, Navigation, and Control Conference, 2018

BT - AIAA Guidance, Navigation, and Control

PB - American Institute of Aeronautics and Astronautics Inc, AIAA

ER -