This paper presents an offline safety analysis framework for neural controllers in model predictive control settings. Building on the insight that a (sensed) reference trajectory can be treated as a disturbance preview, our method constructs a non-adversarial controlled invariant set that both captures realistic operating conditions and includes the adversarial disturbance set. This formulation reduces safety checking to a collection of input–output constraints on the neural network. Leveraging a neural network verifier, our approach identifies counterexamples even when nominal performance matches that of a model predictive controller baseline. In a lane-keeping automated-driving case study, we falsify three neural controllers within minutes. We demonstrate that disturbance preview reduces false alarms in counterexample search and that the workflow scales to networks of practical size. Thus, the framework offers an effective rigorous safety certification of learned controllers in cyber-physical systems.     «

This paper presents an offline safety analysis framework for neural controllers in model predictive control settings. Building on the insight that a (sensed) reference trajectory can be treated as a disturbance preview, our method constructs a non-adversarial controlled invariant set that both captures realistic operating conditions and includes the adversarial disturbance set. This formulation reduces safety checking to a collection of input–output constraints on the neural network. Leveraging...     »