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)

• Record Type: Journal Article
• Authors: Majumdar, Rupak; Mallik, Kaushik; Schmuck, Anne-Kathrin; Soudjani, Sadegh
• Is Part Of: IFAC-PapersOnLine. Volume 54:Issue 5(2021)
• Page Start: 127
• Page End: 132
• Publication Date: 2021
• Subjects: Abstraction-based control design -- Approximate model checking -- Discrete-time stochastic systems -- Finite games -- Formal specifications -- Policy synthesis; Automatic control -- Periodicals; 629.805
• DOI: 10.1016/j.ifacol.2021.08.486
• Languages: English
• ISSNs: 2405-8963

Abstract

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.