TY - CPAPER 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 PY - 2018/// TI - Reachability analysis for neural agent-environment systems UR - https://aaai.org/ocs/index.php/KR/KR18/paper/view/17991 UR - http://hdl.handle.net/10044/1/63044 ER -