Paper deep dive
Limit-sure Winning in Team Games without Shared Randomness
Léonard Brice, Thomas A. Henzinger, Alipasha Montaseri, Ali Shafiee, K. S. Thejaswini
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 95%
Last extracted: 10/12/2026, 5:44:46 AM
Summary
This paper investigates the computational complexity of limit-sure winning in concurrent stochastic team games where agents lack shared randomness. The authors prove that determining if a team can satisfy a reachability objective with probability arbitrarily close to 1 is NP-complete. Conversely, for safety objectives, limit-sure winning coincides with almost-sure winning, placing the problem in P. These results imply that model checking the qualitative fragment of Individually Randomised ATL (IRATL) is P^NP-complete.
Entities (10)
Relation Signals (6)
Limit-sure winning → hascomplexity → NP-complete
confidence 97% · For reachability objectives, we show that this problem is NP-complete.
Limit-sure winning → hascomplexity → P
confidence 97% · For safety objectives, we show that limit-sure winning coincides with almost-sure winning, which is known to lie in P.
Model checking → appliesto → Individually Randomised ATL
confidence 96% · model checking of the qualitative fragment of the logic Individually Randomised ATL
Model checking → hascomplexity → P^NP
confidence 96% · model checking of the qualitative fragment of the logic Individually Randomised ATL ... is P^NP-complete.
Shared randomness → enablesreductionto → Two-player games
confidence 92% · If the agents could access a shared source of randomness, then these games reduce to two-player games.
Concurrent stochastic games → models → Team Games
confidence 90% · We study concurrent stochastic games in which a team of agents plays against an adversarial environment.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:We study concurrent stochastic games in which a team of agents plays against an adversarial environment. If the agents could access a shared source of randomness, then these games reduce to two-player games. Despite being common in the literature on coalition games, this assumption does not accurately model real-world systems. In this paper, we consider the setting where the agents only have access to individual sources of randomness, and must satisfy a given reachability or safety objective. The limit-sure problem asks whether the team can ensure that the objective is satisfied with probability at least $1-\lambda$ for every $\lambda>0$. For reachability objectives, we show that this problem is $\mathsf{NP}$-complete. For safety objectives, we show that limit-sure winning coincides with almost-sure winning, which is known to lie in $\mathsf{P}$. As a corollary of these results, we conclude that model checking of the qualitative fragment of the logic Individually Randomised ATL -- introduced in the recent work of Brice et al. -- is $\mathsf{P}^{\mathsf{NP}}$-complete.
Tags
Links
- Source: https://arxiv.org/abs/2610.13569v1
- Canonical: https://arxiv.org/abs/2610.13569v1
Trouble viewing inline? Open PDF directly →
Full Text
177,189 characters extracted from source content.
Expand or collapse full text
Limit-sure Winning in Team Games without Shared Randomness Léonard Brice Affiliation: Institute of Science and Technology Austria, Klosterneuburg, Austria email: leonard.brice@ista.ac.at , Thomas A. Henzinger Affiliation: Institute of Science and Technology Austria, Klosterneuburg, Austria email: tah@ista.ac.at , Alipasha Montaseri Affiliation: École Polytechnique Fédérale de Lausanne, Lausanne, Switzerland email: alipasha.montaseri@epfl.ch , Ali Shafiee Affiliation: Institute of Science and Technology Austria, Klosterneuburg, Austria email: ali.shafiee@ista.ac.at and K. S. Thejaswini Affiliation: Université libre de Bruxelles, Brussels, Belgium email: thejaswini.raghavan@ulb.be Abstract. We study concurrent stochastic games in which a team of agents plays against an adversarial environment. If the agents could access a shared source of randomness, then these games reduce to two-player games. Despite being common in the literature on coalition games, this assumption does not accurately model real-world systems. In this paper, we consider the setting where the agents only have access to individual sources of randomness, and must satisfy a given reachability or safety objective. The limit-sure problem asks whether the team can ensure that the objective is satisfied with probability at least 1−λ1-λ for every λ>0λ>0. For reachability objectives, we show that this problem is NP-complete. For safety objectives, we show that limit-sure winning coincides with almost-sure winning, which is known to lie in P. As a corollary of these results, we conclude that model checking of the qualitative fragment of the logic Individually Randomised ATL—introduced in the recent work of Brice et al.—is P NP-complete. Keywords: Multi-player games, Concurrent games, Shared randomness 1. Introduction Planning for a group of agents in an uncertain and reactive world is a fundamental problem in multi-agent systems. A standard model is the concurrent stochastic game in which, at every round, each agent simultaneously picks an action, and so does the environment. The next state is selected following a distribution that depends on the state and on the chosen profile. Agents that pursue a common goal against such an environment form a team, and the environment is modelled as a single adversarial opponent. Randomisation is often necessary to achieve the optimal value in concurrent games. If the team players chose their action deterministically, then an adversarial environment would be able to thwart the attempt of this team. This can already be observed in two-player games, like rock-paper-scissors. The usual semantics that describe the winning of a coalition in such graph games include alternating-time temporal logic (ATL) (Alur et al., 2002), and its probabilistic variants: Randomised ATL (RATL) (de Alfaro et al., 1998) and Probabilistic ATL (PATL) (Chen and Lu, 2007). Such logics however model coalitions as a single player, making the implicit assumption that it can resort to a common source of randomness. This fails to accurately model several real-world agents, which may not be able to coordinate their random choices. For example, different sensors cannot coordinate their random choices after a network partition, and different components of a system that were programmed together and then shipped apart do not share a common source of randomness. The team is then restricted to using only product distributions. Recently, the work of Brice et al. (Brice et al., 2026b) initiated a study of team games with individual randomisation, building on previous work of de Alfaro and Faella (de Alfaro and Faella, 2003). We work with the same semantics as in their work and in the work of de Alfaro and Faella. This setting formulates questions that are relevant to both planning and verification. The standard architecture in multi-agent planning is centralised planning followed by decentralised execution. A planner that knows the model designs one controller per agent offline, and at run time each agent executes its own controller with its own source of randomness. For planning scenarios, a planner is given a reliability requirement in addition to a goal, say “reach the target with probability at least 1−λ1-λ”. There are two ways that these questions can be formulated. Can the requirement be met for one given λ, and can it be met for every λ, thus ensuring that the plan succeeds with probability arbitrarily close to 1? We focus on the second question, known as limit-sure winning. A positive instance ensures that one can construct a plan with as much accuracy as needed. s_ fails0s_0s_ goalcc|1,2c scan_1, scan_2ch|2ch scan_2hc|1hc scan_1hh|1,2h scan_1, scan_2ch|1ch scan_1, hc|2hc scan_2 Figure 1. The team game described in Example 1. A game graph with three states: a failure state on the left, the initial state in the middle, and a goal state on the right. The failure and goal states are absorbing and drawn with double circles. From the initial state, the play moves to the failure state if both agents cross and the adversary scans. It moves to the goal state if both agents cross and the adversary waits, or if both agents hide and the adversary scans. It stays in the initial state if both agents hide and the adversary waits, or if the agents disagree, whatever the adversary does. Example 1.0. Two robots must cross a guarded door. At each round, each agent chooses to cross (c) or hide (h), while the opponent chooses to scan either the first robot (1 scan_1) or the second (2 scan_2). If both robots choose to cross, since the door is narrow, the robots break and reach s_ fail irrespective of the opponent’s action. If robot i crosses while the opponent plays i scan_i, robot i is caught, but the team can try again. If exactly one robot, say, robot i attempts to cross, it can reach s_ goal only if the opponent does not choose i scan_i. If both hide, then nothing changes, and the game is tried again. The transitions are shown in Figure 1. If the team had a shared source of randomness, then they could choose between (c,h)(c,h) and (h,c)(h,c) uniformly at random, and the team crosses almost surely irrespective of the opponent strategy, since they end up either in s0s_0 or in s_ goal with positive probability at each attempt. However, if the team had no shared source of randomness, then by choosing between (c,h)(c,h) and (h,c)(h,c), they also choose (c,c)(c,c) and reach the failure state with positive probability. However, even without a shared source of randomness, the team can win limit surely. Let both robots cross with probability ϵ∈(0,1)ε∈(0,1) at every round. Therefore, they can reach the state s_ goal with probability ϵ(1−ϵ)ε(1-ε) for each opponent action. The probability that they both play cross is ϵ2ε^2. Hence, they end up in the same state s0s_0 with probability 1−ϵ1-ε. This therefore gives us Pr(reach s)=ϵ(1−ϵ)ϵ(1−ϵ)+ϵ2=1−ϵ. (reach s_ goal)= ε(1-ε)ε(1-ε)+ε^2=1-ε. For every 1>λ>01>λ>0, choosing 0<ϵ<λ0<ε<λ ensures that the team can succeed with probability greater than 1−λ1-λ. Our contributions. Our main contribution is in showing the computational complexity of limit-sure reachability. We also show the computational complexity of limit-sure safety games. (1) We show that deciding whether a team without shared randomness can satisfy reachability limit surely is NP-complete (Theorem 16). The lower bound follows from the hardness reduction of almost-sure reachability, since both limit-sure and almost-sure winning coincide on those instances (Brice et al., 2026b). We provide an NP upper bound by giving a polynomial certificate that represents the family of strategies, parametrised by λ, that can be verified in polynomial time. (2) For safety objectives, we show that limit-sure winning and almost-sure winning coincide (Theorem 1). Thus, deciding whether a team can limit surely win a safety game is in P. As a corollary, we show in Theorem 1 that model checking the qualitative fragment of the logic IRATL, introduced by Brice et al. (Brice et al., 2026b), is in P NP. We also show that it is complete for this class. To prove the NP upper bound for reachability, we represent a family of team strategies by one team strategy whose action probabilities are algebraic Puiseux series in ϵε (Lemma 5). This follows the approach of Asadi et al. (Asadi et al., 2025), who study POMDPs using Puiseux methods originating with Bewley and Kohlberg (Bewley and Kohlberg, 1976). Only the leading exponent of each action probability matters for our case, defining a notion of rank of an action. Thanks to a standard result linking absorption probabilities to spanning forests (Freidlin and Wentzell, 2012), we reduce our problem to guessing the ranks and then comparing minimum-rank spanning forests (Lemma 11). We also show that these ranks only require polynomially many bits using Cramer’s rule and Hadamard’s inequality (Lemma 9). Guessing the team ranks alone gives an NP NP upper bound by using an NP oracle that detects a violating opponent response using Edmonds’ algorithm (Edmonds, 1967). To improve this and obtain an NP upper bound, we construct an encoded MDP whose rank encoding breaks ties. We guess a response and certify its optimality through local inequalities (Frank, 1981; Schrijver, 2003). This reduces verification to polynomial time. We give the details in Section 3.3. Related work Concurrent games and qualitative objectives. Concurrent stochastic games are the standard model of a controller acting against a reactive environment (de Alfaro et al., 1998). For two players and reachability, the sure, almost-sure and limit-sure winning sets are computable in polynomial time (de Alfaro et al., 2007), and the quantitative threshold decision problem is in the complexity class ∃ℝ (the complexity class associated with the existential theory of the reals (Schaefer et al., 2024)) with SQRTSUM-hardness as the best known lower bound (Chatterjee et al., 2012; Etessami and Yannakakis, 2015). The difference between almost-sure and limit-sure reachability appears already in recursive games (Everett, 1957). The asymptotic analysis of families of strategies ensuring limit-sure winning, by algebraic means, goes back to Bewley and Kohlberg and is an active line of research. For example, Solan used them to analyse perturbed Markov chains, communicating classes, and exit distributions (Solan, 2003). A related use of leading transition exponents appears in Young’s minimum-resistance-tree characterisation of stochastic stability (Young, 1993). Teams, coalitions and sharing randomness. If the team instead had a shared source of randomness, it could be interpreted as a single player, and then the sure, almost-sure and limit-sure reachability sets are all computable in polynomial time (de Alfaro et al., 2007). This setting reduces to two-player concurrent games, and there are several works that study such games (de Alfaro et al., 1998; Chatterjee et al., 2012; Hansen et al., 2009). Brice et al. (Brice et al., 2026b), following the work of de Alfaro and Faella (de Alfaro and Faella, 2003), developed team games where players need not have access to shared randomness. The work of de Alfaro and Faella already established that even for almost-sure reachability (asking whether there is a strategy to reach a goal with probability 1), the problem is NP-complete. In recent work, Brice et al. (Brice et al., 2026b) extended the problem to its quantitative variant and considered the threshold problem, which asks if the target can be reached with a probability strictly greater than a given threshold. They show that memoryless team strategies are sufficient for the threshold problem, which ensures that the threshold problem is in ∃ℝ . The complexity of the limit-sure problem for teams was left open ((Brice et al., 2026b, Problem 3)), together with the limit-sure safety problem ((Brice et al., 2026b, Problem 4)). We settle both. Equilibria vs team games. The gap between shared and individual sources of randomness is the gap that the extensive-form literature calls ex ante versus no coordination. Team-maxmin equilibria were introduced by von Stengel and Koller (von Stengel and Koller, 1997). Celli and Gatti (Celli and Gatti, 2018) consider three different communication models, namely correlation both before and during play, correlation only before play, and none at all, and show that the loss from restricting communication can be unbounded in the size of the game tree. Our setting is similar to their third setting, but on infinite plays on a graph. Follow-up works of the above give algorithms for ex ante coordinated team strategies (Farina et al., 2018; Zhang et al., 2021a). Basilico et al. (Basilico et al., 2017) study team max-min equilibria for one-shot games in normal form and give efficiency bounds and algorithms for teams that cannot correlate their strategy. Kalogiannis et al. (Kalogiannis et al., 2023) consider stationary approximate Nash equilibria in discounted adversarial team Markov games with independent team policies. The literature above works with one-shot games or finite trees, or equilibria, whereas we work on qualitative, limit-sure winning on graphs using different techniques. POMDPs and decentralised planning. Centralised planning with decentralised execution is the standard setting for Dec-POMDPs, where the general problem with finite horizon is NEXP-complete (Bernstein et al., 2002; Oliehoek and Amato, 2016). Such Dec-POMDPs are useful in cooperative multi-agent reinforcement learning (Zhang et al., 2021b). Our model is orthogonal to partial observation, which it replaces with an active adversary. Under partial observation, with infinite horizon, limit-sure reachability is undecidable in general, already for blind POMDPs (Gimbert and Oualhadj, 2010); but Asadi et al. show that it is NP-complete for policies with a fixed memory bound (Asadi et al., 2025). Their proof uses Puiseux strategies to obtain polynomial-size rank witnesses, and our proof builds on this approach. However, fixing a team strategy leaves an adversarial MDP. Our novel ingredient is a polynomial-time verification procedure that certifies the condition against all opponent responses by checking only one response. Logics for multi-agent coalition. Alternating-time Temporal Logic (ATL) (Alur et al., 2002) is used to model multi-agent systems that navigate a graph. Some extensions of ATL, like PATL (Chen and Lu, 2007) or RATL (de Alfaro et al., 1998), also consider randomised strategies. However, their semantics treat a coalition as a meta-player, implicitly assuming that they share randomness. Model checkers for stochastic multi-agent systems (Kwiatkowska et al., 2020) also assume shared randomisation. Individually Randomised ATL (IRATL) (Brice et al., 2026b) was proposed to consider settings where teams do not communicate or share randomness during play. Our results settle the complexity of limit-sure reachability and safety in this logic, which leads to a tight complexity bound for model checking the qualitative fragment of IRATL. Probabilistic Strategy Logic (Aminof et al., 2019) is expressive enough to model individual randomisation, but is undecidable in general. 2. Preliminaries Notation We write ℕN for the set of nonnegative integers. For a finite set X, Δ(X) (X) is the set of probability distributions over X, and (d)=x∈X∣d(x)>0 Supp(d)=\x∈ X d(x)>0\ is the support of d∈Δ(X)d∈ (X). For sets X and Y, YXY^X is the set of functions from X to Y. X+X^+ and XωX^ω are the sets of nonempty finite sequences and of infinite sequences over X. Definition 2.0 (Game). We define a game G as a tuple =⟨Σ,S,(Ap)p∈Σ,δ,Π,s0,⟩G= ,S,(A_p)_p∈ ,δ, ,s_0,W . The sets Σ and S are finite sets of players and states. Each player p has a finite nonempty action set ApA_p. The transition function is δ:S×∏p∈ΣAp→Δ(S)δ S× _p∈ A_p→ (S). The team is Π⊆Σ , and the initial state is s0∈Ss_0∈ S. The objective ⊆SωW S^ω is a set of infinite state sequences. We call the players in Σ∖Π the opponents. For X⊆ΣX , the set AX=∏p∈XApA_X= _p∈ XA_p contains its action profiles. We write a complete profile as (a¯,b¯)∈AΠ×AΣ∖Π( a, b)∈ A_ × A_ . Here, a¯=(ap)p∈Π a=(a_p)_p∈ is the team profile, and b¯ b is the opponents’ profile. The game starts in s0s_0. At each round, every player picks an action simultaneously and independently. If the current state is s and the players pick the profile (a¯,b¯)( a, b), the next state is determined according to δ(s,(a¯,b¯))δ(s,( a, b)). We call the resulting infinite sequence of states a play. The game is zero-sum, meaning that the team wins the plays in W, and the opponents try to keep the play out of W. Definition 2.0 (Strategies, team strategies). A history is a non-empty finite sequence of states, an element of S+S^+. A strategy for player p∈Σp∈ is a mapping σp:S+→Δ(Ap) _p S^+→ (A_p). It is deterministic if σp(h) _p(h) assigns probability 11 to one action at every history h. It is memoryless if σp(h) _p(h) depends only on the last state of h, and we write σp(s) _p(s) for its value at the histories ending in s. A team strategy is a tuple σΠ=(σp)p∈Π _ =( _p)_p∈ of strategies, one per team player. At a history h, it induces the product distribution σΠ(h) _ (h) over AΠA_ , defined for every team profile (ap)p∈Π(a_p)_p∈ by (1) σΠ(h)((ap)p∈Π)=∏p∈Πσp(h)(ap). _ (h) ((a_p)_p∈ )\;=\; _p∈ _p(h)(a_p). Generally, for a set Σ′ of players we write ΛΣ′h=∏p∈Σ′(Δ(Ap))S+ _ ^h\;=\; _p∈ ( (A_p) )^S^+ for the set of tuples (σp)p∈Σ′( _p)_p∈ of strategies, and ΛΣ′⊆ΛΣ′h _ _ ^h for those that are memoryless. A team strategy is thus an element of ΛΠh _ ^h. Remark 2.1. The product form of Equation 1 is the defining feature of our setting: each team player randomises privately, so the team can only play product distributions over AΠA_ . By contrast, a team with shared randomness can play any joint distribution in Δ(AΠ) (A_ ). The game then reduces to a two-player zero-sum concurrent game. Objectives The objective of a game specifies which plays the team wins. We consider reachability and safety objectives. Reachability expresses that the play eventually enters a target state, and safety expresses that the play never leaves the set of safe states. Definition 2.0 (Reachability objective). For a set T⊆ST S of target states, the reachability objective requires to visit T at least once: ◇T=s0s1⋯∈Sω∣∃k≥0,sk∈T. T=\s^0s^1·s∈ S^ω ∃ k≥ 0,\ s^k∈ T\. Definition 2.0 (Safety objective). For a set C⊆SC S of safe states, the safety objective requires that a play remain in C forever: □C=s0s1⋯∈Sω∣∀k≥0,sk∈C. C=\s^0s^1·s∈ S^ω ∀ k≥ 0,\ s^k∈ C\. Definition 2.0 (Markov decision process). A Markov decision process (MDP) is a tuple (V,A,P)(V,A,P), where V is a finite nonempty set of states, A is a finite nonempty set of actions, and P:V×A→Δ(V)P V× A→ (V) is a transition function. Its support is the set of triples (u,a,v)(u,a,v) with P(u,a)(v)>0P(u,a)(v)>0. Fixing a memoryless team strategy σΠ∈ΛΠ _ ∈ _ induces the MDP (S,A,PσΠ)(S,A_ O,P_ _ ), where PσΠ(s,b)(t)=∑a¯∈AΠσΠ(s)(a¯)⋅δ(s,(a¯,b))(t)∀s,t∈S,b∈A.P_ _ (s,b)(t)= _ a∈ A_ _ (s)( a)·δ(s,( a,b))(t) ∀ s,t∈ S,\ b∈ A_ O. Definition 2.0 (Markov chain). A Markov chain (MC) is a pair (V,P)(V,P), where V is a finite nonempty set of states and P:V×V→[0,1]P V× V→[0,1] is a transition matrix. A state u∈Vu∈ V is absorbing if P(u,u)=1P(u,u)=1. For u∈Vu∈ V and R⊆VR V, we write ℙuP(◇R)P_u^P( R) for the probability that the chain started in u eventually visits R. Fixing memoryless strategies σΠ∈ΛΠ _ ∈ _ and τ∈Λτ∈ _ O induces the Markov chain (S,PσΠ,τ)(S,P_ _ ,τ), where PσΠ,τ(s,t)=∑a¯∈AΠ,b∈AσΠ(s)(a¯)⋅τ(s)(b)⋅δ(s,(a¯,b))(t)∀s,t∈S.P_ _ ,τ(s,t)= _ subarrayc a∈ A_ ,b∈ A_ O subarray _ (s)( a)·τ(s)(b)·δ(s,( a,b))(t) ∀ s,t∈ S. By a classical result (Norris, 1998), the probabilities ℙvP(◇R)P_v^P( R) for v∈Vv∈ V form the coordinatewise least solution q∈ℝ≥0Vq _≥ 0^V of the system (2) qv=1 for v∈R,qv=∑w∈VP(v,w)qw for v∈V∖R.q_v=1\ for v∈ R, q_v= _w∈ VP(v,w)\,q_w\ for v∈ V R. Winning conditions Every team strategy σΠ _ and tuple τ _ O of strategies for the opponents induces a probability measure on plays starting in s0s_0, which we denote by ℙs0σΠ,τP_s_0 _ , _ O. In particular, we write ℙs0σΠ,τ()P_s_0 _ , _ O(W) for the probability of satisfying the objective. The team chooses its strategy first and seeks to maximise this probability against every response by the opponents. Definition 2.0 (Almost-sure winning). The team wins almost surely if some team strategy ensures the objective with probability 11 against every tuple of strategies for the opponents: ∃σΠ∈ΛΠh:∀τ∈ΛΣ∖Πh,ℙs0σΠ,τ()=1.∃ _ ∈ _ ^h\;:\;∀ _ O∈ _ ^h, _s_0 _ , _ O(W)=1. Definition 2.0 (Limit-sure winning). The value of a game G is val()=supσΠ∈ΛΠhinfτ∈ΛΣ∖Πhℙs0σΠ,τ().val(G)\;=\; _ _ ∈ _ ^h\, _ _ O∈ _ ^h\,P_s_0 _ , _ O(W). The team wins limit surely if val()=1val(G)=1, or equivalently, if ∀λ∈(0,1):∃σΠ∈ΛΠh:∀τ∈ΛΣ∖Πh,ℙs0σΠ,τ()>1−λ.∀λ∈(0,1)\;:\;∃ _ ∈ _ ^h\;:\;∀ _ O∈ _ ^h, _s_0 _ , _ O(W)>1-λ. Remark 2.2. We may replace the opponents by a single opponent O with action set A=AΣ∖ΠA_ O=A_ . For each fixed team strategy, this does not change the infimum of the winning probability. See the full version. Thus, we assume that there is only one opponent O. We write Λh _ O^h for the strategies of the single opponent and Λ _ O for its memoryless strategies. Let D be the finite set of deterministic memoryless strategies, which we identify with maps τ:S→Aτ S→ A_ O. Since deterministic strategies are sufficient, throughout the paper we assume an opponent response is an element of D. We study the complexity of deciding whether the team wins a given game limit surely. We assume that games are given explicitly. Transition probabilities are rationals encoded in binary, δ is represented by a table indexed by states and complete action profiles, and the objective is specified by its set of target or safe states. The size of the game is the total length of this encoding. 3. Reachability We now focus on the reachability objective =◇TW= T. We assume without loss of generality that each target state is absorbing, that is, δ(t,(a¯,b¯))(t)=1δ(t,( a, b))(t)=1 for every t∈Tt∈ T and action profile (a¯,b¯)∈AΣ( a, b)∈ A_ . Definition 3.0 (Limit-sure reachability problem). Given a reachability game, does the team win limit surely? Brice et al. (Brice et al., 2026b) as well as De Alfaro and Faella (de Alfaro and Faella, 2003) show that almost-sure reachability is NP-complete. The reduction of Brice et al. from the k-clique problem, in particular, produces a game where the team wins almost surely or has value at most 3/43/4 (Brice et al., 2026b, Theorem 4), which also proves NP-hardness for limit-sure reachability. We show in four steps that the problem belongs to NP. First, we show that limit-sure winning can be achieved with team action probabilities given by Puiseux series in ϵε. Second, we show that winning depends only on their leading exponents, called ranks, which can be represented with polynomially many bits. Third, for fixed team and opponent strategies, we check winning by comparing minimum-rank spanning forests. Finally, we give a certificate that uses the team ranks and one opponent response. We check this response through local inequalities in an encoded MDP. These inequalities certify optimality without checking all opponent strategies. We give the full NP proof in the full version. Limit-sure winning Puiseux strategy Polynomial-size action ranks Traps and the forest criterion One stable encoded response Weighted matroid intersection Figure 2. Proof outline for the NP upper bound.Six boxes form a sequence across two rows: limit-sure winning, a Puiseux strategy, polynomial-size action ranks, traps and the forest criterion, one stable encoded response, and weighted matroid intersection. Proposition 3.0 ((Brice et al., 2026b, Theorem 1)). Let t∈[0,1]t∈[0,1]. If some team strategy ensures reachability with probability greater than t against every opponent response, then some memoryless team strategy does. By Proposition 2, restricting the team to memoryless strategies preserves the value. Fixing such a team strategy gives an MDP with an optimal deterministic memoryless opponent strategy. Thus, we restrict attention to memoryless team strategies and deterministic memoryless opponent strategies. 3.1. Puiseux Strategies Limit-sure winning allows the strategy to depend on the error λ. In Example 1, each agent crosses with probability ϵε and hides with probability 1−ϵ1-ε. The winning probability approaches 11 as ϵε goes to zero. Puiseux series describe such a family by a symbolic strategy. Definition 3.0 (Puiseux series). A Puiseux series has the form x=∑i≥i0ciϵi/mx= _i≥ i_0c_iε^i/m, where i0∈ℤi_0 , m∈ℕ>0m _>0, and ci∈ℝc_i . We write K for the field of algebraic Puiseux series. The sign of a nonzero series is the sign of its first nonzero coefficient. Thus, ϵε is a positive infinitesimal, with 0<ϵ<t0<ε<t for every real t>0t>0. For bounded x∈x , its standard part st(x)st(x) is the coefficient of ϵ0ε^0, or zero if absent. We use the following standard properties (Basu et al., 2006). Here, first-order formulas use polynomial equalities and inequalities, logical connectives, and quantifiers. Lemma 3.0 (Puiseux series properties (Basu et al., 2006)). The field K is a real closed ordered extension of ℝR. (i) Transfer. Every first-order sentence with real parameters holds over ℝR if and only if it holds over K. (i) Evaluation. Let x¯=(x1,…,xn)∈n x=(x_1,…,x_n) ^n. Suppose a first-order formula Φ with real parameters satisfies Φ(x¯) ( x) over K. There is a real r0>0r_0>0 such that, for every real 0<r<r00<r<r_0, all series xix_i converge at ϵ=rε=r and Φ(x1(r),…,xn(r)) (x_1(r),…,x_n(r)) holds over ℝR. A Puiseux team strategy is a memoryless strategy with probabilities in K. A Puiseux team strategy σΠ _ is Puiseux-winning if st(ℙs0σΠ,τ(◇T))=1st (P_s_0 _ ,τ( T) )=1 for every opponent response τ∈Dτ∈ D. Lemma 3.0. The team wins limit surely if and only if some Puiseux team strategy is Puiseux-winning. Proof sketch. We express strategy validity by polynomial constraints. We describe reachability values by the least nonnegative solution of (2). Thus, the limit-sure condition is first-order. Transfer with error ϵε gives 1−ϵ<ℙs0σΠ,τ(◇T)≤11-ε<P_s_0 _ ,τ( T)≤ 1 for every τ∈Dτ∈ D. Each probability has standard part 11. Conversely, fix a positive real error λ and a Puiseux-winning strategy. Each success probability is greater than 1−λ1-λ in K. Evaluation gives a real strategy with the same inequalities. One sufficiently small value works for all responses, since D is finite. ∎ We may assume that all strategy exponents are nonnegative integers. Bounded probabilities have no negative exponents. We choose a common denominator d and substitute ϵ=ηdε=η^d. This substitution makes the exponents integers and preserves winning. 3.1.1. Ranks The rank ρ(x)ρ(x) of a nonzero series is its smallest exponent. We put ρ(0)=∞ρ(0)=∞ and min∅=∞ =∞. For nonnegative series, leading coefficients cannot cancel. Hence, ρ(xy) ρ(xy) =ρ(x)+ρ(y),ρ(x+y)=minρ(x),ρ(y), =ρ(x)+ρ(y), ρ(x+y)= \ρ(x),ρ(y)\, ρ(x/y) ρ(x/y) =ρ(x)−ρ(y)if y≠0. =ρ(x)-ρ(y) y≠ 0. We write rp,s,a=ρ(σp(s)(a))r_p,s,a=ρ( _p(s)(a)) for an action rank. Since action probabilities sum to 11, their minimum rank at each (p,s)(p,s) is zero. Conversely, any such ranks are realised by (3) σp(s)(a)=ϵrp,s,a∑a′:rp,s,a′<∞ϵrp,s,a′for all a∈Ap with rp,s,a<∞, _p(s)(a)= ε^r_p,s,a _a :\,r_p,s,a <∞ε^r_p,s,a all a∈ A_p with r_p,s,a<∞, with probability zero for actions of rank ∞. Independence makes profile ranks the sum of action ranks. Against an opponent action b, the transition rank is (4) ρ(s,b,t)=mina¯:δ(s,(a¯,b))(t)>0∑p∈Πrp,s,ap.ρ(s,b,t)= _ a:\,δ(s,( a,b))(t)>0 _p∈ r_p,s,a_p. Example 3.0. The diagram below shows the strategy from Example 1 and its induced MDP. For either opponent action, reaching s_ goal has rank ρ(ϵ(1−ϵ))=1ρ(ε(1-ε))=1, whereas reaching s_ fail has rank ρ(ϵ2)=2ρ(ε^2)=2. Returning to s0s_0 has rank ρ(1−ϵ)=0ρ(1-ε)=0. Thus, success has smaller rank than failure and occurs first with probability tending to 11 as ϵε goes to zero. Boxes show ranks, and black dots mark opponent actions. Absorbing states are double-circled. cross hide agent 1 ϵε 11 1−ϵ1-ε 00 agent 2 ϵε 11 1−ϵ1-ε 00 s0s_0s_ fails_ goal1 scan_12 scan_2ϵ2ε^2 22ϵ(1−ϵ)ε(1-ε) 11ϵ2ε^2 22ϵ(1−ϵ)ε(1-ε) 111−ϵ1-ε 001−ϵ1-ε 0011 00 We use spanning forests to express absorption probabilities. Let R be a set of absorbing states of a finite chain P on V. A spanning forest rooted at R selects one outgoing support edge at each vertex outside R. We require that following the selected edges from any vertex eventually reaches a root in R. If this root is r, we say that the vertex leads to r in the forest. Each root leads to itself. We write ℱF for these forests. For R′⊆R R, we write ℱR′(u)F_R (u) for the forests in which u leads to a root in R′R . The weight and rank of a forest are w(F) w(F) =∏(v,w)∈FP(v,w), = _(v,w)∈ FP(v,w), ρ(F) ρ(F) =∑(v,w)∈Fρ(P(v,w)). = _(v,w)∈ Fρ(P(v,w)). The following lemma combines the classical forest formula (Freidlin and Wentzell, 2012, Chapter 6, Lemma 3.3) with the rank rules. Lemma 3.0. Let P be a finite Puiseux Markov chain on V with absorbing states R. Suppose every state has a support path to R. Then ∑F∈ℱw(F)>0 _F w(F)>0, and for all u∈Vu∈ V and R′⊆R R, (5) ℙuP(◇R′) _u^P( R ) =∑F∈ℱR′(u)w(F)∑F∈ℱw(F), = _F _R (u)w(F) _F w(F), (6) ρ(ℙuP(◇R′)) ρ (P_u^P( R ) ) =minF∈ℱR′(u)ρ(F)−minF∈ℱρ(F). = _F _R (u)ρ(F)- _F ρ(F). Proof sketch. At each nonroot, we choose the first edge of a shortest support path to R. These edges form a forest of positive weight, so the denominator is positive. The classical forest formula (Freidlin and Wentzell, 2012) transfers to K by Lemma 4 and gives (5). Each forest weight has rank ρ(F)ρ(F). Their positive leading coefficients cannot cancel. Thus, each nonzero sum has the minimum rank of its terms. Division subtracts ranks and gives (6). ∎ Example 3.0. The diagram below shows a chain with roots 3,43,4 and its three spanning forests. Bold arrows mark the chosen edges. The forests have weights 1/81/8, 3/83/8, and 1/81/8. Only the last two lead from 11 to 33. By (5), ℙ1P(◇3)=3/8+1/81/8+3/8+1/8=45P_1^P( \3\)= 3/8+1/81/8+3/8+1/8= 45. 1122334412 1234 3412 1214 141111112233441122334411223344w(F)=18w(F)= 1811 leads to 44w(F)=38w(F)= 3811 leads to 33w(F)=18w(F)= 1811 leads to 33 3.1.2. Small ranks A strongly connected component (SCC) is a maximal set of mutually reachable states. A bottom SCC has no outgoing support edge. For each opponent response, we make the bottom SCCs of its chain absorbing. Failure then means reaching a bottom SCC outside T. By (6), this probability is infinitesimal exactly when its forest numerator has a larger minimum rank than the denominator. Thus, winning depends only on the action ranks. Lemma 3.0. Let N=|(p,s,a):p∈Π,s∈S,a∈Ap|N=|\(p,s,a):p∈ ,\ s∈ S,\ a∈ A_p\|. If the team wins limit surely, it has a Puiseux-winning strategy whose finite action ranks are integers between 00 and N/2N^N/2. Proof sketch. We prove it by a system of linear inequalities. We fix the support of a winning strategy. We choose one team profile for each forest edge. The resulting rank is a sum of action ranks, each used at most once. For each opponent response, fix a minimum forest term of the original winning strategy. We require every failure term to exceed this term by at least 11. These inequalities have coefficients in −1,0,1\-1,0,1\. Their right sides are 11. We also keep nonnegativity and the zero ranks. Their right sides are 00. We take a vertex of this nonempty system and scale it to an integer vector. The scaled vector satisfies the same inequalities. Cramer’s rule and Hadamard’s inequality bound its entries by N/2N^N/2. Indeed, at a vertex we select an invertible matrix A∈−1,0,1k×kA∈\-1,0,1\^k× k with k≤Nk≤ N and a right side b∈0,1kb∈\0,1\^k. Multiplying the vertex by |detA|| A| gives integer entries bounded by k/2k^k/2. The multiplier is at least 11, so the inequalities and zero ranks are preserved. Each rank needs O(Nlog(N+1))O(N (N+1)) bits. The realisation in (3) is winning because only ranks matter. ∎ 3.2. Puiseux Markov Decision Processes Different opponent responses may produce different bottom SCCs. We define a failure region that contains every bottom SCC outside the target, under any opponent response. Making this region and the target absorbing gives the same roots for all forest comparisons. 3.2.1. The induced Puiseux MDP We fix action ranks and their realisation as in (3). Let ℳM be the induced MDP, with transitions P(s,b)(t)P(s,b)(t) and ranks as in (4). Each state and action has a successor of rank zero, because its transition probabilities sum to 11. 3.2.2. Traps and the merged MDP An end component is a pair (X,Γ)(X, ), where X is a nonempty set of states and Γ(x) (x) is a nonempty set of opponent actions at each x∈Xx∈ X, such that (1) every action in Γ(x) (x) has all its successors in X, and (2) these actions make X strongly connected. We call (X,Γ)(X, ) a maximal end component (MEC) if X and every Γ(x) (x) are inclusion-maximal. MECs can be computed from an MDP in polynomial time (Chatterjee and Henzinger, 2014). Put =⋃X:(X,Γ) is a MEC and X∩T=∅. Trap= \X:(X, ) is a MEC and X∩ T= \. The opponent can keep the play in Trap once it enters. For example, a non-target state with a deterministic self-loop action belongs to Trap, even if another action reaches the target. We make Trap absorbing and obtain ℳ♯M . We write ℙuτP_u^τ for its probabilities under τ. The next lemma gives the winning criterion. Lemma 3.0. Every response reaches T∪T∪ Trap with probability 11 from every state in ℳ♯M . The strategy σΠ _ is Puiseux-winning if and only if st(ℙs0τ(◇))=0st (P_s_0^τ( Trap) )=0 for every τ∈Dτ∈ D. Proof sketch. Every non-target bottom SCC of a fixed response is contained in a target-free MEC. Thus, the play reaches T∪T∪ Trap with probability 11. Failure in the original MDP implies visiting Trap. Conversely, any response can be changed inside Trap to keep the play there forever. This change preserves the probability of entering Trap. Hence, a response with non-infinitesimal trap probability prevents Puiseux winning. ∎ If s0∈Ts_0∈ T or =∅ Trap= , the strategy wins. If s0∈s_0∈ Trap, or no target is reachable in ℳ♯M , it loses. Otherwise, we merge T into t∗t^* and Trap into f∗f^*. The resulting MDP ℳ M has states V=U∪t∗,f∗V=U∪\t^*,f^*\, where U=S∖(T∪)U=S (T∪ Trap). Ranks into a merged state are the minimum ranks into its members. For example, ρ(u,b,f∗)=minx∈ρ(u,b,x)ρ(u,b,f^*)= _x∈ Trapρ(u,b,x). Its edge set E contains the triples e=(u,b,v)e=(u,b,v) of finite rank. Thus, the team ranks determine the graph for all responses. We fix a response τ:U→Aτ:U→ A_ O. A root-forest is consistent with τ if its edge at u uses τ(u)τ(u). It is trapped if s0s_0 leads to f∗f^* and targeted if s0s_0 leads to t∗t^*. We write ℱτF_τ for the consistent forests. Their minimum trapped and targeted ranks are ρτf∗ _τ^f^* =minρ(F):F∈ℱτ,s0 leads to f∗, = \ρ(F):F _τ,\ s_0 leads to f^*\, ρτt∗ _τ^t^* =minρ(F):F∈ℱτ,s0 leads to t∗. = \ρ(F):F _τ,\ s_0 leads to t^*\. Lemma 3.0. The strategy σΠ _ is Puiseux-winning if and only if ρτf∗>ρτt∗ _τ^f^*> _τ^t^* for every response τ. For a fixed response, both minima are computable in polynomial time. The criterion follows from (6), since the failure probability has rank ρτf∗−minρτf∗,ρτt∗ _τ^f^*- \ _τ^f^*, _τ^t^*\. Each minimum reduces to a minimum-weight directed spanning tree problem (Edmonds, 1967; Chu and Liu, 1965; Tarjan, 1977). For the trapped minimum, we delete t∗t^* and redirect its incoming edges to s0s_0. A consistent forest becomes a tree directed towards f∗f^* exactly when s0s_0 led to f∗f^*. Otherwise, the redirection creates a cycle through s0s_0. We exchange the roots to compute the targeted minimum. Both transformations preserve edge ranks. 3.3. The NP Upper Bound There may be exponentially many opponent responses. For fixed team ranks, an NP oracle can guess a violating response and check it in polynomial time. Guessing the team ranks and asking whether such a response exists gives an NP NP upper bound. To obtain an NP upper bound, we guess the team ranks together with one response in an encoded MDP. We give a criterion that can be checked in polynomial time and certifies that this response is optimal. 3.3.1. The encoded MDP We index the edges of ℳ M as e0,…,em−1e_0,…,e_m-1. For J⊆EJ E, we put ρ^(ei) ρ(e_i) =2m+1ρ(ei)+2i, =2^m+1ρ(e_i)+2^i, ρ^(J) ρ(J) =∑e∈Jρ^(e). = _e∈ J ρ(e). The powers of two distinguish edge sets. Their sum is less than 2m2^m, so the encoding preserves strict comparisons of original ranks. All encoded ranks have polynomially many bits. Let E(u,b)E(u,b) be the edges with source u and label b. We keep the support of ℳ M and replace its probabilities by P~(u,b,v)=ϵρ^(u,b,v)/Zu,b,where Zu,b=∑e∈E(u,b)ϵρ^(e). P(u,b,v)=ε ρ(u,b,v)/Z_u,b, Z_u,b= _e∈ E(u,b)ε ρ(e). Other probabilities are zero and the roots are absorbing. The encoded ranks are exponents before normalisation. For a response τ, let qvτq_v^τ be its probability of reaching f∗f^* in this encoded MDP. The opponent maximises this probability. We write ℱτ(v)F_τ(v) for the forests leading from v to f∗f^*. We put Nvτ=∑F∈ℱτ(v)ϵρ^(F),Dτ=∑F∈ℱτϵρ^(F).N_v^τ= _F _τ(v)ε ρ(F),\ D^τ= _F _τε ρ(F). Each forest uses one edge per nonroot. Thus, every forest weight has the same normalising factors, which cancel in (5). Since Dτ>0D^τ>0, we obtain qvτ=Nvτ/Dτq_v^τ=N_v^τ/D^τ. 3.3.2. One stable response suffices A response τ is stable if (7) quτ≥∑v∈VP~(u,b,v)qvτfor all u∈U and b∈A.q_u^τ≥ _v∈ V P(u,b,v)q_v^τ all u∈ U and b∈ A_ O. The right side is the value of playing b once and then following τ. Equality holds for b=τ(u)b=τ(u). These local inequalities suffice because every response has a support path to a root from each state. Lemma 3.0. A stable response exists. Every stable response is optimal from every state. Proof sketch. We use a minimum principle: if d∈Vd ^V is zero at the roots and satisfies du≥∑vP~(u,τ(u),v)dvd_u≥ _v P(u,τ(u),v)d_v for all u∈Uu∈ U, then d≥0d≥ 0. Otherwise, a negative minimum would propagate along a support path to a root, where d is zero. Fix a stable response τ and any response τ′τ . Stability and the reachability equations show that d=qτ−qτ′d=q^τ-q^τ satisfies the minimum principle under τ′τ . Hence, qτ≥qτ′q^τ≥ q^τ , so τ is optimal. For existence, choose a response maximising ∑vqvτ _vq_v^τ. Such a response exists because there are finitely many responses. If stability fails at (u,b)(u,b), switch the action at u to b. The minimum principle shows that no value decreases. The strict improvement at (u,b)(u,b) gives a larger value at u. This contradicts maximality of the sum. ∎ Lemma 3.0. The team strategy is Puiseux-winning if and only if there exists a stable encoded response τ such that ρτf∗>ρτt∗ _τ^f^*> _τ^t^*. Proof sketch. By Lemma 11, the team strategy is Puiseux-winning only when every response satisfies the forest criterion. If this holds, we choose a stable response using Lemma 12. For the converse, we show that any response violating the criterion has a larger encoded failure probability than every response satisfying it. The encoding multiplies each forest rank by 2m+12^m+1 and adds a number between 00 and 2m−12^m-1. Applying (6) therefore gives ρτf∗≤ρτt∗ _τ^f^*≤ _τ^t^* ⟹ρ(qs0τ)≤2m−1, ρ(q_s_0^τ)≤ 2^m-1, ρτf∗>ρτt∗ _τ^f^*> _τ^t^* ⟹ρ(qs0τ)≥2m+1. ρ(q_s_0^τ)≥ 2^m+1. Here, ρ(0)=∞ρ(0)=∞ also covers the case where no forest leads from s0s_0 to f∗f^*. A positive Puiseux value with smaller rank is larger. Thus, a response violating the criterion has a larger failure probability than one satisfying it. Now suppose a stable response satisfies the criterion. If another response violated it, that response would have a larger failure probability. This contradicts the optimality of the stable response from Lemma 12. Hence every response satisfies the criterion, and the team strategy is Puiseux-winning. ∎ 3.3.3. Checking stability in polynomial time We define the Bellman residual as Rτ(u,b)=quτ−∑v∈VP~(u,b,v)qvτR^τ(u,b)=q_u^τ- _v∈ V P(u,b,v)q_v^τ. Stability requires all residuals to be nonnegative. The residual is zero for b=τ(u)b=τ(u). Fix b≠τ(u)b≠τ(u). For each forest F, we put χF(v)=1 _F(v)=1 if v leads to f∗f^*, and 00 otherwise. Substituting qvτ=Nvτ/Dτq_v^τ=N_v^τ/D^τ gives Zu,bDτRτ(u,b) Z_u,bD^τR^τ(u,b) =∑eϵρ^(e)(Nuτ−Nvτ) = _eε ρ(e)(N_u^τ-N_v^τ) =∑e,F(χF(u)−χF(v))ϵρ^(F)+ρ^(e). = _e,F( _F(u)- _F(v))ε ρ(F)+ ρ(e). Here, e=(u,b,v)e=(u,b,v) ranges over E(u,b)E(u,b) and F over ℱτF_τ. If u,vu,v lead to the same root, the coefficient is zero. Otherwise, adding e joins the two trees of F into one tree. Its coefficient is +1+1 if u leads to f∗f^* and −1-1 otherwise. Let (τ,u,b)T(τ,u,b) contain the spanning trees of the underlying undirected graph that select one edge from each E(z,τ(z))E(z,τ(z)), for z∈Uz∈ U, and one from E(u,b)E(u,b). We retain edge labels. Deleting the latter edge recovers the forest, so these trees correspond to the nonzero terms above. Writing sgn(T)sgn(T) for their coefficients gives (8) Zu,bDτRτ(u,b)=∑T∈(τ,u,b)sgn(T)ϵρ^(T).Z_u,bD^τR^τ(u,b)= _T (τ,u,b)sgn(T)ε ρ(T). Without encoding, minimum-rank trees may cancel out. Encoded ranks are distinct, so the unique minimum tree determines the residual sign, since Zu,bDτ>0Z_u,bD^τ>0. If no tree exists, the residual is zero. Example 3.0. Let U=u,vU=\u,v\ and s0=us_0=u. Action a takes u to v. Action b at u and the only action c at v each have both roots as successors. Below, ei:de_i:d labels edge eie_i of action d. Double circles mark absorbing roots, whose self-loops are omitted. uuvvf∗f^*t∗t^*e0:ae_0:ae1:ce_1:ce2:ce_2:ce3:be_3:be4:be_4:b i01234ρ(ei)01010ρ^(ei)16647216 array[]c|ri&0&1&2&3&4\\ ρ(e_i)&0&1&0&1&0\\ ρ(e_i)&1&66&4&72&16 array Here m=5m=5, so ρ^(ei)=64ρ(ei)+2i ρ(e_i)=64ρ(e_i)+2^i. Suppose τ(u)=aτ(u)=a and τ(v)=cτ(v)=c. Its two forests are Ff∗=e0,e1F_f^*=\e_0,e_1\ and Ft∗=e0,e2F_t^*=\e_0,e_2\. They send u through v to f∗f^* and t∗t^*, respectively. We check action b at u. Adding e3e_3 to Ff∗F_f^* or e4e_4 to Ft∗F_t^* creates an undirected cycle. In both cases, the endpoints already lead to the same root, so the term is zero. The other pairs give the positive tree T+=e0,e1,e4T_+=\e_0,e_1,e_4\ of encoded rank 8383 and the negative tree T−=e0,e2,e3T_-=\e_0,e_2,e_3\ of encoded rank 7777. Both have original rank 11, so their terms without encoding cancel as ϵ−ϵ=0ε-ε=0. After encoding, (8) gives Zu,bDτRτ(u,b)=ϵ83−ϵ77<0Z_u,bD^τR^τ(u,b)=ε^83-ε^77<0. Thus, τ is not stable. Switching to b at u reverses the tree signs when we check a. The new response τ′τ is therefore stable. Its original forest ranks satisfy ρτ′f∗=1>0=ρτ′t∗ _τ ^f^*=1>0= _τ ^t^*, giving the certificate in Lemma 13. Lemma 3.0. Residual signs can be checked in polynomial time. Proof sketch. We restrict the edges to the prescribed groups. Selecting at most one edge per group is a partition matroid constraint. Having no undirected cycle is a graphic matroid constraint. Loops and pairs of parallel edges count as cycles. There are |U|+1=|V|−1|U|+1=|V|-1 groups. Thus, common independent sets of this size select one edge per group and form spanning trees. Weighted matroid intersection finds a tree of minimum encoded rank or reports none exists in polynomial time (Schrijver, 2003). We delete its edge from E(u,b)E(u,b) and follow the forest from u to determine its sign. Equation (8) gives the residual sign. The encoded ranks have polynomial bit length. We check polynomially many residuals. ∎ Algorithm 1 Nondeterministic Algorithm for Limit-Sure Reachability 1: Input: A game G, an initial state s0s_0, and targets T. 2: Output: Accept limit-sure winning or reject 3: Guess rp,s,a∈0,…,B∪∞r_p,s,a∈\0,…,B\∪\∞\ for every (p,s,a)(p,s,a). 4: Reject if minarp,s,a≠0 _ar_p,s,a≠ 0 for some (p,s)(p,s). 5: Build the support and transition ranks of ℳM using (4). 6: Compute Trap as the union of target-free MECs. 7: Accept if s0∈Ts_0∈ T or =∅ Trap= . 8: Make Trap absorbing to obtain ℳ♯M . 9: Reject if s0∈s_0∈ Trap or no path from s0s_0 reaches T in ℳ♯M . 10: Merge T into t∗t^* and Trap into f∗f^* to obtain ℳ M. 11: Compute the encoded edge ranks ρ ρ for the encoded MDP. 12: Guess one action τ(u)∈Aτ(u)∈ A_ O at each u∈Uu∈ U. 13: Check all residual signs using Lemma 15. 14: Reject if Rτ(u,b)<0R^τ(u,b)<0 for any (u,b)∈U×A(u,b)∈ U× A_ O. 15: Using the original ranks ρ, compute the minimum trapped rank ρτf∗ _τ^f^* and targeted rank ρτt∗ _τ^t^* by Lemma 11. 16: Accept if ρτf∗>ρτt∗ _τ^f^*> _τ^t^*, otherwise reject. Theorem 16. The limit-sure reachability problem is NP-complete. Proof. Hardness follows from (de Alfaro and Faella, 2003; Brice et al., 2026b). For the upper bound, we use Algorithm 1 with B=N/2B=N^N/2. Running time. Each rank has O(Nlog(N+1))O(N (N+1)) bits. The guessed response has one action at each nonroot. The graph and encoded ranks have polynomial size. There are at most |U||A||U|\,|A_ O| stability checks. Every check takes polynomial time by Lemma 15. Soundness. If a run accepts, the preprocessing conditions or Lemma 13 give a Puiseux-winning strategy. In the latter case, all residuals are nonnegative and the final forest comparison holds. The team wins limit surely by Lemma 5. Completeness. If the team wins limit surely, Lemma 9 gives winning ranks bounded by B. A run guesses them. Their normalised-power realisation is winning because only ranks matter. It either accepts during preprocessing or accepts with a stable response by Lemma 13. ∎ 4. Safety We now consider the safety objective =□CW= C, where C⊆SC S is the set of safe states. Unlike for reachability, we show limit-sure and almost-sure winning are equivalent. This extends the two-player result (Chatterjee et al., 2012) to teams without shared randomness. The two-player proof constructs a memoryless almost-sure winning optimal strategy from a fixed-point characterisation of the game value. We instead use a compactness argument on the space of team strategies. We only show that an almost-sure winning strategy exists if there exists a limit-sure winning strategy. We equip ΛΠh _ ^h with the product topology on the action probabilities σp(h)(a) _p(h)(a), which makes it a compact set. The proof uses compactness to obtain a strategy that meets all safety thresholds below 11. We give the necessary topological results in the full version. Theorem 1. For a game with a safety objective, the team wins limit surely if and only if it wins almost surely. Proof sketch. Almost-sure winning implies limit-sure winning. For the converse, suppose that the team wins limit surely. For each integer m≥2m≥ 2, let KmK_m be the set of team strategies that guarantee safety probability at least 1−1/m1-1/m against every opponent strategy. Each KmK_m is nonempty by limit-sure winning. It is closed because it is an intersection of closed sets, one for each opponent strategy. The sets decrease as m increases. Compactness therefore gives a strategy σΠ∗∈⋂m≥2Km _ ^*∈ _m≥ 2K_m. Against every opponent strategy, this strategy guarantees safety probability at least 1−1/m1-1/m for every m≥2m≥ 2. The probability must be 11, so σΠ∗ _ ^* is almost-sure winning. ∎ Almost-sure and sure winning also coincide for safety (Brice et al., 2026b). Hence all three winning conditions are equivalent. Moreover, sure safety can be decided in polynomial time (Brice et al., 2026b). Thus, the limit-sure safety problem is also decidable in polynomial time. 5. Individually Randomised ATL Brice et al. (Brice et al., 2026b, Section 6) introduced Individually Randomised ATL (IRATL) to express what coalitions can achieve with individual or shared sources of randomness. We recall its qualitative fragment and apply our results to its model-checking problem. Let G be a game structure without a fixed team, initial state or objective, and let L:S→2QL S→ 2^Q label its states with atomic propositions from Q. State formulas and path formulas are given by φ ::=q|¬φ∣φ∨φ∣⟨C⟩wrθ, ::=q \! C \! _w^rθ, θ θ ::=○φ∣□φ∣φ, ::= \, U\, , where q∈Qq∈ Q, C⊆ΣC , r∈,r∈\ ind, sh\, and w∈,,w∈\ sure, almost, limit\. The logic as introduced also has a quantitative fragment that uses thresholds. However, we restrict our attention to the qualitative fragment with sure, almost-sure, and limit-sure winning. The formula ⟨C⟩wrθ \! C \! _w^rθ holds at s if the coalition C wins the objective described by θ from s with winning condition w and randomisation type r. For r=r= ind, coalition strategies have the product form of Definition 2; for r=r= sh, the coalition chooses a distribution over ACA_C. Semantically, almost-sure and limit-sure winning are as in Definitions 7 and 8, and sure winning requires every play compatible with the chosen strategies and the transition supports to satisfy the objective against every response of the opponents, even if the play has probability 00. On a play s0s1⋯s^0s^1·s, the semantics of ○φ requires φ at s1s^1. The semantics of □φ requires that φ holds at every state, and φψ \, U\,ψ requires ψ at some sks^k and φ at every sjs^j with j<kj<k. Theorem 1. Model checking qualitative IRATL on explicitly represented finite stochastic game structures is P NP-complete. Proof sketch. For each state subformula, we recursively compute the set of states where it is true. Once these sets are known, formulas of the form ○φ and □φ can be checked in polynomial time. Evaluating if a formula of the form φ1φ2 _1\, U\, _2 holds reduces to solving reachability by making target states and states containing ¬φ1 _1 absorbing. For both shared and individual randomisation, sure reachability is in P. Similarly, almost-sure reachability with individual randomisation is in NP (Brice et al., 2026b). Limit-sure reachability is in NP by Theorem 16. Moreover, shared randomisation reduces to the classical two-player games that can be solved in P. There are at most |S|⋅|Sub(φ)||S|·|Sub( )| pairs of states and subformulas. Therefore, they can be solved by a deterministic polynomial-time algorithm with an NP oracle. The hardness follows from an involved reduction from sequentially nested satisfiability (SNSAT), which is P NP-complete (Laroussinie et al., 2001). In fact, the hardness reduction requires only a team of size 2, and it holds even for game structures with deterministic transitions and for the fragment restricted to the sure and almost-sure modalities of the logic. We give the details in the full version. ∎ 6. Conclusions We showed that limit-sure reachability for teams without shared randomness is in NP, and hence NP-complete, and that for safety objectives limit-sure, almost-sure, and sure winning coincide and can be decided in polynomial time. We focus now on some future directions of research. Firstly, for two players, limit-sure winning is well understood for Büchi, co-Büchi and parity conditions (Chatterjee et al., 2011). Our proof for reachability, however, relies on memoryless team strategies being sufficient (Brice et al., 2026b), and we do not know whether this is true for other objectives. Secondly, there are models between full sharing and no sharing: subteams that share a source of randomness, a correlation device used only before the play (Aumann, 1974; Celli and Gatti, 2018), a few shared random bits (Newman, 1991), or a full structure of shared randomness (Brice et al., 2026a). Thirdly, the certificate of Section 3.3 may also be useful outside team games. Perturbing ranks so that all forests get distinct weights, guessing a stable response, and checking residual signs replace a check over exponentially many opponent strategies by a polynomial-time test. Similar checks arise in the analysis of perturbed Markov chains (Solan, 2003), and in limit-sure problems for POMDPs with bounded memory (Asadi et al., 2025), in particular once an adversary is added. Finally, as future work, we propose extending PRISM-games (Kwiatkowska et al., 2020) and MCMAS (Lomuscio et al., 2017), which still merge a coalition into one player. As our certificates are small and checked in polynomial time, these tools could support individually randomised coalitions by using a SAT or ILP solver to obtain the ranks using our proposed techniques. References Alur et al. (2002) Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. 2002. Alternating-time Temporal Logic. Journal of the ACM 49, 5 (2002), 672–713. https://doi.org/10.1145/585265.585270 Aminof et al. (2019) Benjamin Aminof, Marta Kwiatkowska, Bastien Maubert, Aniello Murano, and Sasha Rubin. 2019. Probabilistic strategy logic. In Proceedings of the 28th International Joint Conference on Artificial Intelligence (Macao, China) (IJCAI’19). AAAI Press, 32–38. Asadi et al. (2025) Ali Asadi, Krishnendu Chatterjee, Raimundo Saona, and Ali Shafiee. 2025. Limit-sure Reachability for Small Memory Policies in POMDPs is NP-complete. In Proceedings of the Forty-first Conference on Uncertainty in Artificial Intelligence (Proceedings of Machine Learning Research, Vol. 286). PMLR, 238–256. https://proceedings.mlr.press/v286/asadi25b.html Aumann (1974) Robert J. Aumann. 1974. Subjectivity and correlation in randomized strategies. Journal of Mathematical Economics 1, 1 (1974), 67–96. Basilico et al. (2017) Nicola Basilico, Andrea Celli, Giuseppe De Nittis, and Nicola Gatti. 2017. Team-Maxmin Equilibrium: Efficiency Bounds and Algorithms. In AAAI 2017. AAAI Press, 356–362. https://doi.org/10.1609/AAAI.V31I1.10560 Basu et al. (2006) Saugata Basu, Richard Pollack, and Marie-Françoise Roy. 2006. Algorithms in Real Algebraic Geometry (2nd ed.). Algorithms and Computation in Mathematics, Vol. 10. Springer. Bernstein et al. (2002) Daniel S. Bernstein, Robert Givan, Neil Immerman, and Shlomo Zilberstein. 2002. The complexity of decentralized control of Markov decision processes. Mathematics of Operations Research 27, 4 (2002), 819–840. Bewley and Kohlberg (1976) Truman Bewley and Elon Kohlberg. 1976. The asymptotic theory of stochastic games. Mathematics of Operations Research 1, 3 (1976), 197–208. Brice et al. (2026b) Léonard Brice, Thomas A. Henzinger, Alipasha Montaseri, Ali Shafiee, and K. S. Thejaswini. 2026b. Randomise Alone, Reach as a Team. In Computer Aided Verification, Eva Darulova, Anthony W. Lin, and Philipp Rümmer (Eds.). Springer Nature Switzerland, Cham, 215–236. Brice et al. (2026a) Léonard Brice, Thomas A. Henzinger, and K. S. Thejaswini. 2026a. Dicey Games: Shared Sources of Randomness in Distributed Systems. In Logic in Computer Science (LICS 2026) (LIPIcs, Vol. 380). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 23:1–23:26. https://doi.org/10.4230/LIPIcs.LICS.2026.23 Celli and Gatti (2018) Andrea Celli and Nicola Gatti. 2018. Computational results for extensive-form adversarial team games. In Proceedings of the 32nd AAAI Conference on Artificial Intelligence. AAAI Press, 965–972. https://doi.org/10.1609/aaai.v32i1.11462 Chatterjee et al. (2011) Krishnendu Chatterjee, Luca De Alfaro, and Thomas A. Henzinger. 2011. Qualitative concurrent parity games. ACM Trans. Comput. Logic 12, 4, Article 28 (July 2011), 51 pages. https://doi.org/10.1145/1970398.1970404 Chatterjee et al. (2012) Krishnendu Chatterjee, Luca de Alfaro, and Thomas A. Henzinger. 2012. Strategy improvement for concurrent reachability and safety games. CoRR abs/1201.2834 (2012). Chatterjee and Henzinger (2014) Krishnendu Chatterjee and Monika Henzinger. 2014. Efficient and dynamic algorithms for alternating Büchi games and maximal end-component decomposition. J. ACM 61, 3 (2014), 15:1–15:40. Chen and Lu (2007) Taolue Chen and Jian Lu. 2007. Probabilistic Alternating-time Temporal Logic and Model Checking Algorithm. In Fourth International Conference on Fuzzy Systems and Knowledge Discovery (FSKD 2007), Volume 2. IEEE Computer Society, 35–39. https://doi.org/10.1109/FSKD.2007.458 Chu and Liu (1965) Yoeng-Jin Chu and Tseng-Hong Liu. 1965. On the shortest arborescence of a directed graph. Scientia Sinica 14 (1965), 1396–1400. Courcoubetis and Yannakakis (1995) Costas Courcoubetis and Mihalis Yannakakis. 1995. The complexity of probabilistic verification. J. ACM 42, 4 (1995), 857–907. de Alfaro (1997) Luca de Alfaro. 1997. Formal Verification of Probabilistic Systems. Ph. D. Dissertation. Stanford University. de Alfaro and Faella (2003) Luca de Alfaro and Marco Faella. 2003. Information Flow in Concurrent Games. In ICALP 2003 (Lecture Notes in Computer Science, Vol. 2719). Springer, 1038–1053. https://doi.org/10.1007/3-540-45061-0_80 de Alfaro et al. (1998) Luca de Alfaro, Thomas A. Henzinger, and Orna Kupferman. 1998. Concurrent Reachability Games. In 39th Annual Symposium on Foundations of Computer Science (FOCS 1998). IEEE Computer Society, 564–575. https://doi.org/10.1109/SFCS.1998.743507 de Alfaro et al. (2007) Luca de Alfaro, Thomas A. Henzinger, and Orna Kupferman. 2007. Concurrent reachability games. Theoretical Computer Science 386, 3 (2007), 188–217. Edmonds (1967) Jack Edmonds. 1967. Optimum branchings. Journal of Research of the National Bureau of Standards, Section B 71B, 4 (1967), 233–240. Etessami and Yannakakis (2015) Kousha Etessami and Mihalis Yannakakis. 2015. Recursive Markov Decision Processes and Recursive Stochastic Games. J. ACM 62, 2, Article 11 (May 2015), 69 pages. https://doi.org/10.1145/2699431 Everett (1957) Hugh Everett. 1957. Recursive games. In Contributions to the Theory of Games, Volume I. Annals of Mathematics Studies, Vol. 39. Princeton University Press, 47–78. Farina et al. (2018) Gabriele Farina, Andrea Celli, Nicola Gatti, and Tuomas Sandholm. 2018. Ex ante coordination and collusion in zero-sum multi-player extensive-form games. In Advances in Neural Information Processing Systems, S. Bengio, H. Wallach, H. Larochelle, K. Grauman, N. Cesa-Bianchi, and R. Garnett (Eds.), Vol. 31. Curran Associates, Inc. https://proceedings.neurips.c/paper_files/paper/2018/file/c17028c9b6e0c5deaad29665d582284a-Paper.pdf Frank (1981) András Frank. 1981. A weighted matroid intersection algorithm. Journal of Algorithms 2, 4 (1981), 328–336. Freidlin and Wentzell (2012) Mark I. Freidlin and Alexander D. Wentzell. 2012. Random Perturbations of Dynamical Systems (3rd ed.). Grundlehren der mathematischen Wissenschaften, Vol. 260. Springer. Gimbert and Oualhadj (2010) Hugo Gimbert and Youssouf Oualhadj. 2010. Probabilistic Automata on Finite Words: Decidable and Undecidable Problems. In ICALP 2010 (Lecture Notes in Computer Science, Vol. 6199). Springer, 527–538. https://doi.org/10.1007/978-3-642-14162-1_44 Hansen et al. (2009) Kristoffer Arnsfelt Hansen, Michal Koucký, and Peter Bro Miltersen. 2009. Winning concurrent reachability games requires doubly-exponential patience. In Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science (LICS). IEEE Computer Society, 332–341. Kalogiannis et al. (2023) Fivos Kalogiannis, Ioannis Anagnostides, Ioannis Panageas, Emmanouil V. Vlatakis-Gkaragkounis, Vaggos Chatziafratis, and Stelios Andrew Stavroulakis. 2023. Efficiently Computing Nash Equilibria in Adversarial Team Markov Games. In ICLR 2023. OpenReview.net. https://openreview.net/forum?id=mjzm6btqgV Kwiatkowska et al. (2020) Marta Kwiatkowska, Gethin Norman, David Parker, and Gabriel Santos. 2020. PRISM-games 3.0: Stochastic game verification with concurrency, equilibria and time. In Computer Aided Verification (CAV) (Lecture Notes in Computer Science, Vol. 12225). Springer, 475–487. https://doi.org/10.1007/978-3-030-53291-8_25 Laroussinie et al. (2008) François Laroussinie, Nicolas Markey, and Ghassan Oreiby. 2008. On the Expressiveness and Complexity of ATL. Logical Methods in Computer Science 4, 2, Article 7 (2008), 25 pages. https://doi.org/10.2168/LMCS-4(2:7)2008 Laroussinie et al. (2001) François Laroussinie, Nicolas Markey, and Philippe Schnoebelen. 2001. Model Checking CTL+ and FCTL Is Hard. In Foundations of Software Science and Computation Structures (Lecture Notes in Computer Science, Vol. 2030). Springer, 318–331. https://doi.org/10.1007/3-540-45315-6_21 Lomuscio et al. (2017) Alessio Lomuscio, Hongyang Qu, and Franco Raimondi. 2017. MCMAS: an open-source model checker for the verification of multi-agent systems. Int. J. Softw. Tools Technol. Transf. 19, 1 (2017), 9–30. https://doi.org/10.1007/S10009-015-0378-X Newman (1991) Ilan Newman. 1991. Private vs. common random bits in communication complexity. Inform. Process. Lett. 39, 2 (1991), 67–71. Norris (1998) James R. Norris. 1998. Markov Chains. Cambridge University Press. Oliehoek and Amato (2016) Frans A. Oliehoek and Christopher Amato. 2016. A Concise Introduction to Decentralized POMDPs. Springer. Schaefer et al. (2024) Marcus Schaefer, Jean Cardinal, and Tillmann Miltzow. 2024. The Existential Theory of the Reals as a Complexity Class: A Compendium. CoRR abs/2407.18006 (2024). https://doi.org/10.48550/ARXIV.2407.18006 arXiv:2407.18006 Schrijver (2003) Alexander Schrijver. 2003. Combinatorial Optimization: Polyhedra and Efficiency. Algorithms and Combinatorics, Vol. 24. Springer. Solan (2003) Eilon Solan. 2003. Perturbations of Markov Chains with Applications to Stochastic Games. In Stochastic Games and Applications, Abraham Neyman and Sylvain Sorin (Eds.). NATO Science Series, Vol. 570. Springer, Dordrecht, 265–280. https://doi.org/10.1007/978-94-010-0189-2_17 Tarjan (1977) Robert E. Tarjan. 1977. Finding optimum branchings. Networks 7, 1 (1977), 25–35. von Stengel and Koller (1997) Bernhard von Stengel and Daphne Koller. 1997. Team-maxmin equilibria. Games and Economic Behavior 21, 1–2 (1997), 309–321. https://doi.org/10.1006/game.1997.0527 Young (1993) H. Peyton Young. 1993. The Evolution of Conventions. Econometrica 61, 1 (1993), 57–84. https://doi.org/10.2307/2951778 Zhang et al. (2021b) Kaiqing Zhang, Zhuoran Yang, and Tamer Başar. 2021b. Multi-agent reinforcement learning: A selective overview of theories and algorithms. In Handbook of Reinforcement Learning and Control. Springer, 321–384. https://doi.org/10.1007/978-3-030-60990-0_12 Zhang et al. (2021a) Youzhi Zhang, Bo An, and Jakub Černý. 2021a. Computing ex ante coordinated team-maxmin equilibria in zero-sum multiplayer extensive-form games. In Proceedings of the 35th AAAI Conference on Artificial Intelligence. AAAI Press, 5813–5821. Appendix A Preliminaries Lemma A.0. Let W be a reachability or safety objective. For every team strategy σΠ∈ΛΠh _ ∈ _ ^h, infτ∈ΛΣ∖Πhℙs0σΠ,τ()=infτ∈Λhℙs0σΠ,τ(). _ _ O∈ _ ^hP_s_0 _ , _ O(W)= _τ∈ _ O^hP_s_0 _ ,τ(W). Proof. Fix σΠ _ . Let hD^h be the set of deterministic strategies d:S+→Ad S^+→ A_ O. Each d∈hd ^h can be implemented by the original opponents without shared randomness. At each history, each opponent plays its component of d(h)d(h). Conversely, the single opponent can implement any tuple of strategies of the original opponents by using their product distribution. Hence, infτ∈Λhℙs0σΠ,τ() _τ∈ _ O^hP_s_0 _ ,τ(W) ≤infτ∈ΛΣ∖Πhℙs0σΠ,τ() ≤ _ _ O∈ _ ^hP_s_0 _ , _ O(W) ≤infd∈hℙs0σΠ,d(). ≤ _d ^hP_s_0 _ ,d(W). For the reverse inequality, fix τ∈Λhτ∈ _ O^h. Independently for each history h, sample d(h)d(h) according to τ(h)τ(h). Since the set of histories is countable, these choices define a product probability measure μ on hD^h. Each history is visited at most once along a play. Thus, averaging over d gives the same probability for every finite state sequence as playing τ. For reachability, let nW_n require a visit to the target by time n. For safety, let nW_n require that all states through time n are safe. In both cases, the probabilities of nW_n converge to those of W. Therefore, ℙs0σΠ,τ() _s_0 _ ,τ(W) =limn→∞ℙs0σΠ,τ(n) = _n→∞P_s_0 _ ,τ(W_n) =limn→∞∫hℙs0σΠ,d(n)μ(d) = _n→∞ _D^hP_s_0 _ ,d(W_n)\,dμ(d) (equality on finite prefixes) =∫hℙs0σΠ,d()μ(d) = _D^hP_s_0 _ ,d(W)\,dμ(d) (bounded convergence) ≥infd∈hℙs0σΠ,d() ≥ _d ^hP_s_0 _ ,d(W) (an average is at least the infimum). Taking the infimum over τ proves the reverse inequality and hence the claim. ∎ Appendix B Reachability We now focus on the reachability objective =◇TW= T. We assume that each target state is absorbing, that is, δ(t,(a¯,b¯))(t)=1δ(t,( a, b))(t)=1 for all t∈Tt∈ T and (a¯,b¯)∈AΣ( a, b)∈ A_ . This assumption is without loss of generality, because a play satisfies ◇T T as soon as it visits T. Definition B.0 (Limit-sure reachability problem). Given a game G with a reachability objective, decide whether the team wins limit surely. Brice et al. (Brice et al., 2026b) show that deciding whether the team wins almost surely is NP-complete for reachability objectives. They prove the NP-hardness by a reduction from the k-clique problem. In the games it produces, the team either wins almost surely or has value at most 3/43/4 (Brice et al., 2026b, Theorem 4). The same reduction therefore shows that the limit-sure reachability problem is NP-hard. We show in four steps that the problem belongs to NP. First, we represent the family of team strategies that limit-sure winning requires by a single strategy whose probabilities are series in an infinitesimal ϵε, which are called Puiseux series. Second, we show that whether this strategy wins depends only on the exponents of the leading terms of its probabilities, which we call ranks. Third, we show that once both strategies of the team and the opponent are fixed, deciding whether the resulting Markov chain reaches T with probability infinitesimally close to 11 takes polynomial time, by comparing directed minimum-weight spanning forests. Finally, we show that a certificate consisting of the team ranks and an optimal opponent strategy in an encoded structure has polynomial size and can be checked in polynomial time. Therefore, solving the main problem is in NP. First, we build on a result of Brice et al. (Brice et al., 2026b), which shows that memoryless team strategies suffice. Proposition B.0 ((Brice et al., 2026b, Theorem 1)). Let G be a game with objective ◇T T, and let t∈[0,1]t∈[0,1]. If some team strategy ensures that the play reaches T with probability greater than t against every tuple of strategies of the opponents, then some memoryless team strategy does. By Proposition 2, restricting the team to memoryless strategies leaves the value unchanged. Fixing such a strategy gives the MDP of Definition 5. For the reachability objective, this MDP has an optimal deterministic memoryless opponent strategy. Thus, in the rest of this section, we restrict attention to memoryless team strategies and opponent responses in D. B.1. Puiseux Strategies Limit-sure winning allows the team strategy to depend on the required accuracy. In Example 1, each agent crosses with probability ϵε and hides with probability 1−ϵ1-ε. The team’s winning probability approaches 11 as ϵε tends to zero. We represent such a family by a single symbolic strategy whose probabilities depend on a positive parameter ϵε standing for “an arbitrarily small positive number”. Puiseux series make this idea precise. Their use in the analysis of stochastic games goes back to Bewley and Kohlberg (Bewley and Kohlberg, 1976). Definition B.0 (Puiseux series). A Puiseux series is a series x=∑i≥i0ciϵi/mx= _i≥ i_0c_iε^i/m with i0∈ℤi_0 , m∈ℕ>0m _>0, and ci∈ℝc_i for each integer i. It is algebraic if Q(ϵ,x)=0Q(ε,x)=0 for some nonzero polynomial Q∈ℝ[ϵ,X]Q [ε,X]. In other words, a Puiseux series may have fractional exponents with a common denominator, but only finitely many negative exponents. For example, x=1−ϵ1/2x=1-ε^1/2 is a Puiseux series with the fractional exponent 1/21/2. It is algebraic because it satisfies (1−x)2−ϵ=0(1-x)^2-ε=0. In our setting, such series describe probabilities that depend on a positive parameter tending to zero. Let K denote the field of algebraic Puiseux series. We write a nonzero x∈x as x=∑i≥i0ciϵi/mx= _i≥ i_0c_iε^i/m with ci0≠0c_i_0≠ 0, and call ci0c_i_0 its leading coefficient. We order K by x>0⇔ci0>0,x<y⇔y−x>0.x>0 c_i_0>0, x<y y-x>0. This order extends the order on ℝR and makes ϵε a positive infinitesimal, that is, 0<ϵ<t0<ε<t for every real t>0t>0. For x∈x bounded in absolute value by a real number, its standard part is st(x)=c0∈ℝst(x)=c_0 , with c0=0c_0=0 if ϵ0ε^0 does not occur in x. The following classical properties justify reasoning with these symbolic quantities (Basu et al., 2006). Here a first-order formula in the language of ordered fields is built from polynomial equalities and inequalities using logical connectives and quantifiers over field elements. A sentence is such a formula with no free variables. An ordered field is real closed if every positive element has a square root and every polynomial of odd degree has a root. Lemma B.0 (Puiseux series properties). (i) Ordered field and standard parts: with the order defined above, K is a real closed ordered field extending ℝR. For every x∈x bounded in absolute value by a real number, st(x)st(x) is the unique a∈ℝa such that |x−a|<t|x-a|<t for every real t>0t>0. (i) Transfer: every first-order sentence in the language of ordered fields, with real parameters, holds over ℝR if and only if it holds over K. (i) Evaluation: every x∈x converges at ϵ=rε=r for all sufficiently small real r>0r>0, and we write x(r)∈ℝx(r) for its value. Let Φ be a first-order formula with real parameters and x¯=(x1,…,xn)∈n x=(x_1,…,x_n) ^n. If Φ(x¯) ( x) holds over K, then Φ(x¯(r)) ( x(r)) holds over ℝR for all sufficiently small real r>0r>0, where x¯(r)=(x1(r),…,xn(r))∈ℝn x(r)=(x_1(r),…,x_n(r)) ^n. Real closedness is the property of K that makes transfer in part (i) hold. For our purposes, transfer lets us replace arbitrarily accurate real strategies by one symbolic strategy. Evaluation then turns that symbolic strategy back into real strategies by choosing a sufficiently small positive parameter. Definition B.0 (Puiseux team strategy). A Puiseux team strategy is a memoryless team strategy with probabilities in K rather than ℝR. It is a tuple σΠ=(σp)p∈Π _ =( _p)_p∈ with σp:S→Ap _p S ^A_p, σp(s)(a)≥0 _p(s)(a)≥ 0 for all s∈Ss∈ S and a∈Apa∈ A_p, and ∑a∈Apσp(s)(a)=1 _a∈ A_p _p(s)(a)=1 for all s∈Ss∈ S. A Puiseux Markov chain on V is a Markov chain whose transition matrix is a map P:V×V→P V× V . Its reachability probabilities ℙuP(◇R)P_u^P( R) are the least nonnegative solution of (2) over K, which exists by Lemma 4(i). Definition B.0 (Puiseux-winning). A Puiseux team strategy σΠ _ is Puiseux-winning if st(ℙs0σΠ,τ(◇T))=1st (P_s_0 _ ,τ( T) )=1 for every real-valued memoryless opponent strategy τ∈Dτ∈ D. The following lemma reduces limit-sure winning to the existence of a single symbolic strategy. Lemma B.0. The team wins limit surely if and only if some Puiseux team strategy is Puiseux-winning. Proof. Fixing a memoryless team strategy leaves the opponent with a finite MDP, so responses in D are sufficient. The same holds over K by Lemma 4(i), using the first-order description of reachability probabilities by (2). Suppose the team wins limit surely. By Proposition 2, the sentence ∀λ∈(0,1)∃σΠ∈ΛΠ∀τ∈D:ℙs0σΠ,τ(◇T)>1−λ∀λ∈(0,1)\;∃ _ ∈ _ \;∀τ∈ D:\;P_s_0 _ ,τ( T)>1-λ holds over ℝR. It is a first-order sentence, since strategy validity is expressed by polynomial constraints, reachability probabilities by the coordinatewise least nonnegative solution of (2), and D is finite. By Lemma 4(i), it also holds over K. Taking λ=ϵλ=ε, we obtain a Puiseux team strategy σΠ _ satisfying 1−ϵ<ℙs0σΠ,τ(◇T)≤1for every τ∈D.1-ε<P_s_0 _ ,τ( T)≤ 1 every τ∈ D. These probabilities have standard part 11 by Lemma 4(i), so σΠ _ is Puiseux-winning. Conversely, let σΠ _ be a Puiseux-winning team strategy and fix a real λ∈(0,1)λ∈(0,1). By Lemma 4(i), ℙs0σΠ,τ(◇T)>1−λP_s_0 _ ,τ( T)>1-λ for every τ∈Dτ∈ D. Since D is finite, Lemma 4(i) gives a real r>0r>0 such that the evaluation σΠ(r)∈ΛΠ _ (r)∈ _ satisfies ℙs0σΠ(r),τ(◇T)>1−λfor every τ∈D.P_s_0 _ (r),τ( T)>1-λ every τ∈ D. As responses in D suffice and λ was arbitrary, the team wins limit surely. ∎ Now we show that fractional exponents can also be eliminated. Corollary B.0. If the team wins limit surely, then some Puiseux-winning team strategy has every probability σp(s)(a) _p(s)(a) of the form ∑iciϵri _ic_i\,ε^r_i with coefficients ci∈ℝc_i and exponents ri∈ℕr_i . Proof. Let σΠ _ be a Puiseux-winning team strategy, which exists by Lemma 7. We write x1,…,xk∈x_1,…,x_k for its probabilities σp(s)(a) _p(s)(a) with p∈Πp∈ , s∈Ss∈ S, and a∈Apa∈ A_p. No exponent is negative. Indeed, if xj≠0x_j≠ 0 had leading exponent q∈ℚq with q<0q<0, then xj=ϵq(c+y)x_j=ε^q(c+y) with c∈ℝ>0c _>0 and y∈y infinitesimal, and ϵqε^q is the inverse of a positive infinitesimal, so xjx_j would be larger than every real, contradicting xj≤1x_j≤ 1. Since exponents increase from the leading one, all exponents of xjx_j are nonnegative. We choose d∈ℕ>0d _>0 to be a common multiple of the denominators of the exponents appearing in x1,…,xkx_1,…,x_k, so every exponent of every entry has the form i/di/d with i∈ℕi . Substituting ϵ≔ηdε η^d turns each xjx_j into a series in η with nonnegative integer exponents. This substitution is an order-preserving field bijection of K that coincides with the identity on ℝR, so the transformed strategy is still Puiseux-winning. Renaming η as ϵε gives the strategy required. ∎ B.1.1. Ranks Throughout this subsection, we consider Puiseux team strategies with nonnegative integer exponents, as in Corollary 8. Definition B.0 (Rank). The rank of a nonzero x=∑i≥i0ciϵi∈x= _i≥ i_0c_iε^i with ci0≠0c_i_0≠ 0 is its smallest exponent ρ(x)=i0∈ℤρ(x)=i_0 , and ρ(0)=∞ρ(0)=∞. For a Puiseux team strategy σΠ _ , the rank of an action a∈Apa∈ A_p of a player p∈Πp∈ at a state s∈Ss∈ S is rp,s,a=ρ(σp(s)(a))r_p,s,a=ρ( _p(s)(a)). In a Puiseux Markov chain P on V, the rank of a transition (u,v)∈V×V(u,v)∈ V× V is ρ(P(u,v))ρ(P(u,v)), and the rank of a set F⊆V×VF V× V of transitions is ρ(F)=∑(u,v)∈Fρ(P(u,v))ρ(F)= _(u,v)∈ Fρ(P(u,v)). The rank measures how fast a probability vanishes as ϵ→0ε→ 0. We suppose min∅=∞ =∞ and ∞±k=∞± k=∞ for k∈ℤk . For all x,y∈x,y , ρ(xy) ρ(xy) =ρ(x)+ρ(y), =ρ(x)+ρ(y), ρ(x+y) ρ(x+y) =minρ(x),ρ(y) = \ρ(x),ρ(y)\ if x,y≥0, x,y≥ 0, ρ(x/y) ρ(x/y) =ρ(x)−ρ(y) =ρ(x)-ρ(y) if y≠0. y≠ 0. The first rule holds because leading coefficients multiply, and the second because positive leading coefficients cannot cancel. The third follows from the first, since (x/y)y=x(x/y)\,y=x. For all p∈Πp∈ and s∈Ss∈ S, we have ∑a∈Apσp(s)(a)=1 _a∈ A_p _p(s)(a)=1, so the sum rule gives mina∈Aprp,s,a=0 _a∈ A_pr_p,s,a=0. Conversely, let rp,s,a∈ℕ∪∞r_p,s,a ∪\∞\ for p∈Πp∈ , s∈Ss∈ S, and a∈Apa∈ A_p satisfy mina∈Aprp,s,a=0 _a∈ A_pr_p,s,a=0 for all p∈Πp∈ and s∈Ss∈ S. The Puiseux team strategy (9) σp(s)(a)=ϵrp,s,a/∑a′:rp,s,a′<∞ϵrp,s,a′if rp,s,a<∞,0if rp,s,a=∞ _p(s)(a)= casesε^r_p,s,a / _a r_p,s,a <∞ε^r_p,s,a &if r_p,s,a<∞,\\ 0&if r_p,s,a=∞ cases then has action ranks rp,s,ar_p,s,a, since each denominator has rank 00. Example 10 illustrates ranks in the game of Example 1. cross hide agent 1 ϵε 11 1−ϵ1-ε 00 agent 2 ϵε 11 1−ϵ1-ε 00 s0s_0s_ fails_ goal1 scan_12 scan_2ϵ2ε^2 22ϵ(1−ϵ)ε(1-ε) 11ϵ2ε^2 22ϵ(1−ϵ)ε(1-ε) 111−ϵ1-ε 001−ϵ1-ε 00 Figure 3. The Puiseux-winning team strategy of Example 10 (left) and the MDP it induces for the opponent (right). Boxes show ranks, and black dots are the actions of the opponent.On the left, a table gives the team strategy: each of the two agents crosses with probability epsilon, of rank 1, and hides with probability 1 minus epsilon, of rank 0. On the right, the induced MDP: from the initial state the opponent chooses to scan the first or second robot, with the two actions drawn as black dots. Under either action, the play moves to the failure state with probability epsilon squared (rank 2), to the goal state with probability epsilon times 1 minus epsilon (rank 1), and back to the initial state with probability 1 minus epsilon (rank 0). The goal and failure states are both double-circled. Example B.0 (Ranks of actions and transitions). In the game of Example 1, let each agent cross with probability ϵε and hide with probability 1−ϵ1-ε at s0s_0. Crossing then has rank 11 and hiding has rank 00. Figure 3 shows this team strategy and the MDP it leaves for the opponent. Since the agents randomise independently, each transition probability is a sum of products of action probabilities, and the product and sum rules give its rank. For either opponent action i scan_i, the play reaches s_ fail only if both agents cross, so this transition has rank ρ(ϵ⋅ϵ)=1+1=2ρ(ε·ε)=1+1=2. It reaches s_ goal only if the scanned agent hides and the other crosses, giving rank ρ((1−ϵ)ϵ)=0+1=1ρ((1-ε)ε)=0+1=1. It stays at s0s_0 if both agents hide or only the scanned agent crosses, giving rank ρ((1−ϵ)2+ϵ(1−ϵ))=min0,1=0ρ ((1-ε)^2+ε(1-ε) )= \0,1\=0. Thus, success has smaller rank than failure. Although most rounds return to s0s_0, success occurs before failure with probability 1−ϵ1-ε, which approaches 11 as ϵε goes to zero. To show that only the ranks matter, we express the absorption probabilities of a Markov chain through spanning forests of its support graph. The support graph of a Markov chain on V with transition matrix P has vertex set V and edge set (u,v)∈V×V∣P(u,v)>0\(u,v)∈ V× V P(u,v)>0\. For a set F of edges with at most one outgoing edge per vertex, a vertex u leads to a set R of vertices if following the edges of F from u ends in R, and to a vertex v if it leads to v\v\. Definition B.0 (Spanning forest). Let P be a finite Markov chain on V with a nonempty set R⊆VR V of absorbing states, which we call roots. A spanning forest is a set F⊆V×VF V× V of edges (u,v)(u,v) with P(u,v)>0P(u,v)>0, with exactly one outgoing edge from each vertex in V∖RV R and none from vertices in R, such that every vertex leads to R. Its weight is defined as w(F)=∏(u,v)∈FP(u,v)w(F)= _(u,v)∈ FP(u,v). We write ℱF for the set of spanning forests and ℱR′(u)⊆ℱF_R (u) for those in which u∈Vu∈ V leads to R′⊆R R. Lemma B.0 (Functional forests). Let V be a finite set of vertices, let ∅≠R⊆V ≠ R V, and let F be a set of edges between vertices of V with exactly one edge leaving each vertex of V∖RV R and none leaving R. Every vertex leads to R if and only if F has no cycle. In that case, the graph (V,F)(V,F) has |R||R| connected components, each a tree with exactly one vertex in R. Proof. A directed cycle prevents its vertices from leading to R. Conversely, on a cycle with directions ignored, the restriction to one outgoing edge per vertex forces its edges to form a directed cycle. Thus, F has no such cycle if and only if it has no directed cycle. Without directed cycles, following the edges of F from any vertex ends in R, since V is finite. Without such cycles, (V,F)(V,F) has |V|−|F|=|R||V|-|F|=|R| connected components. Each component contains a vertex of R, since every vertex leads to R. As there are |R||R| components, each contains exactly one. ∎ Lemma B.0 (Forest formula). If every state has a directed path to R in the support graph, then ∑F∈ℱw(F)>0 _F w(F)>0 and ℙuP(◇R′)=∑F∈ℱR′(u)w(F)∑F∈ℱw(F)for all u∈V,R′⊆R.P_u^P( R )\;=\; _F _R (u)w(F) _F w(F) all u∈ V,\ R R. Proof. The lemma is a special case of the classical forest formula (Freidlin and Wentzell, 2012, Chapter 6, Lemma 3.3). It transfers to K by Lemma 4. ∎ Example B.0. Consider the Markov chain on V=1,2,3,4V=\1,2,3,4\, where 33 and 44 are absorbing and P(1,2)=P(1,3)=12,P(2,1)=34,P(2,4)=14,P(1,2)=P(1,3)= 12, P(2,1)= 34, P(2,4)= 14, as depicted in Figure 4. 1122334412 1234 3412 1214 141111112233441122334411223344w(F)=18w(F)= 1811 leads to 44w(F)=38w(F)= 3811 leads to 33w(F)=18w(F)= 1811 leads to 33 Figure 4. The Markov chain of Example 14 and its three spanning forests.A Markov chain with transient states 1 and 2 and absorbing roots 3 and 4, drawn with double circles and self-loops of probability 1. State 1 moves to 2 with probability 1/2 and to 3 with probability 1/2. State 2 moves to 1 with probability 3/4 and to 4 with probability 1/4. Next to it are the three spanning forests rooted at 3 and 4, with the chosen edges in bold: first, edges 1 to 2 and 2 to 4, with weight 1/8, so 1 leads to 4; second, edges 2 to 1 and 1 to 3, with weight 3/8, so 1 leads to 3; third, edges 1 to 3 and 2 to 4, with weight 1/8, so 1 leads to 3. We apply Lemma 13 with roots R=3,4R=\3,4\ to compute the probability of reaching 33 from state 11. Each spanning forest selects one outgoing edge from each of 11 and 22. Selecting both 1→21→ 2 and 2→12→ 1 creates a cycle, so this choice is excluded. The three spanning forests, drawn in Figure 4, are Fw(F)Root to which 1 leads1→2, 2→412⋅14=1841→3, 2→112⋅34=3831→3, 2→412⋅14=183 array[]c|c|cF&w(F)&Root to which 1 leads\\ \1→ 2,\;2→ 4\& 12· 14= 18&4\\ \1→ 3,\;2→ 1\& 12· 34= 38&3\\ \1→ 3,\;2→ 4\& 12· 14= 18&3 array The denominator sums the weights of all three forests, while the numerator sums only those in which 11 leads to 33. Hence ℙ1P(◇3)=38+1818+38+18=45.P_1^P( \3\)= 38+ 18 18+ 38+ 18= 45. Combining the forest formula with the rank rules gives the rank of an absorption probability. Lemma B.0 (Rank criterion). Let P be a Puiseux Markov chain on V with a set R⊆VR V of absorbing states such that every state has a path to R in the support graph. For all u∈Vu∈ V and R′⊆R R, ρ(ℙuP(◇R′))=minF∈ℱR′(u)ρ(F)−minF∈ℱρ(F).ρ (P_u^P( R ) )= _F _R (u)ρ(F)- _F ρ(F). Proof. By Lemma 13 and the rank rules after Definition 9, ρ(ℙuP(◇R′)) ρ (P_u^P( R ) ) =ρ(∑F∈ℱR′(u)w(F))−ρ(∑F∈ℱw(F)) =ρ ( _F _R (u)w(F) )-ρ ( _F w(F) ) =minF∈ℱR′(u)ρ(F)−minF∈ℱρ(F). = _F _R (u)ρ(F)- _F ρ(F). The first equality uses the quotient rule, since the denominator is nonzero. The second uses the sum rule, since each weight w(F)=∏(v,w)∈FP(v,w)w(F)= _(v,w)∈ FP(v,w) is nonnegative and has rank ρ(F)ρ(F) by the product rule. ∎ Definition B.0 (Strongly connected components). A strongly connected component (SCC) of a Markov chain P on V is a maximal nonempty set C⊆VC V such that any two states of C are reachable from one another in the support graph. An SCC C is bottom if P(u,v)=0P(u,v)=0 for all u∈Cu∈ C and v∈V∖Cv∈ V C. Once a Markov chain enters a bottom SCC, it stays there forever. A finite Markov chain reaches a bottom SCC almost surely. Since target states are absorbing, a strongly connected set of states that contains a target state is that state alone. Let σΠ _ be a Puiseux team strategy and τ∈Dτ∈ D. We write R⊆SR S for the union of the bottom SCCs of PσΠ,τP_ _ ,τ, and R′=⋃C∣C is a bottom SCC with C∩T=∅R = \C C is a bottom SCC with C∩ T= \. Making the states of R absorbing gives the Puiseux Markov chain P:S×S→P S× S with P(u,v)=PσΠ,τ(u,v)if u∉R,1if u=v∈R,0otherwise.P(u,v)= casesP_ _ ,τ(u,v)&if u∉ R,\\ 1&if u=v∈ R,\\ 0&otherwise. cases On the spanning forests of P, we consider the condition minF∈ℱR′(s0)ρ(F)>minF∈ℱρ(F). _F _R (s_0)ρ(F)> _F ρ(F). By Lemma 15, (B.1.1) says that the failure probability ℙs0P(◇R′)P_s_0^P( R ) has positive rank. Equivalently, w(F)/w(F∗)w(F)/w(F^*) is infinitesimal for every F∈ℱR′(s0)F _R (s_0) and every F∗∈ℱF^* of minimum rank. Lemma B.0. The strategy σΠ _ is Puiseux-winning if and only if (B.1.1) holds for every τ∈Dτ∈ D. In particular, if a Puiseux team strategy σΠ′ _ has the same action ranks as σΠ _ , then σΠ′ _ is Puiseux-winning if and only if σΠ _ is. Proof. As in the proof of Lemma 7, it suffices to consider opponent strategies in D. We fix τ∈Dτ∈ D and define P, R, and R′R as above. The Markov chain reaches a bottom SCC almost surely. It therefore avoids T exactly when it reaches R′R , so 1−ℙs0σΠ,τ(◇T)=ℙs0P(◇R′).1-P_s_0 _ ,τ( T)=P_s_0^P( R ). The strategy σΠ _ is Puiseux-winning if and only if this failure probability has standard part 00 for every τ. By the definition of the standard part, a bounded x∈x satisfies st(x)=0st(x)=0 if and only if ρ(x)>0ρ(x)>0. Every state of P has a path to R, so by Lemma 15, ρ(ℙs0P(◇R′))>0ρ (P_s_0^P( R ) )>0 is equivalent to (B.1.1). The action ranks determine the transition ranks of PσΠ,τP_ _ ,τ. Indeed, the team players randomise independently, so by the product rule a team profile a¯∈AΠ a∈ A_ at a state s∈Ss∈ S has rank ρ(σΠ(s)(a¯))=∑p∈Πrp,s,apρ( _ (s)( a))= _p∈ r_p,s,a_p. A transition probability is a sum of such probabilities multiplied by positive reals. For all s,t∈Ss,t∈ S, the sum rule therefore gives (10) ρ(PσΠ,τ(s,t))=min∑p∈Πrp,s,ap|a¯∈(σΠ(s)),δ(s,(a¯,τ(s)))(t)>0.ρ (P_ _ ,τ(s,t) )= \ _p∈ r_p,s,a_p\; |\; array[]l a∈ Supp( _ (s)),\\ δ (s,( a,τ(s)) )(t)>0 array \. The action ranks thus determine the support, the bottom SCCs, R, R′R , and both minima in (B.1.1). ∎ Proposition B.0 (Computing forest minima). Let P be a Puiseux Markov chain on V, given by its transition ranks ρ(P(v,w))∈ℕ∪∞ρ(P(v,w)) ∪\∞\, and let R⊆VR V be a set of absorbing states. For u∈V∖Ru∈ V R and R′⊆R R, Algorithm 2 computes minF∈ℱR′(u)ρ(F) _F _R (u)ρ(F) in polynomial time. Proof. We reduce the problem to an instance of the minimum-weight spanning arborescence problem. For this, we contract R′R into a new vertex v v, delete the vertices of R∖R′R R , and redirect every edge into R∖R′R R to u. A set F of edges of the support graph with one outgoing edge at every vertex of V∖RV R becomes a set F F with one outgoing edge at every vertex other than v v, and F∈ℱR′(u)⇔every vertex leads to v^ in F^.F _R (u) vertex leads to v in F. Indeed, if F∈ℱR′(u)F _R (u) then a path of F ending in R∖R′R R continues in F F from u and ends in v v. Conversely, if every vertex leads to v v in F F then the path from u uses no redirected edge, since such an edge would close a cycle at u. Hence, u leads to R′R in F, and every path of F ends in R. The correspondence preserves the sum of ranks. Algorithm 2 therefore returns the minimum with one call to an oracle MinDirectedSpanningForest, which returns the minimum rank of a set F F on the right, or ∞ if no such set exists. By Lemma 12, these sets are the spanning trees directed towards v v. A minimum-weight spanning arborescence algorithm (Edmonds, 1967; Chu and Liu, 1965; Tarjan, 1977) on edges thus implements the oracle in polynomial time. ∎ Algorithm 2 Forest Minimum ForestMin 1: Input: V, ρ(P(v,w))ρ(P(v,w)) for v,w∈Vv,w∈ V, R, u∈V∖Ru∈ V R, R′⊆R R 2: Output: minF∈ℱR′(u)ρ(F) _F _R (u)ρ(F) 3: V^←(V∖R)∪v V←(V R)∪\ v\ 4: E^←∅ E← 5: for all v∈V∖Rv∈ V R and w∈Vw∈ V with ρ(P(v,w))<∞ρ(P(v,w))<∞ do 6: if w∈R′w∈ R then 7: w′←v^w ← v ⊳ Contract R′R 8: else if w∈R∖R′w∈ R R then 9: w′←uw ← u ⊳ Redirect to u 10: else 11: w′←w ← w 12: E^←E^∪ev,w E← E∪\e_v,w\ ⊳ Edge from v to w′w 13: ρ(ev,w)←ρ(P(v,w))ρ(e_v,w)←ρ(P(v,w)) 14: return MinDirectedSpanningForest(V^,E^,ρ,v^) MinDirectedSpanningForest( V, E,ρ, v) Since ℱ=ℱR(s0)F=F_R(s_0) for s0s_0, both minima in (B.1.1) can be computed in polynomial time by Algorithm 2. B.1.2. Small ranks By Lemma 17, a Puiseux-winning strategy is described by its action ranks. To guess such a strategy in nondeterministic polynomial time, we need ranks with polynomially many bits. We now recall two linear-algebra facts that help us show that such ranks exist. Cramer’s rule. For an invertible matrix A∈ℝk×kA ^k× k and a vector b∈ℝkb ^k, the unique solution x∈ℝkx ^k of Ax=bAx=b satisfies xi=detAidetAfor 1≤i≤k,x_i= A_i A 1≤ i≤ k, where Ai∈ℝk×kA_i ^k× k is obtained from A by replacing its iith column with b. If A and b have integer entries, then detA A is a nonzero integer, so |detA|≥1 A ≥ 1 and |detA|x∈ℤk A \,x ^k. Hadamard’s inequality. For a matrix B∈ℝk×kB ^k× k with columns b1,…,bk∈ℝkb_1,…,b_k ^k, |detB|≤∏i=1k‖bi‖2, B ≤ _i=1^k\|b_i\|_2, where ‖bi‖2\|b_i\|_2 is the Euclidean length of column bib_i. In particular, every B∈−1,0,1k×kB∈\-1,0,1\^k× k has ‖bi‖2≤k\|b_i\|_2≤ k for every i and hence |detB|≤k/2 B ≤ k^k/2. Together with Cramer’s rule, we obtain the following bound. If A∈−1,0,1k×kA∈\-1,0,1\^k× k is invertible and b∈0,1kb∈\0,1\^k, then the solution x∈ℝkx ^k of Ax=bAx=b satisfies |detA|x A \,x ∈ℤk, ^k, |detA||xi| A \, x_i =|detAi|≤k/2for 1≤i≤k. = A_i ≤ k^k/2 1≤ i≤ k. Lemma B.0. Let N=|(p,s,a)∣p∈Π,s∈S,a∈Ap|N= \(p,s,a) p∈ ,\ s∈ S,\ a∈ A_p\ . If the team wins limit surely, then there exists a Puiseux-winning team strategy whose finite ranks are nonnegative integers bounded by N/2N^N/2. Proof. We start with a Puiseux-winning team strategy and construct another Puiseux-winning strategy with the same support whose finite action ranks are bounded by N/2N^N/2. We write (B.1.1) as linear inequalities in the action ranks, take a vertex of their solution set, and scale it to an integer vector satisfying the required bound. By Lemmas 7 and 8, we choose without loss of generality a Puiseux-winning strategy with integer action ranks. Let I=(p,s,a)∣p∈Π,s∈S,a∈Ap,σp(s)(a)>0I=\(p,s,a) p∈ ,\ s∈ S,\ a∈ A_p,\ _p(s)(a)>0\ be its support. We denote its finite ranks by r∗=(rp,s,a∗)(p,s,a)∈I∈ℕI.r^*=(r^*_p,s,a)_(p,s,a)∈ I ^I. We keep this support fixed and set k=|I|≤Nk=|I|≤ N. We first express forest ranks as sums of action ranks. We fix τ∈Dτ∈ D and consider the Markov chain P and the sets R and R′R defined before (B.1.1). The support graph of P, the sets R and R′R , and the forest sets ℱF and ℱR′(s0)F_R (s_0) depend only on the support of the team strategy, which we keep fixed. Let F∈ℱF be a spanning forest of P. For each edge (u,v)∈F(u,v)∈ F, we choose a supported team profile α(u)∈(σΠ(u))α(u)∈ Supp( _ (u)) with δ(u,(α(u),τ(u)))(v)>0δ (u,(α(u),τ(u)) )(v)>0. Since F has exactly one edge leaving each state of S∖RS R, these profiles form a map α:S∖R→AΠα S R→ A_ , which we call a choice for F. For a vector r=(rp,s,a)(p,s,a)∈I∈ℝIr=(r_p,s,a)_(p,s,a)∈ I ^I of candidate ranks, we define the cost of F and a choice α by Cτ(F,α,r)=∑(u,v)∈F∑p∈Πrp,u,α(u)p.C_τ(F,α;r)= _(u,v)∈ F _p∈ r_p,u,α(u)_p. If the actions have ranks r, then Cτ(F,α,r)C_τ(F,α;r) is the rank of the term of w(F)w(F) in which each edge (u,v)∈F(u,v)∈ F uses the profile α(u)α(u), and (10) gives ρ(F)=minαCτ(F,α,r)ρ(F)= _αC_τ(F,α;r) over all choices α for F. The cost is linear in r since the coefficient of rp,s,ar_p,s,a is 11 if s∉Rs∉ R and α(s)p=aα(s)_p=a, and 00 otherwise. For each τ∈Dτ∈ D, we choose a forest Fτ∗∈ℱF_τ^* and a choice ατ∗ _τ^* for it whose cost is smallest under the original ranks r∗r^*. By (B.1.1) in Lemma 17, every forest in ℱR′(s0)F_R (s_0) has a strictly larger rank than Fτ∗F_τ^*. Since these ranks are integers, the difference is at least 11. We require the rank r to satisfy Cτ(F,α,r)−Cτ(Fτ∗,ατ∗,r)≥1C_τ(F,α;r)-C_τ(F_τ^*, _τ^*;r)≥ 1 for every τ∈Dτ∈ D, every F∈ℱR′(s0)F _R (s_0), and every choice α for F. We also require r≥0r≥ 0, and rp,s,a=0r_p,s,a=0 whenever rp,s,a∗=0r^*_p,s,a=0. The original vector r∗r^* satisfies this system. Every solution r also satisfies (B.1.1). Indeed, with forest ranks computed from the action ranks r, every τ∈Dτ∈ D and F∈ℱR′(s0)F _R (s_0) satisfy ρ(F) ρ(F) =minαCτ(F,α,r)≥Cτ(Fτ∗,ατ∗,r)+1 = _αC_τ(F,α;r)≥ C_τ(F_τ^*, _τ^*;r)+1 ≥ρ(Fτ∗)+1≥minF′∈ℱρ(F′)+1. ≥ρ(F_τ^*)+1≥ _F ρ(F )+1. The system may have exponentially many constraints, but we use it only to prove that bounded ranks exist. We write the full system as Mr≥d,M∈−1,0,1m×k,d∈0,1m,k≤N,Mr≥ d, M∈\-1,0,1\^m× k, d∈\0,1\^m, k≤ N, where m is the number of inequalities. We include nonnegativity of entries of r among these inequalities and express each equality as two inequalities. Its solution set Q=r∈ℝI∣Mr≥dQ=\r ^I Mr≥ d\ is a nonempty polyhedron in the nonnegative orthant, so it has a vertex z∈Qz∈ Q. At a vertex, the constraints that hold with equality determine a unique point and their coefficient matrix has full rank k, so we can select k linearly independent rows of M. Let A∈−1,0,1k×kA∈\-1,0,1\^k× k consist of these rows and b∈0,1kb∈\0,1\^k of the corresponding entries of d, giving Az=b.Az=b. Thus A is an invertible k×k× k matrix. By Cramer’s rule, r′=|detA|z∈ℤIr = A \,z ^I, and Mr′=|detA|Mz≥|detA|d≥d.Mr = A \,Mz≥ A \,d≥ d. The multiplier |detA| A is at least 11 since detA A is a nonzero integer, so every inequality remains satisfied and coordinates fixed to zero stay zero. By the bound after Hadamard’s inequality, 0≤rp,s,a′≤k/2≤N/2.0≤ r _p,s,a≤ k^k/2≤ N^N/2. The minimum rank at each player-state pair remains zero, so (9), with rp,s,a′=∞r _p,s,a=∞ for (p,s,a)∉I(p,s,a)∉ I, gives a Puiseux team strategy with ranks r′r . It is Puiseux-winning by Lemma 17. ∎ Since N is polynomial in the size of the game and log2(N/2)=N2log2N _2(N^N/2)= N2 _2N, ranks can be encoded with polynomially many bits. Guessing these ranks and checking (B.1.1) for every τ∈Dτ∈ D gives membership in NP NP as (B.1.1) can be checked in polynomial time with Algorithm 2. In the following sections, we improve the bound to NP. B.2. Puiseux Markov Decision Processes By Proposition 18, we can check (B.1.1) for a single τ∈Dτ∈ D in polynomial time. However, the chain P in (B.1.1) depends on τ through its bottom SCCs, and D can be exponentially large. We therefore build one object for all τ∈Dτ∈ D from the MDP induced by σΠ _ . B.2.1. The induced Puiseux MDP We fix action ranks rp,s,a∈ℕ∪∞r_p,s,a ∪\∞\ with mina∈Aprp,s,a=0 _a∈ A_pr_p,s,a=0 for all p∈Πp∈ and s∈Ss∈ S, and let σΠ _ be the Puiseux team strategy (9). Definition B.0 (Induced Puiseux MDP). The Puiseux MDP induced by σΠ _ is the MDP ℳM of Definition 5 for σΠ _ , with transition function P=PσΠ:S×A→SP=P_ _ S× A_ O ^S and transition ranks ρ(s,b,t)=ρ(P(s,b)(t))ρ(s,b,t)=ρ(P(s,b)(t)) for s,t∈Ss,t∈ S and b∈Ab∈ A_ O. These ranks are given by (10) with b in place of τ(s)τ(s), so we can compute them in polynomial time. For τ∈Dτ∈ D, we write ℙuτ=ℙuσΠ,τP_u^τ=P_u _ ,τ for the probabilities in ℳM after fixing τ. Lemma B.0 (Zero-rank transitions). For all s∈Ss∈ S and b∈Ab∈ A_ O, there is t∈St∈ S with ρ(s,b,t)=0ρ(s,b,t)=0. Proof. Since mina∈Aprp,s,a=0 _a∈ A_pr_p,s,a=0 for all p∈Πp∈ , some a¯0∈AΠ a^0∈ A_ has ∑p∈Πrp,s,ap0=0 _p∈ r_p,s,a^0_p=0, so every t∈(δ(s,(a¯0,b)))t∈ Supp(δ(s,( a^0,b))) satisfies ρ(s,b,t)=0ρ(s,b,t)=0 by (10). ∎ B.2.2. Traps and the merged MDP Definition B.0 (End component). An end component of ℳM is a pair (X,Γ)(X, ) with ∅≠X⊆S ≠ X S and ∅≠Γ(x)⊆A ≠ (x) A_ O for x∈Xx∈ X such that (P(x,b))⊆X Supp(P(x,b)) X for all x∈Xx∈ X and b∈Γ(x)b∈ (x), and the graph (X,(x,y)∣P(x,b)(y)>0 for some b∈Γ(x)) (X,\(x,y) P(x,b)(y)>0 for some b∈ (x)\ ) is strongly connected. It is a maximal end component (MEC) if X and every Γ(x) (x) are inclusion-maximal. Lemma B.0 (Computing MECs). The MECs of ℳM can be computed in polynomial time. Proof. End components are defined through the support only. We can therefore run the polynomial-time MEC algorithms for MDPs (Courcoubetis and Yannakakis, 1995; de Alfaro, 1997; Chatterjee and Henzinger, 2014). ∎ Definition B.0 (Trap). We write =⋃X∣(X,Γ) is a MEC of ℳ with X∩T=∅, Trap= \X (X, ) is a MEC of M with X∩ T= \, and obtain ℳ♯M from ℳM by making every state of Trap absorbing. Remark B.1. Inside a MEC, the opponent can select actions that keep the play there. For example, if s∉Ts∉ T and P(s,b)(s)=1P(s,b)(s)=1 for some b∈Ab∈ A_ O, then (s,Γ)(\s\, ) with Γ(s)=b (s)=\b\ is an end component, so s∈s∈ Trap even if another action moves to T. Lemma B.0 (Trap criterion). The Puiseux team strategy σΠ _ is Puiseux-winning if and only if st(ℙs0τ(◇))=0in ℳ♯st (P_s_0^τ( Trap) )=0 M for every τ∈Dτ∈ D. Moreover, ℙuτ(◇(∪T))=1P_u^τ( ( Trap∪ T))=1 in ℳ♯M for all u∈Su∈ S and τ∈Dτ∈ D. Proof. Fix τ∈Dτ∈ D. Every bottom SCC C of the chain of ℳM under τ satisfies C=tC=\t\ for some t∈Tt∈ T or C⊆C Trap, since (C,Γ)(C, ) with Γ(x)=τ(x) (x)=\τ(x)\ is an end component. The play almost surely reaches a bottom SCC, so 1−ℙs0τ(◇T)≤ℙs0τ(◇),1-P_s_0^τ( T) _s_0^τ( Trap), where the right side is the same in ℳM and ℳ♯M . This inequality shows the first direction. For the second direction, let τ′∈Dτ ∈ D agree with τ outside Trap and satisfy τ′(x)∈Γ(x)τ (x)∈ (x) for every MEC (X,Γ)(X, ) with X⊆X Trap and every x∈Xx∈ X. A play under τ′τ never leaves Trap after entering it, so ℙs0τ′(◇T)≤1−ℙs0τ(◇)P_s_0^τ ( T)≤ 1-P_s_0^τ( Trap), which has standard part less than 11 if st(ℙs0τ(◇))>0st (P_s_0^τ( Trap) )>0. Finally, the states of ∪T Trap∪ T are absorbing in ℳ♯M , and by the first argument every other bottom SCC would lie in Trap. ∎ In ℳ♯M , we contract T into a new absorbing state t∗t^* and Trap into a new absorbing state f∗f^*, and obtain a Puiseux MDP ℳ M on V=U∪t∗,f∗,U=S∖(T∪).V=U∪\t^*,f^*\, U=S (T∪ Trap). By the sum rule, its transition ranks into the new states are ρ(u,b,t∗)=mint∈Tρ(u,b,t),ρ(u,b,f∗)=minx∈ρ(u,b,x)ρ(u,b,t^*)= _t∈ Tρ(u,b,t), ρ(u,b,f^*)= _x∈ Trapρ(u,b,x) for u∈Uu∈ U and b∈Ab∈ A_ O. We write n=|V|n=|V|. The edges of ℳ M are the triples in E=(u,b,v)∈U×A×V∣ρ(u,b,v)<∞E=\(u,b,v)∈ U× A_ O× V ρ(u,b,v)<∞\, and an edge e=(u,b,v)e=(u,b,v) has rank ρ(e)=ρ(u,b,v)ρ(e)=ρ(u,b,v). Unlike the chain P in (B.1.1), ℳ M does not depend on τ. Definition B.0 (Spanning root-forests). A spanning root-forest of ℳ M is a set F⊆EF E with exactly one edge leaving each u∈Uu∈ U, such that every vertex leads to t∗,f∗\t^*,f^*\. Its rank is ρ(F)=∑e∈Fρ(e)ρ(F)= _e∈ Fρ(e). It is trapped if s0s_0 leads to f∗f^*, targeted if s0s_0 leads to t∗t^*, and consistent with τ∈Dτ∈ D if F⊆(u,τ(u),v)∣u∈U,v∈VF \(u,τ(u),v) u∈ U,\ v∈ V\. The forests consistent with τ are the spanning forests of the Markov chain ℳ^τ M_τ obtained from ℳ M by fixing τ. In ℳ^τ M_τ, the minimum ranks ρτf∗,ρτt∗∈ℕ∪∞ _τ^f^*, _τ^t^* ∪\∞\ of the trapped and of the targeted forests consistent with τ are ρτf∗=minF∈ℱf∗(s0)ρ(F),ρτt∗=minF∈ℱt∗(s0)ρ(F). _τ^f^*= _F _\f^*\(s_0)ρ(F), _τ^t^*= _F _\t^*\(s_0)ρ(F). Since minF∈ℱρ(F)=minρτf∗,ρτt∗ _F ρ(F)= \ _τ^f^*, _τ^t^*\ in ℳ^τ M_τ, the inequality ρτf∗>ρτt∗ _τ^f^*> _τ^t^* is (B.1.1) for ℳ^τ M_τ with R′=f∗R =\f^*\, and Algorithm 2 computes ρτf∗ _τ^f^* and ρτt∗ _τ^t^* in polynomial time by Proposition 18. Corollary B.0 (Forest criterion). For every τ∈Dτ∈ D, st(ℙs0τ(◇))>0in ℳ♯⟺ρτf∗≤ρτt∗.st (P_s_0^τ( Trap) )>0 M _τ^f^*≤ _τ^t^*. Proof. By Lemma 25, every state of ℳ^τ M_τ has a path to t∗,f∗\t^*,f^*\, and ℙs0τ(◇)P_s_0^τ( Trap) in ℳ♯M equals ℙs0τ(◇f∗)P_s_0^τ( \f^*\) in ℳ M. By Lemma 15, ρ(ℙs0τ(◇f∗))=ρτf∗−minρτf∗,ρτt∗.ρ (P_s_0^τ( \f^*\) )= _τ^f^*- \ _τ^f^*, _τ^t^*\. A probability has positive standard part exactly when its rank is 00, and the right side is 00 exactly when ρτf∗≤ρτt∗ _τ^f^*≤ _τ^t^*. ∎ B.3. The NP Upper Bound We now prove that limit-sure reachability in the general game setting belongs to NP. By Lemma 19, a winning team strategy can be described by action ranks with polynomially many bits. For fixed team ranks, Lemmas 25 and 27 give a winning criterion. It compares forest ranks for every opponent strategy. For one opponent strategy, this comparison takes polynomial time by Proposition 18. However, there may be exponentially many opponent strategies, so checking them one by one takes exponential time. Instead, we use a certificate with two parts. The first part consists of the team’s action ranks. The second part is one opponent strategy in an encoded Puiseux MDP. We check that this opponent strategy is stable. This means that the opponent cannot increase its value by choosing a different action for the next move and then following the original strategy. We show that every stable strategy is optimal and that a stable strategy exists. Finally, because stability implies optimality, we propose an algorithm to check stability in polynomial time. This algorithm uses the structure of the encoded Puiseux MDP. Recalling the setting. Fix action ranks rp,s,a∈ℕ∪∞r_p,s,a ∪\∞\ with minarp,s,a=0 _ar_p,s,a=0 at every (p,s)(p,s), and let σΠ _ be the strategy that realises them as in Section B.2. We use the transition ranks of Definition 20, the set Trap of Definition 24, and the graph ℳ^=(V,E) M=(V,E) of Section B.2.2. The cases listed after Lemma 25 will be handled directly in the algorithm. Therefore, we assume s0∉T∪s_0∉ T∪ Trap, ≠∅ Trap≠ , and that a target is reachable from s0s_0 in the support of ℳ♯M . Recall that V=U∪t∗,f∗V=U∪\t^*,f^*\, where U=S∖(T∪)U=S (T∪ Trap). An edge e=(u,b,v)e=(u,b,v) has source u∈Uu∈ U, action label b, and rank ρ(e)ρ(e). There is at most one edge for each triple (u,b,v)(u,b,v). Write E(u,b)E(u,b) for the edges with source u and label b. This set is nonempty by Lemma 21. Throughout this subsection, an opponent strategy is a deterministic memoryless map τ:U→Aτ U→ A_ O. We use the forests of Definition 26. A vertex leads to a root if following the selected edges ends at that root. Write ℱτF_τ for the forests consistent with τ, and ℱτ(v)F_τ(v) for those in which v leads to f∗f^*. By Lemmas 25 and 27, (11) σΠ is Puiseux-winning⟺ρτf∗>ρτt∗ for every τ. _ is Puiseux-winning _τ^f^*> _τ^t^* for every τ. Here ρτf∗ _τ^f^* and ρτt∗ _τ^t^* are the minimum ranks of trapped and targeted forests from Definition 26, with min∅=∞ =∞. B.3.1. The encoded MDP Breaking ties between forests. Index the edges as e0,…,em−1e_0,…,e_m-1 and define ρ^(ei) ρ(e_i) =2m+1ρ(ei)+2i, =2^m+1ρ(e_i)+2^i, ρ^(J) ρ(J) =∑e∈Jρ^(e)for all J⊆E. = _e∈ J ρ(e) all J E. The powers of two distinguish different sets of edges. Their total is at most 2m−12^m-1, so they cannot reverse a strict comparison of the original integer ranks. More precisely, 0≤ρ^(J)−2m+1ρ(J)≤2m−1. 0≤ ρ(J)-2^m+1ρ(J)≤ 2^m-1. Thus ρ(J)<ρ(J′)ρ(J)<ρ(J ) implies ρ^(J)<ρ^(J′) ρ(J)< ρ(J ). If the encoded ranks are equal, the original ranks must be equal, and then uniqueness of binary representation gives J=J′J=J . Transitions and values. The encoded MDP has state set V, action set A_ O, and absorbing roots t∗,f∗t^*,f^*. For u∈Uu∈ U, put Zu,b Z_u,b =∑e∈E(u,b)ϵρ^(e). = _e∈ E(u,b)ε ρ(e). Its transition probabilities are (12) P~(u,b,v)=ϵρ^(u,b,v)/Zu,b,(u,b,v)∈E,0,otherwise. P(u,b,v)= casesε ρ(u,b,v)/Z_u,b,&(u,b,v)∈ E,\\ 0,&otherwise. cases These are nonnegative elements of K whose sum over v is 11. The support is the same as in ℳ M. The encoded probabilities are chosen for the certificate. Thus, they are not necessarily equal to the probabilities of ℳ♯M . In particular, ρ^(e) ρ(e) is the exponent of an unnormalised weight, not necessarily the rank of a transition probability after division by Zu,bZ_u,b. For an opponent strategy τ, let qvτq_v^τ be its probability of reaching f∗f^* from v in this encoded MDP, as defined by the least nonnegative solution of Equation 2 over K. The opponent seeks to maximise these values. By Lemma 25, every vertex has a support path to a root under each fixed strategy. This path property is unchanged in the encoded MDP. Selecting at every nonroot the first edge of a shortest path to a root gives a forest, since the distance to the roots strictly decreases. Hence ℱτF_τ is nonempty for every τ. Define the forest sums Nvτ N_v^τ =∑F∈ℱτ(v)ϵρ^(F), = _F _τ(v)ε ρ(F), Dτ D^τ =∑F∈ℱτϵρ^(F). = _F _τε ρ(F). Every forest uses one edge from each nonroot. Its probability weight is therefore ϵρ^(F)/∏u∈UZu,τ(u)ε ρ(F)/ _u∈ UZ_u,τ(u). The common denominator cancels in Lemma 13, giving (13) qvτ=NvτDτ,Dτ>0.q_v^τ= N_v^τD^τ, D^τ>0. Thus the value is the fraction of forest weight sending v to the failure root. In particular, qf∗τ=1q_f^*^τ=1 and qt∗τ=0q_t^*^τ=0. By Equation 2, (14) quτ=∑v∈VP~(u,τ(u),v)qvτfor all u∈U.q_u^τ= _v∈ V P(u,τ(u),v)q_v^τ all u∈ U. B.3.2. One stable response suffices A strategy τ is stable if (15) quτ≥∑v∈VP~(u,b,v)qvτfor all u∈U and b∈A.q_u^τ≥ _v∈ V P(u,b,v)q_v^τ all u∈ U and b∈ A_ O. The right-hand side is the value of playing b for one step and then following τ. Stability says that no such change improves the value. Equality holds when b=τ(u)b=τ(u) by Equation 14. This subsection shows that if an opponent strategy is stable, then it is optimal. Moreover, a stable strategy exists. The next lemma gives a principle to compare two strategies. It shows how inequalities in individual states imply an inequality between their values at every state. Lemma B.0 (Minimum principle). Fix τ and d∈Vd ^V with dt∗=df∗=0d_t^*=d_f^*=0. If du≥∑vP~(u,τ(u),v)dvd_u≥ _v P(u,τ(u),v)d_v for every u∈Uu∈ U, then dv≥0d_v≥ 0 for every v∈Vv∈ V. Proof. Suppose δ=minvdv<0δ= _vd_v<0 and let W=v:dv=δW=\v:d_v=δ\. The roots are outside W. For u∈Wu∈ W, δ=du δ=d_u ≥∑vP~(u,τ(u),v)dv≥∑vP~(u,τ(u),v)δ=δ. ≥ _v P(u,τ(u),v)d_v≥ _v P(u,τ(u),v)δ=δ. Equality implies that every positive-probability successor of u also belongs to W. Thus, no vertex of W has a support path to a root, which is a contradiction. ∎ We will apply the minimum principle lemma to the difference between two value vectors. This difference is zero at both roots as the value of any strategy is the same in the absorbing roots. If it satisfies the inequalities in the lemma, it is nonnegative at all states. Thus, one strategy has at least the value of the other in every state. Lemma B.0 (Stable strategies are optimal). A stable strategy exists. Every stable strategy τ satisfies qvτ≥qvτ′q_v^τ≥ q_v^τ for every strategy τ′τ and vertex v. Proof. Suppose τ is stable and fix an arbitrary opponent strategy τ′τ . For every v∈Vv∈ V, put dv=qvτ−qvτ′d_v=q_v^τ-q_v^τ . Both strategies have value 00 at t∗t^* and 11 at f∗f^*. Hence dt∗=df∗=0d_t^*=d_f^*=0. For every u∈Uu∈ U, we have du d_u =quτ−quτ′ =q_u^τ-q_u^τ ≥∑v∈V(P~(u,τ′(u),v)qvτ)−quτ′ ≥ _v∈ V ( P(u,τ (u),v)q_v^τ )-q_u^τ (by stability of τ) =∑v∈VP~(u,τ′(u),v)(qvτ−qvτ′) = _v∈ V P(u,τ (u),v) (q_v^τ-q_v^τ ) (by Equation 14 for τ′τ ) =∑v∈VP~(u,τ′(u),v)dv. = _v∈ V P(u,τ (u),v)d_v. Thus d satisfies all hypotheses of Lemma 28 for the strategy τ′τ . It follows that dv≥0d_v≥ 0 for every v∈Vv∈ V. Therefore qvτ≥qvτ′q_v^τ≥ q_v^τ at every vertex. Since τ′τ was an arbitrary strategy, we conclude that τ is optimal. To prove existence, choose a strategy τ maximising ∑v∈Vqvτ _v∈ Vq_v^τ. Such a choice exists because there are finitely many positional strategies and K is totally ordered. Suppose it is not stable. Choose u,bu,b with ∑vP~(u,b,v)qvτ>quτ _v P(u,b,v)q_v^τ>q_u^τ, and let τ′τ change only the action at u to b. Put dv=qvτ′−qvτd_v=q_v^τ -q_v^τ. At the roots dv=0d_v=0. At every z∈U∖uz∈ U \u\, Equation 14 gives dz=∑vP~(z,τ′(z),v)dvd_z= _v P(z,τ (z),v)d_v. At u, du d_u =∑vP~(u,b,v)qvτ′−quτ = _v P(u,b,v)q_v^τ -q_u^τ >∑vP~(u,b,v)(qvτ′−qvτ)=∑vP~(u,b,v)dv. > _v P(u,b,v)(q_v^τ -q_v^τ)= _v P(u,b,v)d_v. By Lemma 28, every dvd_v is nonnegative. The strict inequality then gives du>0d_u>0, contradicting maximality of the sum. Hence τ is stable. ∎ Now, we connect optimality in the encoded MDP to the original forest criterion in the main Puiseux MDP. For a nonzero series x∈x , write ν(x)ν(x) for its smallest exponent, and put ν(0)=∞ν(0)=∞. Products add these exponents and quotients subtract them. In a sum of positive series, leading coefficients cannot cancel, so its rank is the smallest rank of its summands. Lemma B.0 (Ranks of encoded values). Fix a deterministic memoryless opponent strategy τ. Let ρτf∗,ρτt∗ _τ^f^*, _τ^t^* be its minimum trapped and targeted forest ranks, and qs0τq_s_0^τ its encoded failure probability. (1) If ρτf∗≤ρτt∗ _τ^f^*≤ _τ^t^*, then qs0τ>0q_s_0^τ>0 and ν(qs0τ)≤2m−1ν(q_s_0^τ)≤ 2^m-1. (2) If ρτf∗>ρτt∗ _τ^f^*> _τ^t^*, then qs0τ=0q_s_0^τ=0 or ν(qs0τ)≥2m+1ν(q_s_0^τ)≥ 2^m+1. Proof. If only trapped forests exist, then ρτf∗<ρτt∗=∞ _τ^f^*< _τ^t^*=∞ and qs0τ=1q_s_0^τ=1, so the first claim holds. If only targeted forests exist, then ρτt∗<ρτf∗=∞ _τ^t^*< _τ^f^*=∞ and qs0τ=0q_s_0^τ=0, so the second claim holds. Suppose both kinds of forests exist. Let a and b be their minimum encoded ranks in the encoded MDP, for trapped and targeted forests, respectively. The encoding preserves strict rank comparisons. Thus, forests attaining a and b have ranks ρτf∗ _τ^f^* and ρτt∗ _τ^t^* in the original Puiseux MDP, respectively. Each tie-breaking contribution lies between 00 and 2m−12^m-1, so 2m+1ρτf∗ 2^m+1 _τ^f^* ≤a≤2m+1ρτf∗+2m−1, ≤ a≤ 2^m+1 _τ^f^*+2^m-1, 2m+1ρτt∗ 2^m+1 _τ^t^* ≤b≤2m+1ρτt∗+2m−1. ≤ b≤ 2^m+1 _τ^t^*+2^m-1. Since a trapped forest exists, Ns0τN_s_0^τ contains at least one term. Every term is positive in K, so Ns0τ>0N_s_0^τ>0. The denominator DτD^τ is also positive. By Equation 13, qs0τ q_s_0^τ =Ns0τDτ>0. = N_s_0^τD^τ>0. The leading coefficients in both forest sums are positive and cannot cancel. Hence ν(Ns0τ) ν(N_s_0^τ) =a, =a, ν(Dτ) ν(D^τ) =min(a,b), = (a,b), ν(qs0τ) ν(q_s_0^τ) =a−min(a,b)=max(0,a−b). =a- (a,b)= (0,a-b). If ρτf∗≤ρτt∗ _τ^f^*≤ _τ^t^*, then a−b a-b ≤2m+1(ρτf∗−ρτt∗)+2m−1 ≤ 2^m+1( _τ^f^*- _τ^t^*)+2^m-1 ≤2m−1. ≤ 2^m-1. Therefore ν(qs0τ)≤2m−1ν(q_s_0^τ)≤ 2^m-1, proving the first claim. If ρτf∗>ρτt∗ _τ^f^*> _τ^t^*, both minima are finite integers, so their difference is at least 11. Thus a−b a-b ≥2m+1(ρτf∗−ρτt∗)−(2m−1) ≥ 2^m+1( _τ^f^*- _τ^t^*)-(2^m-1) ≥2m+1. ≥ 2^m+1. Consequently, ν(qs0τ)=a−b≥2m+1ν(q_s_0^τ)=a-b≥ 2^m+1, proving the second claim. ∎ The bounds separate strategies that satisfy the forest criterion from those that violate it. A violating strategy has a strictly larger encoded value at s0s_0. This allows us to check the criterion using one optimal strategy. Lemma B.0 (One-response certificate). Fix the team’s action ranks and let σΠ _ be the Puiseux team strategy that realises them. The following statements are equivalent. (1) In the original game, for every deterministic memoryless opponent strategy τ′τ , st(ℙs0σΠ,τ′(◇T))=1. (P_s_0 _ ,τ ( T) )=1. (2) In the encoded MDP, there exists a stable opponent strategy τ such that ρτf∗>ρτt∗ _τ^f^*> _τ^t^*. Proof. By Lemmas 25 and 27, the first statement holds if and only if ρτ′f∗>ρτ′t∗ _τ ^f^*> _τ ^t^* for every opponent strategy τ′τ . Suppose the first statement holds. A stable strategy τ exists by Lemma 29. It satisfies ρτf∗>ρτt∗ _τ^f^*> _τ^t^*, proving the second statement. Conversely, fix a stable strategy τ satisfying ρτf∗>ρτt∗ _τ^f^*> _τ^t^*. Suppose some strategy τ′τ satisfies ρτ′f∗≤ρτ′t∗ _τ ^f^*≤ _τ ^t^*. By Lemma 30, qs0τ′ q_s_0^τ >0, >0, ν(qs0τ′) ν(q_s_0^τ ) ≤2m−1, ≤ 2^m-1, whereas qs0τq_s_0^τ is zero or has rank at least 2m+12^m+1. Thus qs0τ′>qs0τq_s_0^τ >q_s_0^τ. Indeed, their difference has the same positive leading term as qs0τ′q_s_0^τ . This contradicts Lemma 29. Therefore every opponent strategy satisfies the forest criterion, proving the first statement. ∎ B.3.3. Checking stability in polynomial time Fix a deterministic memoryless strategy τ. For a vertex u∈Uu∈ U and an action b∈Ab∈ A_ O, define the Bellman residual (16) Rτ(u,b)=quτ−∑v∈VP~(u,b,v)qvτ.R^τ(u,b)=q_u^τ- _v∈ V P(u,b,v)q_v^τ. Stability requires every residual to be nonnegative. In this subsection, we propose a polynomial algorithm to determine the sign of the Bellman residuals. Naively evaluating the forest sums is not possible, as checking all possible forests would take exponential time. Moreover, the residual is zero for b=τ(u)b=τ(u) by Equation 14, so we only check the case where b≠τ(u)b≠τ(u). For a forest F∈ℱτF _τ, let χF(v) _F(v) be 11 if the vertex v leads to f∗f^* in the forest F, and 00 otherwise. Let (τ,u,b)T(τ,u,b) consist of the spanning trees that select one edge from E(z,τ(z))E(z,τ(z)) at every z∈Uz∈ U and one additional edge from E(u,b)E(u,b). For such a tree T, let eb(T)e_b(T) be its unique edge from E(u,b)E(u,b). By Lemma 12, F=T∖eb(T)F=T \e_b(T)\ belongs to ℱτF_τ. Define sgn(T)=+1sgn(T)=+1 if χF(u)=1 _F(u)=1, and −1-1 otherwise. Lemma B.0 (Signed tree formula). For u∈Uu∈ U and b≠τ(u)b≠τ(u), (17) Zu,bDτRτ(u,b)=∑T∈(τ,u,b)sgn(T)ϵρ^(T).Z_u,bD^τR^τ(u,b)= _T (τ,u,b)sgn(T)ε ρ(T). Moreover, the residual is zero if and only if (τ,u,b)T(τ,u,b) is empty. Otherwise, its sign is the sign of the unique tree of minimum rank. Proof. Recall that qvτ=Nvτ/Dτq_v^τ=N_v^τ/D^τ. Here NvτN_v^τ is the sum of the weights of forests in which v leads to f∗f^*, and DτD^τ is the sum of all forests. For an edge e=(u,b,v)e=(u,b,v), its transition probability is P~(u,b,v) P(u,b,v) =ϵρ^(e)Zu,b, = ε ρ(e)Z_u,b, Zu,b Z_u,b =∑e∈E(u,b)ϵρ^(e). = _e∈ E(u,b)ε ρ(e). Using the definition of the Bellman residual: Rτ(u,b) R^τ(u,b) =quτ−∑v∈VP~(u,b,v)qvτ =q_u^τ- _v∈ V P(u,b,v)q_v^τ =NuτDτ−∑e=(u,b,v)∈E(u,b)ϵρ^(e)Zu,bNvτDτ. = N_u^τD^τ- _e=(u,b,v)∈ E(u,b) ε ρ(e)Z_u,b N_v^τD^τ. Multiplying by Zu,bDτZ_u,bD^τ gives Zu,bDτRτ(u,b) Z_u,bD^τR^τ(u,b) =Zu,bNuτ−∑e=(u,b,v)∈E(u,b)ϵρ^(e)Nvτ =Z_u,bN_u^τ- _e=(u,b,v)∈ E(u,b)ε ρ(e)N_v^τ =∑e=(u,b,v)∈E(u,b)ϵρ^(e)Nuτ−∑e=(u,b,v)∈E(u,b)ϵρ^(e)Nvτ = _e=(u,b,v)∈ E(u,b)ε ρ(e)N_u^τ- _e=(u,b,v)∈ E(u,b)ε ρ(e)N_v^τ (expand Zu,bZ_u,b) =∑e=(u,b,v)∈E(u,b)ϵρ^(e)(Nuτ−Nvτ). = _e=(u,b,v)∈ E(u,b)ε ρ(e)(N_u^τ-N_v^τ). (combine the two sums) By the definition of χF _F, Nuτ−Nvτ N_u^τ-N_v^τ =∑F∈ℱτ(χF(u)−χF(v))ϵρ^(F). = _F _τ( _F(u)- _F(v))ε ρ(F). Now, we prove Equation 17 by the following bijection. A pair (F,e)(F,e) contributes to the left side only when u and v lead to different roots. Its coefficient is +1+1 if u leads to f∗f^*, and −1-1 otherwise. The forest has two connected components, each containing one root. Thus, adding e joins them without creating a cycle. Also, e∉Fe∉ F since b≠τ(u)b≠τ(u). Hence F∪e∈(τ,u,b)F∪\e\ (τ,u,b). Conversely, deleting eb(T)=(u,b,v)e_b(T)=(u,b,v) from a tree T gives a consistent forest and separates u from v. Each connected component contains one root by Lemma 12. These operations are inverse, and ρ^(T) ρ(T) =ρ^(F)+ρ^(eb(T)), = ρ(F)+ ρ(e_b(T)), sgn(T) (T) =χF(u)−χF(v). = _F(u)- _F(v). This proves Equation 17. Distinct trees have distinct encoded ranks, so the minimum term cannot cancel and determines the sign. Since both Zu,bZ_u,b and DτD^τ are nonnegative, multiplying by them does not change the sign. ∎ Next, we focus on determining the sign of the minimum-rank tree. Define =E(z,τ(z)):z∈U∪E(u,b), =\E(z,τ(z)):z∈ U\∪\E(u,b)\, E′ E =⋃G∈G. = _G G. These are |U|+1=n−1|U|+1=n-1 nonempty, disjoint groups, where n=|V|n=|V|. Let ℐ1I_1 contain the subsets of E′E with at most one edge from each group. Let ℐ2I_2 contain the subsets with no undirected cycle. These are the independent sets of a partition matroid and a graphic matroid, respectively. A common independent set belongs to both. Give each edge the profit W W =∑e∈E′ρ^(e), = _e∈ E ρ(e), (total encoded rank) p(e) p(e) =W+1−ρ^(e). =W+1- ρ(e). (profit of an edge) Weighted matroid intersection finds a common independent set of maximum profit in polynomial time (Schrijver, 2003). Algorithm 3 Residual Sign ResidualSign 1: Input: ℳ M, ρ ρ, τ, u∈Uu∈ U, b≠τ(u)b≠τ(u) 2: Output: The sign of Rτ(u,b)R^τ(u,b) 3: T←MinTree(ℳ^,ρ^,τ,u,b)T← MinTree( M, ρ,τ,u,b) 4: if T=⊥T= then 5: return 00 6: eb←e_b← the unique edge in T∩E(u,b)T∩ E(u,b) 7: F←T∖ebF← T \e_b\ 8: if u leads to f∗f^* in F then 9: return +1+1 10: else 11: return −1-1 Algorithm 4 Minimum Tree MinTree 1: Input: ℳ M, ρ ρ, τ, u∈Uu∈ U, b≠τ(u)b≠τ(u) 2: Output: A minimum encoded-rank tree in (τ,u,b)T(τ,u,b), or ⊥ 3: ←E(u,b)G←\E(u,b)\ 4: for all z∈Uz∈ U do 5: ←∪E(z,τ(z))G ∪\E(z,τ(z))\ 6: E′←⋃G∈GE ← _G G 7: ℐ1←PartitionMatroid()I_1← PartitionMatroid(G) ⊳ At most one edge per group 8: ℐ2←GraphicMatroid(V,E′)I_2← GraphicMatroid(V,E ) ⊳ No undirected cycle 9: W←∑e∈E′ρ^(e)W← _e∈ E ρ(e) 10: for all e∈E′e∈ E do 11: p(e)←W+1−ρ^(e)p(e)← W+1- ρ(e) 12: J←WeightedMI(ℐ1,ℐ2,p)J← WeightedMI(I_1,I_2,p) 13: if |J|<|V|−1|J|<|V|-1 then 14: return ⊥ 15: else 16: return J Lemma B.0 (Polynomial stability test). Algorithm 3 computes the sign of Rτ(u,b)R^τ(u,b) in polynomial time. Consequently, stability of τ can be checked in polynomial time. Proof. A common independent set of size n−1n-1 selects one edge from each group and is acyclic. It is connected since it has n−1n-1 edges on n vertices. Thus, these sets are (τ,u,b)T(τ,u,b). For J⊆E′J E , we have 0≤ρ^(J)≤W0≤ ρ(J)≤ W and p(J) p(J) =∑e∈Jp(e) = _e∈ Jp(e) =(W+1)|J|−ρ^(J). =(W+1)|J|- ρ(J). (sum the edge profits) If |J|>|J′||J|>|J |, then p(J)−p(J′) p(J)-p(J ) =(W+1)(|J|−|J′|)−ρ^(J)+ρ^(J′) =(W+1)(|J|-|J |)- ρ(J)+ ρ(J ) ≥(W+1)−W=1. ≥(W+1)-W=1. For equal sizes, p(J)−p(J′)=ρ^(J′)−ρ^(J)p(J)-p(J )= ρ(J )- ρ(J). Hence maximum profit gives maximum size and then minimum encoded rank. If |J|<n−1|J|<n-1, no required tree exists. Otherwise, J is the unique minimum tree. Following F from u reaches a root in at most |U||U| steps. The returned sign is therefore correct by Lemma 32. Membership in the two matroids is checked by counting edges in each group and testing for undirected cycles. Both checks take polynomial time. All ranks, profits, and their sums have polynomially many bits. Hence the procedure takes polynomial time. Running the procedure for every u and b≠τ(u)b≠τ(u) uses at most |U||A||U|\,|A_ O| calls. The strategy is stable when no call returns −1-1, since the omitted residuals are zero. ∎ B.3.4. The nondeterministic algorithm Theorem 34 (Membership in NP). The limit-sure reachability problem belongs to NP. Proof. Let N be the number of triples (p,s,a)(p,s,a) with a player p∈Πp∈ , a state s∈Ss∈ S, and an action a∈Apa∈ A_p, and put B=N2B=N N2. Use the following nondeterministic algorithm. Algorithm 5 Nondeterministic Algorithm for Limit-Sure Reachability 1: Input: A game and a rank bound B 2: Output: Accept or reject 3: for all p∈Πp∈ and s∈Ss∈ S do 4: Guess a nonempty support Γp,s⊆Ap _p,s A_p. 5: for all a∈Γp,sa∈ _p,s do 6: Guess rp,s,a∈0,…,Br_p,s,a∈\0,…,B\. 7: for all a∈Ap∖Γp,sa∈ A_p _p,s do 8: rp,s,a←∞r_p,s,a←∞ 9: if mina∈Aprp,s,a≠0 _a∈ A_pr_p,s,a≠ 0 then 10: return Reject 11: Compute the induced transition ranks. 12: Compute the MECs and Trap. 13: if s0∈Ts_0∈ T or =∅ Trap= then 14: return Accept 15: if s0∈s_0∈ Trap then 16: return Reject 17: if no target is reachable from s0s_0 in the support of ℳ♯M then 18: return Reject 19: Build ℳ M and its encoded edge ranks ρ ρ. 20: Guess τ:U→Aτ U→ A_ O. 21: for all u∈Uu∈ U do 22: for all b∈A∖τ(u)b∈ A_ O \τ(u)\ do 23: d←ResidualSign(ℳ^,ρ^,τ,u,b)d← ResidualSign( M, ρ,τ,u,b) 24: if d=−1d=-1 then 25: return Reject 26: Compute ρτf∗ _τ^f^* and ρτt∗ _τ^t^* using Proposition 18. 27: if ρτf∗>ρτt∗ _τ^f^*> _τ^t^* then 28: return Accept 29: else 30: return Reject Running time. Each guessed rank has O((N+1)log(N+2))O((N+1) (N+2)) bits, and the guessed opponent strategy has polynomial size because it is memoryless and deterministic. Transition ranks are computed as in Definition 20. MECs are computed in polynomial time by Lemma 23. The graph and the binary encodings of the weights 2i2^i, 2m+1ρ(ei)+2i2^m+1ρ(e_i)+2^i have polynomial size. There are polynomially many calls to Algorithm 3. Proposition 18 computes the last comparison in polynomial time. Soundness. Consider the realisation of the guessed ranks by the normalised powers of ϵε used in Section B.2. Acceptance in the preprocessing cases is correct by Lemma 25. Otherwise, the guessed response is stable. Therefore, the tested inequalities hold, and those for b=τ(u)b=τ(u) are equalities by Equation 14. The last comparison and Lemma 31 show that the team strategy is Puiseux-winning. In either case, Lemma 7 implies that the team wins limit surely. Completeness. If the team wins limit surely, Lemma 19 gives a Puiseux-winning strategy with finite ranks at most N/2≤BN^N/2≤ B. Some run guesses these supports and ranks. Their normalised-power realisation is also Puiseux-winning by Lemma 17. Thus, preprocessing does not reject. Next, Lemma 31 gives a stable response satisfying the final forest comparison. A run guessing that response passes every check and accepts. ∎ Appendix C Safety We now consider the safety objective =□CW= C, for a set C⊆SC S of safe states. We show that, unlike for reachability, limit-sure and almost-sure winning are equivalent. This is an extension of a known result for concurrent games with two players (Chatterjee et al., 2012) to teams without shared randomness. The two-player proof constructs a memoryless almost-sure winning optimal strategy from a fixed-point characterisation of the game value. We instead use a compactness argument on the space of team strategies. We only show that an almost-sure winning strategy exists if there exists a limit-sure winning strategy. In Section C.1, we establish the topological lemmas used in the main proof. We show that the space of team strategies is compact, and for every opponent strategy, the set of team strategies that guarantee a given safety probability is closed. In Section C.2, we use these lemmas to show that limit-sure winning implies almost-sure winning. C.1. Topological Preliminaries For n∈ℕn , let □nC=s0s1⋯∈Sω∣sk∈C for every 0≤k≤n. _nC=\s^0s^1·s∈ S^ω s^k∈ C for every 0≤ k≤ n\. The events □nC _nC form a decreasing sequence and satisfy □C=⋂n≥0□nC C= _n≥ 0 _nC. We view a team strategy as the collection of all probabilities σp(h)(a) _p(h)(a), for every player p∈Πp∈ , history h∈S+h∈ S^+, and action a∈Apa∈ A_p. We use the usual product topology on these probabilities. We equip ΛΠh _ ^h with the product topology. Lemma C.0 (Compactness of the strategy space). The space ΛΠh _ ^h is compact. Proof. For every player p∈Πp∈ and history h∈S+h∈ S^+, the value σp(h) _p(h) belongs to the simplex Δ(Ap) (A_p), which is compact since ApA_p is finite. By Definition 2, ΛΠh=∏p∈Π(Δ(Ap))S+. _ ^h= _p∈ ( (A_p) )^S^+. Hence ΛΠh _ ^h is compact because the product of compact sets is also compact by Tychonoff’s theorem. ∎ We show that a lower bound on the safety probability defines a closed set of strategies. For a threshold c∈[0,1]c∈[0,1] and a fixed tuple τ _ O of strategies for the opponents, let K(τ,c)=σΠ∈ΛΠh∣ℙs0σΠ,τ(□C)≥c.K( _ O,c)= \ _ ∈ _ ^h _s_0 _ , _ O( C)≥ c \. Lemma C.0 (Closed safety guarantees). For every τ∈Λh _ O∈ _ O^h and c∈[0,1]c∈[0,1], the set K(τ,c)K( _ O,c) is closed. Proof. For n≥0n≥ 0, define fn:ΛΠh×Λh⟶[0,1],fn(σΠ,τ)=ℙs0σΠ,τ(□nC).f_n: _ ^h× _ O^h [0,1], f_n( _ , _ O)=P_s_0 _ , _ O( _nC). Fix τ _ O. For fixed n, the map σΠ↦fn(σΠ,τ) _ f_n( _ , _ O) depends only on the strategy choices at histories of length at most n+1n+1. There are finitely many such histories, and the probability is a finite sum of products of strategy probabilities and transition probabilities. Hence this map is continuous. Since □nC _nC decreases to □C C, continuity of probability measures from above gives ℙs0σΠ,τ(□C) _s_0 _ , _ O( C) =limn→∞fn(σΠ,τ) = _n→∞f_n( _ , _ O) (since □nC↓□C _nC C) =infn≥0fn(σΠ,τ). = _n≥ 0f_n( _ , _ O). Therefore: K(τ,c)=⋂n≥0σΠ∈ΛΠh∣fn(σΠ,τ)≥c.K( _ O,c)= _n≥ 0 \ _ ∈ _ ^h f_n( _ , _ O)≥ c \. For every n, the set in the intersection is closed by continuity of σΠ↦fn(σΠ,τ) _ f_n( _ , _ O). Therefore, K(τ,c)K( _ O,c) is closed. ∎ Now, we show an existential argument on closed nested sets. Lemma C.0 (Nested closed sets). Let X be compact and let K2⊇K3⊇⋯K_2 K_3 ·s be nonempty closed subsets of X. Then ⋂m≥2Km≠∅ _m≥ 2K_m≠ . Proof. Suppose that ⋂m≥2Km=∅ _m≥ 2K_m= . For every m≥2m≥ 2, let Um=X∖KmU_m=X K_m. Since KmK_m is closed, UmU_m is open, and X X =X∖⋂m≥2Km =X _m≥ 2K_m (the intersection is empty) =⋃m≥2(X∖Km) = _m≥ 2(X K_m) (by De Morgan’s law) =⋃m≥2Um. = _m≥ 2U_m. Thus (Um)m≥2(U_m)_m≥ 2 is an open cover of X. By the definition of compactness, every open cover of X has a finite subcover. Hence there exist indices m1,…,mkm_1,…,m_k such that X=Um1∪⋯∪UmkX=U_m_1∪·s∪ U_m_k. Let M=maxm1,…,mkM= \m_1,…,m_k\. Since the sets KmK_m are decreasing, the sets UmU_m are increasing, so Umi⊆UMU_m_i U_M for every i. Hence X=UMX=U_M. Therefore KM=∅K_M= , which is a contradiction. ∎ C.2. From Limit-Sure to Almost-Sure Winning Theorem 4 (Limit-sure safety equals almost-sure safety). For a game with a safety objective, the team wins limit surely if and only if it wins almost surely. Proof. Almost-sure winning implies limit-sure winning by Definitions 7 and 8. We prove the converse. Suppose that the team wins limit surely. For every integer m≥2m≥ 2, let Km=σΠ∈ΛΠh|ℙs0σΠ,τ(□C)≥1−1m for every τ∈Λh.K_m= \ _ ∈ _ ^h\; |\;P_s_0 _ , _ O( C)≥ 1- 1m for every _ O∈ _ O^h \. Every KmK_m is nonempty by limit-sure winning. Moreover, Km=⋂τ∈ΛhK(τ,1−1m),K_m= _ _ O∈ _ O^hK ( _ O,1- 1m ), so KmK_m is closed by Lemma 2 because an intersection of closed sets is always closed. The sets are nested (K2⊇K3⊇K4⊇⋯K_2 K_3 K_4 ·s), since 1−1m+1>1−1m1- 1m+1>1- 1m. Thus, (Km)m≥2(K_m)_m≥ 2 is a nested sequence of nonempty closed subsets of the compact space ΛΠh _ ^h. By Lemma 3, ⋂m≥2Km≠∅ _m≥ 2K_m≠ . Fix σΠ∗∈⋂m≥2Km _ ^*∈ _m≥ 2K_m. For every τ∈Λh _ O∈ _ O^h and every m≥2m≥ 2, ℙs0σΠ∗,τ(□C)≥1−1m.P_s_0 _ ^*, _ O( C)≥ 1- 1m. Since the left-hand side does not depend on m and is at most 11, it must be equal to 11. Thus ℙs0σΠ∗,τ(□C)=1for every τ∈Λh.P_s_0 _ ^*, _ O( C)=1 every _ O∈ _ O^h. Hence σΠ∗ _ ^* is almost-sure winning. ∎ By (Brice et al., 2026b, Theorem 8 and Corollary 2), almost-sure and sure winning also coincide for safety. Together with Theorem 4, we obtain that for safety objectives, limit-sure, almost-sure, and sure winning are all equivalent. Moreover, sure safety can be decided in polynomial time by computing the largest set of safe states from which some team profile ensures that, against every opponent action profile, all possible successors remain in the set. Hence limit-sure, almost-sure, and sure safety are all decidable in polynomial time. Appendix D IRATL We prove Theorem 1. Fix the input structure (G,L)(G,L) and write for a state formula ψ: Sat(ψ)=s∈S∣(G,L),s⊧ψSat(ψ)=\s∈ S (G,L),s ψ\ for the set Sat(ψ)Sat(ψ). We omit (G,L)(G,L) from the notation if it is clear from context. From the semantics of boolean logic, the following statements hold. Sat(q) (q) =s∈S∣q∈L(s), =\s∈ S q∈ L(s)\, Sat(¬ψ) ( ψ) =S∖Sat(ψ), =S (ψ), Sat(ψ∨χ) (ψ χ) =Sat(ψ)∪Sat(χ). =Sat(ψ) (χ). We write Sub(φ)Sub( ) for the set of distinct state subformulas of φ , including φ itself and the state formulas appearing as arguments of temporal operators. It has size at most the length of φ . Lemma D.0. Consider a formula ⟨C⟩wrθ \! C \! _w^rθ. Given the set of states satisfying each state formula appearing in θ, we can decide in polynomial time using an NP oracle whether this formula holds at a given state. Proof. First consider individual randomisation for a coalition C. For X⊆SX S, define its sure predecessor by C(X)=s∈S∣∃a¯∈AC∀b¯∈AΣ∖C,(δ(s,(a¯,b¯)))⊆X. CPre_C(X)= \s∈ S ∃ a∈ A_C\ ∀ b∈ A_ C,\ Supp(δ(s,( a, b))) X \. This set can be computed in polynomial time. We first consider individual randomisation since the complexity of the shared randomisation is a well-studied problem (de Alfaro et al., 1998). Next. Let T=Sat(ψ)T=Sat(ψ). For sure, almost-sure and limit-sure, the winning set for ○ψ ψ is C(T) CPre_C(T). If s∈C(T)s∈ CPre_C(T), clearly there is a sure winning strategy from s. Conversely, suppose s∉C(T)s∉ CPre_C(T), and let η>0η>0 be the smallest positive transition probability in G. For every team profile a¯ a, some opponent profile has probability at least η of reaching S∖TS T in the next step. If the opponent chooses uniformly and independently, every opponent profile has probability 1/|AΣ∖C|1/|A_ C|. Hence, against any choice of the team, the probability of reaching S∖TS T is at least η/|AΣ∖C|>0η/|A_ C|>0. This rules out limit-sure winning, and therefore also almost-sure winning. Always. Let U=Sat(ψ)U=Sat(ψ). By Theorem 1, limit-sure safety implies almost-sure safety. An almost-sure safety strategy can be made deterministic by choosing an action that has positive probability by the strategy for each team player at each history. If the resulting strategy admitted an unsafe play, its finite prefix ending at the first unsafe state would have positive probability under the original strategy which leads to a contradiction. Thus all three of sure, limit-sure and almost-sure safety coincide. Their winning set can be computed by repeatedly computing ZiZ_i as below until a fixpoint is reached. Z0=U,Zi+1=U∩C(Zi).Z_0=U, Z_i+1=U∩ CPre_C(Z_i). Indeed, ZiZ_i is the set from which the team can surely remain in U for i transitions. At the fixed point, the witnessing strategy keeps the play inside the set forever. There are at most |S||S| many times this can decrease, so the computation is polynomial. Until. For φ1φ2 _1\, U\, _2, let U=Sat(φ1)U=Sat( _1), T=Sat(φ2)T=Sat( _2), and F=S∖(U∪T)F=S (U∪ T). We make every state in T∪FT∪ F absorbing and use the reachability objective ◇T T. The sets U and T are computed in the original structure. and remain fixed. Strategies in the two games are the same until a vertex in T∪FT∪ F is visited. Reaching T before F satisfies both the original until objective and the modified reachability objective and reaching F first violates both the original until objective and the modified reachability objective. If a play remains in U∖TU T forever, then it violates both objectives. This also covers initial states in T or F, and preserves winning probabilities and sure winning. Hence the reduction preserves sure, almost-sure and limit-sure objectives. Since randomisation is useless for sure reachability, this reduces the problem with sure reachability to two-player case for which there are polynomial algorithms provided by previous works (de Alfaro et al., 2007). Almost-sure reachability is in NP (Brice et al., 2026b, Theorem 6), and limit-sure reachability is in NP by Theorem 16. Shared randomisation. We can merge the coalition C of players into one player that has the action set ACA_C. The opponent also can be always treated as one player. The resulting two-player concurrent game has polynomial-time algorithms for qualitative reachability (de Alfaro et al., 2007). ∎ Before we state the lemma and prove the lower bound for the qualitative fragment, we state the problem from which we reduce, which is sequentially nested SAT. This problem is complete for the complexity class P NP. Definition D.0 ( SNSAT). An instance I consists of an integer n≥1n≥ 1, distinct Boolean variables x1…,xnx_1…,x_n, pairwise disjoint finite sets Y1,…,YnY_1,…,Y_n of Boolean variables, disjoint from the xix_is and 3-CNF formulas F1,…,FnF_1,…,F_n such that Var(Fi)⊆x1,…,xi−1∪YiVar(F_i) \x_1,…,x_i-1\∪ Y_i We inductively define v1,…,vn∈0,1v_1,…,v_n∈\0,1\ as: vi=1if∃νi:Yi→0,1 such that Fi(v1,…,vi−1,νi)=1).v_i=1 ∃\, _i\ :Y_i→\0,1\ such that F_i(v_1,…,v_i-1, _i)=1). The decision problem is to check if vn=1v_n=1. Without loss of generality, we assume that an instance of the problem such that each 3-CNF formula FiF_i has at least one clause and that each clause has three literals per clause. Lemma D.0. Model checking qualitative IRATL on explicitly represented finite stochastic game structures is P NP-hard. Proof. We provide a reduction from the sequentially nested satisfiability problem of Laroussinie, Markey and Schnoebelen (Laroussinie et al., 2001) which is defined in Definition 2. The precise 3-CNF version above is stated in the proof of (Laroussinie et al., 2008, Proposition 3.10), where its P NP-completeness is shown. We reduce from SNSAT, which consists of a sequence of satisfiability questions in which each formula may depend on the the satisfaction of the previous questions. We first give some intuition. We construct a game in which two cooperating players independently choose a clause and a literal within it. The opponent challenges a pair of clauses, checking that the players agree when selecting from the same clause and never select complementary literals. Given a satisfying assignment, the team can choose a true literal from every clause and pass every challenge. Conversely, an almost-sure winning strategy must cover every clause and make mutually consistent choices, from which a satisfying assignment can be extracted. To capture dependencies between questions, a selected literal referring to an earlier answer leads to a state representing that answer or its negation. Nested IRATL formulas then evaluate these states using the preceding formula layer. Some additional states in the construction of the game-gadget ensures that the resulting formula at the positive state for the final question therefore decides the original SN-SAT instance. Construction of the labelled game structure. Let m≥1m≥ 1 be the number of clauses of each FiF_i. We assume that each FiF_i has the same number of clauses without loss of generality. In FiF_i, let the literal ℓ1=i,c,r _1=i,c,r denote the literal at clause c and position r∈1,2,3r∈\1,2,3\. For instance, for a clause (a∨¬b∨c)(a b c), the literal a has position 11 and ¬b b position 2. We also write [d][d] to denote the set 1,…,d\1,…,d\ of positive integers up to d. The players are in the set Σ=a,b,o =\a,b,o\. For the input SNSAT instance that consists of the integer n, we define the game instance GIG_I with 4n+44n+4 many states as follows, with 2n+22n+2 states in S0S_0 and 2n+22n+2 states in S1S_1 defined as follows: S0 S_0 =,∪si+,si−∣i∈[n], =\ t, f\∪\s_i^+,s_i^- i∈[n]\, S1 S_1 =u^∣u∈S0,S=S0∪˙S1. =\ u u∈ S_0\, S=S_0 ∪S_1. The action sets available at each state is Aa=Ab=[m]×[3],Ao=[m]2×[2].A_a=A_b=[m]×[3], A_o=[m]^2×[2]. Intuitively, each player’s action selects a clause and location thereby choosing a literal, while the opponent that selects the action (u,v,h)(u,v,h) challenges a clause u for a and v for clause b and inspect a if h=1h=1 and b if h=2h=2. Finally, we define the state variables Q=q,p,zQ=\q,p,z\ and define the labelling completely as follows: LI()=q,z,LI(u)=q(u∈S0∖),LI(u^)=p(u∈S0).L_I( t)=\q,z\, L_I(u)=\q\\ (u∈ S_0 \ t\), L_I( u)=\p\\ (u∈ S_0). We now define the transition function. From all states except the states that are of the form si−s_i^-, every action profile leads to another state deterministically, and independent of the actions and we first define that. Since this part is deterministic, we define a function D:S×Aa×Ab×Ao→SD:S× A_a× A_b× A_o→ S and then define δ(s,α)(w)=1if w=D(s,α),0otherwise.δ(s,α)(w)= cases1&if w=D(s,α),\\ 0&otherwise. cases For every action profile α, we define D(u^,α) D( u,α) =u =u (u∈S0), (u∈ S_0), D(,α) D( t,α) =^,D(,α)=^, = f, D( f,α)= t, D(si+,α) D(s_i^+,α) =si− = s_i^- (i∈[n]). (i∈[n]). (a) Constant states tq,z\q,z\ fp\p\ fq\q\ tp\p\(b) Variable states, for each i∈[n]i∈[n]si+ s_i^+p\p\si+s_i^+q\q\si− s_i^-p\p\si−s_i^-q\q\ Figure 5. States and their proposition labels. Arrow represents that every action profile and has transition probability 11 to the state. Two panels of states, each drawn as a box with its set of propositions. Base states are blue and hatted copies are orange. Panel (a), constant states: a cycle from t, labelled q and z, to the copy of f, labelled p, to f, labelled q, to the copy of t, labelled p, and back to t. Panel (b), variable states for each i: a chain from the copy of s_i plus, labelled p, to s_i plus, labelled q, to the copy of s_i minus, labelled p, to s_i minus, labelled q. Every arrow is taken with probability 1 under every action profile. It remains to define D at si−s_i^-. For a literal of FiF_i, we define a state for an literal an intermediary mapping τi _i, using which we define D: τi(ℓ)=if ℓ=y or ℓ=¬y for y∈Yi,sj+if ℓ=xj for j<i,sj−if ℓ=¬xj for j<i. _i( )= cases t&if $ =y$ or $ = y$ for $y∈ Y_i$,\\ s_j^+&if $ =x_j$ for $j<i$,\\ s_j^-&if $ = x_j$ for $j<i$. cases Given an action profile of all players, α=((c,r),(d,t),(u,v,h))α=((c,r),(d,t),(u,v,h)), we write ℓa=ℓi,c,r,ℓb=ℓi,d,t. _a= _i,c,r, _b= _i,d,t. We say that the literals are complementary if one is a variable and the other its negation. We now define the remaining transitions from state si−s_i^-. (1) If (c,d)≠(u,v)(c,d)≠(u,v), then D(si−,α)=si−D(s_i^-,α)=s_i^-. (2) If (c,d)=(u,v)(c,d)=(u,v) and either (c=d and r≠t)(c=d and r≠ t) or ℓa,ℓb _a, _b are complementary, then D(si−,α)=^D(s_i^-,α)= f. (3) Otherwise, D(si−,α)=τi(ℓa)^D(s_i^-,α)= _i( _a) if h=1h=1, and D(si−,α)=τi(ℓb)^D(s_i^-,α)= _i( _b) if h=2h=2. This comparison is very similar to the lower bound hardness construction in Brice et al. (Brice et al., 2026b). Similar to their work, where the players guess vertices that form k-clique and the opponent checks if their guesses are consistent, here the players select literals and the opponent check if these choices are consistent. Figure 6 shows these three cases. si−s_i^-q\q\ fp\p\ tp\p\sj+ s_j^+p\p\sj− s_j^-p\p\ fq\q\ tq,z\q,z\sj+s_j^+q\q\sj−s_j^-q\q\(1) Indexdoesn’tmatch(2) Inconsistent choices(3) ℓ=y =y or ¬y y, y∈Yiy∈ Y_i(3) ℓ=xj =x_j, j<ij<i(3) ℓ=¬xj = x_j, j<ij<iall profilesall profilesall profilesall profiles Figure 6. All transition from state si−s_i^-.Transitions from state s_i minus, labelled q. Case 1: if the index does not match, a self-loop back to s_i minus. Case 2: if the choices are inconsistent, a transition to the copy of f. Case 3: a transition to the copy of t if the literal is y or not y for some y in Y_i, to the copy of s_j plus if the literal is x_j with j less than i, and to the copy of s_j minus if the literal is not x_j with j less than i. Each copy, labelled p, moves under all action profiles to the corresponding base state: f labelled q, t labelled q and z, s_j plus labelled q, and s_j minus labelled q. Construction of the state and formula. Let the coalition be C=a,bC=\a,b\ and define the IRATL state formulas inductively by Φ0 _0 =z, =z, Φk+1 _k+1 =¬⟨C⟩(q(p∧⟨∅⟩○Φk)). = \! C \! _ almost ind (q\, U\, (p \! \! _ sure ind _k ) ). The output of the reduction is the model-checking instance ((GI,LI),sn+,Φ2n) ((G_I,L_I),s_n^+, _2n ). We note that the construction is polynomial in the size of SNSAT instance. A consequence of the next and until semantics. For any IRATL state formula ψ, we use the following abbreviation for the state formula to avoid some cumbersome notation χψ=p∧⟨∅⟩○ψ. _ψ=p \! \! _ sure ind ψ. By the labelling and the sure-next semantics in Section 5, u⊧̸χψ(u∈S0),u^⊧χψ⟺u⊧ψ.u _ψ (u∈ S_0), u _ψ u ψ. Indeed, every profile at u u has the single successor u. Every state in S0S_0 satisfies q, and none in S1S_1 does. Consequently, a play starting in S0S_0 satisfies qχψq\, U\, _ψ exactly when its first visit to S1S_1 occurs at a state u u with u⊧ψu ψ. A play that does not visit S1S_1 cannot satisfy the strong-until objective. If its first state in S1S_1 fails χψ _ψ, the objective also fails, since q needs to be visited earlier for until to hold. We now show correctness at si−s_i^-. Proposition D.0. Fix i, an IRATL state formula ψ, and β1,…,βi−1∈0,1 _1,…, _i-1∈\0,1\ such that ⊧ψ,⊧̸ψ, t ψ, f ψ, sj+⊧ψ⟺βj=1,sj−⊧ψ⟺βj=0(j<i). s_j^+ ψ\ \ _j=1, s_j^- ψ\ \ _j=0 (j<i). We claim that si−⊧⟨C⟩(qχψ)⟺∃νi:Yi→0,1Fi(β1,…,βi−1,νi)=1.s_i^- \! C \! _ almost ind(q\, U\, _ψ) ∃ _i:Y_i→\0,1\\;F_i( _1,…, _i-1, _i)=1. Proof. (⟸).( ). Fix a satisfying assignment and choose one true literal position rcr_c in each clause c. At state si−s_i^-, each of a,ba,b independently plays the memoryless strategy (c,rc)(c,r_c) with probability 1/m1/m for each c∈[m]c∈[m] and assigns probability zero to every other action and plays arbitrary distributions at other states. Selected literals agree within a clause, are never complementary, and all selected xjx_j-literals have their prescribed truth values. Whenever the clause indices match the opponent’s indices, the successor therefore satisfies χψ _ψ, by the definition of τi _i. For every opponent action, conditional on still being at si−s_i^-, matching has probability 1/m21/m^2. Using induction on N, we can bound the probability of staying at si−s_i^- for N transitions by (1−1/m2)N(1-1/m^2)^N. The probability of staying there forever is therefore zero. Every first visit to S1S_1 satisfies χψ _ψ. The until semantics proves the left-hand side of the proposition. (⟹).( ). Suppose that (si−⊧⟨C⟩almostind(q,U,χψ))(s_i^- C _almost^ind(q,U, _ψ)). Let Rψ=u^∈S1|u⊧ψ,R_ψ= u∈ S_1 u ψ, where satisfaction of ψ is evaluated in the original structure. From si−s_i^-, every transition either remains at si−s_i^- or visits S1S_1. Moreover, the until objective is satisfied exactly when the first state reached in S1S_1 belongs to RψR_ψ. Therefore, making every state in S1S_1 absorbing and taking RψR_ψ as the reachability target preserves the winning probability from the state si−s_i^- for every strategy profile. By the memoryless sufficiency theorem for almost-sure reachability (Brice et al., 2026b, Theorem 5), there exists a memoryless almost-sure winning team strategy in the modified game. Its action at si−s_i^- also ensures the original until objective is almost surely. For d∈a,bd∈\a,b\ and c∈[m]c∈[m], let Rd(c)=r∈[3]∣σd(si−)(c,r)>0R_d(c)=\r∈[3] _d(s_i^-)(c,r)>0\ be the literal positions player d selects with positive probability in clause c. Every Rd(c)R_d(c) is nonempty. Otherwise, if Ra(c)=∅R_a(c)= , the opponent can play the action (c,1,1)(c,1,1) at every visit to si−s_i^-, forcing the game to stay forever at the state. If Rb(c)=∅R_b(c)= , the opponent can instead play (1,c,1)(1,c,1), thus also preventing the team from winning almost surely. Now the opponent can choose the same clause for both players by choosing the action (c,c,1)(c,c,1). Since the team cannot coordinate their randomness, (r,t)∈Ra(c)×Rb(c)(r,t)∈ R_a(c)× R_b(c) also occurs with positive probability. If r≠tr≠ t, the next state is f, which does not satisfy χψ _ψ and hence does not satisfy the until objective. Thus there is a unique position rcr_c such that Ra(c)=Rb(c)=rcR_a(c)=R_b(c)=\r_c\. The selected literals ℓi,c,rc _i,c,r_c are pairwise noncomplementary since the action (c,d,1)(c,d,1) played by the opponent to two clauses with complementary selected literals reaches the state f with positive probability. Moreover, every selected literal over an earlier variable xjx_j is true under β. If such a literal in clause c were false and if the opponent plays (c,c,1)(c,c,1), the play would reach τi(ℓi,c,rc) _i( _i,c,r_c) with positive probability, and this state fails χψ _ψ by the assumptions on ψ and β. Both cases contradict almost-sure winning. Let us assign each selected local literal to be true, and assign all remaining variables in YiY_i arbitrarily. This defines a consistent valuation νi _i, since no local variable is selected with both signs. Every clause has its selected literal true under (β,νi)(β, _i), so Fi(β1,…,βi−1,νi)=1F_i( _1,…, _i-1, _i)=1. This proves the forward direction. ∎ Correctness of the reduction. Proposition D.0. For the constructed structure (GI,LI)(G_I,L_I) and formulas Φk _k, si−⊧Φk⟺vi=0for every k≥2i−1,si+⊧Φk⟺vi=1for every k≥2i,i∈[n]. aligned s_i^- _k& v_i=0&&for every k≥ 2i-1,\\ s_i^+ _k& v_i=1&&for every k≥ 2i, aligned i∈[n]. Proof. For every k≥0k≥ 0, (18) ⊧Φk+1 t _k+1 ⟺⊧̸Φk, f _k, ⊧Φk+1 f _k+1 ⟺⊧̸Φk, t _k, si+⊧Φk+1 s_i^+ _k+1 ⟺si−⊧̸Φk. s_i^- _k. Since Φ0=z _0=z, we have ⊧Φ0 t _0 and ⊧̸Φ0 f _0. From the first two equivalences, we have ⊧Φk t _k and ⊧̸Φk f _k for all k≥0k≥ 0. We now induct on the index i. Base case: i=1i=1. Fix any k≥1k≥ 1. The formula F1F_1 has no earlier variables, so the fact that ⊧Φk t _k and ⊧̸Φk f _k is enough for Proposition 4 with ψ=Φk−1ψ= _k-1. The team can satisfy the corresponding almost-sure until objective from s1−s_1^- exactly when F1F_1 is satisfiable, that is, when v1=1v_1=1. Since Φk _k is the inverse of this objective, s1−⊧Φk⟺v1=0(k≥1).s_1^- _k v_1=0 (k≥ 1). For any k≥2k≥ 2, the third equivalence in Equation 18 implies that s1+⊧Φk⟺s1−⊧̸Φk−1⟺v1=1.s_1^+ _k s_1^- _k-1 v_1=1. Induction step: i>1i>1. Assume both equivalences in the proposition hold for every j<ij<i. Let k≥2i−1k≥ 2i-1. For each j<ij<i, k−1≥2i−2≥2j.k-1≥ 2i-2≥ 2j. Thus the induction hypothesis ensures that Φk−1 _k-1 satisfies both: sj+⊧Φk−1⟺vj=1,sj−⊧Φk−1⟺vj=0.s_j^+ _k-1 v_j=1, s_j^- _k-1 v_j=0. Together with the fact that ⊧Φk t _k and ⊧̸Φk f _k, this shows that for Proposition 4 with ψ=Φk−1ψ= _k-1 and βj=vj _j=v_j. That equivalence identifies the almost-sure until objective at si−s_i^- with satisfiability of FiF_i after fixing the earlier answers, which is exactly vi=1v_i=1. By the definition of Φk _k, we obtain si−⊧Φk⟺vi=0(k≥2i−1).s_i^- _k v_i=0 (k≥ 2i-1). Finally, for k≥2ik≥ 2i. Since k−1≥2i−1k-1≥ 2i-1, the equivalence just proved and Proposition 4 gives si+⊧Φk⟺si−⊧̸Φk−1⟺vi=1.s_i^+ _k s_i^- _k-1 v_i=1. This completes the induction. ∎ Proposition 5 shows that I∈SNSAT⟺vn=1⟺(GI,LI),sn+⊧Φ2n.I v_n=1 (G_I,L_I),s_n^+ _2n. This completes the proof of the lemma. ∎ See 1 Proof of Theorem 1. We evaluate the input formula φ from the inside out, computing for each state subformula the set of states where it evaluates to true. • For an atom, this set is given by the labelling. • For negation, we take the complement of the set already computed for its argument. • For disjunction, we take the union of the two argument sets. • When we evaluate a subformula of this form ⟨C⟩wrθ \! C \! _w^rθ, the satisfying sets of its arguments are already computed. • We use Lemma 1 to determine, from each state, whether the coalition can ensure the objective under the specified winning condition and type of randomisation. We can use an induction on the formula to show that this procedure computes Sat(φ)Sat( ) correctly. We now show that the problem is in P NP, by showing how to make polynomially many queries to the NP oracle. There are at most |φ|| | state subformulas, and each subformula asking whether a coalition can ensure an objective requires at most one oracle query per state. Each query specifies a winning problem and an instance of that problem, and asks whether the coalition wins from the chosen state. Each query asks which of the winning problems in Lemma 1 is to be decided, and these problems are all in NP. Constructing the queries and computing the remaining states that satisfy the state-formula takes polynomial time. The procedure is therefore deterministic polynomial time with an NP oracle, proving membership in P NP. Hardness. The hardness follows from Lemma 3 even with at most three players and for a fragment that contains deterministic transitions and only sure and almost-sure modalities of the logic. ∎