NNSynth: Neural Network Guided Abstraction-Based Controller Synthesis for Stochastic Systems
In this paper, we introduce NNSynth, a new framework that uses machine learning techniques to guide the design of abstraction-based controllers with correctness guarantees. NNSynth utilizes neural networks (NNs) to guide the search over the space of controllers. The trained neural networks are "projected" and used for constructing a "local" abstraction of the system. An abstraction-based controller is then synthesized from such "local" abstractions. If a controller that satisfies the specifications is not found, then the best found controller is "lifted" to a neural network for additional training. Our experiments show that this neural network-guided synthesis leads to more than $50\times$ or even $100\times$ speedup in high dimensional systems compared to the state-of-the-art.
Code (0)
등록된 구현이 없습니다.
Tasks
Imitation LearningSimilar 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…
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.…
Correct-by-construction reach-avoid control of partially observable linear stochastic systems
We study feedback controller synthesis for reach-avoid control of discrete-time, linear time-invariant (LTI) systems with Gaussian process and measurement noise. The problem is to compute a controller such that, with at …
Continuous ControlProbabilities Are Not Enough: Formal Controller Synthesis for Stochastic Dynamical Models with Epistemic Uncertainty
Capturing uncertainty in models of complex dynamical systems is crucial to designing safe controllers. Stochastic noise causes aleatoric uncertainty, whereas imprecise knowledge of model parameters leads to epistemic unc…
Formal Controller Synthesis for Markov Jump Linear Systems with Uncertain Dynamics
Automated synthesis of provably correct controllers for cyber-physical systems is crucial for deployment in safety-critical scenarios. However, hybrid features and stochastic or unknown behaviours make this problem chall…