Verifying Continuous-time Stochastic Hybrid Systems via Mori-Zwanzig model reduction

Yu Wang; Nima Roohi; Matthew West; Mahesh Viswanathan; Geir E. Dullerud

doi:10.1109/CDC.2016.7798719

Verifying Continuous-time Stochastic Hybrid Systems via Mori-Zwanzig model reduction

Yu Wang, Nima Roohi, Matthew West, Mahesh Viswanathan, Geir E. Dullerud

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

Abstract

In this work, we develop a method for verifying Continuous-time Stochastic Hybrid Systems (CTSHSs) using the Mori-Zwanzig model reduction method, whose behaviors are specified by Metric Interval Temporal Logic (MITL) formulas. By partitioning the state space of the CTSHS and computing the optimal transition rates between partitions, we provide a procedure to both reduce a CTSHS to a Continuous-Time Markov Chain (CTMC), and the associated MITL formulas defined on the CTSHS to MITL specifications on the CTMC. We prove that an MITL formula on the CTSHS is true (or false) if the corresponding MITL formula on the CTMC is robustly true (or false) under certain perturbations. In addition, we propose a stochastic algorithm to complete the verification. Finally, as an example, we implement the method in a Billiard Problem.

Original language	English (US)
Title of host publication	2016 IEEE 55th Conference on Decision and Control, CDC 2016
Publisher	Institute of Electrical and Electronics Engineers Inc.
Pages	3012-3017
Number of pages	6
ISBN (Electronic)	9781509018376
DOIs	https://doi.org/10.1109/CDC.2016.7798719
State	Published - Dec 27 2016
Event	55th IEEE Conference on Decision and Control, CDC 2016 - Las Vegas, United States Duration: Dec 12 2016 → Dec 14 2016

Publication series

Name	2016 IEEE 55th Conference on Decision and Control, CDC 2016

Other

Other	55th IEEE Conference on Decision and Control, CDC 2016
Country/Territory	United States
City	Las Vegas
Period	12/12/16 → 12/14/16

ASJC Scopus subject areas

Artificial Intelligence
Decision Sciences (miscellaneous)
Control and Optimization

Online availability

10.1109/CDC.2016.7798719

Library availability

Discover UIUC Full Text

Cite this

Wang, Y., Roohi, N., West, M., Viswanathan, M., & Dullerud, G. E. (2016). Verifying Continuous-time Stochastic Hybrid Systems via Mori-Zwanzig model reduction. In 2016 IEEE 55th Conference on Decision and Control, CDC 2016 (pp. 3012-3017). Article 7798719 (2016 IEEE 55th Conference on Decision and Control, CDC 2016). Institute of Electrical and Electronics Engineers Inc.. https://doi.org/10.1109/CDC.2016.7798719

Verifying Continuous-time Stochastic Hybrid Systems via Mori-Zwanzig model reduction. / Wang, Yu; Roohi, Nima; West, Matthew et al.
2016 IEEE 55th Conference on Decision and Control, CDC 2016. Institute of Electrical and Electronics Engineers Inc., 2016. p. 3012-3017 7798719 (2016 IEEE 55th Conference on Decision and Control, CDC 2016).

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

Wang, Y, Roohi, N, West, M , Viswanathan, M & Dullerud, GE 2016, Verifying Continuous-time Stochastic Hybrid Systems via Mori-Zwanzig model reduction. in 2016 IEEE 55th Conference on Decision and Control, CDC 2016., 7798719, 2016 IEEE 55th Conference on Decision and Control, CDC 2016, Institute of Electrical and Electronics Engineers Inc., pp. 3012-3017, 55th IEEE Conference on Decision and Control, CDC 2016, Las Vegas, United States, 12/12/16. https://doi.org/10.1109/CDC.2016.7798719

Wang Y, Roohi N, West M , Viswanathan M , Dullerud GE. Verifying Continuous-time Stochastic Hybrid Systems via Mori-Zwanzig model reduction. In 2016 IEEE 55th Conference on Decision and Control, CDC 2016. Institute of Electrical and Electronics Engineers Inc. 2016. p. 3012-3017. 7798719. (2016 IEEE 55th Conference on Decision and Control, CDC 2016). doi: 10.1109/CDC.2016.7798719

@inproceedings{a6ef4d62c53245878468f7961bb50c07,

title = "Verifying Continuous-time Stochastic Hybrid Systems via Mori-Zwanzig model reduction",

abstract = "In this work, we develop a method for verifying Continuous-time Stochastic Hybrid Systems (CTSHSs) using the Mori-Zwanzig model reduction method, whose behaviors are specified by Metric Interval Temporal Logic (MITL) formulas. By partitioning the state space of the CTSHS and computing the optimal transition rates between partitions, we provide a procedure to both reduce a CTSHS to a Continuous-Time Markov Chain (CTMC), and the associated MITL formulas defined on the CTSHS to MITL specifications on the CTMC. We prove that an MITL formula on the CTSHS is true (or false) if the corresponding MITL formula on the CTMC is robustly true (or false) under certain perturbations. In addition, we propose a stochastic algorithm to complete the verification. Finally, as an example, we implement the method in a Billiard Problem.",

author = "Yu Wang and Nima Roohi and Matthew West and Mahesh Viswanathan and Dullerud, {Geir E.}",

note = "Publisher Copyright: {\textcopyright} 2016 IEEE.; 55th IEEE Conference on Decision and Control, CDC 2016 ; Conference date: 12-12-2016 Through 14-12-2016",

year = "2016",

month = dec,

day = "27",

doi = "10.1109/CDC.2016.7798719",

language = "English (US)",

series = "2016 IEEE 55th Conference on Decision and Control, CDC 2016",

publisher = "Institute of Electrical and Electronics Engineers Inc.",

pages = "3012--3017",

booktitle = "2016 IEEE 55th Conference on Decision and Control, CDC 2016",

address = "United States",

}

TY - GEN

T1 - Verifying Continuous-time Stochastic Hybrid Systems via Mori-Zwanzig model reduction

AU - Wang, Yu

AU - Roohi, Nima

AU - West, Matthew

AU - Viswanathan, Mahesh

AU - Dullerud, Geir E.

PY - 2016/12/27

Y1 - 2016/12/27

N2 - In this work, we develop a method for verifying Continuous-time Stochastic Hybrid Systems (CTSHSs) using the Mori-Zwanzig model reduction method, whose behaviors are specified by Metric Interval Temporal Logic (MITL) formulas. By partitioning the state space of the CTSHS and computing the optimal transition rates between partitions, we provide a procedure to both reduce a CTSHS to a Continuous-Time Markov Chain (CTMC), and the associated MITL formulas defined on the CTSHS to MITL specifications on the CTMC. We prove that an MITL formula on the CTSHS is true (or false) if the corresponding MITL formula on the CTMC is robustly true (or false) under certain perturbations. In addition, we propose a stochastic algorithm to complete the verification. Finally, as an example, we implement the method in a Billiard Problem.

AB - In this work, we develop a method for verifying Continuous-time Stochastic Hybrid Systems (CTSHSs) using the Mori-Zwanzig model reduction method, whose behaviors are specified by Metric Interval Temporal Logic (MITL) formulas. By partitioning the state space of the CTSHS and computing the optimal transition rates between partitions, we provide a procedure to both reduce a CTSHS to a Continuous-Time Markov Chain (CTMC), and the associated MITL formulas defined on the CTSHS to MITL specifications on the CTMC. We prove that an MITL formula on the CTSHS is true (or false) if the corresponding MITL formula on the CTMC is robustly true (or false) under certain perturbations. In addition, we propose a stochastic algorithm to complete the verification. Finally, as an example, we implement the method in a Billiard Problem.

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

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

U2 - 10.1109/CDC.2016.7798719

DO - 10.1109/CDC.2016.7798719

M3 - Conference contribution

AN - SCOPUS:85010837002

T3 - 2016 IEEE 55th Conference on Decision and Control, CDC 2016

SP - 3012

EP - 3017

BT - 2016 IEEE 55th Conference on Decision and Control, CDC 2016

PB - Institute of Electrical and Electronics Engineers Inc.

T2 - 55th IEEE Conference on Decision and Control, CDC 2016

Y2 - 12 December 2016 through 14 December 2016

ER -

Verifying Continuous-time Stochastic Hybrid Systems via Mori-Zwanzig model reduction

Abstract

Publication series

Other

ASJC Scopus subject areas

Online availability

Library availability

Related links

Fingerprint

Cite this