摘要：AbstractWe consider the controller synthesis problem for stochastic, continuous-state, nonlinear systems against ω-regular specifications. We synthesize a symbolic controller that ensuresalmost sure(qualitative) satisfaction of the specification. The problem reduces, after some automata-theoretic constructions, to computing thealmost sure winning region—thelargest 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 tosymbolicallycompute this under-approximation via afinite-state abstractionas a21/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.
关键词：KeywordsAbstraction-based control designApproximate model checkingDiscrete-time stochastic systemsFinite gamesFormal specificationsPolicy synthesis
