Skip to main content

Formal verification of neural agents in non-deterministic environments

Akintunde, Michael E., Botoeva, Elena, Kouvaros, Panagiotis, Lomuscio, Alessio (2021) Formal verification of neural agents in non-deterministic environments. Autonomous Agents and Multi-Agent Systems, 36 (1). Article Number 6. ISSN 1387-2532. E-ISSN 1573-7454. (doi:10.1007/s10458-021-09529-3) (KAR id:92680)

PDF Publisher pdf
Language: English

Download (2MB) Preview
[thumbnail of Akintunde2021_Article_FormalVerificationOfNeuralAgen.pdf]
This file may not be suitable for users of assistive technology.
Request an accessible format
Official URL:


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.

Item Type: Article
DOI/Identification number: 10.1007/s10458-021-09529-3
Uncontrolled keywords: Verifcation; Model checking; Neural agents
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 75 Electronic computers. Computer science
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: Amy Boaler
Date Deposited: 13 Jan 2022 11:32 UTC
Last Modified: 14 Jan 2022 09:03 UTC
Resource URI: (The current URI for this page, for reference purposes)
  • Depositors only (login required):


Downloads per month over past year