In this paper we introduce Strategy Logic with Simple Goals (SL[SG]), a fragment of Strategy Logic that strictly extends Alternating-time Temporal Logic ATL by introducing arbitrary quantification over the agents' strategies. Our motivation comes from game-theoretic applications, such as expressing Stackelberg equilibria in games, coercion in voting protocols, as well as module checking for simple goals. We prove that model checking SL[SG] is P-complete, the same as ATL. Thus, the extra expressive power comes at no computational cost as far as verification is concerned. © 2019 International Joint Conferences on Artificial Intelligence. All rights reserved.
Strategy logic with simple goals: Tractable reasoning about strategies / Belardinelli, F.; Jamroga, W.; Kurpiewski, D.; Malvone, V.; Murano, A.. - In: IJCAI. - ISSN 1045-0823. - 2019-August:(2019), pp. 88-94. (Intervento presentato al convegno International Joint Conference on Artificial Intelligence) [10.24963/ijcai.2019/13].
Strategy logic with simple goals: Tractable reasoning about strategies
Jamroga, W.
Membro del Collaboration Group
;Malvone, V.
Membro del Collaboration Group
;Murano, A.
Membro del Collaboration Group
2019
Abstract
In this paper we introduce Strategy Logic with Simple Goals (SL[SG]), a fragment of Strategy Logic that strictly extends Alternating-time Temporal Logic ATL by introducing arbitrary quantification over the agents' strategies. Our motivation comes from game-theoretic applications, such as expressing Stackelberg equilibria in games, coercion in voting protocols, as well as module checking for simple goals. We prove that model checking SL[SG] is P-complete, the same as ATL. Thus, the extra expressive power comes at no computational cost as far as verification is concerned. © 2019 International Joint Conferences on Artificial Intelligence. All rights reserved.I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
