Approximate probabilistic verification of hybrid systems
From MaRDI portal
Applications of Markov chains and discrete-time Markov processes on general state spaces (social mobility, learning theory, industrial processes, etc.) (60J20) Systems biology, networks (92C42) Control/observation systems governed by functional relations other than differential equations (such as hybrid and switching systems) (93C30)
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 . 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.
Recommendations
Cited in
(7)- Higher-order approximations for verification of stochastic hybrid systems
- Hybrid Systems: Computation and Control
- Bounded Verification of Reachability of Probabilistic Hybrid Systems
- End-to-end statistical model checking for parametric ODE models
- Approximate model checking of stochastic hybrid systems
- End-to-end statistical model checking for parameterization and stability analysis of ODE models
- A formal mathematical framework for modeling probabilistic hybrid systems
This page was built for publication: Approximate probabilistic verification of hybrid systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5376905)
