Finite Abstractions for the Verification of Epistemic Properties in Open Multi-Agent Systems



Belardinelli, Francesco, Grossi, Davide ORCID: 0000-0002-9709-030X and Lomuscio, Alessio
(2015) Finite Abstractions for the Verification of Epistemic Properties in Open Multi-Agent Systems. PROCEEDINGS OF THE TWENTY-FOURTH INTERNATIONAL JOINT CONFERENCE ON ARTIFICIAL INTELLIGENCE (IJCAI), 2015-J. pp. 854-860.

[img] Text
ijcai2015.pdf - Unspecified

Download (276kB)

Abstract

We develop a methodology to model and verify open multi-agent systems (OMAS), where agents may join in or leave at run time. Further, we specify properties of interest on OMAS in a variant of firstorder temporal-epistemic logic, whose characterising features include epistemic modalities indexed to individual terms, interpreted on agents appearing at a given state. This formalism notably allows to express group knowledge dynamically. We study the verification problem of these systems and show that, under specific conditions, finite bisimilar abstractions can be obtained.

Item Type: Article
Depositing User: Symplectic Admin
Date Deposited: 28 Apr 2016 10:31
Last Modified: 16 Dec 2022 02:04
Related URLs:
URI: https://livrepository.liverpool.ac.uk/id/eprint/3000635