This HTML5 document contains 22 embedded RDF statements represented using HTML+Microdata notation.

The embedded RDF content will be recognized by any processor of HTML5 Microdata.

Namespace Prefixes

PrefixIRI
dctermshttp://purl.org/dc/terms/
n2https://kar.kent.ac.uk/id/eprint/
wdrshttp://www.w3.org/2007/05/powder-s#
n6http://purl.org/ontology/bibo/status/
n12doi:10.5555/
n8https://kar.kent.ac.uk/id/subject/
rdfshttp://www.w3.org/2000/01/rdf-schema#
n10https://demo.openlinksw.com/about/id/entity/https/raw.githubusercontent.com/annajordanous/CO644Files/main/
n13http://eprints.org/ontology/
n4https://kar.kent.ac.uk/90814/
n18https://kar.kent.ac.uk/id/event/
bibohttp://purl.org/ontology/bibo/
n19https://kar.kent.ac.uk/id/org/
rdfhttp://www.w3.org/1999/02/22-rdf-syntax-ns#
n15https://kar.kent.ac.uk/id/eprint/90814#
owlhttp://www.w3.org/2002/07/owl#
n16https://kar.kent.ac.uk/id/
xsdhhttp://www.w3.org/2001/XMLSchema#
n17https://demo.openlinksw.com/about/id/entity/https/www.cs.kent.ac.uk/people/staff/akj22/materials/CO644/
n14https://kar.kent.ac.uk/id/person/

Statements

Subject Item
n2:90814
rdf:type
bibo:AcademicArticle n13:EPrint bibo:Article n13:ConferenceItemEPrint
rdfs:seeAlso
n4:
owl:sameAs
n12:3398761.3398770
dcterms:title
Formal Verification of Neural Agents in Non-deterministic Environments
wdrs:describedby
n10:export_kar_RDFN3.n3 n17:export_kar_RDFN3.n3
dcterms:date
2020-05-09
dcterms:creator
n14:ext-c9c4c3870e06ff52bb0f076be43ddc21 n14:ext-46b4110bcea5b3cc6c34126bb164cef3 n14:ext-e.botoeva@kent.ac.uk n14:ext-07e3c062d7eb59da02fa6e79906ff696
bibo:status
n6:peerReviewed n6:published
dcterms:publisher
n19:ext-5858288a4bcf7a42f8df9aa980a14f44
bibo:abstract
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 present a novel parallel algorithm 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.
dcterms:isPartOf
n16:repository
dcterms:subject
n8:QA76
bibo:authorList
n15:authors
bibo:presentedAt
n18:ext-6c47793b66e424c109ec604d6c83059d