A two-step scheme for approximate model checking of stochastic hybrid systems
- Conference Paper
In this paper we describe a two-step scheme for approximate model checking of discrete time stochastic hybrid systems. In the first step, the stochastic hybrid system is approximated by a finite state Markov chain. In the second step, the Markov chain is model checked for the desired property. In particular, we consider the probabilistic invariance property and show that, under certain regularity conditions, the invariance probability computed using the approximating Markov chain converges to the invariance probability of the original stochastic hybrid system, as the grid used in the approximation gets finer. A bound on the convergence rate is also provided. Show more
Book titleProceedings of the 18th World Congress
Journal / seriesIFAC Proceedings Volumes
Pages / Article No.
Organisational unit03751 - Lygeros, John / Lygeros, John
MoreShow all metadata