key: cord-0124250-k405380h
authors: Jamroga, Wojciech; Penczek, Wojciech; Sidoruk, Teofil
title: Strategic Abilities of Asynchronous Agents: Semantic Side Effects and How to Tame Them
date: 2020-03-08
journal: nan
DOI: nan
sha: 90df4271138665ad69af00addbc3ce22689dc57f
doc_id: 124250
cord_uid: k405380h

Recently, we have proposed a framework for verification of agents' abilities in asynchronous multi-agent systems, together with an algorithm for automated reduction of models. The semantics was built on the modeling tradition of distributed systems. As we show here, this can sometimes lead to counterintuitive interpretation of formulas when reasoning about the outcome of strategies. First, the semantics disregards finite paths, and thus yields unnatural evaluation of strategies with deadlocks. Secondly, the semantic representations do not allow to capture the asymmetry between proactive agents and the recipients of their choices. We propose how to avoid the problems by a suitable extension of the representations and change of the execution semantics for asynchronous MAS. We also prove that the model reduction scheme still works in the modified framework.

Modal logics of strategic ability. Alternating-time temporal logic ATL * (Alur, Henzinger, and Kupferman 1997; Alur, Henzinger, and Kupferman 2002; Schobbens 2004 ) is probably the most popular logic to describe interaction of agents in multi-agent systems. Formulas of ATL * allow to express statements about what agents (or groups of agents) can achieve. For example, taxi G ¬fatality says that the autonomous cab can drive in such a way that nobody is ever killed, and taxi, passg F destination expresses that the cab and the passenger have a joint strategy to arrive at the destination, no matter what any other agents do. Such statements allow to express important functionality and safety requirements in a simple and intuitive way. Moreover, the provide input to algorithms and tools for verification of strategic abilities, that have been in constant development for over 20 years Alur et al. 2001 ; Kacprzak and Penczek 2004; Lomuscio and Raimondi 2006; Chen et al. 2013; Busard et al. 2014; Pilecki, Bednarczyk, and Jamroga 2014; Huang and van der Meyden 2014; Cermák et al. 2014; Lomuscio, Qu, and Raimondi 2017; Cermák, Lomuscio, and Murano 2015; Belardinelli et al. 2017b; Belardinelli et al. 2017a; Jamroga et al. 2019; Kurpiewski, Jamroga, and Knapik 2019; Kurpiewski et al. 2021) . Still, there are two caveats.

First, all the realistic scenarios of agent interaction, that one may want to specify and verify, involve imperfect information. That is, the agents in the system do not always know exactly the global state of the system, and thus they have to make their decisions based on their local view of the situation. Unfortunately, verification of agents with imperfect information is hard to very hard -more precisely, ∆ P 2 -complete to undecidable, depending on the syntactic and semantic variant of the logic (Schobbens 2004; Guelev, Dima, and Enea 2011; Dima and Tiplea 2011) .

Also, the imperfect information semantics of ATL * does not admit alternation-free fixpoint characterizations (Bulling and Jamroga 2011; Dima, Maubert, and Pinchinat 2014; Dima, Maubert, and Pinchinat 2015) , which makes incremental synthesis of strategies impossible, or at least difficult to achieve (Pilecki, Bednarczyk, and Jamroga 2014; Busard et al. 2014;  Huang and van der Meyden 2014; Busard et al. 2015; Jamroga, Knapik, and Kurpiewski 2017) .

Secondly, the semantics of strategic logics is traditionally based on synchronous concurrent game models. In other words, one implicitly assumes the existence of a global clock that triggers subsequent global events in the system; at each tick of the clock, all the agents choose their actions, and the system proceeds accordingly with a global transition. However, many real-life systems are inherently asynchronous, and do not operate on a global clock that perfectly synchronizes the atomic steps of all the components. Moreover, many systems that are synchronous at the implementation level can be more conveniently modeled as asynchronous on a more abstract level. In many scenarios, both aspects combine. For example, when modeling an antipoaching operation (Fang et al. 2017) , one may take into account the truly asynchronous nature of events happening in different national parks, but also the best level of granularity for modeling the events happening within a single nature reserve.

Asynchronous semantics and partial-order reduction.

We have recently proposed how to adapt the semantics of ATL * to asynchronous MAS (Jamroga et al. 2018) . We also showed that the technique of partial order reduction (POR) (Peled 1993; Peled 1994; Peled 1996; Godefroid and Wolper 1994; Gerth et al. 1999; Lomuscio, Penczek, and Qu 2010a; Lomuscio, Penczek, and Qu 2010b) can be adapted to verification of strategic abilities in asynchronous MAS. In fact, the (almost 30 years old) POR for linear time logic LTL can be taken off the shelf and applied to a significant part of ATL * ir , the variant of ATL * based on strategies with imperfect information and imperfect recall. This is very important, as the practical verification of asynchronous systems is often impossible due to the stateand transition-space explosion resulting from interleaving of local transitions. POR allows for a significant, sometimes even exponential, reduction of the models. Semantic side effects.

While the result is appealing, there is a sting in its tail: the ATL * semantics in (Jamroga et al. 2018) leads to counterintuitive interpretation of strategic properties. First, it disregards finite paths, and evaluates some intuitively losing strategies as winning (and vice versa). Secondly, it provides a flawed interpretation of the concurrency fairness assumption. Thirdly, the representations and their execution semantics do not allow to capture the asymmetry between the agents that control which synchronization branch will be taken, and those influenced by their choices. We tentatively indicated some of the problems in the extended abstract (Jamroga, Penczek, and Sidoruk 2021) . In this paper, we demonstrate them carefully, and propose how they can be avoided. Contribution. Our contribution is threefold. First, we discuss in detail the semantic side effects of adding strategic reasoning on top of classical models of concurrent systems (Priese 1983). We identify the reasons, and demonstrate the problematic phenomena on simple examples. Secondly, we show how to avoid these pitfalls by extending the class of representations and slightly changing the execution semantics of strategies. Specifically, we add "silent" ǫ-transitions in the models and on outcome paths of strategies, and allow for nondeterministic choices in the agents' repertoires. We also identify a family of fairness-style conditions, suitable for the interaction of proactive and reactive agents. No less importantly, we prove that partial order reduction is still correct in the modified framework. Motivation. The variant of ATL * for asynchronous systems in (Jamroga et al. 2018) was proposed mainly as a framework for formal verification. This was backed by the results showing that it submits to partial order reduction. However, a verification framework is only useful if it allows to specify requirements in an intuitive way, so that the property we think we are verifying is indeed the one being verified. In this paper, we show that this was not the case. We also propose how to overcome the problems without spoiling the efficient reduction scheme. The solutions are not merely technical. In fact, they lead to a better understanding of how strategic activity influences the overall behavior of the system, and how it should be integrated with the traditional models of asynchronous interaction.

We first recall the models of asynchronous interaction in MAS, proposed in (Jamroga et al. 2018) and inspired by (Priese 1983; Fagin et al. 1995; Lomuscio, Penczek, and Qu 2010b) .

In logical approaches to MAS, one usually assumes synchronous actions of all the agents (Alur, Henzinger, and Kupferman 2002; Schobbens 2004) .

However, many agent systems are inherently asynchronous, or it is useful to model them without assuming precise timing relationships between the actions of different agents.

As an example, consider a team of logistic robots running in a factory (Schlingloff, Stubert, and Jamroga 2016) . Often no global clock is available to all the robots, and even if there is one, the precise relative timing for robots operating in different places is usually irrelevant.

Such a system can be conveniently represented with a set of automata that execute asynchronously by interleaving local transitions, and synchronize their moves whenever a shared event occurs. The idea is to represent the behavior of each agent by a finite automaton where the nodes and transitions correspond, respectively, to the agent's local states and the events in which it can take part. Then, the global behavior of the system is obtained by the interleaving of local transitions, assuming that, in order for a shared event to occur, all the corresponding agents must execute it in their automata. This motivates the following definition. Definition 2.1 (Asynchronous MAS). An asynchronous multi-agent system (AMAS) S consists of n agents

. . , l ni i }, an initial state ι i ∈ L i , and a set of events Evt i = {α 1 i , α 2 i , . . . , α mi i }. An agent's repertoire of choices 2 R i : L i → 2 Evt i \ {∅} selects the events available at each local state.

That is, T i (l, α) indicates the result of executing event α in local state l from the perspective of agent i.

Let Evt = i∈Agt Evt i be the set of all events, and Loc = i∈Agt L i be the set of all local states in the system. For each event α ∈ Evt , Agent(α) = {i ∈ Agt | α ∈ Evt i } is the set of agents which have α in their repertoires; events shared by multiple agents are jointly executed by all of them. We assume that each agent i in the AMAS is endowed with a disjoint set of its local propositions PV i , and their valuation V i : L i → 2 PVi . The overall set of propositions PV = i∈Agt PV i collects all the local propositions. As our working example, we use the following scenario. 

To understand the interaction between asynchronous agents, we use the standard execution semantics from concurrency models, i.e., interleaving with synchronization on shared events. To this end, we compose the network of local automata (i.e., AMAS) to a single automaton based on the notions of global states and global transitions, see below.

Definition 2.3 (Model). Let S be an AMAS with n agents. Its model IIS(S) extends S with: (i) the set of global states St ⊆ L 1 × . . . × L n , including the initial state ι = (ι 1 , . . . , ι n ) and all the states reachable from ι by T (see below); (ii) the global transition function T :

Models, sometimes called interleaved interpreted systems (IIS), are used to provide an execution semantics to AMAS, and consequently provide us with semantic structures to reason about AMAS. Intuitively, the global states in IIS(S) can be seen as the possible configurations of local states of all the agents. Moreover, the transitions are labeled by events that are simultaneously selected (in the current configuration) by all the agents that have the event in their repertoire. Clearly, private events (i.e., events such that Agent(α) is a singleton) require no synchronization.

Example 2.4 (Conference). The model for the asynchronous MAS of Example 2.2 is shown in Figure 1 .

We say that event α ∈ Evt is enabled at g ∈ St if T (g, α) = g ′ for some g ′ ∈ St. The set of events enabled at g is denoted by enabled(g). The global transition function is assumed to be serial, i.e., at each g ∈ St there exists at least one enabled event.

Discussion. This modeling approach is standard in theory of concurrent systems, where it dates back to the early 1980s and the idea of APA Nets (asynchronous, parallel automata nets) (Priese 1983). Note that APA Nets and their models were not proposed with causal interpretation in mind. In particular, they were not meant to capture the interaction of purposeful agents that freely choose their strategies, but rather a set of reactive components converging to a joint behavior. Despite superficial differences, the same applies to process-algebraic approaches to concurrency, such as CSP (Hoare 1978) , CCS (Milner 1980) , ACP (Bergstra and Klop 1985) , and πcalculus (Milner, Parrow, and Walker 1992) .

Definition 2.1 extends that with the repertoire functions from synchronous models of MAS (Lomuscio, van der Meyden, and Ryan 2000; Alur, Henzinger, and Kupferman 2002) . Agent i's repertoire lists the events available to i, and is supposed to define the space of i's strategies. As we show further, this is not enough in case of asynchronous MAS.

Alternating-time temporal logic ATL * (Alur, Henzinger, and Kupferman 1997; Alur, Henzinger, and Kupferman 2002; Schobbens 2004) generalizes the branching-time temporal logic CTL * (Clarke and Emerson 1981) by replacing the path quantifiers E, A with strategic modalities A γ, expressing that agents A can enforce the temporal property γ. While the semantics of ATL * is typically defined for models of synchronous systems, a variant for asynchronous MAS was proposed recently (Jamroga et al. 2018) . We summarize the main points in this section.

Let PV be a set of propositional variables and Agt the set of all agents. The language of ATL * is defined as below.

ϕ :

where p ∈ PV, A ⊆ Agt, X stands for "next", and U for "strong until" (γ 1 U γ 2 denotes that γ 1 holds until γ 2 becomes true). The other Boolean operators and constants are defined as usual. "Release" can be defined as γ 1 R γ 2 ≡ ¬((¬γ 1 ) U (¬γ 2 )). "Eventually" and "always" can be defined as F γ ≡ true U γ and G γ ≡ false R γ. Moreover, the CTL * operator "for all paths" can be defined as Aγ ≡ ∅ γ. Example 3.1 (Conference). Formula sc F open expresses that the Steering Chair can enforce that the conference is eventually opened. Moreover, formula gc, oc G ¬epid says that the General Chair and the Organizing Chair have a joint strategy to avoid high epidemiological risk.

We adopt Schobbens' taxonomy and notation for strategy types (Schobbens 2004) : ir, Ir, iR, and IR, where I (resp. i) denotes perfect (resp. imperfect) information, and R (resp. r) denotes perfect (resp. imperfect) recall. In particular, an imperfect information/imperfect recall strategy (ir-strategy) for i is a function σ i :

We denote the set of such strategies by Σ ir i . A collective strategy σ A for a coalition A = (1, . . . , m) ⊆ Agt is a tuple of strategies, one per agent i ∈ A. The set of A's collective ir strategies is denoted by Σ ir A . We will sometimes use σ A (g) = (σ a1 (g), . . . , σ am (g)) to denote the tuple of A's selections at state g.

Example 3.2 (Conference). A collective strategy for the General Chair and the OC Chair in the conference scenario is shown in Figure 1 .

An infinite sequence of global states and events π =

. is the sequence of events in π, and π[i] = g i is the i-th global state of π. Π M (g) denotes the set of all paths in model M starting at g. Intuitively, the outcome of σ A in g is the set of all the paths that can occur when the agents in A follow σ A and the agents in Agt \ A freely choose events from their repertoires. To define it formally, we first refine the concept of an enabled event, taking into account the choices of A in strategy σ A . Definition 3.3 (Enabled events). Let A = (1, . . . , m), g ∈ St, and let − → α A = (α 1 , . . . , α m ) be a tuple of events such that every α i ∈ R i (g i ). That is, every α i can be selected by its respective agent i at state g. We say that event β ∈ Evt is enabled by −

Thus, β is enabled by − → α A if all the agents that "own" β can choose β for execution, even when − → α A has been selected by the coalition A. We denote the set of such events by

Example 3.4 (Conference). Consider state g = 000 and the choices of agents A = {gc, oc} shown in Figure 1 , i.e., − → α A = (proceed, online). The only events enabled by − → α A are proceed and giveup. Event onsite is not enabled because A chose different events for execution; online is not enabled because it requires synchronization which is impossible at 000. Definition 3.5 (Outcome paths). The outcome of strategy

One often wants to look only at paths that do not consistently ignore agents whose choice is always enabled. Formally, a path π satisfies concurrency-fairness (CF) if there is no event α enabled in all states of π from π[n] on and such that for every α i actually executed in π[i], i = n, n + 1, . . . , we have Agent(α) ∩ Agent(α i ) = ∅. We denote the set of all such paths starting at g by Π CF M (g).

The semantics of ATL * ir in AMAS is defined by the following clause for strategic modalities (Jamroga et al. 2018) :

The clauses for Boolean and temporal operators are standard. Moreover, the concurrency-fair semantics |= CF ir of ATL and ATL * is obtained by replacing out M (g, σ A ) with out CF M (g, σ A ) in the above clause. Example 3.7 (Conference). Clearly, formula gc, oc G ¬epid holds in (M conf , 000), in both |= ir and |= CF ir semantics. To see that, fix σ gc (0) = proceed and σ gc (1) = σ oc (0) = online in the collective strategy of {gc, oc}. Note also that M conf , 000 |= ir ¬ gc, oc F closed because, after executing proceed and online (or onsite), event rest may be selected forever.

On the other hand, such paths are not concurrency-fair, and thus M conf , 000 |= CF ir gc, oc F closed.

Discussion. Strategic play assumes proactive attitude: the agents in A are free to choose any available strategy σ A . This is conceptually consistent with the notion of agency (Bratman 1987) . At the same time, it is somewhat at odds with the standard semantics of concurrent processes, where the components cannot stubbornly refuse to synchronize if that is the only way to proceed with a transition. This seems a minor problem, but it is worrying that a strategy can have the empty set of outcomes, and equally worrying that such strategies are treated differently from the other ones. Indeed, as we will show in the subsequent sections, the semantics proposed in (Jamroga et al. 2018) leads to a counterintuitive interpretation of strategic formulas. Example 4.1 (Conference). Recall the 3-agent AMAS of Figure 1 , together with its model M conf (Figure 2 ). Clearly, M conf has no deadlock states. Let us now look at the collective strategies of coalition {gc, oc}, with agent sc serving as the opponent. It is easy to see that the coalition has no way to prevent the opening of the conference, i.e., it cannot prevent the system from reaching state 101. However, the strategy depicted in Figure 1 produces only one infinite path: (000 giveup 002 giveup . . . ). Since the ATL * semantics in Section 3 disregards finite paths, we get that M conf , 000 |= gc, oc G ¬open, which is counterintuitive.

Things can get even trickier. In particular, the outcome of a strategy can be empty -in fact, it may even happen that a coalition has only strategies with empty outcomes. Example 4.2 (Voting). Consider the AMAS in Figure 3 that depicts a simple voting scenario. A voter v can fill in an electronic ballot with a vote for candidate a or b, and then push the send button. The Electronic Ballot Machine ebm duly registers the choices of the voter. Note that all the joint strategies of {v, ebm} produce only finite sequences of transitions. This is because ebm must choose a single event at location 0 in a memoryless strategy, and thus v and ebm are bound to "miscoordinate" either at the first or at the second step. Since finite paths are not included in the outcome sets, and the semantics in Section 3.3 rules out strategies with empty outcomes, we get that IIS(S vote ), 00 |= ¬ v, ebm F ⊤, which is quite strange. Notice that removing the non-emptiness requirement from the semantic clause in Section 3.3 does not help. In that case, any joint strategy of {v, ebm} could be used to demonstrate that v, ebm G ⊥.

To deal with the problem, we augment the model of the system with special "silent" transitions, labeled by ǫ, that are fired whenever no "real" transition can occur. In our case, the ǫ-transitions account for the possibility that some agents miscoordinate and thus block the system. Moreover, we redefine the outcome set of a strategy so that an ǫ-transition is taken whenever such miscoordination occurs. In other words, "silent" loops are added in the states where a combination of the agents' actions can block the system.

Paths are defined as in Section 2.2. The following is trivial.

Proposition 4.4. For any AMAS S, any state g ∈ IIS ǫ (S), and any strategy σ A , we have that enabled IIS ǫ (S) (g, σ A (state)) = ∅. For the strategy in Example 4.1, notice that its outcome in M ǫ conf contains two infinite paths: not only (000 giveup 002 giveup 002 . . .), but also (000 proceed 101 ǫ 101 . . .). Since the latter path invalidates the temporal formula G ¬open, we get that M conf , 000 |= gc, oc G ¬open, as expected.

Example 4.6 (Voting). The undeadlocked model for the voting scenario is presented in Figure 4 . Note that formula ¬ v, ebm F ⊤ does not hold anymore, because the joint strategies of {v, ebm} have nonempty outcomes in IIS ǫ (S vote ). On the other hand, the formula v F voted a (and even v, ebm F voted a ) does not hold, which is contrary to the intuition behind the modeling. We will come back to this issue in Section 7.

Discussion. Adding "silent" transitions to account for the control flow when no observable event occurs is pretty standard. The crucial issue is where to add them. Here, we add the ǫ-transitions whenever a subset of agents might choose to miscoordinate (and stick to their choices). Again, this is in line with the notion of agency and strategic play in MAS (Bratman 1987; Pauly 2001b ). In the next section, we will discuss a concept of "agent fairness" where the addition of ǫ-transitions is constrained by the assumption that only a given subset of agents is fully proactive.

The examples used in this section expose an important feature of agent systems. The execution semantics of concurrent processes is often defined by a state-transition graph (or, alternatively, by the tree of paths generated by the graph, i.e., the tree unfolding of the graph). For systems that involve proactive agents, this is not enough. Rather, the execution semantics should map from the possible coalitions and their available strategies to the outcome sets of those strategies. In this sense, the possible behaviors of an agent system should be understood via the set of possible execution trees, rather than a single tree. This is consistent with the theoretical model of MAS in (Goranko and Jamroga 2015) , based on path effectivity functions.

An alternative way out of the problem is to include finite maximal paths in the outcomes of strategies. However, the interpretation of strategic modalities over finite paths is rather nonstandard (Belardinelli et al. 2018) and may pose new problems in the asynchronous setting. Moreover, our approach allows to reuse the existing techniques and tools, which are typically built for infinite path semantics, including the verification and partial order reduction functionalities of tools like SPIN (Holzmann 1997) and STV (Kurpiewski et al. 2021) . In general, this is a design dilemma between changing the logical semantics of the formulas vs. updating the execution semantics of the representations. Here, we choose the latter approach.

The solution proposed in Section 4.2 is based on the assumption that an agent is free to choose any event in its repertoire -even one that prevents the system from executing anything. The downside is that, for most systems, only safety goals can be achieved (i.e., properties specified by A G ϕ). For reachability, there is often a combination of the opponents' choices that blocks the execution early on, and prevents the coalition from reaching their goal. In this section, we define a fairness-style condition that constrains the choices of more "reactive" opponents. We also show a construction to verify the abilities of the coalition over the resulting paths in a technically simpler way.

Given a strategy σ A , the agents in A are by definition assumed to be proactive. Below, we propose an execution semantics for σ A which assumes that A cannot be stalled forever by miscoordination on the part of the opponents. Definition 5.1 (Opponent-reactiveness). A path π = g 0 α 0 g 1 α 1 g 2 . . . in IIS ǫ (S) is opponent-reactive for strategy σ A iff we have that α n = ǫ implies enabled(g n , σ A (g n )) = {ǫ}. In other words, whenever the agents outside A have a way to proceed, they must proceed. The reactive outcome (or React-outcome) of σ A in g, denoted out React (g, σ A ), is the restriction of out(g, σ A ) to its opponent-reactive paths. On the other hand, consider coalition {gc, sc}, and the following strategy of theirs: σ gc (0) = proceed, σ gc (1) = onsite, σ sc (0) = proceed. The same path is not opponentreactive for the strategy because the only opponent (oc) has a response at state 101 that enables a "real" transition (onsite). Proposition 5.3. In out React IIS ǫ (S) (g, σ A ), the only possible occurrence of ǫ is as an infinite sequence of ǫ-transitions following a finite prefix of "real" transitions.

Proof. Take any π = g 0 α 0 g 1 α 1 g 2 · · · ∈ out React IIS ǫ (S) (g, σ A ) such that ǫ occurs on π, and let i be the first position on π st. α i = ǫ. By Definition 5.1, we get that enabled(g i , σ A (g i )) = {ǫ}. Moreover, state i+1 = g i , so also enabled(g i+1 , σ A (g i+1 )) = {ǫ}. Thus, α i+1 = ǫ. It follows by simple induction that α j = ǫ for every j ≥ i.

The opponent-reactive semantics |= React ir of ATL * is obtained by replacing out M (g, σ A ) with out React M (g, σ A ) in the semantic clause presented in Section 3.3.

If we adopt the assumption of opponent-reactiveness for coalition A, there is an alternative, technically simpler way to obtain the same semantics of strategic ability as in Section 4.2. The idea is to introduce the "silent" transitions already at the level of the AMAS.

In other words, we add a module with a single local state and a "silent" loop labeled by ǫ, as in Figure 5 . We will denote the undeadlocked variant of S by S ǫ . Note that S ǫ can be seen as a special case of AMAS. Thus, the outcome sets and reactive outcomes of strategies in IIS(S ǫ ) are defined exactly as before.

Example 5.5 (Voting). The undeadlocked AMAS ASV ǫ 1,2 is obtained by augmenting ASV 1,2 with the auxiliary agent in Figure 5 . Obviously, the extra agent adds ǫ-loops to the model of S, i.e., to IIS(S). We show now that, under the assumption of opponent-reactiveness, the view of A's strategic ability in the undeadlocked AMAS S ǫ corresponds precisely to A's abilities in the undeadlocked model of the original AMAS S, i.e., IIS ǫ (S). This allows to deal with deadlocks and finite paths without redefining the execution semantics for AMAS, set in Definition 2.3, and thus use the existing tools such as SPIN (Holzmann 1997 ) in a straightforward way. Proposition 5.6. Let A ⊆ Agt. In out React IIS(S ǫ ) (g, σ A ), the only possible occurrence of ǫ is as an infinite suffix of ǫtransitions.

Proof. Analogous to Proposition 5.3.

Theorem 5.7. For every strategy σ A in S, we have that

Suppose that π includes ǫtransitions, with α i being the first one. Then, we have that α j = ǫ and α j ∈ enabled IIS ǫ (S) (g j , σ A (g j )) for every j < i, hence also α j ∈ enabled IIS(S) (g j , σ A (g j )) ⊆ enabled IIS(S ǫ ) (g j , σ A (g j )). (*) By Proposition 5.3, g j = g i and α j = ǫ for every j ≥ i. By Definition 5.1, enabled IIS ǫ (S) (g j , σ A (g j )) = {ǫ}.

Hence, enabled IIS(S) (g j , σ A (g j )) = ∅ and enabled IIS(S ǫ ) (g j , σ A (g j )) = {ǫ}. (**) Thus, by (*) and (**), π ∈ out React

: Analogous, with Proposition 5.6 used instead of Proposition 5.3.

Discussion. Opponent-reactiveness is to strategic properties what fairness conditions are to temporal properties of asynchronous systems. If an important property cannot be satisfied in all possible executions, it may at least hold under some reasonable assumptions about which events can be selected by whom in response to what. Clearly, the condition can be considered intuitive by some and problematic by others. The main point is, unlike in the previous semantics, now it is made explicit, and can be adopted or rejected depending on the intuition. Note that the semantic extensions proposed in this paper (silent transitions and nondeterministic choices for strategies) make sense both with and without opponent-reactiveness.

Note that, under the reactiveness assumption, we have that M ǫ conf , 000 |= React ir gc, sc F epid and M ǫ conf , 000 |= React ir oc G ¬epid. This seems to contradict the commonly accepted requirement of regularity in games (Pauly 2001a) . However, the contradiction is only superficial, as the two formulas are evaluated under different execution assumptions: for the former, we assume agent oc to be reactive, whereas the latter assumes gc and sc to react to the strategy of oc.

In Def. 3.6, we recalled the notion of concurrency-fair outcome of (Jamroga et al. 2018) . The idea was to remove from out(g, σ A ) the paths that consistently ignore agents whose events are enabled at the level of the whole model. Unfortunately, the definition has unwelcome side effects, too.

We first show that, contrary to intuition, Definition 3.6 automatically disregards deadlock paths, i.e., paths with finitely many "real" transitions.

Proposition 6.1. Consider an AMAS S and a path π in IIS ǫ (S) such that, from some point i on, π includes only ǫ-transitions. Then, for every strategy σ A in S, we have that π / ∈ out CF IIS ǫ (S) (g, σ A ).

Proof. Take π as above, i.e., π = g 0 α 0 g 1 α 1 . . . g i ǫg i ǫg i . . . . Since the transition function in IIS ǫ (S) is serial, there must be some event β = ǫ enabled in g i . In consequence, β is always enabled from i on, but none of its "owners" in Agent(β) executes an event on π after i. Hence, π does not satisfy CF, and does not belong to out CF IIS ǫ (S) (g, σ A ) for any strategy σ A .

Thus, the CF condition eliminates all the deadlock paths from the outcome of a strategy (for instance, the path (000 proceed 101 ǫ 101 . . .) in Example 4.5). In consequence, reasoning about concurrency-fair paths suffers from the problems that we identified in Section 4.1, even for undeadlocked models. Moreover, combining the temporal and strategic fairness (i.e., CF and React) collapses the undeadlocked execution semantics altogether, see below.

Proposition 6.2. Reasoning about reactive and fair outcomes in an undeadlocked model reduces to reasoning about the fair executions in the original model without ǫ-transitions. Formally, let out React,CF

. For any AMAS S and any strategy σ A in S, we have:

Proof. Clearly, we have out CF IIS(S) (g, σ A ) ⊆ out React,CF IIS ǫ (S) (g, σ A ), since out React,CF IIS ǫ (S) (g, σ A ) can only add to out CF IIS(S) (g, σ A ) new paths that include ǫ-transitions. For the other direction, take any π ∈ out React,CF IIS ǫ (S) (g, σ A ), and suppose that it contains an ǫ-transition. By Proposition 5.3, it must have an infinite suffix consisting only of ǫ-transitions. Then, by Proposition 6.1, π / ∈ out CF IIS ǫ (S) (g, σ A ), which leads to a contradiction. Thus, π contains only transitions from IIS(S), and hence π ∈ out CF IIS(S) (g, σ A ), QED.

So, how should fair paths be properly defined for strategic reasoning? The answer is simple: in relation to the outcome of the strategy being executed.

Definition 6.3 (Strategic CF). π = g 0 α 0 g 1 α 1 g 2 . . . is a concurrency-fair path for strategy σ A and state g iff g 0 = g, and there is no event α s.t., for some n and all i ≥ n, we have α ∈ enabled(π[i], σ A (π[i])) and Agent(α) ∩ Agent(α i ) = ∅. That is, agents with an event always enabled by σ A cannot be ignored forever.

The following formal results show that SCF does not suffer from the problems demonstrated in Section 6.1.

Proposition 6.4. There is an AMAS S, a strategy σ A in S, and a deadlock path π in IIS ǫ (S) such that π is concurrency-fair for σ A .

Proof. To demonstrate the property, it suffices to take the AMAS and the strategy of {gc, oc} depicted in Figure 1 , and the path π = (000 proceed 101 ǫ 101 . . .).

Theorem 6.5. Opponent-reactiveness and strategic concurrency-fairness are incomparable. Formally, there exists an AMAS S, a state g in IIS ǫ (S), and a strategy σ A such that out SCF IIS ǫ (S) (g, σ A ) ⊆ out React IIS ǫ (S) (g, σ A ), and vice versa.

Proof. Consider the undeadlocked model M ǫ conf in Example 4.5, and the strategy discussed in Example 5.2: σ gc (0) = proceed, σ gc (1) = onsite, σ sc (0) = proceed. Let π 1 = (000 proceed 101 ǫ 101 onsite 211 rest 211 handle 211 rest 211 . . . ). We have π 1 ∈ out SCF M ǫ conf (g, σ A ), but π 1 / ∈ out React M ǫ conf (g, σ A ). On the other hand, for path π 2 = (000 proceed 101 onsite 211 rest 211 rest . . . ), we have that π 2 / ∈ out SCF M ǫ conf (g, σ A ), but π 2 ∈ out React M ǫ conf (g, σ A ).

Discussion. Theorem 6.5 suggests that reactiveness and fairness conditions arise from orthogonal concerns. The two concepts refer to different factors that influence which sequences of events can occur. Opponent-reactiveness constrains the choices that (a subset of) the agents can select. Concurrency-fairness and its strategic variant restrict the way in which the "scheduler" (Nature, Chance, God...) can choose from the events selected by the agents.

Now, we point out that AMAS are too restricted to model the strategic aspects of asymmetric synchronization in a natural way (e.g., a sender sending a message to a receiver).

We demonstrate the problem on an example. The problem arises because the repertoire functions in AMAS are based on the assumption that the agent can choose any single event in R i (l i ). This does not allow for natural specification of situations when the exact transition is determined by another agent. For the AMAS in Example 4.2, the decision to vote for candidate a or b (or to press send) should belong solely to the voter. Thus, setting the EBM repertoire as R ebm (0) = {vote a , vote b , send} does not produce a good model of strategic play in the scenario.

As a remedy, we extend the representations so that one can indicate which agent(s) control the choice between events.

Definition 7.2 (AMAS with explicit control). Everything is exactly as in Definition 2.1, except for the repertoires of choices, which are now functions R i : L i → 2 2 Evt i \{∅} \{∅}. That is, R i (l) lists nonempty subsets of events X 1 , X 2 , · · · ⊆ Evt i , each capturing an available choice of i at the local state l. If the agent chooses X j = {α 1 , α 2 , . . .}, then only an event in that set can be executed within the agent's module; however, the agent has no firmer control over which one will be fired. Accordingly, we assume that T i (l, α) is defined iff α ∈ R i (l). 3

Notice that the AMAS of Definition 2.1 can be seen as a special case where R i (l) is always a list of singletons. The definitions of IIS and undeadlocked IIS stay the same, as agents' repertoires of choices are not actually used to generate the state-transition structure for the model of S. Moreover, undeadlocked AMAS with explicit control can be obtained analogously to Definition 5.4 by adding the auxiliary "epsilon"-agent with R ǫ (q ǫ 0 ) = {{ǫ}} in its sole local state. Strategies still assign choices to local states; hence, the type of agent i's strategies is now σ i :

. The definition of the outcome set is updated accordingly, see below.

Definition 7.3 (Outcome sets for AMAS with explicit control). First, we lift the set of events enabled by − → α A = (α 1 , . . . , α m ) at g to match the new type of repertoires and strategies. Formally, β ∈ enabled(g, − → α A ) iff: (1) for every i ∈ Agent(β) ∩ A, we have β ∈ α i , and (2) for every i ∈ Agent(β) \ A, it holds that β ∈ R i (g i ).

The outcome, React-outcome, and SCF-outcome of σ A in M, g are given as in Definitions 3.5, 5.1, and 6.3. Example 7.4 (Voting) . We improve our voting model by assuming repertoires of choices for the voter and the EBM as follows:

That is, the voter's choices are as before, but the EBM only listens to what the voter selects.

Clearly, v, ebm F voted a holds in the new AMAS. Moreover, ebm F voted a does not hold anymore, even assuming opponent-reactiveness.

It is easy to see that Propositions 4.4, 5.3, 5.6, and 6.4, as well as Theorems 5.7 and 6.5 still hold in AMAS with explicit control.

Discussion. When reasoning about strategic play of asynchronous agents, two kinds of asymmetry come into the picture. On the one hand, the processes (agents) being modeled often synchronize in an asymmetric way. For example, the sender chooses which message to send to the receiver. On the other hand, the agents A in formula A ϕ choose the strategy and thus push the other agents to respond accordingly. The variant of AMAS introduced in (Jamroga et al. 2018) does not allow to capture the former kind of asymmetry. In consequence, the choice between the available synchronization branches belongs solely to the agents indicated by the formula. Unfortunately, there is no natural way to model the converse situation, i.e., when the agents in A are forced by the choices of their opponents. With the new variant of AMAS, we extend the representations so that the modeler can explicitly specify the degree of autonomy of each participating agent. Without that, the degree of autonomy is implicit and comes from the formula being evaluated. Related modeling approaches. Various forms of asymmetric synchronization are present in most process algebras. For example, π-calculus distinguishes between the action c a of sending the value a on channel c, and action c(x) of listening on channel c and storing whatever comes in variable x. CSP goes further, and allows for a similar degree of flexibility to ours through suitable combinations of deterministic choice, nondeterministic choice, and interface parallel operators. Other synchronization primitives are also possible, see e.g. (Bloem et al. 2015) for an overview. Instead of allowing for multiple synchronization primitives, we come up with a single general primitive that can be instantiated to cover different kinds of interaction.

We note in passing the similarity of our new repertoire functions in Definition 7.2 to state effectivity functions (Pauly 2001b; Pauly 2002) and especially alternating transition systems (Alur, Henzinger, and Kupferman 1998) .

Partial order reduction (POR) has been defined for temporal and temporal-epistemic logics without "next" (Peled 1993; Penczek et al. 2000; Gerth et al. 1999; Lomuscio, Penczek, and Qu 2010b) , and recently extended to strategic specifications (Jamroga et al. 2018) . The idea is to take a network of automata (AMAS in our case), and use depth-first search through the space of global states to generate a reduced model that satisfies exactly the same formulas as the full model. Essentially, POR removes paths that change only the interleaving order of an "irrelevant" event with another event. Importantly, the method generates the reduced model directly from the representation, without generating the full model at all.

POR is a powerful technique to contain state-space explosion and facilitate verification, cf. e.g. the experimental results in (Jamroga et al. 2020) . In this paper, we extend the class of models, and modify their execution semantics. We need to show that the reduction algorithm in (Jamroga et al. 2018) , defined for the flawed semantics of ability, is still correct after the modifications. Our main technical result in this respect is Theorem A.11, presented below. The detailed definitions, algorithms and proofs are technical (and rather tedious) adaptations of those in (Jamroga et al. 2018) . We omit them here for lack of space, and refer the inquisitive reader to Appendix A.

Theorem A.11. Let M = IIS (S ǫ ), M ǫ = IIS ǫ (S) and let A ⊆ Agt be a subset of agents. Moreover, let M ′ ⊆ M and M ǫ′ ⊆ M ǫ be the reduced models generated by DFS with the choice of enabled events E(g ′ ) given by conditions C1, C2, C3 and the independence relation I A,PV . For each sATL * ir formula ϕ over PV , that refers only to coalitionŝ A ⊆ A, we have: 1. M, ι |= React ir ϕ iff M ′ , ι ′ |= React ir ϕ, and 2. M ǫ , ι |= ir ϕ iff M ǫ′ , ι ′ |= ir ϕ.

Thus, the reduced models can be used to model-check the sATL * ir properties of the full models. Proof idea. We aim at showing that the full model M and the reduced one M ′ satisfy the same formulas of ATL * ir referring only to coalitions ⊆ A and containing no nested strategic operators. Thanks to the restriction on the formulas, the proof can be reduced to showing that M ′ satisfies the condition AE A , which states that for each strategy and for each path of the outcome of this strategy in M there is an equivalent path in the outcome of the same strategy in M ′ . In order to show that AE A holds, we use the conditions on the selection of events E(g ′ ) to be enabled at state g ′ in M ′ . The conditions include the requirement that ǫ is always selected, together with the three conditions C1, C2, C3 adapted from (Peled 1994; Clarke, Grumberg, and Peled 1999; Jamroga et al. 2018) .

Intuitively, C1 states that, along each path π in M which starts at g ′ , each event that is dependent on an event in E(g ′ ) cannot be executed in M unless an event in E(g ′ ) is executed first in M . C2 says that E(g ′ ) either contains all the events, or only events that do not change the values of relevant propositions. C3 guarantees that for every cycle in M ′ containing no ǫ-transitions, there is at least one node g ′ in the cycle for which all the enabled events of g ′ are selected.

First, we show that M and M ′ are stuttering-equivalent, i.e., they have the same sets of paths modulo stuttering (that is, finite repetition of states on a path). The crucial observation here is that the reduction of M under the conditions C1, C2, C3 is equivalent to the reduction of M without the ǫ-loops under the conditions C1, C2, C3 of (Peled 1994) , and then adding the ǫ-loops to all the states of the reduced model. Therefore, for the paths without ǫ-loops the stuttering equivalence can be shown similarly to (Clarke, Grumberg, and Peled 1999, Theorem 12) while for the paths with ǫ-loops we need more involved arguments in the proof. It turns out that in addition to the fact that M and M ′ are stuttering equivalent, we can show that stuttering equivalent paths of M and M ′ have the same maximal sequence of visible events. From that, we can prove that AE A holds.

In this paper, we reconsider the asynchronous semantics of strategic ability for multi-agent systems, proposed in (Jamroga et al. 2018) . We have already hinted at certain problems with the semantics in the extended abstract (Jamroga, Penczek, and Sidoruk 2021) . Here, we demonstrate in detail how the straightforward combination of strategic reasoning and models of distributed systems leads to counterintuitive interpretation of formulas. We identify three main sources of problems. First, the execution semantics does not handle reasoning about deadlockinducing strategies well. Secondly, fairness conditions need to be redefined for strategic play. Thirdly, the class of representations lacks constructions to resolve the tension between the asymmetry imposed by strategic operators on the one hand, and the asymmetry of interaction, e.g., between communicating parties.

We deal with the problems as follows. First, we change the execution semantics of strategies in asynchronous MAS by adding "silent" ǫ-transitions in states where no "real" event can be executed. We also propose and study the condition of opponent-reactiveness that assumes the agents outside the coalition to not obstruct the execution of the strategy forever. Note that, while the assumption may produce similar interpretation of formulas as in (Jamroga et al. 2018) , it is now explicit -as opposed to (Jamroga et al. 2018) , where it was "hardwired" in the semantics. The designer or verifier is free to adopt it or reject it, depending on their view of how the agents in the system behave and choose their actions.

Secondly, we propose a new notion of strategic concurrency-fairness that selects the fair executions of a strategy. Thirdly, we allow for nondeterministic choices in agents' repertoires. This way, we allow to explicitly specify that one agent has more control over the outcome of an event than the other participants of the event.

The main technical result consists in proving that partial order reduction for strategic abilities (Jamroga et al. 2018) is still correct after the semantic modifications. Thus, the new, more intuitive semantics admits efficient verification.

Beyond ATL ir . In this study, we have concentrated on the logic ATL * ir , i.e., the variant of ATL * based on memoryless imperfect information strategies. Clearly, the concerns raised here are not entirely (and not even not primarily) logical. ATL * ir can be seen as a convenient way to specify the players and the winning conditions in a certain class of games (roughly speaking, 1.5-player games with imperfect information, positional strategies, and LTL objectives). The semantic problems, and our solutions, apply to all such games interpreted over arenas given by asynchronous MAS.

Moreover, most of the claims presented here are not specific to ir-strategies. In fact, we conjecture that our examples of semantic side effects carry over to the other types of strategies (except for the existence of coalitions whose all strategies have empty outcomes, which can happen for neither perfect information nor perfect recall). Similarly, our technical results should carry over to the other strategy types (except for the correctness of POR, which does not hold for agents with perfect information). We leave the formal analysis of those cases for future work.

Other issues. An interesting question concerns the relationship between asynchronous and synchronous models. We conjecture that AMAS with explicit control can be simulated by concurrent game structures and alternating transition systems. Similarly, it should be possible to simulate CGS and ATS by AMAS with explicit control, at the expense of using a huge space of fully synchronized actions. For the model checking complexity in AMAS with explicit control, we expect the same results as in (Jamroga et al. 2020) .

MOCHA: Modularity in model checking

jMocha: A model-checking tool that exploits design structure

Alternating-time Temporal Logic

Alternating-time Temporal Logic

Alternating-time Temporal Logic

Verification of broadcasting multi-agent systems against an epistemic strategy logic

Verification of multi-agent systems with imperfect information and public actions

Alternating-time temporal logic on finite traces

Algebra of communicating processes with abstraction

Decidability of Parameterized Verification

Intentions, Plans, and Practical Reason

Alternating epistemic mu-calculus

Improving the model checking of strategies under partial observability and fairness constraints

Reasoning about memoryless strategies under partial observability and unconditional fairness constraints

MCMAS-SLK: A model checker for the verification of strategy logic specifications

Verifying and synthesising multi-agent systems against one-goal strategy logic specifications

PRISM-games: A model checker for stochastic multi-player games

Design and synthesis of synchronization skeletons using branching time temporal logic

Model Checking

Memory-efficient algorithms for the verification of temporal properties

Model-checking ATL under imperfect information and perfect recall semantics is undecidable

The expressive power of epistemic µ-calculus. CoRR abs/1407.5166. Dima

PAWS -A deployed game-theoretic application to combat poaching

A partial order approach to branching time logic model checking

A partial approach to model checking

State and path coalition effectivity models of concurrent multi-player games. Autonomous Agents and Multi-Agent Systems 1-40

An alternatingtime temporal logic with knowledge, perfect recall and past: axiomatisation and model-checking

Communicating sequential processes

The model checker SPIN

Symbolic model checking epistemic strategy logic

Approximate verification of strategic abilities under imperfect information

Towards partial order reductions for strategic ability

Fixpoint approximation of strategic abilities under imperfect information

Strategic abilities of asynchronous agents: Semantic side effects

Unbounded model checking for alternating-time temporal logic

STV+Reductions: Towards practical verification of strategic ability using model reductions

STV: Model checking for strategies under imperfect information

MCMAS : A model checker for multi-agent systems

Partial order reductions for model checking temporal epistemic logics over interleaved multi-agent systems

Partial order reductions for model checking temporal-epistemic logics over interleaved multi-agent systems

MCMAS: An open-source model checker for the verification of multiagent systems

Knowledge in multiagent systems: initial configurations and broadcast

Hiding actions in multi-player games

A calculus of mobile processes

A Calculus of Communicating Systems

A logical framework for coalitional effectivity in dynamic procedures

A modal logic for coalitional power in games

All from one, one for all: On model checking using representatives

Combining partial order reductions with on-the-fly model-checking

Partial order reductions: Model checking using representatives

Improving partial order reductions for universal branching time properties

Synthesis and verification of uniform strategies for multi-agent systems

Collaborative embedded systems -a case study

Alternating-time logic with imperfect recall

We thank the anonymous reviewers for their insightful comments. The authors acknowledge the support of the National Centre for Research and Development, Poland (NCBR), and the Luxembourg National Research Fund (FNR), under the PolLux/FNR-CORE project STV (POLLUX-VII/1/2019). W. Penczek and T. Sidoruk acknowledge support from CNRS/PAS project PARTIES.

All the results in this appendix are formulated and proved for the semantics of ATL ir over undeadlocked AMAS with explicit control. Also, we restrict the formulas to ATL * without nested strategic modalities and the next step operator X ("simple ATL * ", or sATL * ). As noted in (Jamroga et al. 2018) , sATL * is sufficient for most practical specifications and much more expressive than LTL. Yet, as we prove below, it enjoys the same efficiency of partial order reduction.We begin by introducing the relevant notions of equivalence. Then, we propose conditions on reduced models that preserve the stuttering equivalence with and without the assumption of opponent-reactiveness (React). We point out algorithms that generate such models, and prove their correctness.It should be stressed that the reduction scheme proposed here is general, in the sense that it preserves equivalent representatives of both fair and unfair paths in the model. In particular, we do not propose a variant of POR, optimized for strategic concurrency-fair paths, analogous to reductions of (Peled 1993) for CF. A variant of POR for sATL ir under the SCF assumption is planned for future work.

Given an undeadlocked AMAS S ǫ , partial order reduction attempts to generate only a subset of states and transitions that is sufficient for verification of S ǫ , i.e., a relevant sub-. Proof. Note that each joint ir-strategy in M is also a well defined ir-joint strategy in M ′ as it is defined on the local states of each agent of an AMAS which is extended by both M and M ′ . The lemma follows directly from the definition of React-outcome (Def. 5.1 and 7.3), plus the fact that. be the sequence of the events of agent i in π. For each b j let π[b j ] denote the global state from which b j is executed in π. By induction we can show that for each j ≥ 0, we have πAssume that the thesis holds for j = k. The induction step follows from the fact the local evolution T i is a function,Thus, by Def. 5.1 and 7.3, for each ir-strategy σ i we have π ∈ out React M (ι, σ i ) iff π ′ ∈ out React M (ι, σ i ), which concludes the proof. Lemma A.3 can be easily generalized to joint strategies σ A ∈ Σ ir A .

Let M be a model, M ′ ⊆ M , and PV ⊆ PV a subset of propositions. Stuttering equivalence says that two paths can be divided into corresponding finite segments, each satisfying exactly the same propositions. Stuttering path equivalence 4 requires two models to always have corresponding, stuttering-equivalent paths. Definition A.4 (Stuttering equivalence). Two paths π ∈ Π M (ι) and. . of the states of π, and an analogous partition B ′ 0 , B ′ 1 , . . . of the states of π ′ , s.t. for each j ≥ 0 : B j and B ′ j are nonempty and finite, and Clarke, Grumberg, and Peled 1999) 

Intuitively, an event is invisible iff it does not change the valuations of the propositions. 6 Additionally, we can designate a subset of agents A whose events are visible by definition. Furthermore, two events are independent iff they are not events of the same agent and at least one of them is invisible. Definition A.6 (Invisible events). Consider a model M , a subset of agents A ⊆ Agt, and a subset of propositions PV ⊆ PV. An event α ∈ Evt is invisible wrt. A and PV if Agent(α) ∩ A = ∅ and for each two global states g, g ′ ∈ St we have that gThe set of all invisible events for A, PV is denoted by Invis A,PV , and its closure -of visible eventsby V is A,PV = Evt \ Invis A,PV . Definition A.7 (Independent events). The notion of independence I A,PV ⊆ Evt × Evt is defined as:

Rather than generating the full model M = IIS (S ǫ ), one can generate a reduced model M ′ satisfying the following property:We define a class of algorithms that generate reduced models satisfying AE A (Section A.4), and then prove that these models preserve sATL * ir (Section A.4). Algorithms for partial order reduction. POR is used to reduce the size of models while preserving satisfaction for a class of formulas. The standard DFS (Gerth et al. 1999) or DDFS (Courcoubetis et al. 1992) is modified in such a way that from each visited state g an event α to compute the successor state g 1 such that g α → g 1 , is selected from E(g) ∪ {ǫ} such that E(g) ⊆ enabled(g) \ {ǫ}. That is, the algorithm always selects ǫ, plus a subset of the enabled events at g. Let A ⊆ Agt. The conditions on the heuristic selection of E(g) given below are inspired by (Peled 1994; Clarke, Grumberg, and Peled 1999; Jamroga et al. 2018) . C1 Along each path π in M that starts at g, each event that is dependent on an event in E(g) cannot be executed in π without an event in E(g) being executed first in π. Formally, ∀π ∈ Π M (g) such that π = g 0 α 0 g 1 α 1 . . . with g 0 = g, and ∀b ∈ Evt such that Proof. Let M ′ ⊆ M = IIS (S ǫ ) be the reduced model generated as specified. Notice that the reduction of M under the conditions C1, C2, C3 above is equivalent to the reduction of M without the ǫ-loops under the conditions C1, C2, C3 of (Peled 1994) , and then adding the ǫloops to all the states of the reduced model. Although the setting is slightly different, it can be shown similarly to (Clarke, Grumberg, and Peled 1999, Theorem 12 ) that the conditions C1, C2, C3 guarantee that the models: (i) M without ǫ-loops and (ii) M ′ without ǫ-loops are stuttering path equivalent. More precisely, for each path π = g 0 a 0 g 1 a 1 · · · with g 0 = ι (without ǫ-transitions) in M there is a stuttering equivalent path π ′ = g ′ 0 a ′ 0 g ′ 1 a ′ 1 · · · with g ′ 0 = ι (without ǫ-transitions) in M ′ such that Evt (π)| V isA = Evt (π ′ )| V isA , i.e., π and π ′ have the same maximal sequence of visible events for A. (*)We will now prove that this implies M ≡ s M ′ . Removing the ǫ-loops from M eliminates two kinds of paths: (a) paths with infinitely many "proper" events, and (b) paths ending with an infinite sequence of ǫ-transitions. Consider a path π of type (a) from M . Notice that the path π 1 , obtained by removing the ǫ-transitions from π, is stuttering-equivalent to π. Moreover, by (*), there exists a path π 2 in M ′ without ǫ-transitions, which is stuttering-equivalent to π 1 . By transitivity of the stuttering equivalence, we have that π 2 is stuttering equivalent to π. Since π 2 must also be a path in M ′ , this concludes this part of the proof.Consider a path π of type (b) from M , i.e., π ends with an infinite sequence of ǫ-transitions. Let π 1 be the sequence obtained from π after removing ǫ-transitions, and π 2 be any infinite path without ǫ-transitions such that π 1 is its prefix. Then, it follows from (*) that there is a stuttering equiva-1 is a sequence in M ′ and can be extended with an infinite number of ǫ-transitions to the path π ′ in M ′ . It is easy to see that π and π ′ are stuttering equivalent.So far, we have shown that our reduction under the conditions C1, C2, C3 guarantees that the models M and M ′ are stuttering path equivalent, and more precisely that for each path π = g 0 a 0 g 1 a 1 · · · with g 0 = ι in M there is a stuttering equivalent path π ′ = g ′ 0 a ′ 0 g ′ 1 a ′ 1 · · · with g ′ 0 = ι in M ′ such that Evt (π)| V isA = Evt (π ′ )| V isA , i.e., π and π ′ have the same maximal sequence of visible events for A. To show that M ′ satisfies AE A , consider an ir-joint strategy σ A and π ∈ out React M (ι, σ A ). As demonstrated above, there is π ′ ∈ Π M ′ (ι) such that π ≡ s π ′ and Evt(π)| V isA = Evt(π ′ )| V isA . Since Evt i ⊆ V is A for each i ∈ A, the same sequence of events of each Evt i is executed in π and π ′ . Thus, by the generalization of Lemma A.3 to ir-joint strategies we get π ′ ∈ out React M (ι, σ A ). So, by Lemma A.2 we have π ′ ∈ out React M ′ (ι, σ A ). Algorithms generating reduced models, in which the choice of E(g) is given by similar conditions, can be found for instance in (Peled 1994; Peled 1993; Clarke, Grumberg, and Peled 1999; Gerth et al. 1999; Penczek et al. 2000; Lomuscio, Penczek, and Qu 2010b) . POR for proactive opponents. The same reduction still works without the assumption of opponent-reactiveness (React). Theorem A.9. Let M ǫ = IIS ǫ (S) be an undeadlocked IIS. Then, its reduced model M ǫ′ , generated as in Theorem A.8, satisfies AE A . Proof (Sketch) . In this setting, there is no auxiliary agent in the AMAS, and ǫ-transitions are added directly to the IIS in accordance with Definition 4.3. Hence, not every global state of M ǫ necessarily has an ǫ loop, but only those where a miscoordinating combination of events exists. However, this does not impact the reduction itself.First, note that Lemma A.2 still holds, directly from the definition of outcome (Definition 3.5). Furthermore, because in the undeadlocked IIS M ǫ the ǫ-transitions do not belong to any agent, Lemma A.3, where sequences of some agent i's events are considered, also holds. Note that the React condition only restricts the outcome sets, and not the model itself: both M = IIS(S ǫ ) and M ǫ contain the same two types (a) and (b) of paths with ǫ-transitions as discussed in Theorem A.8. Hence, following its reasoning, it can first be shown that models M ǫ and M ǫ′ without their ǫtransitions are stuttering path equivalent, and that it remains the case also when both types of paths including ǫ loops are included.Note that the remark about M ′ being equivalent to reducing M without ǫ loops and adding them to each global state obviously does not apply to M ǫ (not every global state of M ǫ has them in the first place). However, this observation has no bearing on the proof. As before, ǫ is explicitly stated to be selected for the subset E(g), ensuring preservation of representative paths with ǫ in M ǫ′ .Correctness of reductions satisfying AE A . We show that the reduced models satisfying AE A preserve sATL * ir . Theorem A.10. Let A ⊆ Agt, and let models M ′ ⊆ M , M ǫ′ ⊆ M ǫ satisfy AE A . For each sATL * ir formula ϕ over PV , that refers only to coalitions ⊆ A, we have that:Proof. Proof by induction on the structure of ϕ. We show the case ϕ =  γ. The cases for ¬, ∧ are straightforward.Notice that out React M ′ (ι, σÂ) ⊆ out React M (ι, σÂ), which together with the condition AE A implies that the sets out React M (ι, σÂ) and out React M ′ (ι, σÂ) are stuttering path equivalent. Analogously, this is the case for out M ′ (ι, σÂ) ⊆ out M (ι, σÂ), i.e. without the React assumption. Hence, (1) and (2) follow from Theorem A.5.Together with Theorems A.8 and A.9, we obtain the following. Theorem A.11. Let M = IIS (S ǫ ), M ǫ = IIS ǫ (S) and let M ′ ⊆ M and M ǫ′ ⊆ M ǫ be the reduced models generated by DFS with the choice of E(g ′ ) for g ′ ∈ St ′ given by conditions C1, C2, C3 and the independence relation I A,PV . For each sATL * ir formula ϕ over PV , that refers only to coalitions ⊆ A, we have:1. M, ι |= React ir ϕ iff M ′ , ι ′ |= React ir ϕ, and 2. M ǫ , ι |= ir ϕ iff M ǫ′ , ι ′ |= ir ϕ.This concludes the proof that the adaptation of POR for LTL −X to sATL * ir , originally presented in (Jamroga et al. 2018) , remains sound in the updated semantics proposed in Sections 4 and 7. That is, the structural condition AE A is sufficient to obtain correct reductions for sATL * ir with and without the new opponent-reactiveness assumption (Theorem A.11). Thanks to that, one can potentially reuse or adapt the existing POR algorithms and tools for LTL −X , and the actual reductions are likely to be substantial.