Reachability computation for switching diffusions: Finite abstractions with certifiable and tuneable precision - Laurenti, L; Abate, A; Bortolussi, L; Cardelli, L; Ceska, M; Kwiatkowska, M (Association for Computing Machinery, 2017)
We consider continuous time stochastic hybrid systems with no resets and continuous dynamics described by linear stochastic differential equations - models also known as switching diffusions. We show that for this class of models reachability (and dually, safety) properties can be studied on an abstraction defined 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 diffusions.