Oxford logo
[ABK+17] A. Abate, L. Bortolussi, M. Kwiatkowska, L. Cardelli, M. Ceska and L. Laurenti. Reachability Computation for Switching Diffusions: Finite Abstractions with Certifiable and Tuneable Precision. In Hybrid Systems: Computation and Control, 20th ACM International Conference, ACM. To appear. 2017. [pdf] [bib]
Downloads:  pdf pdf (337 KB)  bib bib
Abstract. We consider continuous time stochastic hybrid systems with no resets and continuous dynamics described by linear stochastic diff erential equations - models also known as switching diff usions. We show that for this class of models reachability (and dually, safety) properties can be studied on an abstraction defi ned in terms of a discrete time and finite space Markov chain (DTMC), with provable error bounds. The technical contribution of the paper is a characterization of the uniform convergence of the time discretization of such stochastic processes with respect to safety properties. This allows us to newly provide a complete and sound numerical procedure for reachability and safety computation over switching diff usions.