Symbolic Qualitative Control for Stochastic Systems via Finite Parity Games⁎R. Majumdar and K. Mallik are funded through the DFG (Deutsche Forschungsgemeinschaft or German Science Foundation) project 389792660 TRR 248-CPEC, A.-K. Schmuck is funded through the DFG project SCHM 3541/1-1, and S. Soudjani is funded through the EPSRC-funded CodeCPS project (EP/V043676/1). Issue 5 (2021) - Majumdar, Rupak; Mallik, Kaushik; Schmuck, Anne-Kathrin; Soudjani, Sadegh
Abstract: 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.