NNSynth: Neural Network Guided Abstraction-Based Controller Synthesis for Stochastic Systems

TL;DR

NNSynth introduces a neural network-guided framework for abstraction-based controller synthesis in stochastic systems, significantly accelerating the process while maintaining correctness guarantees.

Contribution

It presents a novel method combining neural networks with abstraction-based synthesis, enabling faster controller design for complex stochastic systems.

Findings

Achieves over 50x speedup in high-dimensional systems

Uses neural networks to guide controller search efficiently

Maintains correctness guarantees in controller synthesis

Abstract

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.