Poster Abstract: Controller Synthesis for Nonlinear Stochastic Games via Approximate Probabilistic Relations

Motivations. In the past two decades, synthesizing correct-byconstruction controllers for continuous-space stochastic systems has received significant attentions in real-life safety-critical applications, such as self-driving cars, power grids, etc. However, formal controller synthesis for complex stochastic systems with continuous state and input sets is very challenging since there is no closed-form solutions of these controllers in general. To cope with this difficulty, a promising approach is to approximate the original continuous-space systems by simpler ones with finite-state sets (a.k.a., finite abstractions). A critical step during this approximation phase is to provide formal guarantees when refining the controller synthesized over (simpler) finite models back to original complex systems. Related Works and Contributions. An abstraction-based approach for synthesizing controllers over stochastic systems with continuous state and input sets was initially proposed in [2]. Later on, this approach was improved and extended in terms of scalability, specifications, and different probabilistic guarantees. We refer the interested readers to [5] for more details and related literature. In this work, we focus on synthesizing controllers for those stochastic systems affected by both control inputs and (rational) adversarial inputs over finite time horizon. In particular, the objectives of these adversarial inputs are opposed to that of control inputs, and we, therefore, model such systems as general discrete-time stochastic games (gDTSGs) between two non-cooperative players. Based on these settings, we propose abstraction-based approaches to synthesize controllers over gDTSGs against high-level logic specifications characterized by deterministic finite automata (DFA) [3]. Particularly, we propose our techniques on top of an (?, d)-approximate probabilistic relation [6] that characterizes the probabilistic dependency between the original game and its finite abstraction. Compared with those results (e.g., [4]) that employ a grid-based approximation framework without considering such dependency in the controller synthesis phase, our results provide less conservative lower bounds on the probability of satisfying the desired properties.