Imperial College London


Faculty of EngineeringDepartment of Computing

Professor of Logic for Multiagent Systems



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




504Huxley BuildingSouth Kensington Campus






BibTex format

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)

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 -