Approximate Verification of Strategic Abilities under Imperfect Information Using Local Models

1 Introduction

Logics of strategic ability. Many relevant properties of multi-agent systems (MAS) refer to strategic abilities of agents and their groups. Such properties can be conveniently specified in modal logics of strategic ability, in particular Alternating-time Temporal Logic ATL [Alur et al., 2002; Schobbens, 2004] and Strategy Logic SL [Mogavero et al., 2010; Mogavero et al., 2014; Berthon et al., 2017]. For example, the ATL formula ⟨⟨taxi⟩⟩G¬fatality expresses that the autonomous cab can drive in such a way that no one gets ever killed. Similarly, ⟨⟨taxi, passg⟩⟩Fdestination says that the cab and the passenger have a joint strategy to arrive at the destination, no matter what the other agents do.

Verification of strategic ability. Specifications in agent logics can be used as input to algorithms and tools for model checking, that have been in constant development for over 20 years [Alur et al., 1998; Alur et al., 2001; Kacprzak and Penczek, 2004; Lomuscio and Raimondi, 2006; Chen et al., 2013; Busard et al., 2014; Pilecki et al., 2014; Huang and van der Meyden, 2014; Cermak et al., 2014; Lomuscio et al., 2017; Cerm´ak et al., 2015; Belardinelli et al., 2017; Belardinelli et al., 2017; Jamroga et al., 2019; Kurpiewski et al., 2019; Kurpiewski et al., 2021; Kaminski et al., 2024]. However, model checking of strategic abilities is hard, both theoretically and in practice. First, it suffers from the well-known state/transition-space explosion.

Moreover, the space of possible strategies is at least exponential on top of the state-space explosion, and incremental synthesis of strategies is not possible in general - especially in the realistic case of agents with partial observability. Even for the more restricted (and computation-friendly) logic ATL, model checking of its imperfect information variants is ∆P2 - to PSPACE-complete for agents playing memoryless strategies [Bulling et al., 2010; Schobbens, 2004] and EXPTIME-complete to undecidable for agents with perfect recall [Dima and Tiplea, 2011; Guelev et al., 2011]. The theoretical results concur with outcomes of empirical studies on benchmarks [Busard et al., 2015; Jamroga et al., 2019; Lomuscio et al., 2017], as well as attempts at verification of real-life multi-agent scenarios [Jamroga et al., 2020b; Kim et al., 2022; Kurpiewski et al., 2023].

Fixpoint approximation. An interesting idea was proposed in [Jamroga et al., 2019] for model checking of ATLir, i.e., the variant of ATL for agents with imperfect information and imperfect recall. There, we provided a translation of ATLir formulas to alternating epistemic µ-calculus, such that, whenever the translation of ϕ was true in a given model M, the original formula must also hold there. Thus, in a sense the translation provides a lower bound for the optimal output of verification. The approximation proved conclusive and relatively efficient in many instances of benchmarks [Jamroga et al., 2019], including models of real-life voting procedures [Kurpiewski et al., 2022]. Still, it operates on the global model of the system, which means that it still suffers from the state- and transition-space explosion.

Contribution. We observe that, for asynchronous MAS, one can leverage the additional information coming from the modular representation of the system [Jamroga et al., 2020a]. In particular, the fixpoint approximation algorithm in [Jamroga et al., 2019], has the property that, with most fixpoint iterations, it adds or removes whole epistemic classes, rather than arbitrary subsets of global states. Since epistemic classes in the global model correspond to local states in the modular representation, one can equivalently do the fixpoint computation on the (exponentially smaller) local model(s) of the given agent(s). We formalize the idea through a translation to appropriate µ-calculus formulas interpreted in the local model, prove its correctness, and evaluate its efficiency through experiments on two scalable benchmarks.

In this paper, we only consider individual abilities and observable reachability/safety goals. The case of proper coalitions and non-observable goals is left for future work.

2 Preliminaries

We start by introducing representations of asynchronous MAS, their models, and the relevant logical formalisms. In our presentation, we follow [Jamroga et al., 2021].

2.1 Models of Asynchronous Interaction

Definition 1 (Asynchronous MAS). An asynchronous multi-agent system (AMAS) S consists of n agents A = {1, . . . , n}, each associated with a tuple Ai = (Li, ιi, Evti,Ri, Ti, PVi, Vi) including a set of local states Li = {l1 i , l2 i , . . . , lni i }, a designated initial state ιi ∈ Li, a nonempty finite set of events Evt i = {α1 i , α2 i , . . . , αmi i }, and a repertoire of choices Ri : Li → 22Evti . For each li ∈ Li, Ri(li) = {E1, . . . , Em} is a nonempty list of nonempty choices available to i at li. If the agent chooses Ej = {α1, α2, . . .}, then only an event in Ej can be executed at li within the agent's module. Moreover, Ti ⊆ Li × Evti × Li is a local transition relation, where (li, α, l′i ) ∈ Ti represents that event α ∈ ⋃ Ri(li) changes the local state from li to l′i . Agents are endowed with mutually disjoint, finite and possibly empty sets of local propositions PVi, and their valuations Vi : Li → 2PVi .

Note that each agent "owns" the events affecting its state, but some of the events may be shared with other agents. Those can only be executed synchronously by all the involved parties. Moreover, the agent's strategic choices are restricted by its repertoire function.

Example 1 (Asynchronous Simple Voting). Consider a simple voting system ASVkn with n + 1 agents (n voters and 1 coercer). Each Voteri agent can cast her vote for a candidate {1, . . . , k}, and decide whether to share her vote receipt with the Coercer agent. The coercer can choose to punish the voter or refrain from it. A graphical representation of the agents for n = 1, k = 2 is shown in Fig. 1. We assume that the coercer only registers if the voter hands in a receipt for candidate 1 or not. The repertoire of the coercer is defined as Rc(qc0 ) = {{gv1,1, gv1,2, ng1}} and Rc(qc g ) =

Rc(qcn ) = {{pun1}, {npun1}}, i.e., the coercer first receives the voter's decision regarding the receipt, and then controls whether the voter is punished or not. Analogously, the voter's repertoire is given by: R1(q1 0 ) = {{vote1,1}, {vote1,2}}, R1(q1 j ) = {{gv1,j}, {ng1}} for j = 1, 2, and R1(q1 1,g ) = R1(q1 1,n ) = R1(q1 2,g ) = R1(q1 2,n ) = {{pun1, npun1}}.

Notice that the coercer cannot determine which of the events gv1,1, gv1,2, ng1 will occur; this is entirely under the voter's control. This way we model the situation where it is the decision of the voter to show her vote or not. Similarly, the voter cannot avoid punishment by choosing the strategy allowing only npun1, because the choice {npun1} is not in the voter's repertoire. She can only execute {pun1, npun1}, and await the decision of the coercer.

The execution semantics is based on interleaving with synchronization on shared events.

Definition 2 (Interleaved interpreted system). Let S be an AMAS with n agents. The interleaved interpreted system IIS(S) extends S with: (i) the initial states ι = (ι1, . . . , ιn); (ii) the set of global states St ⊆ L1 × . . . × Ln that collects all the configurations of local states, reachable from ι by T (see below); (iii) the (partial) global transition function T : St × Evt ⇀ St, defined by T(g1, α) = g2 iff Ti(g i1 , α) = g i2 for all i ∈ Agent(α) and g i1 = g i2 for all i ∈ A \ Agent(α); 1 (iv) the global valuation of propositions V : St → 2PV , defined as V (l1, . . . , ln) = ⋃i∈A Vi(li).

We will sometimes write g1 α -→ g2 instead of T (g1, α) = g2. Also, we define relation ∼A= {(g, g ′ ) ∈ St × St | ∃i ∈ A. g i = g ′i } to connect states that are indistinguishable for at least one agent i ∈ A.

Definition 3 (Enabled events). Let A = {a1, . . . , ak} ⊆ A = {1, . . . , n} and -→E A = (Ea1 , . . . , Eak ) for some k ≤ n, such that Ei ∈ Ri(g i ) for every i ∈ A. Event β ∈ Evt is enabled by the vector of choices -→E A at g ∈ St iff, for every i ∈ Agent(β)∩A, we have β ∈ Ei, and for every i ∈ Agent(β)\ A, it holds that β ∈ ⋃ Ri(g i ). That is, the "owners" of β in A have selected choices that admit β, while all the other "owners" of β might select choices that do the same. We denote the set of such events by enabled(g, -→E A).

Some combinations of choices enable no events. To account for this, the models of AMAS are augmented with "silent" ϵ-loops, added when no "real" event can occur.

Definition 4 (Undeadlocked IIS). Let S be an AMAS, and assume that no agent in S has ϵ in its alphabet of events. The model of S, denoted IISϵ (S, I), extends the model IIS(S, I) as follows:

• Evt IISϵ(S) = EvtIIS(S) ∪ {ϵ}, where Agent(ϵ) = ∅;
• For each g ∈ St, we add the transition g ϵ -→ g iff there is a selection of all agents' choices -→E A = (E1, . . . , En), such that Ei ∈ Ri(gi ) and enabledIIS(S,I)(g, -→E A) = ∅. Then, for every A ⊆ A, we also fix enabledIISϵ(S) (g, -→E A) = enabledIISϵ(S) (g , -→E A) ∪ {ϵ}.

1 g i denotes agent i's state in g = (l1, . . . , ln), i.e., g i = li.

In other words, an ϵ-loop is enabled whenever EA allows the grand coalition to collectively block the execution of any "real" event.

Example 2. The model of ASV21 is shown in Figure 2. Note that it contains no ϵ-transitions, since no choices of the voter and the coercer can cause a deadlock.

2.2 Reasoning About Strategies

Let PV be a set of propositions and A the set of all agents. The syntax of alternating-time logic ATL [Alur et al., 2002; Schobbens, 2004] is given by:

where p ∈ PV , A ⊆ A, X stands for "next," G for "always from now on," U for "until," and ⟨⟨A⟩⟩γ for "agent coalition A has a strategy to enforce γ." Derived boolean connectives and constants (∨,⊤,⊥) are defined as usual. "Sometime" is defined as F φ ≡ ⊤ U φ.

Example 3. Voter enfranchisement can be expressed by formula ∧ȷ∈Candidates ⟨⟨Voter⟩⟩F votedj .

Strategic ability of agents. Following [Jamroga et al., 2021], a positional imperfect information strategy (irstrategy) for agent i is defined by a function σi : Li → 2Evti , such that σi(l) ∈ Ri(l) for each l ∈ Li. Note that σi is uniform by construction, as it is based on local, and not global states. The set of such strategies is denoted by Σir i . Joint strategies ΣirA for A = {a1, . . . , ak} ⊆ A are defined as usual, i.e., as tuples of strategies σi, one for each agent i ∈ A. By σA(g) = (σa1 (g), . . . , σak (g)), we denote the joint choice of coalition A at global state g. An infinite sequence of global states and events π = g0α0g1α1g2 . . . is called a path if gj αj -→ gj+1 for every j ≥ 0. The set of all paths in model M starting at state g is denoted by ΠM(g).

Definition 5 (Standard outcome). Let A ⊆ A. The standard outcome of strategy σA ∈ ΣirA in state g of model M is the set out Std M (g, σA) ⊆ ΠM(g) such that π = g0α0g1α1 · · · ∈ outM(g, σA) iff g0 = g, and for each m ≥ 0 we have that αm ∈ enabledM(gm, σA(gm)).

Definition 6 (Reactive outcome). The reactive outcome is the set out React M (g, σA) ⊆ out Std M (g, σA) such that π = g0α0g1α1 · · · ∈ out React M (g, σA) iff αm = ϵ implies enabledM(gm, σA(gm)) = {ϵ}.

Intuitively, the standard outcome collects all the paths where agents in A follow σA, while the others freely choose from their repertoires. The reactive outcome includes only those outcome paths where the opponents cannot miscoordinate on shared events. Let x ∈ {Std, React}. We extend the above definitions to subsets of global states G ⊆ St by out xM (G, σA) = ⋃g∈G out xM (g, σA). Now, the irsemantics of ATL in asynchronous MAS [Alur et al., 2002; Schobbens, 2004; Jamroga et al., 2021] is defined by:

M, g |=x p iff g ∈ V (p), for p ∈ PV ;

M, g |=x ⟨⟨A⟩⟩Xφ iff there is sA ∈ Σir A such that, for each path λ ∈ out xM ([g]∼A , sA), we have M, λ[1] |=x φ.

M, g |=x ⟨⟨A⟩⟩Gφ iff there is sA ∈ Σir A such that, for each λ ∈ out xM ([g]∼A , sA) and i ≥ 0, we get M, λ[i] |=x φ.

M, g |=x ⟨⟨A⟩⟩φ1 Uφ2 iff there is sA ∈ Σir A such that, for each path λ ∈ out xM ([g]∼A , sA), we have M, λ[i] |=x φ2 for some i ≥ 0 and M, λ[j] |=x φ1 for all 0 ≤ j < i.

Example 4. Let M = IISϵ (ASV k n ), i.e., the model of the AMAS in Example 1. Note that the Std and React semantics coincide on M, as it includes no ϵ-transitions. Clearly, M, (q1 0 , . . . , qn 0 , qc0 ) |= ∧ȷ∈Candidates ⟨⟨Voter⟩⟩F votedj.

In this paper, we focus on formulas with no next step operators X and no nested strategic modalities. The corresponding "simple" subset of ATL is denoted by sATL. The restriction is less prohibitive than it seems at a glance. First, the X operator is of little value for asynchronous systems. Secondly, nested strategic modalities would only allow us to express an agent's ability to endow another agent with ability (or deprive the other agent of ability). Such properties are sometimes relevant, but simpler properties like ⟨⟨Voter⟩⟩Fvotedj or ⟨⟨Voter⟩⟩G¬punished are usually of more interest.

2.3 AlternatingMu-Calculus

For strategies with perfect information, ATL can be embedded in a variant of µ-calculus with ⟨⟨A⟩⟩X as the basic modality and no alternation of fixpoint operators [Alur et al., 2002]. At the same time, the analogous variant of µ-calculus for imperfect information has incomparable expressive power to ATLir [Bulling and Jamroga, 2011].

Formally, alternation-free alternating µ-calculus with imperfect information (af-AEµC) takes the next-time fragment of ATLir and adds the least fixpoint operator µ. The greatest fixpoint operator ν is defined as dual to µ. Let Vars be a set of second-order variables ranging over 2St . The language of af-AEµC is defined by:

where p ∈ PV , Z ∈ Vars, a ∈ A, A ⊆ A, and the formulae are Z-positive, i.e., each free occurrence of Z is in the scope of an even number of negations. We define νZ(ϕ(Z)) ≡ ¬µZ(¬ϕ(¬Z)), where ϕ(¬Z) denotes the result of substituting in ϕ all free occurrences of Z with ¬Z. Additionally, every formula of af-AEµC in its negation normal form must contain no occurrences of ν (resp. µ) on any syntactic path from an occurrence of µZ (resp. νZ) to a bound occurrence of Z.

We evaluate the formulae of af-AEµC with respect to the valuations of Vars, i.e., functions V : Vars → 2St . We denote the set of all the valuations of Vars by Vals. If X ∈ Vars, Z ⊆ St, and V ∈ Vals, then by V[X := Z] we denote the valuation of Vars such that V[X := Z](Y ) = V(Y ) for Y ̸= X and V[X := Z](X) = Z. The denotational semantics of af-AEµC assigns to each formula ϕ the set of states [[ϕ]]MV where ϕ is true under the valuation V ∈ Vals:

• [[p]]MV = V(p),
• [[Z]]MV = V(Z),
• [[¬ϕ]]MV = St \ [[ϕ]]MV ,
• [[ϕ ∧ψ]]MV = [[ϕ]]MV ∩ [[ψ]]MV ,
• [[⟨A⟩ϕ]]MV = {q ∈ St | ∃sA ∈ ΣA ∀λ ∈ out irM (q, sA) λ[1] ∈ [[ϕ]]MV },
• [[µZ(ϕ)]]MV = ⋂{Q ⊆ St | [[ϕ]]MV[Z:=Q] ⊆ Q},

where ϕ ∈af-AEµC, p ∈ PV , Z ∈ Vars , A ⊆ A, and a ∈ A. If ϕ is a sentence, i.e., it contains no free variables, then its validity does not depend on the valuation V, and we write M, q |= ϕ instead of q ∈ [[ϕ]]MV .

3 New Fixed-Point Approximations

In multi-agent systems, the verification of properties often requires analyzing the global model, which can be computationally expensive due to the state space explosion problem. To mitigate this, we propose focusing on the local model of an agent, which is a more tractable approach. By approximating the global model from the perspective of selected agent, we can efficiently verify properties while maintaining a high degree of accuracy.

3.1 Local ApproximationModels of Ability

Definition 7 (Local Approximating Model). The local approximating model for an agent i captures the essential behavior of the agent within the context of the entire system. This model is defined as a tuple Mi = (Li, Evt i, Ri, PVi, Tappi), where Li represents the set of local states, Evti the set of events, Ri the repertoire function, PVi the set of propositions, and Tappi the transition relation. The transition relation Tappi is particularly crucial as it defines how the agent transitions between local states based on events. Additionally, to account for the potential livelock for i, we introduce an auxliary event symbol τ, such that Agents(τ ) = ∅.

In this section, we formalize the new fixpoint approximation by defining the transition relation in the local approximating model and proving its properties. We also introduce the concepts of enabled events, standard outcomes, and reactive outcomes within this model. These definitions lay the groundwork for the execution semantics of the approximated model and the subsequent model checking procedures.

By leveraging the local approximating model, we aim to provide a scalable and efficient method for verifying multiagent systems, ensuring that the verification process remains feasible even as the complexity of the system increases.

Definition 8 (Transition Relation in Local Approximating Model). The transition relation Tappi is defined as follows:

• (l, ϵ, l) ∈ Tappi if there exist g ∈ St such that gi = l and T (g, ϵ) = g.
• (l, τ, l) ∈ Tappi if there exist g1, g2, . . . , gn+1 ∈ St and α1, α2, . . . , αn ∈ Evt \ Evt i such that:
• ∀j ∈ {1, 2, . . . , n}, (gj)i = l and T(gj, αj) = gj+1,
• gn+1 = g1.

In other words, there exists a sequence of global states in the global model that starts and ends in the global state containing the local state l, with all transitions in-between labeled by events that are not in the agent i's set of events.

• (l, α, l′ ) ∈ Tappi for α ∈ Evti if there exist g1, g2, . . . , gn+1 ∈ St and α1, α2, . . . , αn ∈ Evt such that:
• ∀j ∈ {1, 2, . . . , n}, (gj)i = l and T(gj, αj) = gj+1,
• ∀j ∈ {1, 2, . . . , n - 1}, i /∈ Agent(αj),
• (gn+1)i = l′ and αn = α.

In other words, there exists a finite path fragment in the global model that runs entirely within the local state l (except possibly the last transition) and ends in a global state containing the local state l′ , with the last transition labeled by α and no other event executed by i.

The transition relation Tappi captures the essential behavior of agent i within the global model. It defines how the agent transitions between local states based on events, ensuring that the local approximating model accurately represents the agent's interactions with the system. Consistent with the standard AMAS S (Definition 1), the transition relation is characterized as a partial transition function, defined for events within the agent's repertoire of choices.

In order to talk about agent's strategies, we need to define the enabled events in the local approximating model. An event is enabled at a local state l if there exists a transition from l to another local state l′ labeled with that event. This concept is essential for defining the standard and reactive outcomes of a strategy in the local approximating model.

Definition 9 (Enabled events in Local Approximating Model). Event α ∈ Evti is enabled at state l ∈ Li in the local approximating model Mi if l α -→Mi l′ for some l′ ∈ Li, i.e., Tappi(l, α) = l′ . The set of such events is denoted by enabledMi (l).

The standard outcome captures the possible sequences of events that can be executed by the agent according to its strategy, while the reactive outcome further refines this by considering the enabled events at each local state.

Definition 10 (Standard outcome in Local Approximating Model). Let i ∈ A. The standard outcome of strategy σi ∈

Σir i in state l ∈ Li of the local approximating model Mi is the set out Std Mi (l, σi) ⊆ ΠMi (l) such that π = l0α0l1α1 · · · ∈ out Std Mi (l, σi) iff l0 = l, and for each m ≥ 0 we have that αm ∈ enabledMi (lm, σi(lm)).

Definition 11 (Reactive outcome in Local Approximating Model). Let i ∈ A. The reactive outcome of strategy σi ∈ Σir i in state l ∈ Li of the local approximating model Mi is the set out React Mi (l, σi) ⊆ out Std Mi (l, σi) such that π = l0α0l1α1 · · · ∈ out React Mi (l, σi) iff αm = lϵ for each m ≥ 0 implies enabledMi (lm, σi(lm)) = {ϵ}.

3.2 Fixpoint Approximation on Local Models

Now we can define the model checking procedure for the local approximating model. The model checking of a formula ϕ in the local approximating model Mi is performed by checking whether the formula holds for all sequences in the outcome of the agent's strategy in the initial state of the model.

Definition 12 (Model Checking Local Approximating Model). Let x ∈ {Std, React} and i ∈ A. Mi, l |=x ⟨⟨i⟩⟩ϕ iff there is a strategy σi ∈ Σir i such that for all π ∈ out xMi (l, σi) we have Mi, π |=x ϕ.

To utilize the local approximating model for verifying the formula ϕ in the original global model, we must impose certain restrictions on the set of possible formulas. Specifically, all propositions that appear in ϕ must belong to the set PVi of agent i. This requirement arises because the approximated model retains only the local states of the agent from the original model, omitting information about other agents. Consequently, we focus exclusively on singleton coalitions in our formulas. Additionally, similar to standard model checking for AMAS S, we restrict our attention to formulas that exclude next step operators X and nested strategic modalities. These constraints ensure the feasibility and accuracy of verification within the local approximating model framework.

We use the following translations of simple formulas of ATLir, that provide the lower approximation.

Definition 13 (Lower Approximation for sATL ir).

1. trL(⟨⟨i⟩⟩Fϕ) = µZ.(ϕ ∨ ⟨i⟩Z);
2. trL(⟨⟨i⟩⟩Gϕ) = νZ.(ϕ ∧ ⟨i⟩Z;
3. trL(⟨⟨i⟩⟩ψUϕ) = µZ.(ϕ ∨ (ψ ∧ ⟨i⟩Z)).

Next, we prove that, if trL(ϕ) is satisfied in the local model, then ϕ must hold in the corresponding global model.

3.3 Correctness of the Approximation

Here, we present the main theoretical results of the paper, showing that procedure proposed in Section 3 provides a lower approximation of the verification problem for ATLir. To this end, we introduce the additional concept of a partial ir-strategy, which is simply a partial function σi : Li ⇀ 2Evti with the standard constraints. The outcome of such σi is defined analogously (note that it can contain infinite as well as finite paths!). Additionally, for l ∈ Li and L ⊆ Li, we will write "g ∈ l" instead of "gi = l," and "g ∈ L" instead of "g ∈ l for some l ∈ L."

Theorem 1 (Approximation of reachability). Let x ∈ {Std, React}, i ∈ A, and l ∈ StMi . If Mi, l |=x µZ.(ϕ ∨ ⟨i⟩Z) then, for every g ∈ l, we have M, g |=x ⟨⟨i⟩⟩Fϕ.

Theorem 1 is a direct consequence of the following lemma.

Lemma 1. Let Satxn (Mi, µZ.(ϕ ∨ ⟨i⟩Z)) be the set of states in Mi, computed by the standard least fixpoint algorithm for µZ.(ϕ∨⟨i⟩Z) with at most n fixpoint iterations (equivalently: with at most n executions of the preimage operation for ⟨i⟩).

We claim that, for every n ∈ N, if L = Satxn (Mi, µZ.(ϕ ∨ ⟨i⟩Z)) then, for every g ∈ L, we have M, g |=x ⟨⟨i⟩⟩Fϕ.

Proof. Proof by induction on n.

Base Case, n = 0: If n = 0, then L = Satx0 (Mi, µZ.(ϕ ∨ ⟨i⟩Z)) contains only the states where ϕ is satisfied. Therefore, for every g ∈ StM such that gi = l ∈ L, we have M, g |=x ϕ. Hence, M, g |=x ⟨⟨i⟩⟩Fϕ.

Inductive Step: Assume that the lemma holds for some n ≥ 0. We need to show that it also holds for n + 1. Let Ln+1 = Satxn+1 (Mi, µZ.(ϕ∨⟨i⟩Z)). By the definition of the least fixpoint algorithm, Ln+1 is the set of states where either ϕ is satisfied or there exists a transition to a state in Ln. Formally, Ln+1 = {l | Mi, l |= ϕ ∨ ∃l′∈Ln (l, α, l′ ) ∈ Tappi}.

Consider any g ∈ StM such that gi = l ∈ L. We have two cases to consider:

1. Mi, l |= ϕ: In that case, M, g |=x ϕ, and henceM, g |=x ⟨⟨i⟩⟩F ϕ.

2. ∃l′∈Ln (l, α, l′ ) ∈ Tappi: By the inductive hypothesis, for every g′ ∈ StM st. g′i = l′ , we have M, g′ |=x ⟨⟨i⟩⟩Fϕ.

Since (l, α, l′ ) ∈ Tappi, there exists a corresponding set of transitions in the original model M from state g to some states g′ such that g′i = l′ . Since l′ was added in the current iteration of the least fixpoint algorithm, it means that there exists an event α ∈ Evti such that (l, α, l′ ) ∈ Tappi. Therefore, there exists a partial strategy in M for agent i to ensure that ϕ is eventually satisfied starting from state g. By following this strategy, agent i can navigate through the states in M to reach a state where ϕ holds, thus satisfying the reachability condition in the original model. Hence, M, g |=x ⟨⟨i⟩⟩Fϕ.

Formally, we proceed as follows:

(i) By the induction lemma, we obtain a partial strategy σa defined on Ln, such that for every global state g ∈ Ln and path λ ∈ outx (g, σa), the path λ is infinite and there exists an index i ∈ N such that M, λ[i] |= ϕ.

(ii) From the (n + 1)-th iteration, we derive a partial strategy σ′a defined on Ln+1 \ Ln, such that for every global state g ∈ Ln+1 \ Ln and path λ ∈ outx (g, σ′a ), the path λ is finite and last(λ) ∈ Ln.

(iii) Since σa and σ′a are defined on disjoint subsets of locations, they can be combined into a new strategy σ′′ a = σa ∪ σ′a . Consequently, every path λ′′ ∈ outx (g, σ′′ a ) is infinite and consists of the concatenation of a finite prefix λ′ ∈ outx (g, σ′a ) with an infinite path λ ∈ outx (ˆ g, σa) for some ˆ g ∈ Ln. Therefore, there must exist some index j ∈ N such that M, λ[j] |= ϕ, which completes the proof that M, g |=x ⟨⟨i⟩⟩Fϕ.

Therefore, by induction, the claim holds for all n ∈ N.

Theorem 2 (Approximation of safety). Let x ∈ {Std, React}, i ∈ A, and l ∈ StMi . If Mi, l |=x νZ.(ϕ ∧ ⟨i⟩Z) then, for every g ∈ l, we have M, g |=x ⟨⟨i⟩⟩Gϕ.

Theorem 2 is a direct consequence of Lemma 2, that uses the "bounded always" operator Gn with semantics given by:

M, g |=x ⟨⟨A⟩⟩Gnφ iff there is a strategy sA ∈ Σir A such that, for each path λ ∈ out xM (g, sA), we have M , λ[i] |=x φ for all 0 ≤ i ≥ n.

Lemma 2. Let Satxn (Mi, νZ.(ϕ ∧ ⟨i⟩Z)) be the set of states in Mi, computed by the standard greatest fixpoint algorithm for νZ.(ϕ ∧ ⟨i⟩Z) with at most n fixpoint iterations (equivalently: at most n executions of the preimage for ⟨i⟩).

We claim that, for every n ∈ N, if L = Satxn (Mi, νZ.(ϕ ∧ ⟨i⟩Z)) then, for every g ∈ L, we have M, g |=x ⟨⟨i⟩⟩Gnϕ.

Proof. Proof by induction on n.

Base Case, n = 0: If n = 0, then L = Satx0 (Mi, νZ.(ϕ ∧ ⟨i⟩Z)) contains only the states where ϕ is satisfied. Therefore, for every g ∈ StM such that gi = l ∈ L, we have M, g |=x ϕ. Hence, M, g |=x ⟨⟨i⟩⟩G0ϕ.

Inductive Step: Assume that the lemma holds for some n ≥ 0. We need to show that it also holds for n + 1.

Let Ln+1 = Satxn+1 (Mi, νZ.(ϕ ∧ ⟨i⟩Z)). By the definition of the greatest fixpoint algorithm, Ln+1 ⊆ Ln, i.e. all the states from Ln from which transition going back to Ln can't be enforced, were removed. Formally: Ln+1 = Ln \ {l | Ln, ∀α∈Ri(l)∃l′ ̸∈Ln (l, α, l′ ) ∈ Tappi} = {l | Ln, ∃α∈Ril∀l′∈Mi ((l, α, l′ ) ∈ Tappi) =⇒ l′ ∈ Ln}.

Consider any g ∈ StM such that gi = l ∈ Ln+1. We need to show that ∃α∈Ri(l)∀l′∈Mi ((l, α, l′ ) ∈ Tappi) =⇒ l′ ∈ Ln: by the inductive hypothesis, for every g′ ∈ StM such that g′i = l′ ∈ Ln, we have M, g′ |=x ⟨⟨i⟩⟩Gnϕ.

By the induction lemma, we obtain a partial strategy σa defined on Ln, such that for every global state g ∈ Ln and path λ ∈ outx (g, σa), the path λ is of length at least n and for all i ≤ n we have M, λ[i] |= ϕ.

From the (n+1)-th iteration, we derive a partial strategy σ′a defined on Ln+1, such that for every global state g ∈ Ln+1 and path λ ∈ outx (g, σ′a ), the path λ is of length at least 1 and for all i ≤ n + 1 we have λ[i] ∈ Ln+1, and thus also λ[i] |= ϕ. Since Ln+1 ⊂ Ln, we have that for all i ≤ n + 1 we have λ[i] ∈ Ln. Therefore, by the inductive hypothesis, we have M, λ[i] |= ϕ for all i ≤ n + 1. Hence, we can use σ′a to demonstrate that M, g |=x ⟨⟨i⟩⟩Gn+1ϕ.

Therefore, by induction, the claim holds for all n ∈ N.

The characterization for "until" formulas only slightly extends that of reachability (Theorem 1). We only mention the theorem and the main lemma here, as the rest of the proof is completely analogous.

Theorem 3 (Approximation of until). Let x ∈ {Std, React}, i ∈ A, and l ∈ StMi . If Mi, l |=x µZ.(ϕ∨ (ψ ∧ ⟨i⟩Z)) then, for every g ∈ l, we have M, g |=x ⟨⟨i⟩⟩ψUϕ.

Lemma 3. Let Satxn (Mi, µZ.(ϕ ∨ (ψ ∧ ⟨i⟩Z))) be the set of states in Mi, computed by the standard least fixpoint algorithm for µZ.(ϕ ∨ (ψ ∧ ⟨i⟩Z)) with at most n fixpoint iterations (equivalently: with at most n executions of the preimage operation for ⟨i⟩).

We claim that, for every n ∈ N, if L = Satxn (Mi, µZ.(ϕ ∨ (ψ ∧ ⟨i⟩Z)) then, for every g ∈ L, we have M, g |=x ⟨⟨i⟩⟩ψ U ϕ.

4 Experimental Evaluation

In this section we evaluate the proposed method on the asynchronous simple voting protocol of [Jamroga et al., 2020a].

4.1 Verification

We conducted two sets of experiments to evaluate the performance of our approach. The first set focused on the standard Asynchronous Simple Voting model, while the second set examined the same model with the addition of revoting. In the experiments, we compared the verification time of fixpoint approximation on local approximation models vs. the performance of the fixpoint approximation on standard global model, implemented in the state-of-art model checker STV [Kurpiewski et al., 2024], that operates on explicit representation of global states. We used STV due to its applicability to ATLir (i.e., imperfect information strategies), unlike most other model checkers, such as MCMAS and PRISM-GAMES, that focus on perfect-information strategies. The results (discussed further) show astonishing gains. One may notice, however, that in order to run the approximate verification, we should first generate the local approximating model. The code for the experiments is available at https://tinyurl.com/sup7888.

4.2 Generating ApproximatedModels

The naive approach would be to generate the full global model, and then project it to local states and transitions of a given agent a. To avoid this, we tried a smarter procedure, that translates the existence of a sequence of transitions between two locations l, l′ into a CTL verification problem, and runs a dedicated CTL model checker to get the answer. For the experiments, we employed the UPPAAL model checker as a sub-routine to generate the approximated local model, which was then used with the STV model checker for verification of strategic ability [Behrmann et al., 2004].

All calls to UPPAAL were managed by an auxiliary script that reads the model specification (provided in .xta format with event labels assigned to edges) and constructs a corresponding pair of model and query in a BFS manner, starting from the initial local state. For every candidate triplet (s, α, s′ )-composed of source local state s, event label α, and target local state s′-the script processes the model.

In the study, each event available to the given agent is associated with an auxiliary Boolean variable, which evaluates to true only when that event was the last to occur at a current (global) state. For each source local state, every outgoing edge with the given event label is duplicated with an additional guard (matching the valuation from the source local state) and update assignments (matching the last occurred event). Fragments outside of the potential predecessors are truncated, and remaining edges are appended with the opposing update assignment. To enforce progressive semantics, all locations are set to the committed type.

The obtained model is then queried for the reachability of the target local state counterpart, with the auxiliary variable from the last occurred event matching the one from the triplet. Next, the computed local states are verified for livelocks [Ashcroft, 1975]-the existence of a cycle of global states and events that neither leads to a change in the given local state nor involves events from the studied agent's repertoire-using the original model specification.

The straightforward application of UPPAAL for generating the approximated local model was inefficient. When the query with the triplet has no counterpart in the global model, the verifier needs to generate the entire state space to conclude that. However, we implemented several optimizations to improve efficiency. Firstly, we noted the symmetry within the homogeneous modules of voters; none of the voters have transitive interactions with each other-they only interact with the coercer. This semantic analysis allowed us to conclude that the order in which different voters perform their actions does not affect the composition of their local models. Consequently, we enhanced the generation of the local model by using UPPAAL's specific process priority feature, assigning the given voter the highest priority among all other voters, and adding an edge connecting the target local state with an auxiliary sink location, which has a single self-loop.

4.3 Results

The results of the experiments are summarized in Tables 1 and 2. The first column indicates the number of voters considered. In all scenarios, there were two candidates and one coercer. The tables present the model generation times for the standard global model and two approximated models: one without optimizations (standard) and one with optimizations (optimized) in UPPAAL. Verification was performed using a fixpoint algorithm, and the verified formula was ϕ1 = ⟨⟨V oter1⟩⟩F (vote1,1∧¬give1). The approximated model was generated for agent V oter1. All times are reported in seconds, with a timeout set to two hours.

All experiments were conducted on a machine equipped with a 3.0 GHz 8-core AMD Ryzen 7 5700X3D CPU and 64 GB of RAM. The model generation and verification times were measured using the time command in a Linux environment to ensure precise and consistent timing measurements.

As observed, the model generation times for few voters are lower for the global model compared to the approximate models. However, this trend reverses as the number of voters increases. The optimized version of the approximate model is consistently faster than the standard version, although its time still increases exponentially for the model without revoting. In the scenario with revoting, the optimized approach exhibits linear time growth, allowing us to generate a model for even 50 voters in under one minute. The verification time for the global model also increases exponentially, whereas the verification time for the approximate model remains constant. This is because the size of the approximated model does not change, as the local model of the voter remains the same regardless of the number of voters in the system.

Interestingly, the optimized version yields a more substantial reduction in model generation time for the case with revoting. Without revoting, the exponential growth in time can be mainly attributed to the detection of potential livelocks. In the absence of a witnessing livelock cycle, the model checker must generate the entire fragment of the source local state's predecessor states to reach a conclusion.

Note that in both the straightforward and optimized versions, there is room for further improvement in efficiency through parallel computation of the reachable successors from the already discovered states of the local model. This would allow more efficient generation of the approximated model, especially for larger numbers of voters.

5 Conclusions

The model checking problem for ATLir is indeed challenging. Nevertheless, some feasible approaches for tackling this problem exist. We have taken the first step in optimizing fixpoint approximations, by focusing on the local model of the agent whose strategic abilities we aim to verify. In consequence, the verified model grows much slower, and in some cases might even remain constant, regardless of the number of agents in the scenario. Consequently, the verification time also decreases. However, the approximate model needs to be generated. We have shown that existing tools like UPPAAL can be used for this task, and with proper optimizations, the generation times for the approximated model can increase linearly rather than exponentially.

The present method has several limitations: observable safety/reachability goals, only individual strategies, no nesting of strategic modalities. They arise from technical feasibility (e.g., scalability and semantic alignment with experiments), rather than theoretical constraints. Our experiments show very promising results, and we plan to extend the method to handle general non-observable properties, proper coalitions, and nested strategic reasoning in future work.

Acknowledgments

The work has been supported by NCBR Poland and FNR Luxembourg under the PolLux/FNR-CORE project SpaceVote (POLLUX-XI/14/SpaceVote/2023 and C22/IS/17232062/SpaceVote). For the purpose of open access, and in fulfilment of the grant agreement, the authors have applied CC BY 4.0 license to any Author Accepted Manuscript version arising from this submission.