We study a class of synchronous, perfect-recall multi-agent systems with imperfect information and broadcasting, i.e., fully observable actions. We define an epistemic extension of strategy logic with incomplete information and the assumption of uniform and coherent strategies. In this setting, we prove that the model checking problem, and thus rational synthesis, is non-elementary decidable. We exemplify the applicability of the framework on a rational secret-sharing scenario.
Verification of broadcasting multi-agent systems against an epistemic strategy logic / Belardinelli, Francesco; Lomuscio, Alessio; Murano, Aniello; Rubin, Sasha. - In: IJCAI. - ISSN 1045-0823. - (2017), pp. 91-97. (Intervento presentato al convegno 26th International Joint Conference on Artificial Intelligence, IJCAI 2017 tenutosi a Melbourne; Australia nel 2017) [10.24963/ijcai.2017/14].
Verification of broadcasting multi-agent systems against an epistemic strategy logic
Murano, Aniello
Membro del Collaboration Group
;Rubin, Sasha
Membro del Collaboration Group
2017
Abstract
We study a class of synchronous, perfect-recall multi-agent systems with imperfect information and broadcasting, i.e., fully observable actions. We define an epistemic extension of strategy logic with incomplete information and the assumption of uniform and coherent strategies. In this setting, we prove that the model checking problem, and thus rational synthesis, is non-elementary decidable. We exemplify the applicability of the framework on a rational secret-sharing scenario.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
