Bisimilar finite abstractions of stochastic control systems

Abstraction-based approaches to the design of complex control systems construct finite-state models that are formally related to the original control systems, then leverage symbolic techniques from finite-state synthesis to compute controllers satisfying specifications given in a temporal logic, and finally refine the obtained control schemes back to the given concrete complex models. While such approaches have been successfully used to perform synthesis over non-probabilistic control systems, there are only few results available for probabilistic models: hence the goal of this paper, which considers continuous-time controlled stochastic differential equations. We show that for every stochastic control system satisfying a stochastic version of incremental input-to-state stability, and for every ε > 0, there exists a finite-state abstraction that is ε-approximate bisimilar to the stochastic control system (in the sense of moments). We demonstrate the effectiveness of the construction by synthesizing a controller for a stochastic control system with respect to linear temporal logic specifications. Since stochastic control systems are a common mathematical models for many complex safety critical systems subject to uncertainty, our techniques promise to enable a new, automated, correct-by-construction controller synthesis approach for these systems.