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

Research output: Chapter in Book/Report/Conference proceedingConference 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 languageEnglish (US)
Title of host publication2016 IEEE 55th Conference on Decision and Control, CDC 2016
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages3012-3017
Number of pages6
ISBN (Electronic)9781509018376
DOIs
StatePublished - Dec 27 2016
Event55th IEEE Conference on Decision and Control, CDC 2016 - Las Vegas, United States
Duration: Dec 12 2016Dec 14 2016

Publication series

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

Other

Other55th IEEE Conference on Decision and Control, CDC 2016
CountryUnited States
CityLas Vegas
Period12/12/1612/14/16

ASJC Scopus subject areas

  • Artificial Intelligence
  • Decision Sciences (miscellaneous)
  • Control and Optimization

Fingerprint Dive into the research topics of 'Verifying Continuous-time Stochastic Hybrid Systems via Mori-Zwanzig model reduction'. Together they form a unique fingerprint.

Cite this