Automata-based Controller Synthesis for Stochastic Systems: A Game Framework via Approximate Probabilistic Relations
In this work, we propose an abstraction and refinement methodology for the controller synthesis of discrete-time stochastic systems to enforce complex logical properties expressed by deterministic finite automata (a.k.a. DFA). Our proposed scheme is based on a notion of so-called $(\epsilon,\delta)$-approximate probabilistic relations, allowing one to quantify the similarity between stochastic systems modeled by discrete-time stochastic games and their corresponding finite abstractions. Leveraging this type of relations, the lower bound for the probability of satisfying the desired specifications can be well ensured by refining controllers synthesized over abstract systems to the original games. Moreover, we propose an algorithmic procedure to construct such a relation for a particular class of nonlinear stochastic systems with slope restrictions on the nonlinearity. The proposed methods are demonstrated on a quadrotor example, and the results indicate that the desired lower bound for the probability of satisfaction is guaranteed.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
An Automaton Learning Approach to Solving Safety Games over Infinite Graphs
We propose a method to construct finite-state reactive controllers for systems whose interactions with their adversarial environment are modeled by infinite-duration two-player games over (possibly) infinite graphs. The …
Motion PlanningLearning-Based Synthesis of Safety Controllers
We propose a machine learning framework to synthesize reactive controllers for systems whose interactions with their adversarial environment are modeled by infinite-duration, two-player games over (potentially) infinite …
Motion PlanningFrom Small-Gain Theory to Compositional Construction of Barrier Certificates for Large-Scale Stochastic Systems
This paper is concerned with a compositional approach for the construction of control barrier certificates for large-scale interconnected stochastic systems while synthesizing hybrid controllers against high-level logic …
Sandboxing (AI-based) Unverified Controllers in Stochastic Games: An Abstraction-based Approach with Safe-visor Architecture
In this paper, we propose a construction scheme for a Safe-visor architecture for sandboxing unverified controllers, e.g., artificial intelligence-based (a.k.a. AI-based) controllers, in two-players non-cooperative stoch…
Compositional Construction of Control Barrier Functions for Continuous-Time Stochastic Hybrid Systems
In this work, we propose a compositional framework for the construction of control barrier functions for networks of continuous-time stochastic hybrid systems enforcing complex logic specifications expressed by finite-st…