Strategy Logic with Simple Goals: Tractable Reasoning about Strategies

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):

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.

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]. □

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.

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).