Symbolic Control for Stochastic Systems via Finite Parity Games
We consider the problem of computing the maximal probability of satisfying an omega-regular specification for stochastic nonlinear systems evolving in discrete time. The problem reduces, after automata-theoretic constructions, to finding the maximal probability of satisfying a parity condition on a (possibly hybrid) state space. While characterizing the exact satisfaction probability is open, we show that a lower bound on this probability can be obtained by (I) computing an under-approximation of the qualitative winning region, i.e., states from which the parity condition can be enforced almost surely, and (II) computing the maximal probability of reaching this qualitative winning region. The heart of our approach is a technique to symbolically compute the under-approximation of the qualitative winning region in step (I) via a finite-state abstraction of the original system as a 2.5-player parity game. Our abstraction procedure uses only the support of the probabilistic evolution; it does not use precise numerical transition probabilities. We prove that the winning set in the abstract 2.5-player game induces an under-approximation of the qualitative winning region in the original synthesis problem, along with a policy to solve it. By combining these contributions with (a) a symbolic fixpoint algorithm to solve 2.5-player games and (b) existing techniques for reachability policy synthesis in stochastic nonlinear systems, we get an abstraction-based algorithm for finding a lower bound on the maximal satisfaction probability. We have implemented the abstraction-based algorithm in Mascot-SDS (Majumdar et al., 2020), where we combined the outlined abstraction step with our recent tool FairSyn. We evaluated our implementation on the nonlinear model of a perturbed bistable switch from the literature. We outperform a recently proposed tool for solving this problem by a large margin.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Winning Strategy Templates for Stochastic Parity Games towards Permissive and Resilient Control
Stochastic games play an important role for many purposes such as the control of cyber-physical systems (CPS), where the controller and the environment are modeled as players. Conventional algorithms typically solve the …
Symbolic Models for Infinite Networks of Control Systems: A Compositional Approach
This paper presents a compositional framework for the construction of symbolic models for a network composed of a countably infinite number of finite-dimensional discrete-time control subsystems. We refer to such a netwo…
QuantizationVerified Compositional Neuro-Symbolic Control for Stochastic Systems with Temporal Logic Tasks
Several methods have been proposed recently to learn neural network (NN) controllers for autonomous agents, with unknown and stochastic dynamics, tasked with complex missions captured by Linear Temporal Logic (LTL). Due …
Robot NavigationSymbolic Self-triggered Control of Continuous-time Non-deterministic Systems without Stability Assumptions for 2-LTL Specifications
We propose a symbolic self-triggered controller synthesis procedure for non-deterministic continuous-time nonlinear systems without stability assumptions. The goal is to compute a controller that satisfies two objectives…
Regression under demographic parity constraints via unlabeled post-processing
We address the problem of performing regression while ensuring demographic parity, even without access to sensitive attributes during inference. We present a general-purpose post-processing algorithm that, using accurate…
AttributeMulti-class Classificationregression