Scalable Verification of Strategy Logic through Three-Valued Abstraction

1 Introduction

In multi-agent systems, logics for strategic reasoning play a key role. In this domain, one of the success stories is Alternating-time Temporal Logic (ATL∗ )[Alur et al., 2002], which can express cooperation and competition among teams of agents in order to achieve temporal goals, such as fairness, liveness, safety requirements. In fact, ATL∗ extends the well known branching-time temporal logic CTL∗ [Halpern and Shoham, 1986] by generalizing the existential E and universal A path quantifiers of CTL∗ with the strategic modalities ⟨⟨C⟩⟩ and [[C]], where C is a coalition of agents. However, it has been observed that ATL∗ suffers from a number of limitations that, on the one hand, make the model-checking and satisfiability problems decidable (both are 2ExpTimecomplete); but, on the other hand, make the logic too weak to express key game-theoretic concepts, such as Nash equilibria [Mogavero et al., 2012]. To overcome these limitations, Strategy Logic (SL) [Mogavero et al., 2014; Chatterjee et al., 2010] has been put forward. A key aspect of SL is to consider strategies as first-order objects that can be existentially or universally quantified over by means of the strategy quantifiers ∃x and ∀x, respectively. Then, by means of a binding operator (a, x), a strategy x can be associated to a specific agent a. This allows to reuse strategies as well as to share them among different agents. Since its introduction, SL has proved to be a powerful formalism: it can express complex solution concepts, including Nash equilibria, and subsumes all previously introduced logics for strategic reasoning, including ATL∗ . The high expressivity of SL has spurred its analysis in a number of directions and extensions, such as prompt [Aminof et al., 2016], graded [Aminof et al., 2018], fuzzy [Bouyer et al., 2019], probabilistic [Aminof et al., 2019], and imperfect [Berthon et al., 2021; Belardinelli et al., 2020] strategic reasoning.

As one may expect, the high expressivity of SL comes at a price. Indeed, its model-checking problem turns out to be non-elementary [Mogavero et al., 2014]. Moreover, the model checking procedure is not immune to the wellknown state-space explosion, as faithful models of real-world systems are intrinsically complex and often infeasible even to generate, let alone verify. These issues call for techniques to make model checking SL amenable at least in practice. A technique that has been increasingly used in industrial settings to verify hardware and software systems is state abstraction, which allows to reduce the state space to manageable size by clustering "similar" concrete states into abstract states. Abstraction has been first introduced for stand-alone systems [Clarke et al., 1994], then extended to two-agent system verification [Grumberg et al., 2007; Shoham and Grumberg, 2004; Bruns and Godefroid, 2000; Aminof et al., 2012]. Recently, abstraction approaches have been investigated for multi-agent systems w.r.t. ATL∗ specifications [Kouvaros and Lomuscio, 2017; Belardinelli et al., 2019; Belardinelli and Lomuscio, 2017; Jamroga et al., 2016; Jamroga et al., 2020; Belardinelli et al., 2023; Ferrando and Malvone, 2023; Belardinelli et al., 2022; Belardinelli et al., 2018; Belardinelli and Malvone, 2020; Ferrando and Malvone, 2021; Ferrando and Malvone, 2022]. A natural direction is then to investigate a form of abstraction suitable for Strategy Logic as well.

Our Contribution. In this paper we introduce the first notion of three-valued abstraction for SL. The contribution of this paper is threefold. First, in Sec. 3 we define a threevalued semantics for SL where, besides the standard truth values true ⊤ and false ⊥, we have a third value undefined u that models situations where the verification procedure is not able to return a conclusive answer. Second, in Sec. 4 we introduce an abstraction procedure for SL, which can reduce significantly the size of the state space of SL models, although at the cost of making some formulas undefined. The main theoretical result is the Preservation Theorem 4.2, which allows us to model check SL formulas in the three-valued abstraction and then lift any defined answer to the original twovalued model. Third, in Sec. 6 we evaluate empirically the trade-off between state-space reduction and definiteness, by applying our abstraction procedure to a scheduling scenario. What we observe empirically is a significant reduction of the model size, which allows us to verify instances that are not amenable to current model checking tools.

Related Work. The present contribution is inspired by a long tradition of works on the abstraction of MAS models, including through three-valued semantics. An abstractionrefinement framework for the temporal logic CTL over a three-valued semantics was first studied in [Shoham and Grumberg, 2004; Shoham and Grumberg, 2007], and then extended to the full µ-calculus [Grumberg et al., 2007] and hierarchical systems [Aminof et al., 2012]. Three-valued abstractions for the verification of Alternating-time Temporal Logic have been put forward in [Ball and Kupferman, 2006; Lomuscio and Michaliszyn, 2014; Lomuscio and Michaliszyn, 2015; Lomuscio and Michaliszyn, 2016]. In [Ball and Kupferman, 2006; Shoham and Grumberg, 2004] ATL∗ is interpreted under perfect information; while [Lomuscio and Michaliszyn, 2014; Lomuscio and Michaliszyn, 2015; Lomuscio and Michaliszyn, 2016] consider non-uniform strategies [Raimondi and Lomuscio, 2005]. Finally, [Jamroga et al., 2016; Jamroga et al., 2020] introduce a multi-valued semantics for ATL∗ that is a conservative extension of the classical two-valued variant. Related to this line, three-valued logics have been extensively applied to system verification, including [Bruns and Godefroid, 1999; Huth et al., 2001; Godefroid and Jagadeesan, 2003]

Clearly, we build in this long line of works, but the expressiveness of SL raises specific challenges that the authors of the contributions above need not to tackle. We briefly mention them here and refer to specific sections for further details. First, we have to introduce individual must and may actions and strategies as under- and over- approximations of the behaviours of our agents. Second, the loosely-coupled nature of agents requires to consider non-deterministic transitions in the abstraction (Sec. 4). Third, the arbitrary alternation of existential and universal strategy quantifiers makes proving the Preservation Theorem 4.2 significantly more challenging, and complicates our experiments in verifying three-valued SL in the two-valued model-checking tool MCMAS (Sec. 6).

2 Reasoning about Strategies

In this section we recall the definitions of basic notions for Strategy Logic [Mogavero et al., 2014].

2.1 Syntax

Strategy Logic (SL) syntactically extends LTL with two strategy quantifiers, the existential ∃x and universal ∀x, and an agent binding (a, x), where a is an agent and x a variable. Intuitively, these additional elements can be respectively read as

"there exists a strategy x", "for all strategies x", and "bind agent a to the strategy associated with the variable x". Since negated quantifiers often prove problematic in many valued settings, we restrict the syntax of SL to formulas in Negation Normal Form (NNF), without loss of expressiveness. In that case, the universal strategic quantifier ∀x and the temporal operator "Release" R are added as primitives, and negation is allowed only at the level of literals. Note that every formula of SL can be equivalently transformed to one in NNF, with at most a linear blowup [Mogavero et al., 2014].

Definition 2.1 (SL Syntax). Given the set AP of atoms, variables Var, and agents Ag, the formal syntax of SL is defined as follows, where p ∈ AP, x ∈ Var, and a ∈ Ag:

We introduce the derived temporal operators as usual: Fφ = ⊤Uφ ("eventually") and Gφ = ⊥Rφ ("always").

Usually, predicate logics need the concepts of free and bound placeholders in order to formally define their semantics. In SL, since strategies can be associated to both agents and variables, we introduce the set of free agents/variables free(φ) as the subset of Ag ∪ Var containing (i) all agents a for which there is no binding (a, x) before the occurrence of a temporal operator, and (ii) all variables x for which there is a binding (a, x) but no quantification ∃x or ∀x. A formula φ without free agents (resp., variables), i.e., with free(φ) ∩ Ag = ∅ (resp., free(φ) ∩ Var = ∅), is called agent-closed (resp., variable-closed). If φ is both agent- and variable-closed, it is a sentence.

2.2 Two-valued Semantics

We now provide a formal semantics to Strategy Logic.

Models. Tomodel the behaviour of multi-agent systems, we use a variant of concurrent game structures [Alur et al., 2002].

Definition 2.2 (CGS). A concurrent game structure (CGS) is a tuple G = ⟨Ag, St , s0, Act, τ, AP, V ⟩ such that (i) Ag is a finite, non-empty set of agents. (ii) St is a finite, non-empty set of states, with initial state s0 ∈ St. (iii) Act is a finite, nonempty set of actions. We use ACT = Act|Ag| for the set of all joint actions (a.k.a. action profiles), i.e., tuples of individual actions, played synchronously by all agents. (iv) τ : St × ACT → 2St is the transition function assigning successor states {s′ , s′′ , . . . } = τ(s, ⃗α) to each state s ∈ St and joint action ⃗α ∈ ACT . We assume that the transitions in a CGS are deterministic, i.e., τ(s, ⃗α) is always a singleton. 1 (v) AP is a set of atomic propositions, and (vi) V : St × AP → {⊤, ⊥} is a two-valued labelling function.

By Def. 2.2 a CGS describes the interactions of a group Ag of agents, starting from the initial state s0 ∈ St , according to the transition function τ. We use G as a subscript for AgG, StG, etc., whenever the model is not clear from the context.

1 The deterministic transitions in a CGS are usually defined by a function of type τ : St × ACT → St. We use a slightly different (but equivalent) formulation. This will make it easier for us to extend it to nondeterministic transitions in three-valued models (see Def. 3.1).

Note that the CGSs used in the semantics of Strategy Logic assume that all the actions are available to every agent at every state [Mogavero et al., 2014]. This is because a strategy assigned to variable x can be later associated with any agent a by means of the binding operator (a, x). As a consequence, the available strategies (and hence also the available actions) are the same for every agent.

Tracks, Paths, Strategies. We denote the i-th element of a tuple v as vi, the prefix of v of lenght i as v≤i, and with last(v) as the last element of v. A track is a finite nonempty sequence of states ρ ∈ St + such that, for all 0 ≤ i ≤ |ρ| - 1, there is an action profile ⃗α ∈ ACT with (ρ)i+1 ∈ τ ((ρ)i, ⃗α). Similarly, a path is an infinite sequence of states π ∈ St ω such that, for all i ∈ N, there is ⃗α ∈ ACT with (π)i+1 ∈ τ((π)i, ⃗α). The set Trk ⊆ St + contains all the tracks in the model, and Trk(s) the tracks starting at state s ∈ St. The sets Pth and Pth(s) are defined analogously. We denote the prefix of a path π up to position i ∈ N as π≤i.

A strategy is a partial function f : Trk → Act that maps each track in its domain to an action. Intuitively, a strategy is a conditional plan that, for some tracks of G, prescribes an action to be executed. A strategy is memoryless (or positional), if last(ρ) = last(ρ′ ) implies f(ρ) = f(ρ′ ), that is, the strategy only depends on the last state. The set Str = Trk → Act (resp., Str(s) = Trk(s) → Act) contains all strategies (resp., strategies starting from s).

Assignments. Let Var be the set of variables. An assignment is a partial function χ : Var ∪ Ag → Str mapping variables and agents in its domain to strategies. An assignment χ is complete if it is defined on all agents, i.e., Ag ⊆ dom(χ). The set Asg = Var ∪ Ag → Str contains all assignments. Moreover, Asg(X)=X→Str indicates the subset of X-defined assignments, i.e., assignments defined on X ⊆ Var ∪ Ag.

As in first-order logic, in order to quantify over strategies or bind a strategy to an agent, we update an assignment χ by associating an agent or a variable l with a new strategy f. Let χ ∈ Asg be an assignment, f ∈ Str a strategy and l ∈ Var∪Ag either an agent or a variable. Then, χ[l ↦→ f] ∈ Asg denotes the new assignment that returns f on l and the same value that χ would return on the rest of its domain.

Outcome Plays of a Strategy. A play is the unique outcome of the game settled by all agent strategies engaged in it. Formally, given a state s ∈ St and a complete assignment χ ∈ Asg(s), the function play(χ, s) returns the path π ∈ Pth(s) such that, for all i ∈ N, it holds that {πi+1} = τ(πi, ⃗α), where ⃗α(a) = χ(a)(π≤i) for each a ∈ Ag.

We now define the translation of an assignment together with a related path (resp. state). It is used to keep track, at a certain stage of the play, of the current state and its updated assignment. For a path π and an assignment χ ∈ Asg, the i-th global translation of (χ, π) with i ∈ N is the pair (χ, π)i = (χπ≤i , πi) of an assignment and a state. Moreover, for a state s ∈ St , we define (χ, s)i = (χ, play(χ, s))i .

As in the case of components of a model, in order to avoid any ambiguity, we sometimes use the name of the model as a subscript of the sets and functions introduced above.

Satisfaction. The (two-valued) satisfaction relation for SL is defined as follows.

Definition 2.3 (Two-valued Satisfaction). Given a model G, for all SL formulas φ, states s ∈ St, and assignments χ ∈ Asg with free(φ) ⊆ dom(χ), the satisfaction relation (G, χ, s) |=2 φ is inductively defined as follows:

• (G, χ, s) |=2 p iff V (s, p) = ⊤, for p ∈ AP.
• Boolean operators are interpreted as usual.
• (G, χ, s) |=2 ∃xφ iff for some strategy f ∈ Str(s), (G, χ[x ↦→ f ], s) |=2 φ.
• (G, χ, s) |=2 ∀xφ iff for all strategies f ∈ Str(s), (G, χ[x ↦→ f ], s) |=2 φ.
• (G, χ, s) |=2 (a, x)φ iff (G, χ[a ↦→ χ(x)], s) |=2 φ.
• Finally, if the assignment χ is also complete, it holds that:
• (G, χ, s) |=2 Xφ iff (G, (χ, s)1 ) |=2 φ;
• (G, χ, s) |=2 φ1Uφ2 iff for some index i ∈ N, (G, (χ, s)i ) |=2 φ2 and, for all j < i, it holds that (G, (χ, s)j ) |=2 φ1;
• (G, χ, s) |=2 φ1Rφ2 iff, for all i ∈ N, (G, (χ, s)i ) |=2 φ2 or there is j ≤ i such that (G, (χ, s)i ) |=2 φ1.

Due to the semantics of the Next X, Until U, and Release R operators, LTL semantics is clearly embedded into the SL one. Furthermore, since the satisfaction of a sentence φ does not depend on assignments, we omit them and write (G, s) |= φ, when s is a generic state in St , and G |= φ when s = s0.

Note that we can easily define the memoryless variant of strategy logic by restricting the clauses for operators ∃x and (a, x) to memoryless strategies.

Finally, we define the (two-valued) model checking problem for SL as determining whether an SL formula ϕ holds in a CGS G, that is, whether G |=2 ϕ. We conclude this section by stating the related complexity result.

Theorem 2.4 ([Mogavero et al., 2014]). The model checking problem for Strategy Logic is non-elementary.

3 Three-Valued Strategy Logic

In this section we introduce a novel three-valued semantics for Strategy Logic starting by extending CGSs.

3.1 Three-Valued CGSs

We extend (two-valued) CGSs with must and may transitions as under- and over-approximations of the strategic abilities of agents.

Definition 3.1 (Three-valued CGS). A three-valued CGS is a tuple G=⟨Ag, St , s0, Actmay, Actmust, τ may, τ must, AP, V ⟩, where:

• Ag, St , s0, AP are defined as in Def. 2.2.
• Actmay and Actmust provide respectively the upper and lower approximation of the available actions. We assume that Actmust ⊆ Actmay . The sets of may and must action profiles are given by ACT may = (Actmay )|Ag| and ACT must = (Actmust )|Ag| , respectively.

• τ may : St ×ACT may → 2St is the may transition function, and τ must : St ×ACT may → 2St the must transition function. Note that both functions are possibly nondeterministic and are defined on all the potential action profiles in the system, i.e., ACT may . However, we only require that they return nonempty successor sets on their respective action profiles. That is, τ may (s, ⃗α) ̸= ∅ for every state s ∈ St and action profile ⃗α ∈ ACT may , and τ must (s, ⃗α) ̸= ∅ for every state s ∈ St and action profile ⃗α ∈ ACT must . 2 Moreover, it is required that τ must (s, ⃗α) ⊆ τ may (s, ⃗α) for every s ∈ St and ⃗α ∈ ACT may . In other words, every must transition is also a may transition, but not necessarily viceversa.
• The labelling function V : St × AP → {⊥,⊤, u} maps now each pair of a state and an atom to a truth value of "true," "false," or "undefined."

The notions of tracks, paths, and the definitions of sets Trk , Trk (s), Pth, Pth(s) carry over from Section 2.2.

May/Must Strategies and their Outcomes. A maystrategy (resp. must-strategy) is a function f : Trk → Actmay (resp. Actmust ) that maps each track to a may (resp. must) action. Note that each must-strategy is a maystrategy, but not necessarily the other way around. Moreover, we can define memoryless may- and must-strategies in the standard way. The sets Strmay and Strmust are defined analogously to Section 2.2.

Given a state s ∈ St and a profile of (may and/or must) strategies, represented by a complete assignment χ ∈ Asg, we define two kinds of outcome sets, plays may (χ, s) and plays must (χ, s). The former over-approximates the set of paths that can really occur when executing χ from s, while the latter under-approximates it. Typically, we will use plays may to establish that the value of a temporal formula φ is ⊤ (if φ holds in all such paths), and plays must for ⊥ (if φ is false in at least one path). Formally, the function plays may (χ, s) returns the paths π ∈ Pth(s) such that, for all i ∈ N, it holds that πi+1 ∈ τ may (πi, ⃗α), where ⃗α(a) = χ(a)(π≤i) for each a ∈ Ag. The definition of plays must (χ, s) is analogous, only with τ must being used instead of τ may .

3.2 Three-valued Semantics

We now define the Three-valued satisfaction relation for Strategy Logic.

Definition 3.2 (Three-valued Satisfaction). Given a 3-valued model G, for all SL formulas φ, states s ∈ St, and assignments χ ∈ Asg(s) with free(φ) ⊆ dom(χ), the satisfaction relation (G, χ, s |=3 φ)=tv is inductively defined as follows.

• (G, χ, s |=3 p) = V (s, p), for p ∈ AP.
• Boolean operators are interpreted as in Łukasiewicz's three valued logic [Łukasiewicz, 1920].
• For ϕ = ∃xφ,
• (G, χ, s |=3 ϕ) = ⊤ iff (G, χ[x ↦→ f], s |=3 φ) = ⊤ for some must -strategy f ∈ Strmust (s);

2 Note that the function τ must is total because we assume the empty set as an element of the co-domain.

• (G, χ, s |=3 ϕ) = ⊥ iff (G, χ[x ↦→ f], s |=3 φ) = ⊥ for all may-strategies f ∈ Strmay (s);
• otherwise, (G, χ, s |=3 ϕ) = u.
• For ϕ = ∀xφ,
• (G, χ, s |=3 ϕ) = ⊤ iff for all may-strategies f ∈ Strmay (s), (G, χ[x ↦→ f ], s |=3 φ) = ⊤;
• (G, χ, s |=3 ϕ) = ⊥ iff for some must-strategy f ∈ Strmust (s), (G, χ[x ↦→ f ], s |=3 φ) = ⊥;
• otherwise, (G, χ, s |=3 ϕ) = u.
• (G, χ, s |=3 (a, x)φ) = (G, χ[a ↦→χ(x)], s |=3 φ).
• Finally, if the assignment χ is also complete, we define:
• (G, χ, s |=3 Xφ) = ⊤ iff for all π ∈ plays may (χ, s), we have (G, (χ, π)1 |=3 φ) = ⊤;
• (G, χ, s |=3 Xφ) = ⊥ iff for some π ∈ plays must (χ, s), we have (G, (χ, π)1 |=3 φ) = ⊥;
• otherwise, (G, χ, s |=3 Xφ) = u.
• (G, χ, s |=3 φ1Uφ2) = ⊤ iff for all π ∈ plays may (χ, s), there is i ∈ N such that (G, (χ, π)i |=3 φ2) = ⊤, and for all j < i we have (G, (χ, π)j |=3 φ1) = ⊤;
• (G, χ, s |=3 φ1Uφ2) = ⊥ iff for some π ∈ plays must (χ, s) and all i ∈ N, we have (G, (χ, π)i |=3 φ2) = ⊥ or there exists j < i such that (G, (χ, π)j |=3 φ1) = ⊥;
• otherwise, (G, χ, s |=3 φ1Uφ2) = u.
• (G, χ, s |=3 φ1Rφ2) = ⊤ if for all π ∈ plays may (χ, s) and i ∈ N, we have (G, (χ, π)i |=3 φ2) = ⊤ or there exists j ≤ i such that (G, (χ, π)j |=3 φ1) = ⊤;
• (G, χ, s |=3 φ1Rφ2) = ⊥ iff for some π ∈ plays must (χ, s) and i ∈ N, we have (G, (χ, π)i |=3 φ2) = ⊥ and for all j ≤ i, we have (G, (χ, π)j |=3 φ1) = ⊥;
• otherwise, (G, χ, s |=3 φ1Rφ2) = u.

Again, we can define the memoryless, three-valued satisfaction relation for SL by restricting the clauses for operators ∃x, ∀x, and (a, x) to memoryless strategies. Similarly to Section 2, if ϕ is a sentence, then (G, s |=3 φ) = (G, χ, s |=3 φ) for any assignment χ, and (G |=3 φ) = (G, s0 |=3 φ).

We now show that our three-valued semantics in Def. 2.3 is a conservative extension of the standard two-valued interpretation in Sec. 2.

Theorem 3.3 (Conservativeness). Let G be a standard CGS, that is, Actmay = Actmust , τ may = τ must are functions, and the truth value of every atom is defined (i.e., it is equal to either ⊤ or ⊥). Then, for every formula ϕ in SL,

Proof. The result follows from the fact that in standard CGS the clauses for the three-valued satisfaction relation collapse to those for two-valued satisfaction, whenever Actmay = Actmust , τ may = τ must are functions, and the truth value of every atom is defined.

Remark 3.4 (Model checking). For any syntactic fragment L of SL, model checking of L with 3-valued semantics can be reduced to 2-valued model checking of L by a construction similar to [Jamroga et al., 2016, Theorem 4]. Note also that 2-valued model checking for L is a special case of its 3valued counterpart, due to Theorem 3.3. Thus, the decidability and complexity for 2-valued model checking in fragments of SL carry over to 3-valued verification.

4 Three-valued Abstraction for SL

Here, we define the 3-valued state abstraction for CGS. The idea is to cluster the states of a CGS (called the concrete model) according to a given equivalence relation ≈, e.g., one provided by a domain expert. Typically, two states are deemed equivalent if they agree on the evaluation of atoms, possibly just the atoms appearing on a given formula ϕ to be checked. In some cases, such an equivalence relation might be too coarse and therefore more domain-dependent information could be taken into account.

Then, the sets of may (resp. must) actions and the may (resp. must) transitions are computed in such a way that they always overapproximate (resp. underapproximate) the actions and transitions in the concrete model. Formally, the abstraction is defined as follows.

Definition 4.1 (Abstraction). Let G = ⟨Ag, St, s0,Act, τ, AP, V ⟩ be a CGS, and ≈⊂ St × St an equivalence relation. We write [s] for the equivalence class of ≈ that contains s. The abstract model of G w.r.t. ≈ is defined as the 3-valued CGS A(G) = ⟨A(Ag), A(St ), A(s0), Amay (Act), Amust (Act), Amay (τ ), Amust (τ ), A(AP ), A(V )⟩, with:

• A(Ag) = Ag and A(AP ) = AP .
• A(St) = {[s] | s ∈ St} with A(s0) = [s0].
• Amay (Act) = Act.
• Amay (τ) = τ may : A(St) × (Amay (Act))|A(Ag)| → 2A(St) such that τ may ([s], ⃗α) = {[ssucc] | ∃s′ ∈ [s] ∃s′succ ∈ [ssucc] . s′succ ∈ τ(s′ , ⃗α)}).
• Amust (τ) = τ must : A(St) × (Amay (Act))|A(Ag)| → 2A(St) such that τ must ([s], ⃗α) = {[ssucc] | ∀s′ ∈ [s] ∃s′succ ∈ [ssucc] . s′succ ∈ τ(s′ , ⃗α)}).
• Amust (Act) is a maximal 3 set Actmust ⊆ Act such that ∀s ∈ St ∀⃗α ∈ (Actmust )|A(Ag)| . τ must ([s], ⃗α) ̸= ∅. Note that a unique maximal set does not always exist. In such cases, a natural heuristics would be to choose the maximal subset of actions with the largest cardinality, breaking ties lexicographically in case there are still multiple solutions.

Note that A(G) can be computed in polynomial time w.r.t. the size of G, assuming the above heuristics for Amust (Act).

3 with respect to set inclusion.

We now prove that the abstraction preserves classical truth values. Given a strategy f in G, we define the set of corresponding may-strategies in A(G) by abstrmay (f) = {f † | f † ([s0], . . . , [sn]) = f(s′0 , . . . , s′n ) for some s′0 ∈ [s0], . . . , s′n ∈ [sn]}. Moreover, abstrmust (f) = abstrmay (f) ∩ Strmust . Note that abstrmay (f) is always nonempty. Also, abstrmust (f) is either empty or a singleton.

Conversely, given a (may or must) strategy f in A(G), we define the set of corresponding concrete strategies in G by concr(f) = {f ∗ | f ∗ (s0, . . . , sn) = f([s0], . . . , [sn])}. Notice that concr(f) is always a singleton for must strategies, and either empty or a singleton for may strategies. We lift abstrmay , abstrmust , concr to sets of strategies in the standard way. Clearly, f ∈ concr(abstrmay (f)) for any concrete strategy, and f ∈ abstrmust (concr(f)) for any muststrategy. We lift the notation to assignments analogously. Observe that, in every χ∗ ∈ concr(χ[x ↦→ f]), x is assigned with f ∗ ∈ concr(f).

Theorem 4.2 (Preservation). Let G be a CGS and A(G) its abstraction induced by equivalence relation ≈. Then, for every formula ϕ in SL, every (may or must) assignment χ and state s in A(G), every assignment χ∗ ∈ concr(χ), and state t ∈ s in G, it holds that:

Proof. The proof is by induction on the structure of ϕ.

Induction base (ϕ = p): ((A(G), χ, s) |=3 ϕ) = ⊤ iff A(V )(s, p) = ⊤, iff for all t ∈ s, V (t, p) = ⊤, that is, (G, χ∗ , t) |=2 ϕ. The case for ⊥ is proved similarly. The case of ϕ = ¬p is analogous.

Case ϕ = ψ1 ∧ψ2: ((A(G), χ, s) |=3 ϕ) = ⊤ iff ((A(G), χ, s) |=3 ψ1) = ⊤ and ((A(G), χ, s) |=3 ψ2) = ⊤. By induction, for all χ∗ ∈ concr(χ) and t ∈ s, (G, χ∗ , t) |=2 ψ1 and (G, χ∗ , t) |=2 ψ2. Thus, (G, χ∗ , t) |=2 ψ1 ∧ ψ2.

Further, ((A(G), χ, s) |=3 ϕ) = ⊥ iff ((A(G), χ, s) |=3 ψ1) = ⊥ or ((A(G), χ, s) |=3 ψ2) = ⊥. By induction, for all χ∗ ∈ concr(χ) and t ∈ s, (G, χ∗ , t) ̸|=2 ψ1 or for all χ∗ ∈ concr(χ) and t ∈ s, (G, χ∗ , t) ̸|=2 ψ2. Thus, for all χ∗ ∈ concr(χ) and t ∈ s, (G, χ∗ , t) ̸|=2 ψ1 ∧ ψ2. The case of ϕ = ψ1 ∨ ψ2 is analogous.

Case ϕ = ∃xψ: (A(G), χ, s |=3 ϕ) = ⊤ iff for some muststrategy f ∈ Strmust (s), (A(G), χ[x ↦→ f], s |=3 ψ) = ⊤. By induction, for all χ∗ ∈ concr(χ[x ↦→ f]) and t ∈ s, it holds that (G, χ∗ , t) |=2 ψ. Assume that concr(χ[x ↦→ f]) is nonempty, and consider the sole concrete strategy f ∗ ∈ concr(f). Clearly, χ∗ = χ∗ [x ↦→ f ∗ ] for every χ∗ ∈ concr(χ[x ↦→ f]). Thus, (G, χ∗ [x ↦→ f ∗ ], t) |=2 ψ, and hence also (G, χ∗ , t) |=2 ∃xψ. Assume now, to the contrary, that concr(χ[x ↦→ f]) is empty. In that case, (G, χ∗ [x ↦→ f ∗ ], t) |=2 ψ holds vacuously for all χ∗ = χ∗ [x ↦→ f ∗ ], and hence again (G, χ∗ , t) |=2 ∃xψ.

Further, (A(G), χ, s |=3 ϕ) = ⊥ iff for every maystrategy f ∈ Strmay (s), (A(G), χ[x ↦→ f], s |=3 ψ) = ⊥. Take any concrete strategy g in G, and consider any g† ∈ abstrmay (f). By the above, (A(G), χ[x ↦→ g† ], s |=3

ψ) = ⊥. Thus, by induction, (G, χ∗ , t) ̸|=2 ψ for all χ∗ ∈ concr(χ[x ↦→ g† ]) and t ∈ s. Similarly to the previous paragraph, either (i) concr(χ[x ↦→ g† ]) is nonempty and χ∗ [x ↦→ g] ∈ χ∗ , thus (G, χ∗ [x ↦→ g], t) ̸|=2 ψ for all such χ∗ , or (ii) the same statement holds vacuously. In both cases, (G, χ∗ , t) ̸|=2 ∃xψ.

The cases ϕ = ∀xψ and ϕ = (a, x)ψ are analogous.

Case ϕ =Xψ: (A(G), χ, s |=3 ϕ) = ⊤ iff for all π ∈ plays may (χ, s), we have (G, (χ, π)1 ) |=3 ψ) = ⊤. By induction, (G, χ∗ , t) |=2 ψ for every π ∈ plays may (χ, s), χ∗ ∈ concr(χπ≤1 ) and t ∈ (π)1. Take any state t′ ∈ s and assignment χ′ in G such that χ′π∗≤1 = χ∗ for some π∗ ∈ plays(χ′ , t′ ). Since may paths in A(G) overapproximate paths in G, we get that (G, χ′ , t′ ) |=2 Xψ.

Further, (A(G), χ, s |=3 ϕ) = ⊥ iff for some π ∈ plays must (χ, s), we have (G, (χ, π)1 |=3 φ) = ⊥. By induction, there is π ∈ plays must (χ, s) such that (G, χ∗ , t) ̸|=2 ψ for every χ∗ ∈ concr(χπ≤1 ) and t ∈ (π)1. Take any state t′ ∈ s and assignment χ′ in G. Since must paths in A(G) underapproximate paths in G, there must be a path π∗ ∈ plays(χ′ , t′ ) such that χ′π∗≤1 = χ∗ . Thus, (G, χ′ , t′ ) ̸|=2 Xψ.

Corollary 4.3. For any CGS G and SL formula ϕ:

It is easy to see that the above results hold also for the semantic variant of SL based on memoryless strategies.

5 Implementation

We implemented a prototype tool in Java 4 , which accepts CGSs and SL properties as input, on top of MCMAS, the de facto standard model checker for MAS [Lomuscio et al., 2015]. Specifically, our tool exploits MCMAS as a blackbox, for performing the actual verification step. In fact, our tool focuses on the abstraction procedure for the verification of SL formulas (as presented in this paper), while their verification is obtained through MCMAS.

From a practical perspective, there are various aspects to report, that can be summarised as (i) input/output of the tool; (ii) abstraction of the CGS; (iii) verification in MCMAS.

(i) The implementation allows for the definition of CGSs as external JSON 5 formatted input files. In this way, any end user may easily interact with the tool, independently from the CGS's internal representation (i.e., the corresponding data structures). As CGSs, also the definition of the SL formula to check is handled as an external parameter to the tool. Once the verification ends, the outcome is returned to the user.

(ii) As presented in the paper, in order to improve the verification performance, the CGS is first abstracted. The abstraction is obtained by clustering multiple states into a single abstract state of the CGS. This step is based on an equivalence relation (≈), as presented in Definition 4.1. An abstract state may be labeled by atoms. As presented in Definition 4.1, an atom holds (resp. does not hold) in the abstract state iff it holds (resp. does not hold) in all the concrete states which have been collapsed into the abstract state. Otherwise, the atom is considered undefined. Note that, since atoms can hold, not hold, or being undefined in a state, they are explicitly labeled in each state. In practice, this is obtained by duplicating each atom p into atoms p⊤ and p⊥, which correspond to p holding or not holding in a certain state of the abstract CGS; whereas being undefined can be marked by having neither p⊤ nor p⊥ present in the abstract state.

4 https://github.com/AngeloFerrando/3-valuedSL

5 https://www.json.org/

(iii) The abstract CGS is then verified in MCMAS against an SL formula. In more detail, our tool exploits the MCMAS extension for SL[1G], i.e., the one goal fragment [Cerm´ak et al., 2015], and the MCMAS extension for SLK, i.e., an epistemic extension of SL, [Cerm´ak et al., 2014].

Note that, to make use of the MCMAS model checker, our CGSs need to be first translated into Interpreted Systems [Fagin et al., 1995]. In fact, MCMAS does not support CGSs, and it expects Interpreted Systems expressed using a domain specific language called Interpreted Systems Programming Language (ISPL). Thus, a pre-processing step before calling MCMAS is always required, where the CGS of interest is first automatically translated into its ISPL representation. This is only a technical detail, since CGSs and Interpreted Systems are equally expressive [Belardinelli et al., 2020; Goranko and Jamroga, 2004].

It is important to report that the ISPL generation is performed on standard CGSs, not on their abstraction. Indeed, the abstract CGSs as described in Definition 4.1 cannot be used in MCMAS straight away, but need to be reprocessed first. To generate a CGS which can then be verified into MCMAS, the tool splits the 3-valued CGS into two CGSs. Such a split is determined by the SL formula under evaluation; that is, given an SL formula φ, we extract two sets of agents, E and U, whose strategies are only existentially and universally quantified in φ, respectively. By using these two sets, we split the 3-valued CGS into two CGSs: one CGS where agents in E use must-strategies, while agents in U use may-strategies; one CGS where agents in E use may-strategies, while agents in U use must-strategies. The first CGS can be used to prove the satisfaction of φ, while the second CGS can be used to prove the violation of φ. This follows from Definition 2.3, third and fourth bullet points.

As a consequence of how the verification is performed in practice, we remark an important difference between the theory presented in this paper and its implementation: the implementation handles SL formulas with arbitrary alternation of universal (∀x) and existential (∃x) quantifiers, as long as for each agent (a) in the formula, there is one single binding (a, x). Even though at the theoretical level our abstraction method can handle all SL formulas, at the implementation level this is not the case. In fact, our tool is based on MCMAS, and because of that, we cannot handle formulas where the agents need to swap between universally and existentially quantified strategies. This would require to modify MCMAS internally, which we leave as future work.

6 Experiments

We carried out the experiments on a machine with the following specifications: Intel(R) Core(TM) i7-7700HQ CPU @ 2.80GHz, 4 cores 8 threads, 16 GB RAM DDR4. The case study we experimented on consists in a scheduler, where N agents, i.e., processes (called Pi for 1 ≤ i ≤ N) compete to get CPU time, while an Arbiter agent decides which process to grant access (one at a time). The full description of the example can be found in [Cerm´ak et al., 2018]. The corresponding CGS can be parameterised over the number N of processes. Naturally, such parameter largely influences the size and complexity of the resulting CGS. Table 1 reports experimental results we obtained by applying our tool to the scheduler case study. We considered the verification of the same SL formula φ verified in [Cerm´ak et al., 2018], that is:

Intuitively, φ asserts that at most one process (Pi) owns the resource (rs) at any given point in time. In Table 1, each row refers to a fixed number of processes, from 2 to 9, used to generate the corresponding CGS. Each row also reports the number of states and transitions of the CGS, and the time required to perform its verification in MCMAS, both on the original CGS and its 3-valued abstraction, for comparison. For the latter, the time required to generate such an abstraction is reported. For the experiments with the scheduler, the abstraction is assumed to be guided by an expert of the system. In more detail, all states where at least one process is waiting to be selected by the scheduler are clustered together. This choice, as apparent in Table 1, largely reduces the number of states and transitions of the CGS. Nonetheless, this does not prevent the verification process to correctly conclude the satisfaction of φ on both the CGS and its 3-valued version, i.e., the abstraction does not remove any information necessary to determine the satisfaction of φ. Table 1 also reports the execution time required for the actual verification of both the CGS and its 3-valued abstraction. As we can observe, without the abstraction step, the verification of the CGS times out when 3 processes are considered. In fact, MCMAS cannot model check φ in less than 3 hours, which was set as the time out (both for the SL[1G] and SLK extensions of MCMAS). Instead, thanks to the abstraction, the verification can be performed for up to 9 (a more realistic number of processes). Note that, the verification of the 3-valued CGS could have been performed for even larger numbers of processes. However, the CGS with 10 processes did not fit into the available memory of the machine used for the experiments; so, it was not possible to apply our technique to generate its 3-valued abstraction. Nonetheless, we expect the tool to handle even the case with 10 processes via abstraction. Figure 1 reports the data compression obtained in the scheduler case study. It is immediate to observe the huge compression obtained via abstraction. Indeed, the larger is the number of processes involved, the more significant is such compression. Note that, for more than 6 processes, the abstraction produces a CGS with ∼99% less states and transitions. Besides φ, we experimented with other specifications as well. Specifically, we carried out experiments over a large set of randomly-generated SL formulas. The goal of these experiments is to understand how many times our tool would return a conclusive answer (i.e., not u). We automatically synthesised 10,000 different SL formulas and verified them in the scheduler case study; where we kept the same abstraction as for Table 1. Over the 10,000 different SL formulas, the tool was capable of providing a defined truth value (either true or false) in the 83% of cases. Of course, this is a preliminary evaluation, which needs to be corroborated through additional experiments, also involving further real-world scenarios. Nonetheless, the results we obtained are promising, and allow us to empirically show the effectiveness of our approach, not only from a datacompression perspective, but also from a computational one.

7 Conclusion

The high complexity of the verification problem for Strategy Logic hinders the development of practical model checking tools and therefore its application in critical, real-life scenarios. As a consequence, it is of upmost importance to develop techniques to alleviate this computational burden and allow the use of Strategy Logic in concrete use cases, such as the scheduler scenario here analysed. This contribution is meant to be the first step in this direction.

Acknowledgements

1. Jamroga acknowledges the support of NCBR Poland, NCN Poland, and FNR Luxembourg under projects STV (POLLUX-VII/1/2019), SpaceVote (POLLUXXI/14/SpaceVote/2023), and SAI (2020/02/Y/ST6/00064). A. Murano acknowledges the support of the PNNR FAIR project, the InDAM project "Strategic Reasoning in Mechanism Design", and the PRIN 2020 Project RIPER.