Abstract
In this work, we introduce a framework for the statistical verification of Metric Interval Temporal Logic (MITL) formulas on continuous-time dynamical systems. By considering the continuous-time Markov process associated with the dynamical system, we apply the Mori-Zwanzig method to reduce the original system to a Continuous-Time Markov Chain (CTMC). Accordingly, the MITL formulas on the original system can be reduced to MITL formulas on the CTMC. Furthermore, we propose a statistical verification algorithm for checking the MITL formulas on the CTMCand show that the original MITL formulas on the original system can be checked by this procedure.
| Original language | English (US) |
|---|---|
| Pages (from-to) | 267-273 |
| Number of pages | 7 |
| Journal | IFAC-PapersOnLine |
| Volume | 48 |
| Issue number | 27 |
| DOIs | |
| State | Published - 2015 |
ASJC Scopus subject areas
- Control and Systems Engineering