Parameterised Verification of Infinite State Multi-Agent Systems via Predicate Abstraction

Autor:	Panagiotis Kouvaros, Alessio Lomuscio
Rok vydání:	2017
Předmět:	General Medicine
Zdroj:	Proceedings of the AAAI Conference on Artificial Intelligence. 31
ISSN:	2374-3468 2159-5399
DOI:	10.1609/aaai.v31i1.10710
Popis:	We define a class of parameterised infinite state multi-agent systems (MAS) that is unbounded in both the number of agents composing the system and the domain of the variables encoding the agents. We analyse their verification problem by combining and extending existing techniques in parameterised model checking with predicate abstraction procedures. The resulting methodology addresses both forms of unboundedness and provides a technique for verifying unbounded MAS defined on infinite-state variables. We illustrate the effectiveness of the technique on an infinite-domain variant of an unbounded version of the train-gate-controller.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::e4e8581cde3ef3b4213497082ddb1380 https://doi.org/10.1609/aaai.v31i1.10710 Zobrazit plný text záznamu