Bounded and Unbounded Verification of RNN-Based Agents in Non-deterministic Environments

We consider closed-loop Agent-Environment Systems (AESs), where the agent is controlled by a Recurrent Neural Network (RNN) with ReLU activations in a non-deterministic environment. We introduce a new approach based on Mixed-Integer Linear Programming to verify such systems, which allows for more optimised complete and sound verification of bounded temporal properties of such AESs. Using our approach, we additionally, devise a sound algorithm for the unbounded verification of such AESs for the first time.