[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]
|
Abstract.
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.
|