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{Belardinelli:2014:10.1613/jair.4424,
author = {Belardinelli, F and Lomuscio, A and Patrizi, F},
doi = {10.1613/jair.4424},
journal = {The Journal of Artificial Intelligence Research},
title = {Verification of agent-based artifact systems},
url = {http://dx.doi.org/10.1613/jair.4424},
volume = {51},
year = {2014}
}
Download

RIS format (EndNote, RefMan)

TY  - JOUR
AB  - Artifact systems are a novel paradigm for specifying and implementing business processes described in terms of interacting modules called artifacts. Artifacts consist of data and lifecycles, accounting respectively for the relational structure of the artifacts states and their possible evolutions over time. In this paper we put forward artifact-centric multi-agent systems, a novel formalisation of artifact systems in the context of multi-agent systems operating on them. Differently from the usual process-based models of services, we give a semantics that explicitly accounts for the data structures on which artifact systems are defined.We study the model checking problem for artifact-centric multi-agent systems against specifications expressed in a quantified version of temporal-epistemic logic expressing the knowledge of the agents in the exchange. We begin by noting that the problem is undecidable in general. We identify a noteworthy class of systems that admit bisimilar, finite abstractions. It follows that we can verify these systems by investigating their finite abstractions; we also show that the corresponding model checking problem is EXPSPACE-complete. We then introduce artifact-centric programs, compact and declarative representations of the programs governing both the artifact system and the agents. We show that, while these in principle generate infinite-state systems, under natural conditions their verification problem can be solved on finite abstractions that can be effectively computed from the programs. We exemplify the theoretical results here pursued through a mainstream procurement scenario from the artifact systems literature.
AU  - Belardinelli,F
AU  - Lomuscio,A
AU  - Patrizi,F
DO  - 10.1613/jair.4424
PY  - 2014///
SN  - 1076-9757
TI  - Verification of agent-based artifact systems
T2  - The Journal of Artificial Intelligence Research
UR  - http://dx.doi.org/10.1613/jair.4424
UR  - https://jair.org/index.php/jair/article/view/10910
UR  - http://hdl.handle.net/10044/1/64610
VL  - 51
ER  -
Download