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

In the last decade, abstraction-based controller synthesis techniques have gained considerable attention due to their ability to synthesize correct-by-design feedback controllers from high-level specifications. Nevertheless, a significant drawback of these techniques is the need to explore large spaces of quantized state and input spaces to find a controller that satisfies the specification. On the contrary, recent advances in machine learning, in particular imitation learning and reinforcement learning, paved the way to several techniques to design controllers (or policies) for highly nonlinear systems with large state and input spaces, albeit their lack of rigorous correctness guarantees. This motivates the question of how to use machine learning techniques to guide the synthesis of abstraction-based controllers. In this paper, we introduce NNSynth, a novel tool for abstraction-based controller synthesis. Unique to NNSynth is the use of machine learning techniques to guide the search over the space of controllers to find candidate Neural Network (NN)-based controllers. Next, these NNs are "projected" and the control actions that are close to the NN outputs are used to construct a "local" abstraction for the system. An abstraction-based controller is then synthesized from such a "local" abstract model. If a controller that satisfies the specifications is not found, then the best found controller is "lifted" to a neural network controller for additional training. Our experiments show that this neural network-guided synthesis leads to more than 50x or even 100x speedup in high dimensional systems compared to the state-of-the-art.