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 Michliszyn, J},
pages = {662--670},
title = {Verification of multi-agent systems via predicate abstraction against ATLK specifications},
url = {},
year = {2016}

RIS format (EndNote, RefMan)

AB - Copyright © 2016, International Foundation for Autonomous Agents and Multiagent Systems ( 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. MCMASPA supports 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 MCMASPA can verify infinite-state multi-agent systems of interest.
AU - Lomuscio,A
AU - Michliszyn,J
EP - 670
PY - 2016///
SN - 1548-8403
SP - 662
TI - Verification of multi-agent systems via predicate abstraction against ATLK specifications
UR -
ER -