Learning and Verification of Dynamical Systems with Neural Network Components

Abstract

Cyber-physical systems (CPSs) with learning-enable components (LECs) are becoming very popular, especially in the area of autonomous vehicles such as unmanned aircraft, autonomous and partially autonomous cars, and underwater vehicles. However, before they can be widely adopted in these safety-critical applications, we need to ensure their design and operation are correct and safe. The main challenges to verify their behavior include the formal modelling of the dynamics defining the interaction of the CPS with the real world, and the lack of transparency on the internal operation of the LECs. The following dissertation presents approaches to both challenges and case studies to evaluate the performance of our techniques. We present a novel method for learning the behavior of dynamical systems that present both continuous and discrete dynamics with the use of a hybrid automata learning framework with nonlinear dynamics. We also present case studies on the verification of autonomous CPS with LECs, more specifically with feedforward neural network controllers. Finally, we present a formal verification framework for a recently introduced deep learning architecture that can be utilized both as a part of a control system and as a dynamical model, named neural ordinary differential equations (neural ODEs). We extend its definition to provide a general class of neural ODEs, and evaluate our verification framework on several benchmarks in the area of dynamical systems, control systems and image recognition.