Correct-by-Design Synthesis of Neural Network Controllers

Abstract

The use of artificial neural networks is becoming ever more ubiquitous as the computational power available to use grows. The widespread implementation of neural networks as controllers in the field of systems and control is however being hindered by the lack of verifiability of these controllers. One type of controller that does not lack verifiability is the correct-by-design controller. The main drawback of correct-by-design controllers is that they inherently produce large data structures in order to store their control rules. In this work, a novel methodology to synthesize correct-by-design neural network controllers is presented in order to alleviate these issues. This methodology combines reinforcement learning techniques and abstraction based correct-by-design control verification techniques in order to synthesize neural network controllers that are correct-by-design. The procedure does so by alternating between a controller training routine and a controller verification routine in a system abstraction framework. This framework ensures that numerical training and verification results in a controller with formal guarantees applicable to real systems. Using the proposed methodology, neural network controllers are synthesized and verified in order to prove that the methodology works. In addition to this, the resulting correct-by-design neural network controllers are compared to conventional correct-by-design controllers in order to judge their performance and data requirements. This comparison also includes alternative structures used to store these different controllers. Based on this comparison, a conclusion is drawn regarding when to use which type of controller. The proposed methodology is implemented into a correct-by-design neural network synthesis framework called COSYNNC. This framework is intended as a basis for further research into correct-by-design neural network control and is publicly available.