Imperial College London

ProfessorAlessioLomuscio

Faculty of EngineeringDepartment of Computing

Professor of Logic for Multiagent Systems
 
 
 
//

Contact

 

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

 
 
//

Location

 

504Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@inproceedings{2016,
pages = {662--670},
title = {Verification of multi-agent systems via predicate abstraction against ATLK specifications},
url = {http://hdl.handle.net/10044/1/34132},
year = {2016}
}

RIS format (EndNote, RefMan)

TY  - CPAPER
AB - Copyright © 2016, International Foundation for Autonomous Agents and Multiagent Systems (www.ifaamas.org). All rights reserved. We present a predicate abstraction technique for the verification of multi-agent systems against specifications defined in the epistemic logic ATLK, interpreted on a three-valued semantics. We reduce an infinite-state multi-agent program to a finite model by generating predicates automatically via SMT calls. We show that if an ATLK specification is either true or false in the abstract model, then that is also the case on the original infinite state model. We introduce and describe MCMASPA, a toolkit implementing the technique here described. MCMASPAsupports the three-valued semantics for ATLK, automatically generates program abstractions for a multi-agent system by means of automatic SMT calls, encodes the corresponding program in BDDs and reports the result. The experimental results obtained confirm that MCMASPAcan verify infinite-state multi-agent systems of interest.
EP - 670
PY - 2016///
SN - 1548-8403
SP - 662
TI - Verification of multi-agent systems via predicate abstraction against ATLK specifications
UR - http://hdl.handle.net/10044/1/34132
ER -