TY - GEN
T1 - Towards the Combination of Model Checking and Runtime Verification on Multi-agent Systems
AU - Ferrando, Angelo
AU - Malvone, Vadim
N1 - Publisher Copyright:
© 2022, The Author(s), under exclusive license to Springer Nature Switzerland AG.
PY - 2022/1/1
Y1 - 2022/1/1
N2 - Multi-Agent Systems (MAS) are notoriously complex and hard to verify. In fact, it is not trivial to model a MAS, and even when a model is built, it is not always possible to verify, in a formal way, that it is actually behaving as we expect. Usually, it is relevant to know whether an agent is capable of fulfilling its own goals. One possible way to check this is through Model Checking. Specifically, by verifying Alternating-time Temporal Logic (ATL) properties, where the notion of strategies for achieving goals can be described. Unfortunately, the resulting model checking problem is not decidable in general. In this paper, we present a verification procedure based on combining Model Checking and Runtime Verification, where sub-models of the MAS model belonging to decidable fragments are verified by a model checker, and runtime monitors are used to verify the rest. We present our technique and show experimental results.
AB - Multi-Agent Systems (MAS) are notoriously complex and hard to verify. In fact, it is not trivial to model a MAS, and even when a model is built, it is not always possible to verify, in a formal way, that it is actually behaving as we expect. Usually, it is relevant to know whether an agent is capable of fulfilling its own goals. One possible way to check this is through Model Checking. Specifically, by verifying Alternating-time Temporal Logic (ATL) properties, where the notion of strategies for achieving goals can be described. Unfortunately, the resulting model checking problem is not decidable in general. In this paper, we present a verification procedure based on combining Model Checking and Runtime Verification, where sub-models of the MAS model belonging to decidable fragments are verified by a model checker, and runtime monitors are used to verify the rest. We present our technique and show experimental results.
KW - Model checking
KW - Runtime verification
KW - Strategic reasoning
U2 - 10.1007/978-3-031-18192-4_12
DO - 10.1007/978-3-031-18192-4_12
M3 - Conference contribution
AN - SCOPUS:85141855364
SN - 9783031181917
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 140
EP - 152
BT - Advances in Practical Applications of Agents, Multi-Agent Systems, and Complex Systems Simulation. The PAAMS Collection - 20th International Conference, PAAMS 2022, Proceedings
A2 - Dignum, Frank
A2 - Mathieu, Philippe
A2 - Corchado, Juan Manuel
A2 - De La Prieta, Fernando
A2 - Corchado, Juan Manuel
PB - Springer Science and Business Media Deutschland GmbH
T2 - 20th International Conference on Practical Applications of Agents and Multi-Agent Systems , PAAMS 2022
Y2 - 13 July 2022 through 15 July 2022
ER -