Finite Abstractions for the Verification of Epistemic Properties in Open Multi-Agent Systems
Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence. Main Track. Pages 854-859.
Abstract
We develop a methodology to model and verify open multi-agent systems (OMAS), where agents may join in or leave at run time. Further, we specify properties of interest on OMAS in a variant of first-order temporal-epistemic logic, whose characterising features include epistemic modalities indexed to individual terms, interpreted on agents appearing at a given state. This formalism notably allows to express group knowledge dynamically. We study the verification problem of these systems and show that, under specific conditions, finite bisimilar abstractions can be obtained.
@inproceedings{ijcai2015p125,
title = {Finite Abstractions for the Verification of Epistemic Properties in Open Multi-Agent Systems},
author = {Belardinelli, Francesco and Grossi, Davide and Lomuscio, Alessio},
booktitle = {Proceedings of the Twenty-Fourth International Joint Conference on
Artificial Intelligence, {IJCAI-15}},
publisher = {International Joint Conferences on Artificial Intelligence},
editor = {Qiang Yang and Michael Wooldridge},
pages = {854--859},
year = {2015},
month = {7},
note = {Main Track},
url = {https://ijcai.org/proceedings/2015/125},
}
TY - CPAPER TI - Finite Abstractions for the Verification of Epistemic Properties in Open Multi-Agent Systems AU - Belardinelli, Francesco AU - Grossi, Davide AU - Lomuscio, Alessio T2 - Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence, IJCAI-15 PB - International Joint Conferences on Artificial Intelligence PY - 2015 SP - 854 EP - 859 UR - https://ijcai.org/proceedings/2015/125 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
