Verifying Stochastic Hybrid Systems with Temporal Logic Specifications via Model Reduction

TL;DR

This paper introduces a scalable approach for verifying stochastic hybrid systems by reducing them to finite Markov chains using the Mori-Zwanzig method, enabling effective model checking against temporal logic specifications.

Contribution

It presents the first statistical model checking algorithms for stochastic hybrid systems using Markov chain reductions and distributional equivalence.

Findings

Constructed finite Markov chain reductions of stochastic hybrid systems.

Proved approximate distributional equivalence between original and reduced models.

Developed statistical model checking algorithms for iLTL and MITL properties.

Abstract

We present a scalable methodology to verify stochastic hybrid systems. Using the Mori-Zwanzig reduction method, we construct a finite state Markov chain reduction of a given stochastic hybrid system and prove that this reduced Markov chain is approximately equivalent to the original system in a distributional sense. Approximate equivalence of the stochastic hybrid system and its Markov chain reduction means that analyzing the Markov chain with respect to a suitably strengthened property, allows us to conclude whether the original stochastic hybrid system meets its temporal logic specifications. We present the first statistical model checking algorithms to verify stochastic hybrid systems against correctness properties, expressed in the linear inequality linear temporal logic (iLTL) or the metric interval temporal logic (MITL).