Approximate probabilistic verification of hybrid systems

TL;DR

This paper introduces a probabilistic approximation method for analyzing hybrid systems governed by non-linear ODEs, enabling verification of biological models against temporal logic specifications.

Contribution

It develops a novel stochastic approximation of hybrid systems as Markov chains, facilitating probabilistic verification of complex biological models.

Findings

Applicable to biological processes like cardiac and circadian systems

Provides a sequential hypothesis testing procedure for high-probability verification

Demonstrates effectiveness through case studies on real biological models

Abstract

Hybrid systems whose mode dynamics are governed by non-linear ordinary differential equations (ODEs) are often a natural model for biological processes. However such models are difficult to analyze. To address this, we develop a probabilistic analysis method by approximating the mode transitions as stochastic events. We assume that the probability of making a mode transition is proportional to the measure of the set of pairs of time points and value states at which the mode transition is enabled. To ensure a sound mathematical basis, we impose a natural continuity property on the non-linear ODEs. We also assume that the states of the system are observed at discrete time points but that the mode transitions may take place at any time between two successive discrete time points. This leads to a discrete time Markov chain as a probabilistic approximation of the hybrid system. We then show that for BLTL (bounded linear time temporal logic) specifications the hybrid system meets a specification iff its Markov chain approximation meets the same specification with probability $1$. Based on this, we formulate a sequential hypothesis testing procedure for verifying -approximately- that the Markov chain meets a BLTL specification with high probability. Our case studies on cardiac cell dynamics and the circadian rhythm indicate that our scheme can be applied in a number of realistic settings.