Symbolic Qualitative Control for Stochastic Systems via Finite Parity Games

We consider the controller synthesis problem for stochastic, continuous-state, nonlinear systems against ω-regular specifications. We synthesize a symbolic controller that ensures almost sure (qualitative) satisfaction of the specification. The problem reduces, after some automata-theoretic constructions, to computing the almost sure winning region—the largest set of states from which a parity condition can be satisfied with probability 1 (on a possibly hybrid state space). While characterizing the exact almost sure winning region is still open for the considered system class, we propose an algorithm for obtaining a tight under-approximation of this set. The heart of our approach is a technique to symbolically compute this under-approximation via a finite-state abstraction as a 21/2-player parity game. Our abstraction procedure uses only the support of the probabilistic evolution; it does not use precise numerical transition probabilities. We have implemented our approach and evaluated it on the nonlinear model of the perturbed Dubins vehicle.