Imperial College London


Faculty of EngineeringDepartment of Computing

Professor of Logic for Multiagent Systems



+44 (0)20 7594 8414a.lomuscio Website




504Huxley BuildingSouth Kensington Campus






BibTex format

author = {Lomuscio, AR and akitunde, M and maganti, L and Pirovano, E},
publisher = {Association for the Advancement of Artificial Intelligence},
title = {Reachability Analysis for Neural Agent-Environment Systems},
url = {},

RIS format (EndNote, RefMan)

AB - We develop a novel model for studying agent-environmentsystems, where the agents are implemented via feed-forwardReLU neural networks. We provide a semantics and developa method to verify automatically that no unwanted states arereached by the system during its evolution. We study severalreachability problems for the system, ranging from one-stepreachability, to fixed multi-step and arbitrary-step to studythe system evolution. We also study the decision problem ofwhether an agent, realised via feed-forward ReLU networkswill 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 programmingproblems. We present an implementation and discuss the ex-perimental results obtained on a range of test cases.
AU - Lomuscio,AR
AU - akitunde,M
AU - maganti,L
AU - Pirovano,E
PB - Association for the Advancement of Artificial Intelligence
TI - Reachability Analysis for Neural Agent-Environment Systems
UR -
ER -