Imperial College London
Portrait Picture

ProfessorAlessioLomuscio

Faculty of Engineering, Department of Computing

Professor of Safe Artificial Intelligence
 
 
 
//

Contact

 

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

 
 
//

Location

 

Imperial-XTranslation & Innovation Hub BuildingWhite City Campus

//

Summary

 

Publications

Citation

BibTex format

@article{Akintunde:2022:10.1007/s10458-021-09529-3,
author = {Akintunde, ME and Botoeva, E and Kouvaros, P and Lomuscio, A},
doi = {10.1007/s10458-021-09529-3},
journal = {Autonomous Agents and Multi-Agent Systems},
title = {Formal verification of neural agents in non-deterministic environments},
url = {http://dx.doi.org/10.1007/s10458-021-09529-3},
volume = {36},
year = {2022}
}
Download

RIS format (EndNote, RefMan)

TY  - JOUR
AB  - We introduce a model for agent-environment systems where the agents are implemented via feed-forward ReLU neural networks and the environment is non-deterministic. We study the verification problem of such systems against CTL properties. We show that verifying these systems against reachability properties is undecidable. We introduce a bounded fragment of CTL, show its usefulness in identifying shallow bugs in the system, and prove that the verification problem against specifications in bounded CTL is in coNEXPTIME and PSPACE-hard. We introduce sequential and parallel algorithms for MILP-based verification of agent-environment systems, present an implementation, and report the experimental results obtained against a variant of the VerticalCAS use-case and the frozen lake scenario.
AU  - Akintunde,ME
AU  - Botoeva,E
AU  - Kouvaros,P
AU  - Lomuscio,A
DO  - 10.1007/s10458-021-09529-3
PY  - 2022///
SN  - 1387-2532
TI  - Formal verification of neural agents in non-deterministic environments
T2  - Autonomous Agents and Multi-Agent Systems
UR  - http://dx.doi.org/10.1007/s10458-021-09529-3
UR  - http://gateway.webofknowledge.com/gateway/Gateway.cgi?GWVersion=2&SrcApp=PARTNER_APP&SrcAuth=LinksAMR&KeyUT=WOS:000716471800006&DestLinkType=FullRecord&DestApp=ALL_WOS&UsrCustomerID=1ba7043ffcc86c417c072aa74d649202
UR  - https://link.springer.com/article/10.1007/s10458-021-09529-3
UR  - http://hdl.handle.net/10044/1/95834
VL  - 36
ER  -
Download