Validation of Neural Network-Based Controllers in Closed Loop Systems with UPPAAL SMC

The analysis of a neural network controller in a closed loop system is fundamental, especially in safety-critical domains such as autonomous transportation and industrial automation, where controller reliability directly impacts operational safety. For controllers implemented via neural networks, traditional control theory fails to accommodate theirs complex and black-box nature. This paper introduces an approach to statistically validate the behavior of such a closed loop system under a variety of operation scenarios based on statistical model checking. The proposed approach establishes a Python-UPPAAL interface, enabling inference on PyTorch models from a network of stochastic timed automata.