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{Lomuscio:2015,
author = {Lomuscio, A and Michaliszyn, J},
pages = {189--198},
title = {Verifying multi-agent systems by model checking three-valued abstractions},
year = {2015}
}

RIS format (EndNote, RefMan)

TY  - CPAPER
AB - Copyright © 2015, International Foundation for Autonomous Agents and Multiagent Systems. We develop the theoretical foundations of a predicate abstraction methodology for the verification of multi-agent systems. We put forward a specification language based on epistemic logic and a weak variant of the logic ATL interpreted on a three-valued semantics. We show that the model checking problem for multi-agent systems in this setting is tractable by giving a provably correct procedure which admits a PTIME bound. We give a constructive technique for generating abstract approximations of concrete multi-agent systems models and show that the truth values are preserved between abstract and concrete models. We evaluate the effectiveness of the methodology on a variant of the bit-transmission problem.
AU - Lomuscio,A
AU - Michaliszyn,J
EP - 198
PY - 2015///
SN - 1548-8403
SP - 189
TI - Verifying multi-agent systems by model checking three-valued abstractions
ER -