University of Birmingham > Talks@bham > Theoretical computer science seminar > Bounded and Unbounded Verification of RNN-Based Agents in Non-deterministic Environments

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

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact George Kaye.

Zoom details


In this talk I will present our research on the verification of bounded and unbounded temporal specifications of closed-loop Agent-Environment Systems (AESs) with memoryful agents. This presentation is based on our paper, titled “Bounded and Unbounded Verification of RNN -Based Agents in Non-deterministic Environments”, appearing in AAMAS 2023 . Such AESs are useful for modelling and analysing the interactions of autonomous agents within uncertain environments. Examples of such scenarios are Autonomous Unmanned Vehicles (AUVs), deployed in unfamiliar environments, where the vehicle has to remember past actions and observations. We assume that the memory of the agents is implemented using a Recurrent Neural Network (RNN). We introduce an approach based on Bound Propagation (BP) and Mixed-Integer Linear Programming (MILP) to verify temporal specifications of such systems. Not only does this approach, for the first time, allow us to verify unbounded temporal specifications of AESs with memoryful agents, but it also allows for more optimised complete and sound verification of bounded temporal specifications of such AESs.

This talk is part of the Theoretical computer science seminar series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


Talks@bham, University of Birmingham. Contact Us | Help and Documentation | Privacy and Publicity.
talks@bham is based on from the University of Cambridge.