Correct-by-Construction Control for Stochastic and Uncertain Dynamical Models via Formal Abstractions
Automated synthesis of correct-by-construction controllers for autonomous systems is crucial for their deployment in safety-critical scenarios. Such autonomous systems are naturally modeled as stochastic dynamical models. The general problem is to compute a controller that provably satisfies a given task, represented as a probabilistic temporal logic specification. However, factors such as stochastic uncertainty, imprecisely known parameters, and hybrid features make this problem challenging. We have developed an abstraction framework that can be used to solve this problem under various modeling assumptions. Our approach is based on a robust finite-state abstraction of the stochastic dynamical model in the form of a Markov decision process with intervals of probabilities (iMDP). We use state-of-the-art verification techniques to compute an optimal policy on the iMDP with guarantees for satisfying the given specification. We then show that, by construction, we can refine this policy into a feedback controller for which these guarantees carry over to the dynamical model. In this short paper, we survey our recent research in this area and highlight two challenges (related to scalability and dealing with nonlinear dynamics) that we aim to address with our ongoing research.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
A Stability-Based Abstraction Framework for Reach-Avoid Control of Stochastic Dynamical Systems with Unknown Noise Distributions
Finite-state abstractions are widely studied for the automated synthesis of correct-by-construction controllers for stochastic dynamical systems. However, existing abstraction methods often lead to prohibitively large fi…
Verifying the Unknown: Correct-by-Design Control Synthesis for Networks of Stochastic Uncertain Systems
In this paper, we present an approach for designing correct-by-design controllers for cyber-physical systems composed of multiple dynamically interconnected uncertain systems. We consider networked discrete-time uncertai…
Uncertainty Propagation in Stochastic Systems via Mixture Models with Error Quantification
Uncertainty propagation in non-linear dynamical systems has become a key problem in various fields including control theory and machine learning. In this work we focus on discrete-time non-linear stochastic dynamical sys…
Data-Driven Yet Formal Policy Synthesis for Stochastic Nonlinear Dynamical Systems
The automated synthesis of control policies for stochastic dynamical systems presents significant challenges. A standard approach is to construct a finite-state abstraction of the continuous system, typically represented…
Promises of Deep Kernel Learning for Control Synthesis
Deep Kernel Learning (DKL) combines the representational power of neural networks with the uncertainty quantification of Gaussian Processes. Hence, it is potentially a promising tool to learn and control complex dynamica…
Gaussian ProcessesUncertainty Quantification