--- title: "Strategy Logic with Simple Goals: Tractable Reasoning about Strategies" authors: - "Francesco Belardinelli" - "Wojciech Jamroga" - "Damian Kurpiewski" - "Vadim Malvone" - "Aniello Murano" doi: "10.24963/ijcai.2019/13" url: "https://ijcai.org/proceedings/2019/13" pdf: "https://ijcai.org/proceedings/2019/0013.pdf" venue: "Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence" year: 2019 pages: "88-94" track: "Main track" keywords: - "Agent-based and Multi-agent Systems: Agent Theories and Models" - "Agent-based and Multi-agent Systems: Formal Verification, Validation and Synthesis" --- # Strategy Logic with Simple Goals: Tractable Reasoning about Strategies Francesco Belardinelli, Wojciech Jamroga, Damian Kurpiewski, Vadim Malvone, Aniello Murano *Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence*, pages 88-94. DOI: [10.24963/ijcai.2019/13](https://doi.org/10.24963/ijcai.2019/13) ## Abstract In this paper we introduce Strategy Logic with simple goals (SL[SG]), a fragment of Strategy Logic that strictly extends the well-known 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. Most importantly, we prove that the model checking problem for SL[SG] is PTIME-complete, the same as ATL. Thus, the extra expressive power comes at no computational cost as far as verification is concerned. ## Full text ## 1 Introduction Formal verification of multi-agent systems (MAS) has been a thriving area of investigation in the last two decades, which has led to a wealth of logics to specify the temporal, epistemic, and strategic capabilities of agents, including Alternating-time Temporal Logic [Alur et al., 2002], possibly enriched with strategy contexts [Laroussinie and Markey, 2015], irrevocable strategies [ ˚Agotnes et al., 2007], or operators for individual and group knowledge [Jamroga and van der Hoek, 2004; Hoek and Wooldridge, 2003]; Coalition Logic [Pauly, 2002]; and Strategy Logic [Chatterjee et al., 2010; Mogavero et al., 2014]. Besides theoretical results, some model checking tools have also been developed [Alur et al., 2001; Cimatti et al., 2002; Kacprzak et al., 2008; Huang and van der Meyden, 2014; Lomuscio et al., 2015; Cerm´ak et al., 2015; Cerm´ak et al., 2018]. The verification of MAS generates a tension between two conflicting demands. On the one hand, we need an expressive language to capture subtle temporal, epistemic, and game-theoretic notions such as reachability, common and distributed knowledge, and solution concepts in games. On the other hand, we need formalisms with a tractable model checking problem, for which efficient verification algorithms can be implemented. The same tension appears in the seminal paper [Alur et al., 2002] that introduced Alternating-time Temporal Logic. Two variants of the logic are presented: ATL∗ is rather expressive, but with 2EXPTIME verification complexity. Its fragment ATL has less expressivity, but allows to model check strategic properties in polynomial time. This leads to a nice balance of expressivity and computational complexity - indeed, ATL model checking is supported by a number of tools [Alur et al., 2001; Kacprzak et al., 2008; Lomuscio et al., 2015]. The question is: can we use a language that is more expressive than ATL, and still retains its polynomial-time complexity of model checking? We answer the question affirmatively in this paper. Our starting point is Strategy Logic (SL) [Mogavero et al., 2014], an expressive extension of ATL∗ that allows to characterize sophisticated game-theoretic solution concepts, e.g., Nash equilibria, dominant strategies, subgame-perfect equilibria, etc. Unfortunately, its model checking complexity is non-elementary, and hence highly unlikely to enable efficient implementation. Even restricted variants of SL, such as SL with memoryless strategies [Cerm´ak et al., 2014], nestedgoal, Boolean-goal, and one-goal SL [Mogavero et al., 2012] do not help much, as their model checking problems range from 2EXPTIME-complete to non-elementary [Mogavero et al., 2014; Bouyer et al., 2015; Gardy et al., 2018]. We then propose to take one-goal SL, and further restrict goals to simple LTL formulas of type Xφ (next φ), φUφ′ (φ until φ′ ), and φRφ′ (φ releases φ′ ), similarly to the restriction of ATL∗ to ATL in [Alur et al., 2002]. The result, Strategy Logic with simple goals (SL[SG]), can also be seen as the extension of ATL to arbitrary quantification on the agents' strategies. We use SL[SG] to capture Stackelberg equilibria in games, express coercion-resistance in voting protocols [Tabatabaei et al., 2016], and characterize module checking for simple goals [Jamroga and Murano, 2014]. These are all relevant agent-related concepts, that cannot be expressed in ATL. Hence, SL[SG] is provably more expressive than ATL. Most importantly, we show that reasoning about SL[SG] is no more complex as ATL, as it also enjoys polynomial-time model checking. This is achieved by generalising the fixed-point procedures for ATL model checking. In consequence, Strategy Logic with simple goals offers an arguably better balance between expressivity and complexity than ATL. We further show the advantages by means of a case study, based on a simple voting scenario. ## 2 Logics for Strategies We begin by recalling Strategy Logic (SL) [Mogavero et al., 2014], as well as its relevant syntactic fragments. Then, we provide an interpretation to these languages by means of concurrent game structures (CGS), as it is customary. Strategy Logic. Fix an infinite set AP of atomic propositions (atoms), a finite set Ag of agents, and an infinite set Var of variables x0, x1, . . . for strategies. Formulas in Strategy Logic are defined as follows, for p ∈ AP, x ∈ Var, a ∈ Ag: Next X and until U are temporal operators. The strategy quantifier ∃x reads as "for some strategy x, . . . ", and the binding operator (x, a) intuitively means that "by using strategy x, agent a can achieve . . . ". Hereafter we use standard abbreviations, e.g., ∀xϕ for ¬∃x¬ϕ, as well as temporal operators releases R, globally G, and eventually F. We assume the standard definition of set free(ϕ) of free agents and variables appearing in a formula ϕ [Mogavero et al., 2014]. Moreover, shr(x, ϕ) denotes the set of agents that use strategy x in the evaluation of formula ϕ. Models. Given sets Ag of agents and AP of atoms, a concurrent game structure (CGS) is a tuple G = 〈S, s0, {Acta}a∈Ag, τ,L〉 such that: S is a non-empty finite set of states and s0 ∈ S is the initial state of G; for every agent a ∈ Ag, Acta is a finite non-empty set of actions, and ACT = ∏a∈Ag Acta is the set of joint actions; τ : S ×ACT → S is the transition function; finally, L : S → 2AP is the labelling. A path is a (finite or infinite) sequence π ∈ S∗ ∪ Sω such that for every j ≥ 1, πj+1 = τ(πj, ⃗αj) for some joint action ⃗αj ∈ ACT . We distinguish between finite paths, or histories, and infinite paths, or computations. For a path π and j ≥ 1, π≤j denotes the initial history of length j, and last(h) is last element in history h. Strategies. A memoryfull strategy for an agent a ∈ Ag, or a-strategy, is a function σ : S+ → Acta. The set of all strategies, for all agents, is denoted as Σ(G). A joint strategy σAg assigns a strategy for a to every agent a ∈ Ag. By the above definitions, given a strategy σ for an agent a, if a different agent b is such that the range of strategy σ is a subset of Actb (i.e., ran(σ) ⊆ Actb), then intuitively also agent b can use strategy σ. Finally, an assignment is a function χ : Var ∪ Ag → Σ(G) such that for every agent a ∈ Ag, χ(a) is a strategy for a. For z ∈ Var ∪ Ag and σ ∈ Σ(G), the variant χzσ is the assignment that maps z to σ and coincides with χ on all other variables and agents. Given a history h ∈ S+, an assignment χ defines a unique computation λ(h, χ) = h 〈χ(a)(h)〉a∈Ag --------→ s1 〈χ(a)(h·s1)〉a∈Ag ----------→ s2 . . . starting with h and consistent with χ. Semantics. Given a CGS G, we inductively define the satisfaction relation (G, h, χ) |= ϕ where h is a history, ϕ is a formula, and χ is an assignment such that for every x ∈ Var, χ(x) is a strategy for all agents in shr(x, ϕ) (we omit the standard clauses for Boolean operators): Figure 1: A simple model of voting and coercion ![Image](https://ijcai.org/proceedings/2019/fulltext/13/image_000000_fd125d3ad349d0ad51cf413c546a8d2da21475e2cce9eccd4bdb88e93e03616d.png) We write (G, h) |= ϕ iff (G, h, χ) |= ϕ for every assignment χ, and G |= ϕ iff (G, s0) |= ϕ. Relevant Fragments. One-Goal Strategy Logic (SL[1G]) is the syntactic fragment of SL where each temporal subformula is preceded by a binding prefix that mentions all agents in Ag, and by a quantification prefix 1 referring to all the preceding strategy variables [Mogavero et al., 2012]. Furthermore, ATL∗ can be seen as the fragment of SL[1G] that admits at most one alternation of strategic quantifiers (either ∃∀ or ∀∃), and does not allow to bind different agents to the same variable. Finally, ATL is the fragment of ATL∗ where each group of strategic quantifiers is followed by exactly one temporal operator. Interestingly, SL[1G] has been proved strictly more expressive than ATL∗ , while having the same complexity of the model checking problem [Mogavero et al., 2014]. In this paper, we look for an analogous extension of ATL. Example 1 (Simple Voting) Consider a simple model of voting, inspired by [Jamroga et al., 2017a]. There are k voters v1, . . . , vk and a single coercer c. At the beginning, each voter decides to wait or cast her vote for one of the n candidates. Then, she can wait again, give her vote receipt to the coercer or refuse to give it. Finally, the coercer can either punish the voter, or refrain from punishment. The interaction between the coercer and different voters is independent. The CGS SV1,2 for k = 1 and n = 2 is presented in Figure 1. An example formula that holds in SV2,2 is ∀xc∃xv1 ∀xv2 (xc, c)(xv1 , v1)(xv2 , v2)F(votedv,1 ∧ ¬pun), expressing that, for every strategy of c, the first voter has a counterstrategy ensuring that she can vote for candidate 1 without getting punished, regardless of the other voter. The counterstrategy is simply to vote for 1, and then execute wait. 1 We will formally introduce both notions in the next section. ## 3 Strategy Logic with Simple Goals Inspired by the relationship between the Alternating-time Temporal Logics ATL∗ and ATL, we introduce a novel restriction of SL[1G] to "simple" goals. ## 3.1 The Formal Language We begin with some terminology. A binding prefix over sets A ⊆ Ag of agents and V ⊆ Var of variables is a finite sequence ♭ ∈ {(x, a) | a ∈ A and x ∈ V }|A| of length |♭| = |A|, such that every agent a ∈ A occurs exactly once in ♭. In contrast, the same variable x ∈ V can occur several times in ♭, i.e., intuitively, the same strategy denoted by x can be used by several agents in A. A quantification prefix over a set V ⊆ Var of variables is a finite sequence ℘ ∈ {∃x, ∀x | x ∈ V }|V | of length |℘| = |V | such that every variable x ∈ V occurs exactly once in ℘. Then, Qnt(V ) ⊂ {∃x, ∀x | x ∈ V }|V | and Bnd(A) ⊂ {(x, a) | a ∈ A and x ∈ Var}|A| denote the sets of all quantification and binding prefixes over variables in V and agents in A. Definition 2 (SL[SG]) The formulas in Strategy Logic with simple goals are defined in BNF as follows, where ♭ ∈ Bnd(Ag), ℘ ∈ Qnt(free(♭ϕ)): By Def. 2, SL[SG] restricts SL[1G] to simple LTL objectives of type Xϕ, ϕUϕ′ , and ϕRϕ′ (the latter can be introduced by using U and dual quantification). We also consider the fragment SL-[SG], for which Def. 2 is restricted to binding prefixes ♭ where every variable occurs at most once. That is, one cannot bind different agents with the same strategy. Further, we define fragments SLn[SG], for which quantification prefixes ℘ are restricted to at most n alternations of existential and universal quantifiers. Finally, we introduce fragments SL-n [SG] as the intersection of SL-[SG] and each SLn[SG]. Example 3 Clearly, the formula in Example 1 is a formula of SL[SG], more precisely of SL-2 [SG]. In Fig. 2 we summarize the main syntactic inclusions between our fragments. We also remark that ATL can be thought of as the fragment of SL[SG] in which the clauses for formulas of type ℘♭ Xϕ and ℘♭(ϕUϕ) are restricted to quantification prefixes ℘ with at most one alternation, as well as binding prefixes ♭ where every variable occurs at most once. In fact, ATL corresponds exactly to SL-1 [SG], whereas Computation Tree Logic (CTL) corresponds to SL-0 [SG]. ## 3.2 Expressiveness An important observation that formally justifies our study is that SL[SG] is strictly more expressive than ATL. That is, SL[SG] allows to characterize all the properties expressible in ATL, but not vice versa. We also show that SL[SG], SL-[SG], and SL1[SG] all differ with respect to their expressiveness. Consider two logical systems L1 and L2. L1 is at least as expressive as L2 (written L2 ⪯e L1) if every formula of L2 can be equivalently translated to some formula of L1. Moreover, L1 is at least as distinguishing as L2 (L2 ⪯d L1) if every pair of models that can be distinguished by a formula of L2 can also be distinguished by some formula of L1. Figure 2: Syntactic inclusions for fragments of SL ![Image](https://ijcai.org/proceedings/2019/fulltext/13/image_000001_2372c01ffa18e403f11bb881a6d5f03311167565191707cb129287ac4a13dd76.png) Theorem 4 SL-2 [SG] (and thus also SL[SG]) has strictly greater expressive and distinguishing power than ATL. Proof. The embedding of ATL into SL-2 [SG] is straightforward. To show that ATL does not cover the distinguishing power (and hence also the expressive power) of SL-2 [SG], we can use the counterexample from the proof of [Mogavero et al., 2014, Theorem 4.3]. □ Figure 3: Models M1 and M2 in the proof of Theorem 5 ![Image](https://ijcai.org/proceedings/2019/fulltext/13/image_000002_1b7fc1936497d3ab443f0b28ef261de548e67c069ff69ff4994120ecef3a2c36.png) Interestingly, we also have that for every n ∈ N, SLn[SG] is strictly more expressive than SL-n [SG]. That is, being able to bind the same strategy to different agents strictly increases the expressive power of Strategy Logic with simple goals. Theorem 5 For every n ≥ 0, we have: 1. SL-n [SG]≺eSLn[SG], and therefore SL-n [SG]≺dSLn[SG]; Proof. We adapt the proof of [Belardinelli et al., 2018, Lemma 32.1]. Clearly, SL-n [SG] ⪯e SLn[SG] and therefore also SL-n [SG] ⪯d SLn[SG]. Since SL0[SG] ⪯d SLn[SG] and SL-n [SG] ⪯d SL-[SG], to show that SLn[SG] ̸⪯d SL-n [SG], we prove that: To do so, we provide two models that satisfy the same formulas in SL-[SG] but are distinguished by a formula of SL0[SG]. Consider the CGS's M1 and M2 with Ag = {1, 2}, depicted in Fig. 3. Since SL-[SG] can be shown invariant under renaming of action labels, both models satisfy the same formulas of SL-[SG]. However, M1 satisfies the SL0[SG]-formula ∃x(x, 1)(x, 2) Xp, while M2 does not. Thus, SL0[SG] ̸⪯d SL-[SG] and therefore also SLn[SG] ̸⪯d SL-n [SG] and SLn[SG] ̸⪯e SL-n [SG] for every n ∈ N. As regards 2., clearly, SL-[SG] ⪯e SL[SG], and therefore SL-[SG] ⪯d SL[SG]. Since SL0[SG] ⪯d SL[SG] and SL0[SG] ̸⪯d SL-[SG] (item (1)), then SL[SG] ̸⪯d SL-[SG]. So, SL-[SG]≺eSL[SG], and thus SL-[SG] ≺d SL[SG]. □ The discussion above highlights logics SL0[SG] and SL1[SG] as variants of CTL = SL-0 [SG] and ATL = SL-1 [SG] that allow for strategy sharing. Such extensions have not been considered in the literature. Nonetheless, by Theorem 5, they are strictly more expressive than CTL and ATL respectively. ## 3.3 Motivating Examples and Applications Strategy Logic enables to address complex interaction between strategies of different players, who may pursue adversarial, collaborative, or uncorrelated goals. Also, the goals can be based on sophisticated temporal patterns. This expressivity comes at the expense of tractability, or even decidability of decision problems for SL. At the other end, we have ATL where only a single alternation is allowed in strategy quantification. Moreover, the agents' goals can only be phrased in terms of reachability. This results in a somewhat rigid specification language, albeit one with a big advantage: the model checking problem becomes tractable. With SL[SG], we extend ATL by allowing arbitrarily many alternations of strategy quantifiers. We argue that the extra expressivity is useful, i.e., it allows for specification of relevant properties of agent interaction in multi-agent systems. To this end, we propose a number of motivating examples. Example 6 (Stackelberg equilibria) Stackelberg games concern scenarios where one player (the leader) exposes his strategy first, and the other player (the follower) adapts to that strategy by choosing her best response. For example, coercion in voting often has a Stackelberg structure: the coercer must lay out his coercion strategy in a believable way to force the voter to vote as requested. A desirable property in voting systems is that the voter can resist coercion, i.e., for every strategy of the coercer (c) there exists a response of the voter (v) such that for every run of the environment (e) the voter will have voted as she intended without being punished [Tabatabaei et al., 2016]. This is captured by the following formula of SL[SG]: Example 7 (Coercion in voting, ctd.) A more realistic model of coercion allows the coercer to split his strategy into a public and a private part. We can simulate that by splitting the model of the coercer into two agents: cpub and cprv, each responsible for different parts of the coercion strategy. Moreover, some voting protocols include a process that can add decoy votes after the election to deceive the coercer. This can be incorporated into our specification of coercion-resistance as follows: This specification can intuitively be read as: for every public strategy of the coercer (xc1 ), there exists a response by the voter (xv) such that, no matter what the coercer does privately (xc2 ), the decoy process d can use decoy votes to make sure that the voter votes as she likes without being punished. Example 8 (Module checking for strategic abilities) The problem of module checking asks, for an open system embedded in a nondeterministic environment, whether the correctness specification holds for every possible strategy of the environment 2 . It has been proved that module checking of either temporal or strategic specifications cannot be expressed in ATL [Jamroga and Murano, 2014]. The ability of an autonomous taxi (t) to serve an unbounded stream of customers (e) so that no accident occurs, regardless of what the agents a1, . . . , ak do, can be captured as A careful reader may notice that the results in Section 3.2 indeed apply to the above specifications. That is, the formulas in Examples 6-8 cannot be equivalently expressed in ATL. ## 4 Model Checking Given a CGS G and a formula φ in language L, the model checking problem w.r.t. L consists in determining whether G |= φ. In this section we study model checking for Strategy Logic with simple goals and its fragments. These results are essential for applications of SL[SG] to the verification of multi-agent systems, including the specifications in Examples 6-8. Our main theoretical result is that verification of SL[SG] is tractable with respect to the size of the CGS (i.e., the number of its transitions) and the length of the formula. We first prove that the fixed-point characterisation of ATL carry over to SL[SG]. Proposition 9 The following formula is a validity in SL[SG]: Proof. The proof makes use of the preimage function Pre() that is defined in Algorithm 2 and will be described in detail in the proof of Theorem 10. As regards the implication from left to right, suppose that ℘♭(ϕ1 Uϕ2) holds in some state s. Then, if ϕ2 does not hold in s, ϕ1 does. Moreover, consider set Y ⊆ S such that s ∈ Pre(℘, ♭, Y, ϵ), i.e., the successors of s that are consistent with the quantification and binding prefixes. Since (G, s) |= ℘♭(ϕ1 Uϕ2) and (G, s) ̸|= ϕ2, for every s′ ∈ Y , we have (G, ss′ ) |= ℘♭(ϕ1 Uϕ2): indeed every strategy σi witnessing an existential quantifier Qi in ℘ at s, also witnesses Qi in history ss′ . In particular, (G, ss′ ) |= ℘♭(ϕ1 Uϕ2), and finally, (G, s) |= ℘♭X℘♭(ϕ1 Uϕ2) by the way s′ was chosen. As for the implication from right to left, if ϕ2 holds at state s, then ℘♭(ϕ1 Uϕ2) is also the case. On the other hand, suppose that (G, s) |= ϕ1 ∧ ℘♭X℘♭(ϕ1 Uϕ2). In particular, every existential quantifier Qi in ℘ is witnessed in s by some strategy σi, and in every "successor" state s′ ∈ Y , Qi is witnessed in history ss′ by some (possibly different) strategy σ′i . Then, define strategies σ′′ i such that σ′′ i (s) = σi(s) and σ′′ i (s · h) = σ′i (h) for all h ∈ S+. In particular, each σ′′ i witnesses Qi at s, that is, (G, s) |= ℘♭(ϕ1 Uϕ2). Observe the essential use of perfect recall in the construction of strategy σ′′ i from σi and σ′i . □ 2 Admittedly, to represent module checking properly we need CGSs with non-deterministic transitions. Nonetheless, the characterization of module checking in SL[SG] would remain the same. ## Algorithm 1 SL[SG] Model Checking ``` procedure MODELCHECKING(G,ϕ) for all ϕ′ in Sub(ϕ) do case ϕ′ = p: [ϕ′ ] := Reg(p); case ϕ′ = ¬θ: [ϕ′ ] := S \ [θ]; case ϕ′ = θ1 ∧ θ2: [ϕ′ ] := [θ1] ∩ [θ2]; case ϕ′ = ℘♭ Xθ: [ϕ′ ] := Pre(℘, ♭, [θ], ϵ); case ϕ′ = ℘♭(θ1 U θ2): Y := ∅; Z := [θ2]; while Z ̸⊆ Y do Y := Y ∪Z; Z := Pre(℘, ♭, Y, ϵ) ∩ [θ1]; end while [ϕ′ ] := Y ; end for return [ϕ]; end procedure ``` By using Prop. 9 we can prove the main theoretical result. Theorem 10 Model checking SL[SG] is P-complete. Proof. Recall that CTL corresponds to the SL-0 [SG] fragment of SL[SG]. Then, the lower bound follows immediately from the P-hardness of model checking CTL [Katoen, 2008]. As for the upper bound, Algorithm 1 shows a procedure for model checking SL[SG], which manipulates sets of states in S. The procedure is inspired by the standard model checking algorithm for ATL [Alur et al., 2002], but the preimage operator for the ATL modality 〈〈A〉〉X is now replaced by the Pre operator in Algorithm 2 for an arbitrary block of strategy quantifiers. Specifically, Algorithm 1 uses the following primitive operations: - The function Sub returns a sequence of syntactic subformulas of a given formula ϕ. - The function Reg returns the set {s ∈ S | p ∈ L(s)} of states s ∈ S labelled with a given atom p ∈ AP . - The function Pre, when given a quantification prefix ℘ = Q1x1 . . .Qkxk, a binding prefix ♭ = (x1, a1,1) . . . (x1, a1,m1 ) . . . (xk, ak,1) . . . (xk, ak,mk )3 , a set Y ⊆ S of states, and a tuple ⃗α of actions for all agents a ∈ Ag such that (x, a) appears in ♭ and x does not appear in ℘, returns the set of states s ∈ S from which there exist transitions consistent with ℘, ♭, and ⃗α, ending up in Y . Formally, Pre is a recursive function defined on the length of ℘. For the base case ℘ = ϵ, notice that ⃗α is a joint action for all agents in Ag, and therefore Pre returns the set of states s ∈ S such that τ(s, ⃗α) ∈ Y . As for the recursive step, s ∈ Pre(℘, ♭, Y, ⃗α) iff for ℘1 = ∃ (resp. ∀), for some (resp. every) action β, it is the case that s ∈ Pre(℘>1, ♭, Y, update(♭, ⃗α, var(℘1), β)), where function update(♭, ⃗α, x, β), given a binding ♭, a tuple ⃗α of actions, variable x, and action β, returns a tuple ⃗α′ of actions such that for every a ∈ Ag, if (x, a) appears in ♭ then ⃗α′a = β, otherwise ⃗α′a = ⃗αa. For more details on function Pre, see Algorithm 2. - Union, intersection, difference, and inclusion test for sets of states. 3 The parameter mi represents the number of agents assigned to variable xi, for each 1 ≤ i ≤ k. ## Algorithm 2 Preimage of a set Y of states ``` procedure P re(℘, ♭, Y, ⃗α) if ℘ = ϵ then return {s ∈ S | τ(s, ⃗α) ∈ Y }; else if ℘1 = ∃ then return ⋃β∈⋂(var(℘1),a)∈♭ Acta P re(℘>1, ♭, Y, update(♭, ⃗α, var(℘1), β)); else return ⋂β∈⋂(var(℘1),a)∈♭ Acta P re(℘>1, ♭, Y, update(♭, ⃗α, var(℘1), β)); end if end procedure ``` Algorithm 1 works bottom-up on the structure of the formula; the cases of interest are for strategy formulas. For ϕ′ = ℘♭ X θ, the procedure calls function Pre to compute the set of states that are "bound" to end up in satisfaction set [θ]. As regard ϕ′ = ℘♭(θ1 U θ2), the procedure computes the least fixed-point of operator F(Z) = [θ2] ∪ ([θ1] ∩ ℘♭X℘♭(Z)). We observe that, since F is monotone, such a fixed-point always exists. Further, Algorithm 1 runs in polynomial time in the size of the CGS and the size of the formula 4 . Termination of Algorithm 1 is guaranteed, as the state space S is finite. Soundness and completeness can be proved by induction on the structure of the input formula ϕ by using Proposition 9 for the case ϕ′ = ℘♭(θ1 U θ2). □ By Theorem 10 we immediately obtain that for all fragments of SL[SG] in Fig. 2 model checking is P-complete. ## 5 Experimental Evaluation With SL[SG], we propose a logic that enhances the expressivity of ATL while enjoying the same, polynomial-time complexity of model checking. Alternatively, we sacrifice some expressiveness of SL[1G] in order to reduce the verification complexity from highly intractable (2EXPTIMEcomplete) to tractable. In consequence, one would expect that the verification algorithm for SL[SG], presented in Section 4, should perform better than the general algorithm that handles the whole "one-goal" fragment of SL [Cerm´ak et al., 2015]. However, theoretical complexity results rely on worst case complexity. Thus, it can be that the practical performance of SL[1G] model checking is much better than the 2EXPTIME classification suggests. In particular, one may ask if the specialized SL[SG] algorithm of the previous section performs significantly better than the general algorithm in [Cerm´ak et al., 2015] on the formulas of SL[SG]. To answer this question, we have conducted a series of experiments with a scalable benchmark, based on the simple voting and coercion scenario of Examples 1 and 6. We consider models ESVk,n (Extended Simple Voting with k voters and n candidates), constructed as follows. The initial state q0 is handled by a new election authority ea, who decides whether to implement low or high anti-coercion protection. The former choice leads to a copy of the SVk,n CGS. The latter proceeds to a modified copy of the same model, with proposition puni satisfied only in the states where the coercer has decided to punish the voter and the voter gave him her voting receipt. 4 Notice, however, that the number of transitions in a CGS can be exponential w.r.t. the number of agents. Table 1: Experimental results for the simple voting model | #v | #states | SL[SG] - tgen | SL[SG] - tverif | SL[1G] - tg+tv | SLK - tg+tv | |------|-----------|-----------------|-------------------|------------------|---------------| | 1 | 29 | 0.001 | 0.002 | 0.42 | 0.04 | | 2 | 395 | 0.02 | 0.17 | 27.76 | 0.08 | | 3 | 5573 | 0.98 | 45.31 | 5247.65 | 530.40 | | 4 | 79187 | 30.40 | 8502.12 | timeout | timeout | | 5 | 1130669 | 805.38 | timeout | timeout | timeout | Moreover, we consider the formula: expressing that the election authority can make sure that, for every strategy of the coercer, voter 1 has a strategy to eventually complete her participation in the election, having voted for candidate 1 without getting punished. Clearly, the formula is true in every model ESVk,n (the strategy for e being high protection, and for the voter to never give away her vote). In the experiments, we have only used models with n = 2. Thus, the number of voters (k) was the sole scaling factor. We implemented the model checking algorithm in Section 4 in Python 3, using explicit representation of states and transitions. The tool is available on-line 5 . For the general SL[1G] algorithm, we used the MCMAS-SL[1G] extension of MCMAS [Cerm´ak et al., 2015] and the MCMAS-SLK extension. The experiments were conducted on an Intel Core i76700 CPU with dynamic clock speed of 2.60-3.50 GHz and 32 GB RAM, running under 64bit Windows 10. The timeout was set to 5 hours. The experimental results are presented in Tab. 1. All times are given in seconds. The first two columns describe the model configuration and its size. The next two columns show the model generation time and the verification time for our algorithm. Finally, the last column presents the performance of the general SL[1G] tool. The results show significant improvement in running time when using the specialized algorithm (by orders of magnitude). Moreover, our implementation was able to verify models of up to nearly 80, 000 states, while the more general tool handled only 10 times smaller models. ## 6 Conclusions In this paper we advanced the state of the art on tractable logics for strategic reasoning in MAS. Inspired by the restriction of the Alternating-time Temporal Logic ATL∗ to ATL, we introduced Strategy Logic with simple goals (SL[SG]), a fragment of Strategy Logic that only allows for simple goals of form Xφ, φUφ′ , and φRφ′ . Alternatively, SL[SG] can be seen as the extension of ATL to arbitrary quantification on the agents' strategies. Such an extension is motivated by relevant specification requirements in Game Theory, voting protocols, and formal verification. In particular, we showed that subtle notions, such as Stackelberg equilibria, coercion-resistance, module checking, can all be naturally represented in SL[SG]. Then, we analysed the comparative expressivity of SL[SG], and introduced the family of logics SLn[SG] and SL-n [SG], for n ∈ N, inbetween CTL and SL[SG]. We pointed out that ATL is strictly less expressive than SL[SG] and even SL-2 [SG] (Theorem 4). We showed that strategy binding strictly increases the expressive power of our fragments (Theorem 5). Most importantly, the enhanced expressivity of SL[SG] w.r.t. ATL comes at no extra computational cost: model checking SL[SG] is P-complete, the same complexity as ATL (Theorem 10). Because of its tractable model checking problem, SL[SG] lends itself to an efficient implementation. As an evidence, in Section 5 we presented an implementation of the proposed SL[SG] model checking algorithm and conducted a series of experiments that have showed striking improvements in running time with respect to the implementation of the SL[1G] algorithm in [Cerm´ak et al., 2015]. 5 https://github.com/slsgijcai19/StrategyLogicSimpleGoals. RelatedWork. Logics for strategies are a powerful tool for strategic reasoning in MAS. Their major bottleneck is the high complexity of the related decision problems. To overcome this, two main lines of research have been followed recently. One deals with semantical restrictions, mainly by limiting the number of strategies to evaluate [Chatterjee et al., 2014; Vester, 2013; Brihaye et al., 2009; Jamroga et al., 2017b; Bruy`ere et al., 2013]; while the other deals with the syntax, e.g., by looking at "simpler" fragments [Alur and La Torre, 2004; Pauly, 2002; Mogavero et al., 2014]. In this paper, we focused on this second line. Among such fragments, one of the most studied is ATL, a proper sublanguage of ATL∗ [Alur et al., 2002]. Recently, the syntactic restriction to simple goals behind the success of ATL has also been investigated in the context of more powerful logics for strategic reasoning. In [Malvone et al., 2018] the authors consider the simple vanilla fragment of Graded SL[1G] (GSL[1G]), but for two agents only. Hence, their contribution is orthogonal to ours: it is more general, as they can count strategies, but also more restricted, since it only considers two agents. Further, in [Laroussinie and Markey, 2015] the authors consider the ATL-like restriction of ATL∗ with strategy contexts. However, this restriction does not reduce the expressive power nor the complexity of the related decision problems. FutureWork. Anatural direction for future work is to look for more expressive, yet tractable, formalisms. For instance, [Bulling and Jamroga, 2010] introduced ATL+ that sits between ATL and ATL∗ . This fragment includes only formulas where each temporal operator is followed by a state formula, and allows cooperation modalities to be followed by a Boolean combination of path formulas. Notably, model checking ATL+ is PSPACE-complete. We envisage an extension of SL[SG] similar to ATL+, hopefully with a PSPACEcomplete model checking problem too. We also plan to release our model checking prototype as a verification tool. ## Acknowledgements F. Belardinelli acknowledges the support of the ANR JCJC Project SVeDaS (ANR-16-CE40-0021). W. Jamroga and D. Kurpiewski acknowledge the support of the National Centre for Research and Development NCBiR, Poland, and the National Research Fund FNR, Luxembourg, under the PolLux/FNR-INTER project VoteVerif (POLLUXIV/1/2016). ## References 1. [Ågotnes et al., 2007] T. Ågotnes, V. Goranko, and W. Jamroga. Alternating-Time Temporal Logics with Irrevocable Strategies. In TARK'07, pages 15-24, 2007. 2. [Alur and La Torre, 2004] R. Alur and S. La Torre. Deterministic generators and games for LTL fragments. ACM Trans. Comput. Log., 5(1):1-25, 2004. 3. [Alur et al., 2001] R. Alur, L. de Alfaro, R. Grosu, T. Henzinger, A. Thomas, M. Kang, C. Kirsch, R. Majumdar F. Mang, and B- Y. Wang. jMocha: A model checking tool that exploits design structure. In ICSE'01, pages 835-836. IEEE, 2001. 4. [Alur et al., 2002] R. Alur, T. A. Henzinger, and O. Kupferman. Alternating-time temporal logic. J. ACM, 49(5):672-713, 2002. 5. [Belardinelli et al., 2018] F. Belardinelli, C. Dima, and A. Murano. Bisimulations for logics of strategies: A study in expressiveness and verification. In KR'18, pages 425-434, 2018. 6. [Bouyer et al., 2015] P. Bouyer, P. Gardy, and N. Markey. Weighted strategy logic with boolean goals over one-counter games. In FSTTCS'15, pages 69-83, 2015. 7. [Brihaye et al., 2009] T. Brihaye, A. Da Costa Lopes, F. Laroussinie, and N. Markey. ATL with strategy contexts and bounded memory. In LFCS'09, pages 92-106, 2009. 8. [Bruyère et al., 2013] V. Bruyère, E. Filiot, M. Randour, and J. F. Raskin. Meet your expectations with guarantees: Beyond worst- case synthesis in quantitative games. CoRR,abs/1309.5439, 2013. 9. [Bulling and Jamroga, 2010] N. Bulling and W. Jamroga. Verifying agents with memory is harder than it seemed. AI Communica- tions, 23:380-403, 2010. 10. [Cermák et al., 2014] P. Cermák, A. Lomuscio, F. Mogavero, and A. Murano. MCMAS-SLK: A model checker for the verification of strategy logic specifications. In CAV'14, pages 525-532, 2014. 11. [Cermák et al., 2015] P. Cermák, A. Lomuscio, and A. Murano. Verifying and synthesising multi-agent systems against one-goal strategy logic specifications. In AAAI'15, pages 2038-2044, 2015. 12. [Cermák et al., 2018] P. Cermák, A. Lomuscio, F. Mogavero, and A. Murano. Practical verification of multi-agent systems against SLK specifications. I&C, 261(Part 3):588-614, 2018. 13. [Chatterjee et al., 2010] K. Chatterjee, T.A. Henzinger, and N. Piterman. Strategy Logic. I&C, 208(6):677-693, 2010. 14. [Chatterjee et al., 2014] K. Chatterjee, L. Doyen, S. Nain, and M. Y. Vardi. The complexity of partial-observation stochastic parity games with finite-memory strategies. In ICFSSCS'14, pages 242-257, 2014. 15. [Cimatti et al., 2002] A. Cimatti, E. M. Clarke, E. Giunchiglia, F. Giunchiglia, M. Pistore, M. Roveri, R. Sebastiani, and A. Tac- chella. NUSMV2: An open-source tool for symbolic model checking. In CAV'02, pages 359-364, 2002. 16. [Gammie and van der Meyden, 2004] P. Gammie and R. van der Meyden. MCK: Model checking the logic of knowledge. In CAV'04, pages 479-483, 2004. 17. [Gardy et al., 2018] P. Gardy, P. Bouyer, and N. Markey. Depen- dences in strategy logic. In STACS'18, pages 34:1-34:15, 2018. 18. [Hoek and Wooldridge, 2003] W. van der Hoek and M. Wooldridge. Cooperation, knowledge, and time: Alternating- time temporal epistemic logic and its applications. Studia Logica, 75(1):125-157, 2003. 19. [Huang and van der Meyden, 2014] X. Huang and R. van der Mey- den. Symbolic model checking epistemic strategy logic. In AAAI'14, pages 1426-1432, 2014. 20. [Jamroga and Bulling, 2011] W. Jamroga and N. Bulling. Compar- ing variants of strategic ability. In IJCAI'11, pages 252-257, 2011. 21. [Jamroga and Murano, 2014] W. Jamroga and A. Murano. On mod- ule checking and strategies. In AAMAS'14, pages 701-708, 2014. 22. [Jamroga and van der Hoek, 2004] W. Jamroga and W. van der Hoek. Agents that know how to play. Fundamenta Informati- cae, 62:1-35, 2004. 23. [Jamroga et al., 2017a] W. Jamroga, M. Knapik, and D. Kurpiewski. Fixpoint approximation of strategic abilities under imperfect information. In AAMAS'17, pages 1241-1249, 2017. 24. [Jamroga et al., 2017b] W. Jamroga, V. Malvone, and A. Murano. Reasoning about natural strategic ability. In AAMAS'17, pages 714-722, 2017. 25. [Kacprzak et al., 2008] M. Kacprzak, W. Nabialek, A. Niewiadom- ski, W. Penczek, A. Pólrola, M. Szreter, B. Woźna, and A. Zbrzezny. Verics 2007 -a model checker for knowledge and real-time. Fundamenta Informaticae, 85(1):313-328, 2008. 26. [Katoen, 2008] C. Baier J. P. Katoen. Principles of Model Checking (Representation and Mind Series). The MIT Press, 2008. 27. [Laroussinie and Markey, 2015] F. Laroussinie and N. Markey. Augmenting atl with strategy contexts. I&C, (245):98-123, 2015. 28. [Lomuscio et al., 2015] A. Lomuscio, H. Qu, and F. Raimondi. MCMAS: A model checker for the verification of multi-agent systems. Software Tools for Technology Transfer, 2015. 29. [Malvone et al., 2018] V. Malvone, F. Mogavero, A. Murano, and L. Sorrentino. Reasoning about graded strategy quantifiers. I&C, 259:390 -411, 2018. 30. [Mogavero et al., 2012] F. Mogavero, A. Murano, G. Perelli, and M. Vardi. What makes ATL* decidable? a decidable fragment of strategy logic. In CONCUR'12, pages 193-208, 2012. 31. [Mogavero et al., 2014] F. Mogavero, A. Murano, G. Perelli, and M. Y. Vardi. Reasoning about strategies: On the model-checking problem. ACM Trans. Comput. Log., 15(4):34:1-34:47, 2014. 32. [Mogavero et al., 2017] F. Mogavero, A. Murano, G. Perelli, and M. Y. Vardi. Reasoning about strategies: on the satisfiability problem. Logical Methods in Computer Science, 13(1), 2017. 33. [Pauly, 2002] M. Pauly. A modal logic for coalitional power in games. J. Log. Comput., 12(1):149-166, 2002. 34. [Tabatabaei et al., 2016] M. Tabatabaei, W. Jamroga, and Pe- ter Y. A. Ryan. Expressing receipt-freeness and coercion- resistance in logics of strategic ability: Preliminary attempt. In PrAISe@ECAI 2016, pages 1:1-1:8, 2016. 35. [Vester, 2013] S. Vester. Alternating-time temporal logic with finite-memory strategies. In GandALF'13, pages 194-207, 2013.