Imperial College London

ProfessorAlessioLomuscio

Faculty of EngineeringDepartment of Computing

Professor of Logic for Multiagent Systems
 
 
 
//

Contact

 

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

 
 
//

Location

 

569Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@article{Boureanu:2012,
author = {Boureanu, I and Jones, AV and Lomuscio, A},
journal = {11th International Conference on Autonomous Agents and Multiagent Systems 2012, AAMAS 2012: Innovative Applications Track},
pages = {1072--1079},
title = {Automatic verification of epistemic specifications under convergent equational theories},
volume = {2},
year = {2012}
}

RIS format (EndNote, RefMan)

TY  - JOUR
AB - We present a methodology for the automatic verification of multi-agent systems against temporal-epistemic specifications derived from higher-level languages defined over convergent equational theories. We introduce a modality called rewriting knowledge that operates on local equalities. We discuss the conditions under which its interpretation can be approximated by a second modality that we introduce called empirical knowledge. Empirical knowledge is computationally attractive from a verification perspective. We report on an implementation of a technique to verify this modality with the open source model checker MCMAS. We evaluate the approach by verifying multi-agent models of electronic voting protocols automatically extracted from high-level descriptions. Copyright © 2012, International Foundation for Autonomous Agents and Multiagent Systems (www.ifaamas.org). All rights reserved.
AU - Boureanu,I
AU - Jones,AV
AU - Lomuscio,A
EP - 1079
PY - 2012///
SP - 1072
TI - Automatic verification of epistemic specifications under convergent equational theories
T2 - 11th International Conference on Autonomous Agents and Multiagent Systems 2012, AAMAS 2012: Innovative Applications Track
VL - 2
ER -