Strategy Logic with Simple Goals: Tractable Reasoning about Strategies

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.