AAAI Publications, Sixteenth International Conference on Principles of Knowledge Representation and Reasoning

Font Size: 
Reachability Analysis for Neural Agent-Environment Systems
Michael Akintunde, Alessio Lomuscio, Lalit Maganti, Edoardo Pirovano

Last modified: 2018-11-28


We develop a novel model for studying agent-environment systems, where the agents are implemented via feed-forward ReLU neural networks. We provide a semantics and develop a method to verify automatically that no unwanted states are reached by the system during its evolution. We study several reachability problems for the system, ranging from one-step reachability, to fixed multi-step and arbitrary-step to study the system evolution. We also study the decision problem of whether an agent, realised via feed-forward ReLU networks will perform an action in a system run. Whenever possible, we give tight complexity bounds to decision problems intro- duced. We automate the various reachability problems stud- ied by recasting them as mixed-integer linear programming problems. We present an implementation and discuss the ex- perimental results obtained on a range of test cases.


Verification, Neural Networks, Learning-enabled Cyber-physical Systems

Full Text: PDF