Controller Synthesis for Probabilistic Safety Specifications using Observers.

We present a method for the correct-by-design synthesis of controllers that maximize the safety probability of partially observable stochastic systems. Given a stochastic system with outputs that are corrupted by Gaussian measurement noise, we construct a stochastically contracting observer that produces estimates of the internal state of the system. The contractivity guarantees that the distance between the internal state and the estimate produced by the observer remains bounded, and we can treat the observer as a fully observable abstraction of the original system. For the bounded-horizon probabilistic safety objective, we can synthesize a control law for the observer using a modified safe region according to the bound on the distance above. The control law applied to the original system guarantees that the safety objective is met with some given probability. We showcase the approach on a temperature control problem using a Kalman filter as the observer for a linear stochastic model.