TY - GEN
T1 - Graded strategy logic
T2 - 15th International Conference on Autonomous Agents and Multiagent Systems, AAMAS 2016
AU - Aminof, Benjamin
AU - Malvone, Vadim
AU - Murano, Aniello
AU - Rubin, Sasha
N1 - Publisher Copyright:
Copyright © 2016, International Foundation for Autonomous Agents and Multiagent Systems (www.ifaamas.org). All rights reserved.
PY - 2016/1/1
Y1 - 2016/1/1
N2 - Strategy Logic (SL) is a well established formalism for strategic reasoning in multi-agent systems. In a nutshell, SL is built over LTL and treats strategies as first-order objects that can be associated with agents by means of a binding operator. In this work we introduce Graded Strategy Logic (GradedSL), an extension of SL by graded quantifiers over tuples of strategy variables such as "there exist at least g different tuples (x1,⋯, xn) of strategies". We study the model-checking problem of Graded-SL and prove that it is no harder than for SL, i.e., it is non-elementary in the quantifier rank. We show that Graded-SL allows one to count the number of different strategy profiles that are Nash equilibria (NE), or subgame-perfect equilibria (SPE). By analyzing the structure of the specific formulas involved, we conclude that the important problems of checking for the existence of a unique NE or SPE can both be solved in 2ExpTime, which is not harder than merely checking for the existence of such equilibria.
AB - Strategy Logic (SL) is a well established formalism for strategic reasoning in multi-agent systems. In a nutshell, SL is built over LTL and treats strategies as first-order objects that can be associated with agents by means of a binding operator. In this work we introduce Graded Strategy Logic (GradedSL), an extension of SL by graded quantifiers over tuples of strategy variables such as "there exist at least g different tuples (x1,⋯, xn) of strategies". We study the model-checking problem of Graded-SL and prove that it is no harder than for SL, i.e., it is non-elementary in the quantifier rank. We show that Graded-SL allows one to count the number of different strategy profiles that are Nash equilibria (NE), or subgame-perfect equilibria (SPE). By analyzing the structure of the specific formulas involved, we conclude that the important problems of checking for the existence of a unique NE or SPE can both be solved in 2ExpTime, which is not harder than merely checking for the existence of such equilibria.
KW - Graded modalities
KW - Nash equilibrium
KW - Strategic logics
M3 - Conference contribution
AN - SCOPUS:84992063118
T3 - Proceedings of the International Joint Conference on Autonomous Agents and Multiagent Systems, AAMAS
SP - 698
EP - 706
BT - AAMAS 2016 - Proceedings of the 2016 International Conference on Autonomous Agents and Multiagent Systems
PB - International Foundation for Autonomous Agents and Multiagent Systems (IFAAMAS)
Y2 - 9 May 2016 through 13 May 2016
ER -