Paper deep dive
Algorithms for Equilibria in Concurrent Stopping Games
Léonard Brice, Thomas A. Henzinger, K. S. Thejaswini
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 94%
Last extracted: 7/28/2026, 3:18:17 AM
Summary
This paper addresses the constrained existence problem for Nash equilibria in concurrent stopping games, which is known to be undecidable. The authors propose two approaches to achieve tractability: first, an approximate algorithm for ε-Nash equilibria that runs in exponential time with a PSPACE-hardness lower bound; second, an analysis of extreme risk-sensitive equilibria (XRSE), proving the constrained existence problem for XRSE is NP-complete on concurrent games.
Entities (10)
Relation Signals (8)
Constrained Existence Problem → hascomplexity → Undecidable
confidence 98% · The associated constrained existence problem... is undecidable
Constrained Existence Problem → hascomplexity → NP-complete
confidence 96% · We prove that the constrained existence problem for XRSE is NP-complete
Constrained Existence Problem → appliesto → Extreme Risk-Sensitive Equilibria
confidence 95% · constrained existence problem for XRSE is NP-complete
Constrained Existence Problem → appliesto → Concurrent Stopping Games
confidence 95% · remains so even for 10-player stopping games
Extreme Risk-Sensitive Equilibria → appliesto → Concurrent Games
confidence 94% · constrained existence problem for XRSE is NP-complete on concurrent games
Approximate Algorithm → solves → Nash Equilibrium
confidence 94% · decides whether an ε-Nash equilibrium with the prescribed payoffs exists
Approximate Algorithm → hascomplexity → EXPTIME
confidence 93% · The algorithm runs in exponential time
Approximate Algorithm → haslowerbound → PSPACE-hardness
confidence 92% · We complement it with a PSPACE-hardness lower bound
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Concurrent games are a standard model for multi-agent systems, with Nash equilibrium as their central solution concept. The associated \emph{constrained existence problem}---does a game admit a Nash equilibrium whose expected payoff lies within a prescribed interval for every player?---is undecidable, and remains so even for 10-player \emph{stopping} games, in which a terminal state is reached almost surely under every strategy profile. We give two routes to tractability. We first relax exactness and consider the problem of approximate constrained existence problem, parametrised by $\varepsilon$-NE, which decides whether an \(\varepsilon\)-Nash equilibrium with the prescribed payoffs exists. The algorithm runs in exponential time, and only polynomially in the bit-size of \(\varepsilon\). We complement it with a \PSPACE-hardness lower bound that holds already for turn-based games, and for pure equilibria as well. We then relax the solution concept, turning to \emph{extreme risk-sensitive equilibria} (XRSE), recently introduced for turn-based stochastic games. Here the players are partitioned into optimists and pessimists, who evaluate a strategy profile by the best, respectively the worst, payoff attainable with positive probability, instead of the expected payoff. We prove that the constrained existence problem for XRSE is \NP-complete on concurrent games, as for turn-based games.
Tags
Links
- Source: https://arxiv.org/abs/2607.24219v1
- Canonical: https://arxiv.org/abs/2607.24219v1
Trouble viewing inline? Open PDF directly →
Full Text
83,537 characters extracted from source content.
Expand or collapse full text
Algorithms for Equilibria in Concurrent Stopping Games Léonard Brice#Ñ Institute of Science & Technology Austria Thomas A. Henzinger#Ñ Institute of Science & Technology Austria K. S. Thejaswini#Ñ Université Libre de Bruxelles Abstract Concurrent games are a standard model for multi-agent systems, with Nash equilibrium as their central solution concept. The associated constrained existence problem—does a game admit a Nash equilibrium whose expected payoff lies within a prescribed interval for every player?— is undecidable, and remains so even for 10-player stopping games, in which a terminal state is reached almost surely under every strategy profile. We give two routes to tractability. We first relax exactness and consider the problem of approximate constrained existence problem, parametrised byε-NE, which decides whether anε-Nash equilibrium with the prescribed payoffs exists. The algorithm runs in exponential time, and only polynomially in the bit-size ofε. We complement it with aPSPACE-hardness lower bound that holds already for turn-based games, and for pure equilibria as well. We then relax the solution concept, turning to extreme risk-sensitive equilibria (XRSE), recently introduced for turn-based stochastic games. Here the players are partitioned into optimists and pessimists, who evaluate a strategy profile by the best, respectively the worst, payoff attainable with positive probability, instead of the expected payoff. We prove that the constrained existence problem for XRSE is NP-complete on concurrent games, as for turn-based games. 2012 ACM Subject Classification Theory of computation Ñ Automata over infinite objects Keywords and phrases Nash Equilibria, Risk Measure 1 Introduction We now live surrounded by decentralised automated systems involving multiple agents—multi- agent systems. Stochastic games constitute a powerful tool to model those, with applications in epidemic processes [19], formal verification [15], learning theory [1], cyber-physical systems [21], distributed and probabilistic programs [12], and probabilistic planning [22]. More expressive than their turn-based counterparts, concurrent games are stochastic games meant to capture synchronous behaviors. A play in a concurrent game can be described as a sequence of moves of a token on the vertices of a graph: from a given vertex, each player selects, simultaneously and independently, an action. The selected action profile induces a probability distribution over the outgoing edges: the token then moves to a new vertex according to that distribution. In this paper, we consider terminal-reward concurrent games (also known as simple quantitative concurrent games): the graph contains some terminal vertices, where the game stops, and each player receives a specified reward. Preferences of each player among the different plays depend entirely on which terminal vertex is reached, no matter which path was taken. In stochastic games, a natural solution concept is Nash equilibrium (NE). A strategy profile is a Nash equilibrium if no player can improve their expected payoff by deviating from their strategy, assuming the other players stick to theirs. Nash equilibria are known to exist in stochastic games, but may be unsatisfying, as they yield poor payoffs to the arXiv:2607.24219v1 [cs.GT] 27 Jul 2026 2Algorithms for Equilibria in Concurrent Stopping Games players [10,23]. A more ambitious question is known as the constrained existence problem: given a stochastic game and a constraint (usually given as bounds on the players’ expected payoffs), does the game contain an NE that satisfies the constraint? This problem hits the undecidability wall, even in turn-based games with a number of players fixed to 10 [25]. To overcome that barrier and find decidable variants, three natural approaches arise. The first one consists in restricting either the class of games considered, or the class of strategies allowed. Restrictions on the stochastic nature of the problem are unsatisfying: the problem remains undecidable when the players are not allowed to randomise, as well as when the game is deterministic [24]. It is only known to be decidable (in polynomial space) when those two restrictions apply simultaneously, thus ruling out any form of stochasticity [6]. If the players are restricted to memoryless strategies, i.e., play only according to the current vertex, then the problem reduces to deciding the validity of a formula in the existential theory of the reals, which can be done in polynomial space [17]. Such a restriction, although interesting for some formalisms, is of little help in settings such as control theory, where the game graph models an environment for a robot to traverse and the multiple players depict different independent controllers with their own objectives [5,18,16]. Requiring memoryless strategies amounts to the absurdity of a robot repeating the same action every time it revisits a location; encoding the needed memory into the game graph itself causes a significant increase in the size of such an enhanced game graph [18]. The second approach consists in designing approximate algorithms, i.e., algorithms that return yes on positive instances, and no on instances that are sufficiently far from positive— but may return either outputs on instances that are close to the border (using the notion of ε-NE), with a specified acceptable error term. However, to this date, approximate algorithms have only been designed combined with the first approach: the approximate constrained existence problem of memoryless NEs was recently shown to be in the class DRX NP NP [3]. The third approach consists in looking for variants of the notion of NE itself, for which the equivalent problem would be decidable. For classical refinements, such as subgame-perfect equilibria, an easy adaptation of the classical undecidability proof shows that the same result holds. However, a new equilibrium notion was recently proposed for which an algorithm exists: extreme risk-sensitive equilibria [8] (XRSEs). XRSEs are defined as Nash equilibria, with the slight difference that instead of maximising their expected payoffs, the players intend to maximise either the minimal payoff they get with positive probability (pessimistic players), or the maximal one (optimistic players). The constrained existence problem of XRSEs was shown decidable, andNP-complete, in turn-based stochastic games, under randomised or pure strategies. However, the case of concurrent games was left open. Contributions. In this paper, we focus on a classical restriction of concurrent games, namely stopping games. A concurrent game is stopping if for every strategy profile, it is almost sure that some terminal vertex will be reached. This notion rules out a specific case of plays, those that remain in the game forever, which is a sound restriction to model processes that are expected to eventually end, but with no duration bound. The undecidability result cited above still applies with that restriction. In this setting, our contribution is twofold. First, we provide the first known approximate algorithm for the constrained existence problem of NEs, without any restriction on the players’ strategies. That algorithm relies on three ideas: (1) we show that every NE can be transformed into anε-NE with finite memory horizon, meaning that it eventually follows a memoryless strategy profile. Then, (2) we define the characteristic vector of a strategy profile, containing the information of each player’s expected payoff, and the maximal expected payoff they can obtain by deviating. Léonard Brice, Thomas A. Henzinger, K. S. Thejaswini3 Thus, that vector is a finite-dimension object that contains the necessary data to decide whether the strategy profile witnesses a positive instance of the problem. Finally, (3) we show how to iteratively construct an over-approximation of the set of characteristic vectors of strategy profiles with memory horizonk, for any integerk. The over-approximation relies on a discretisation of the space of characteristic vectors: instead of computing the exact set, we compute a union of cubes that covers it. Based on step (1), we compute a number k(which depends on the error term) such that an over-approximation of strategy profiles with memory horizonkis sufficient to decide the problem. The resulting algorithm takes exponential time: thus, switching from the exact problem to the approximate version changes the complexity from undecidable to EXPTIME. We also give a PSPACE lower bound. Our second contribution concerns XRSEs, whose constrained existence problem we prove isNP-complete on concurrent stopping games (Theorem 29), matching the lower bound of the same problem in the turn-based setting [8, Lemma 20]; the work is in theNP-upper bound. It reduces, as in turn-based games, to showing that only polynomial memory for a witness XRSE to exist. Concurrency however makes this step non-trivial and a naïve adaptation of the turn-based proof would lead to an exponential blow-up in the number of players. A further concurrent-specific obstacle is the punishment of players that deviate. When one player deviates, the other players can be assume to form a punishing coalition: however, this punishment may require randomisation, and the punishing players cannot resort to a common randomness source to do so, hence this setting is not reducible to a two-player one, unlike the assumptions in earlier work [2,13]. Since the team in a concurrent game cannot correlate its randomisation, we appeal to recent results that show that memoryless team-punishment strategies without shared randomness [7]. Structure of the paper. In Section 2, we introduce the necessary definitions. In Section 3, we give our approximate algorithm for Nash equilibria, and the lower bound. In Section 4, we give our exact algorithm for XRSEs. We end with a discussion in Section 5. 2 Preliminaries Tuples. For any setXand any finite setI(assumed clear from the context), a tuplepx i q iPI will usually be denoted by ̄x; and conversely, when we are given a tuple ̄x, we denote itsith coordinate asx i . For a fixed elementi P I, we also use the notation ̄x ́i “ px j q jPIztiu , and denote byp ̄x ́i ,x 1 i qthe tuple whoseith element isx 1 i , and whosejth element, for everyj ‰ i, is x j . When the set I corresponds to players, we use the word profile instead of tuple. Distributions and Support. For a finite setX, we denote byDpXqthe set of probability distributions overX, i.e. the set of mappingsd:X Ñ r0,1ssatisfying ř xPX dpxq “1. For a given distribution d, we denote the support of d as Supppdq “ tx P X | dpxq ą 0u. Games. In this paper, we focus on terminal-reward concurrent stochastic multiplayer games. When the context is clear, we simply call them concurrent games or games. § Definition 1 (Concurrent game). A concurrent game is a tuple: G “ pV,v 0 ,T, Π,pA i q iPΠ ,pAv i q iPΠ , ∆,μq consisting of: a finite setVof vertices, containing an initial vertexv 0 and a subsetT Ď Vof terminal vertices; 4Algorithms for Equilibria in Concurrent Stopping Games a finite set Π of players; for each playeri PΠ, a finite setA i of actions, and a mappingAv i :VzT Ñ A i that maps each vertexvto the set of actions available to playeriinv. We also writeA “ ś i A i for the set of action profiles, and Avpvq “ ś iPΠ Av i pvq for the action profiles available in v; a transition function ∆ :pVzTq ˆ ś iPΠ A i Ñ DpVq. For an action profile ̄aplayed at vertex v, the quantity ∆pv, ̄aqpwq denotes the probability of transitioning to vertex w; a payoff functionμ:T Ñ R Π assigning a reward profile to each terminal vertex. For each player i and terminal vertex t, we denote by μ i ptq the ith coordinate of the profile μptq. As specific case, a game is deterministic if for every vertexvand action profile ̄a, the support of the distribution ∆pv, ̄aqis a singleton. It is turn-based if from everyv, only one player faces a non-trivial choice, i.e., the setAv i pvqis a singleton for all players except one. A Markov decision process (MDP) is a game with one player. A Markov chain is a game with zero players. A note on representation. For each vertex, the set of transition probabilities is given as a matrix with dimension|Π|. The size of the transition matrix is exponential in the number of players that have more than one distinct action available at that vertex. If every player has more than one action available, this leads to a size exponential in the number of players; but if at mostcplayers have a non-trivial choice in each state, wherecis a constant, then the space needed to represent the transition function is bounded by Op|V|pmax i |A i |q c q. Plays and histories. A play in the gameGis a sequence of states and action profiles π “ pv 0 , ̄a 0 ,v 1 ,...qthat is either infinite, or ends with a terminal vertex, i.e. a word in the setv 0 ApV Aq ω Y v 0 ApV Aq ̊ T. A history is a finite prefixhof a play that ends with a vertex, i.e. a word in the setpV Aq ̊ V. Given a historyh, we denote the last vertex inhbylastphq. The set of histories is denoted by Hist. The payoff functionμis extended to plays, by definingμpπq “ μptqif the playπeventually reaches the terminal vertex t, and μpπq “ p0q iPΠ if π is infinite. Strategies. A strategy for playeriis a mappingσ i that takes a historyhending in a non-terminal statev, and outputs a probability distribution over the setAv i pvq. A strategy is pure if for every historyh, there is an actionawithσ i phqpaq “1. It is memoryless if for every two histories h,h 1 , we have σ i phq “ σ i ph 1 q whenever lastphq “ lastph 1 q. It is positional if it is simultaneously memoryless and pure. These definitions extend to strategy profiles, and given a historyhand a strategy profile, we abusively write ̄σphqfor the distribution ̄a ÞÑ ś i σ i pa i q. Given a strategyσ i and a historyhv, we denote byσ iæhv the residual strategy the maps each history h 1 starting in v to the distribution σ i phh 1 q. A playπ “ pv 0 , ̄a 0 ,v 1 ,...qis compatible with a strategyσ i if for every stepk, there exists an action profile ̄a P ś iPΠ Supppσ i pπ ďk qqsuch thatv k`1 P Suppp∆pv k , ̄aqq. This definition extends naturally to strategy profiles, and to histories. A complete strategy profile ̄σ “ pσ i q iPΠ defines a probability distributionP ̄σ over plays in the game G. Then, we liberally identify every history h to the event: tπ | the history h is a prefix of πu, by writing for instance P ̄σ phq for the probability that the history h is followed. Under such a probability measure, the payoff functionμ, extended to plays, can be seen as a (measurable) random variable ranging over the spaceR Π . We writeEp ̄σqfor its expected value, and E i p ̄σq for player i’s expected payoff. Léonard Brice, Thomas A. Henzinger, K. S. Thejaswini5 Stopping Games. In this work, we restrict our attention to stopping games. A game is stopping if for every strategy profile ̄σ, the probability of reaching the setTunder ̄σis exactly 1. This hypothesis guarantees that the set of infinite plays has a probability measure of 0, independently from the strategy profile considered. Consequently, the assumption μpπq “ p0q iPΠ for infinite plays π has no impact on expected payoffs. Nash equilibria and their constrained existence problem. The most classical solution concept in multiplayer games is Nash equilibrium. §Definition 2 (Nash equilibrium). A strategy profile ̄σin the gameGis a Nash equilibrium if and only if for each player i and every strategy σ 1 i , we have E i p ̄σ ́i ,σ 1 i q ď E i p ̄σq. Then, a natural decision problem to study is the following one. § Problem 1 (Constrained existence problem of NEs). Given a concurrent gameG, and two payoff profiles ̄x, ̄y P R Π , does there exist a Nash equilibrium ̄σinGsatisfyingx i ď E i p ̄σq ď y i for every player i? However, it is known from the work of Ummels and Wojczak [25, Theorem 4.9] that this problem is undecidable. Their proof goes by a reduction from the halting problem of two-counter machines. A careful reading of that proof shows that the game that is constructed is always stopping, hence this result holds in our more restricted setting. §Theorem 3 ([25]). The constrained existence problem of NEs is undecidable, even in stopping games. Here, we overcome this difficulty by exhibiting two new decidable variants: the approximated version of this problem, and the constrained existence problem of XRSEs. 3 An approximate algorithm for Nash equilibria 3.1 The problem As discussed in the introduction, the constrained existence problem of Nash equilibria is undecidable. In this section, we therefore consider its approximate version, and present the first known algorithm to decide it. §Problem 2 (Approximate constrained existence problem of NEs in stopping games). Given a stopping gameG, two payoff profiles ̄x, ̄y P Q Π , and a rational quantityε ą0, such that we have the guarantee that either: there exists a Nash equilibrium ̄σ in G satisfying x i ď E i p ̄σq ď y i for each player i, or there exists noε-Nash equilibrium satisfyingx i ́ ε ď E i p ̄σq ď y i ` εfor each playeri, are we in the first case? We assume an instance of the problem, and denote the number of non-terminal vertices in the gameGbyN, the maximum reward absolute value byR “ max iPΠ max tPT |μ i ptq|, and the least transition probabilityp min “ min vPV min ̄aPAvpvq min wPSuppp∆pv, ̄aqq ∆pv, ̄aqpwq. The quantity ε is sometimes called error term. 6Algorithms for Equilibria in Concurrent Stopping Games 3.2 A bound on stopping probabilities The gameGis assumed stopping: under every strategy profile, it is almost sure that some terminal vertex will eventually be reached. The following lemma shows that the probability of avoiding terminal vertices for a given amount of time can be bounded. §Lemma 4. Letλ “1 ́ p N min . For every strategy profile ̄σand everyk P N, we have P ̄σ pV kN`1 q ď λ k . Proof. Let us consider the MDP obtained fromG, by merging all players into one agent selecting all players’ actions. Consider the objective of avoiding terminal vertices for at least kN `1 steps. 1 By standard probabilistic theorems [20, Theorem 4.4.2], the agent has a pure strategyσ 0 that maximises the probability of satisfying this objective. Now, from any vertex v, when following that strategy, since the game is stopping, it is almost sure that a terminal will be reached. Therefore, there is a path fromvtoTthat is compatible withσ 0 ; and that path can be chosen of length at mostN `1. Since the strategyσ 0 is pure, each transition along that path is followed with probability at leastp min , which means that said path is followed with probability at leastp N min . Consequently, from any pathv, when followingσ 0 , the probability of avoidingTforN `1 steps is smaller than or equal to 1 ́ p N min “ λ. By iterating this reasoning, the probability of avoidingTforkN `1 steps is smaller than or equal toλ k . By optimality ofσ 0 , the same bound applies to any strategy profile fromv 0 .đ 3.3 Strategy profiles with finite memory horizon In this subsection, we show that Nash equilibria can be approximated byε-NEs with finite memory horizon, a special case of finite-memory strategy profiles. §Definition 5 (Memory horizon). A strategy profile with memory horizonkis a strategy profile ̄σsuch that for every historyhof lengthk, there exist memoryless strategy profile ̄τ h , such that for every history h 1 of which h is a prefix, we have ̄σph 1 q “ ̄τph 1 q. As we will see, a succinct representation of strategy profiles with finite horizon can be constructed in a finite amount of time. This yields us an algorithm thanks to the following lemma: an NE can be approximated by anε-NE with finite memory horizon, by following the NE for some number of steps and then truncate it, to follow memoryless strategies. §Lemma 6 (App. A.1). Let ̄σbe a Nash equilibrium in the gameG. Letδ ą0, and letk such thatλ k ď δ 4R . Then, there exists aδ-Nash equilibrium with memory horizonkNwhere each player has an expected payoff that is at most different by δ2. In all what follows, we fixKas the least integer satisfyingλ K ď ε 8R —such that for every NE, there a ε 2 -NE with memory horizonKNthat has the same expected payoffs. That number grows exponentially with the instance size. § Lemma 7. The numberKgrows exponentially with the game size, and polynomially with the bit-size of ε. Proof. We have: K “ S ́ log ` ε 8R ̆ ́ logpλq W ď log ` ε 8R ̆ logpλq ` 1. On the one hand, the quantity ́ log ` ε 8R ̆ is linear in the bit sizes ofεandR. On the other hand, we have ́ logpλq “ ́ logp1 ́ p N min q „ p N min “ O ` 2 G ̆ .đ 1 By steps, we always mean the number of vertex visits—the number of action interactions is then kN. Léonard Brice, Thomas A. Henzinger, K. S. Thejaswini7 3.4 Characteristic vectors The main idea of our algorithm is that although a history-dependent strategy profile may not be described with finite space, only a small amount of data is needed to decide whether it witnesses a positive instance. That data is captured by its characteristic vector. §Definition 8 (Characteristic vector). Given a gameGand a strategy profile ̄σinG, we define the characteristic vector of ̄σas the vector ̄χ ̄σ P R Πˆtreg,devu where for each playeri, we have χ ireg “ E i p ̄σq, and χ idev “ sup σ 1 i E i p ̄σ ́i ,σ 1 i q. Note that the strategy profile ̄σ is an ε-NE if and only if we have χ ̄σ idev ď χ ̄σ ireg ` ε. 3.5 An over-approximation of finite-memory-horizon strategy profiles We now show how to construct, for everyk, an over-approximation of the set of characteristic vectors of strategy profiles with memory horizonk. We fixD “2pK `1q ̈ R ε , and discretise the space r ́R,Rs Πˆtreg,devu into D 2|Π| cubes of the form: C “ ź γPΠˆtreg,devu „ R d γ D ,R d γ ` 1 D ȷ , where eachd γ is an integer ranging from ́DtoD ́1. The set of those cubes is denotedC. §Definition 9 (The sequencepX k q k ). We define the sequencepX k q k , where each X k is a mapping that maps each vertex to a subset ofr ́R,Rs Πˆtreg,devu , inductively as follows. First, for each vertexv, the set X 0 pvq is the union of all cubesC P Cthat contain a vector ̄χ ̄σ , where ̄σis a memoryless strategy fromv. Then, for eachk, the set X k pvq is the union of all cubes C P C such that there exist: a vector ̄χ P C; vectors ̄χ ̄aw P X k ́1 pwq for each action profile ̄a P Avpvq and w P V , and coefficients α ia P r0, 1s for each player i and action a P Av i pvq, such that, for each player i: we have ř aPAv i pvq α ia “ 1; we have χ ireg “ ř ̄aPAvpvq ř wPV ∆pv, ̄aqpwq ́ ś j α ja j ̄ χ ̄aw ireg ; and we have χ idev “ max a i PAv i pvq ř ̄a ́i PAv ́i pvq ř wPV ∆pv, ̄aqpwq ́ ś j‰i α ja j ̄ χ ̄aw idev . Intuitively, each coefficientα ia represents the probability that playeriperforms actiona at the first step. Then, the vector ̄χ ̄aw represents the characteristic vector of the strategy profile that is followed after performing the action profile ̄aand reaching the vertexw: the vector ̄χ is then the characteristic vector of a strategy profile fromv. Since the whole cube Cis added to the set X k pvq, and not only the vector ̄χ, this set is an over-approximation of the set of characteristic vectors of strategy profiles with memory horizonk; but since the cube size was chosen small enough, the accumulated errors is controlled. §Lemma 10 (App. A.2). For everykand eachv, the set X k pvqcontains all vectors of the form ̄χ ̄σ , where ̄σis a strategy profile fromvwith memory horizonk. Conversely, for every vector ̄χ PX k pvq, there exists a strategy profile ̄σfromvwith memory horizonksatisfying ̄χ ́ ̄χ ̄σ ď pk ` 1q R D . Finally, let us show that those sets can be computed in exponential time. §Lemma 11 (App. A.3). Given the gameG, a vertexvand a numberk, the set X k pvqcan be computed in exponential time. 8Algorithms for Equilibria in Concurrent Stopping Games 3.6 Algorithm We can now use the results proven above to present an algorithm. § Theorem 12. The approximate constrained existence problem of NEs in stopping games is decidable in time exponential in the game size, and polynomial in the bit-size of ε. Proof.We first present the algorithm, then prove its correctness, and later on its complexity. The algorithm. Forkranging from 0 toKN, compute all sets X k pvq. If, for somek, there is a vector ̄χ PX k pv 0 qsuch thatx i ́ ε 2 ď χ ireg ď y i ` ε 2 andχ idev ď χ ireg ` ε 2 for each player i, then stop the algorithm and return yes. Otherwise, return no. If the algorithm returns yes, then we have a positive instance. Assume it returns yes at stepk. Let ̄χ PX k pv 0 qbe the vector detected. By Lemma 10, there is a strategy profile ̄σ fromv 0 such that ̄χ ́ ̄χ ̄σ ď pk ` 1q R D ď pK `1q R D “ ε 2 , by definition ofD. Then, for each player i, we have: χ ̄σ ireg ď χ ireg ` ε 2 ď y i ` ε 2 ` ε 2 ď y i ` ε by the stopping criterion; and similarly, we have χ ̄σ ireg ě x i ́ ε, and: χ ̄σ idev ď χ idev ` ε 2 ď χ ireg ` ε 2 ` ε 2 “ χ ireg ` ε. This shows that the strategy profile ̄σis anε-NE withx i ́ε ď E i p ̄σq ď y i `εfor each player i, and by the guarantee given on the problem instances, that we have a positive instance. If the algorithm returns no, then we have a negative instance. If the algorithm returns no, then the set X KN pv 0 q contains no vector satisfying the stopping criterion. By Lemma 10 again, this means there is no ε 2 -NE with memory horizonKNsatisfyingx i ́ ε 2 ď E i p ̄σq ď y i ` ε 2 for each playeri. Now, by Lemma 6, applied withδ “ ε 2 , any Nash equilibrium satisfying x i ď E i p ̄σq ď y i for each playeriwould yield an ε 2 -NE with memory horizonKNwhose expected payoffs lie inrx i ́ ε 4 , y i ` ε 4 s Ď rx i ́ ε 2 , y i ` ε 2 s: there is therefore no such Nash equilibrium, that is, we have a negative instance. Complexity. The maximal number of steps of this algorithm isK, which is exponential in the size of the game and linear in the bit-size of ε. At each step, by Lemma 11, the computation of the sets X k pvqtakes exponential time in the size ofG. Checking the stopping criterion amounts to checking, for each cubeC ĎX k pvq whether it intersects the polytope of vectors satisfying the stopping criterion: the can be done in a time polynomial in the size of the systems of inequalities representing those polytopes, i.e. in time polynomial in the instance size. Since the set X k may contain exponentially (in the size ofG) many cubes, checking the stopping criterion takes time exponential in the size ofGand polynomial in the size ofε. Overall, this algorithm shows the desired complexity.đ 3.7 The pure case We quickly turn our attention to a variant of Problem 2, the constrained existence problem of pure NEs, where the players are restricted to pure strategies. The algorithm described above can be adapted to that version. Léonard Brice, Thomas A. Henzinger, K. S. Thejaswini9 §Theorem 13. The approximate constrained existence problem of pure NEs in stopping games is decidable in time exponential in the game size, and polynomial in the bit-size of ε. Proof.The algorithm described above applies also to pure NEs. The only necessary modification is in the definition of the sets X k pvq, where the coefficientsα ia must all be equal to either 0 or 1. With that slight change, all proofs are analogous.đ 3.8 Hardness We close this subsection with a lower bound on the complexity of this problem. §Theorem 14 (App. A.4). The approximate constrained existence problem of NEs in stopping games isPSPACE-hard, even in turn-based stopping games. So is the approximated constrained existence problem of pure NEs. 4 An exact algorithm for XRSE 4.1 Definitions and problem We start this section by recalling the definition of extreme risk measures precisely, along with the definition of extreme risk-sensitive equilibria. We assume the player set Π is partitioned into two sets: P (pessimists) and O (optimists). Pessimistic Risk Measure (PM). Fori P P, playerimaximises the lowest payoff achieved with positive probability, i.e., the quantityPM i p ̄σq “ suptx P R | Ppμ i ě xq “1u.In stopping games, this is exactly mintμ i pπq | π is a play with P ̄σ pπq ą 0u. Optimistic Risk Measure (OM). Fori P O, playerimaximises the highest payoff achieved with positive probability: OM i p ̄σq “ inftx P R | Ppμ i ď xq “ 1u “ maxtμ i pπq | π is a play with P ̄σ pπq ą 0u. We group these under the notationX i p ̄σq, referring to PM wheni P Pand OM ifi P O. We also write Xp ̄σq “ pX i p ̄σq iPΠ . §Definition 15 (Extreme risk-sensitive equilibria (XRSE)). Given a concurrent gameGand a partitionpP,Oq, a strategy profile ̄σ is an extreme risk-sensitive equilibrium (XRSE) if for every player i P Π and every alternative strategy σ 1 i , we have X i p ̄σ ́i ,σ 1 i q ď X i p ̄σq. We focus on the following decision problem: §Problem 3 (Constrained existence problem of XRSEs). Given a gameG, a partitionpP,Oq of the set of players into pessimists and optimists, and two payoff profiles ̄x, ̄y P Q Π , does there exist an XRSE ̄σ in G satisfying x i ď X i p ̄σq ď y i for each player i? We show that in concurrent stopping games, the constrained existence problem of XRSEs is inNP. The proof goes by showing that if an XRSE exists, there also exist an equivalent XRSE, meaning that every player has the same extreme risk measure, that uses (polynomial) finite memory. Let us therefore define that notion. §Definition 16 (Memory structure and memory states). A memory structure for a gameGis a tuple M “ pM,m 0 ,α up , ̄σ choice q consisting of: 10Algorithms for Equilibria in Concurrent Stopping Games v ̋ 2 ̋ 2 : t J t K : ̋ 0 ̋ 0 v R v L t R : ̋ 1 ̋ 2 t L : ̋ 2 ̋ 1 ̋ H ̋ T , ̋ T ̋ H ̋ P ̋ ̊, ̋ ̊ ̋ P ̋ T ̋ T ̋ H ̋ H 1 2 1 2 1 2 1 2 (a) v anchor t ̋, ̋u t J v L v R t L t R v anchor ̋ v v R v L t R t L v anchor H anchor ̋ ̋ H ̋ T , ̋ T ̋ H ̋ T ̋ T ̋ H ̋ H 1 2 1 2 1 2 1 2 ̋ H ̋ T , ̋ T ̋ H ̋ H ̋ T , ̋ T ̋ H ̋ H ̋ H ̋ T ̋ T 1 2 1 2 1 2 1 2 ̋ T ̋ H (b) Figure 1 (a) The game of Example 17. (b). A representation of the strategy profile ̄σ, along with the memory states. Punishing plays are not depicted. a finite set M of memory states; an initial memory state m 0 P M; a memory update functionα up :M ˆ V ˆ Aˆ V Ñ Mupdates the memory state based on the edge that is taken—i.e., the source vertex, the action profile that is performed, and the new vertex reached; a tuple ̄σ choice “ pσ choice i q iPΠ of choice functionsσ choice i :M ˆ V Ñ DpA i qthat output, on each vertex and in each state, the action distribution that is prescribed to player i. Given a memory structureM, we extend the update function into a function ˆα up : Hist Ñ Mwhereˆα up pv 0 q “ m 0 andˆα up ph ̈ ̄a ̈vq “ α up p ˆα up phq, lastphq, ̄a,vq. Then, a memory structure defines a strategy profile ̄σ, withσ i :h ÞÑ σ choice i p ˆαphqqfor each playeri. Note the order: when an edge is taken, the memory is updated first, and then the choice function is applied, based on the new memory state. A strategy profile ̄σis finite-memory if it is defined by a memory structure. 4.2 An example The core of our proof is the sufficiency of polynomial finite-memory XRSEs; but the proof of that statement is significantly more involved than in the turn-based case. Let us first use an example to give intuition on how and when memory is needed. § Example 17. Consider the following game, with two pessimistic players2and ̋ , and six verticestv,v L ,v R ,t K ,t J ,t L ,t R u, where the terminal vertices aret K ,t J ,t L ,andt R , andvis the starting vertex. The actions available at the start vertex are:tH,T,Pu(heads, tails, and punish). The other verticesv L ,v R are such that each player has only one action, and therefore represented as stochastic vertices in Figure 1(a). In this game, is there an XRSE ̄σsuch thatX ̋ p ̄σq “ X ̋ p ̄σq “1? The answer is yes, and we describe one such XRSE below. The strategy profile. Since both players are pessimists, achievingX ̋ “ X ̋ “1 means that each player must be given a payoff of 1 with positive probability. When the play starts, both players choose randomly betweenHandT. If the vertexv L has been visited before in the history, then player ̋ already had a positive probability of getting payoff 1: then, player2always performsHand player ̋ randomises betweenHandT, so that player2 Léonard Brice, Thomas A. Henzinger, K. S. Thejaswini11 also gets payoff 1 with positive probability. If2deviates from this positional strategy, then actionPis played by player ̋ at any further visit ofv, to punish him. The players behave symmetrically when v is visited after v R has been seen, and when player ̋ deviates. Here, memory is used to remember who has already been given a payoff 1 with positive probability—and who still needs to be given such a payoff. In other words, which players are being anchored. We define the concept formally later; but we describe here the corresponding memory structure. The memory structure. The strategy profile described above is defined by a memory structure with six states:tanchor ̋, ̋ ,anchor ̋ ,anchor ̋ ,anchor H ,punish ̋ ,punish ̋ u. The choice functions at v are: in state anchor ̋, ̋ (initial): both players play H and T uniformly at random; in state anchor ̋ : player ̋ plays H; player2 plays H and T uniformly at random; in state anchor ̋ : player2 plays T; player ̋ plays H and T uniformly at random; in state anchor H : player ̋ plays H, player2 plays T (the game ends in t J ); in state punish i : the player other than i plays P; player i’s choice is arbitrary. The memory is updated as follows. From stateanchor ̋, ̋ , upon visiting the vertexv R , the memory moves toanchor ̋ , and upon visiting vertexv L toanchor ̋ . From stateanchor ̋ , uponpH,Hqv R vit moves toanchor H ; fromanchor ̋ , uponpT,Tqv L vit moves toanchor H . If some playeriplays an action outside the support prescribed by the current state, the memory moves to punish i and remains there. The plays compatible with ̄σreach exactly the terminalst J ,t R andt L , and nevert K ; hence X ̋ p ̄σq “ X ̋ p ̄σq “ 1. Those plays are described in Figure 1 (b). This strategy profile is an XRSE. Both players being pessimists, it suffices to show that whenever they deviate, they always get payoff 0 or 1 with positive probability; we argue for 2, the case of ̋ being symmetric. From the second visit to vertexv, if player2deviates, either the game has visited the vertexv R , and then he anyway gets risk measure 1; or it has visitedv L , and then he is prescribed to play deterministically—any deviation is detectable and he will be punished with positive probability, giving him a risk measure of 0. When the game starts, deviating would mean playingHorTpurely. Then, either he reachesv R first, and then receives risk measure 1 sincet R is reached with probability 12. Or, he reachesv L first, and then the memory switches toanchor ̋ , hence againt R is reached with positive probability. Either case, he has no incentive to deviate. About the necessity of randomisation and of memory. Critically, both randomisation and memory are required here. For randomisation: if either player, say2, was playingH(or T) deterministically from the beginning, then player ̋ would an incentive to purely playT so that the terminalt J is reached almost surely, giving her payoff 2. For memory: if some player, again, say2, was always randomising betweenHandTat every occurrence of the vertexv, then player ̋ would have a profitable deviation by playingT, to reacht J ort R , and get payoff 2. 4.3 Anchored players We now assume given an XRSE ̄σ. We aim to construct an equivalent finite-memory one. We denote the set of histories compatible with ̄σbyH, and the profileXp ̄σqby ̄z. Given a historyh P H, every historyh ̄av P His called a child ofh. Following from the intuition 12Algorithms for Equilibria in Concurrent Stopping Games from Example 17, we need to define formally the set of players that are anchored after each history. Let us first define anchorable players. § Definition 18 (Anchorable players). Leth P Hbe a history compatible with ̄σ, and letibe a player. We say that player i is anchorable at h if either: player i is an optimist and X i p ̄σ æh q “ z i ; or player i is a pessimist, and for every strategy σ 1 i , we have X i p ̄σ ́iæh ,σ 1 i q ď z i . However, the fact that some playeriis anchored at historyhdoes not say anything about how far we are from reaching the terminal where their risk measure is realised. This is why we define the notion of i-rank. § Definition 19 (i-rank). Letibe a player, and lethbe a history where playeriis anchorable. The historyhhasi-rank 0 if it ends in a terminal. Otherwise, itsi-rank is the smallest integer k such that: player i is an optimist, and there is a child h ̄av of h that has i-rank k ́ 1; or playeriis a pessimist, and for every actiona i P Supppσ i phqq, there is an action profile ̄a ́i P Suppp ̄σ ́i phqqand a vertexv P Suppp∆plastphq, ̄aqqsuch that the childh ̄avhas i-rank lesser than k. § Lemma 20. Every history where player i is anchorable has an i-rank. Proof.If playeriis an optimist, and gets risk measurez i in the strategy profile ̄σ æh , then there is an extensionπofhthat reaches a terminal where playerigets payoffz i , i.e., a history where playeriis anchorable and withi-rank 0. Then the historyhhasi-rank at most |π| ́|h|. Now, letibe a pessimist. Assume playeriis anchorable at some historyhthat has no i-rank. Then, there is an actiona i such that for every action profile ̄a ́i P Suppp ̄σ ́i phqq, and vertexv P Suppp∆plastphq, ̄aqq, the childh ̄avhas noi-rank. By iterating this reasoning from every such child, we can construct a strategy for playerithat guarantees that no history with ani-rank is ever constructed. Then, in particular, no history withi-rank 0 is generated, i.e., no terminal where playerigets payoffz i is ever reached. On the other hand, that strategy always performs actions in the support of the strategyσ i , hence it never reaches a terminal where playerigets less thanz i . Thus, since the game is stopping, it gives playeria risk measure that is strictly greater thanz i , contradicting the fact that playeriis anchorable at h.đ We now define a labelling Λ :H Ñ2 Π ; for every historyh, we will say that the players in the set Λphq are anchored at h. §Lemma 21 (App B.2). There exists a labelling Λ :H Ñ2 Π that has the following properties: 1. we have Λpv 0 q “ Π; 2. for every history h and child h ̄av of h, we have Λph ̄avq Ď Λphq; 3. for every history h, all players in Λphq are anchorable at h; 4.for every historyhand every optimisti PΛphq, there is exactly one childh ̄avofhsuch that i P Λph ̄avq, and h ̄av has i-rank smaller than h; 5.for every historyhand every pessimisti PΛphq, for every actiona i P Supppσ i phqq, there is exactly one action profile ̄a ́i and one vertexv P Supppδplastphq, ̄aqqsuch that i P Λph ̄avq, and h ̄av has i-rank smaller than h. Later on, we refer to these as Properties 1, 2, 3, 4, and 5. Léonard Brice, Thomas A. Henzinger, K. S. Thejaswini13 4.4 About the number of anchored sets We now show that the number of distinct sets that are anchored in the labelling Λ is polynomial in the size of the game. The reader may have noted that each pessimist that randomises after a historyhwhere they are anchored are are also anchored at|Supppσ i phqq| children ofh. Contrary to the turn-based case, that may cause an exponential blowup: the number of anchored sets may be exponential in the number of players. However, a main observation is that this is only possible if many players randomise simultaneously on some vertex; in which case, the space needed to represent the game is also exponential in the number of players that randomise. § Lemma 22. Letpbe the number of players inG. Then, the number of anchored sets is smaller than or equal to p 2 ` 1qG. Proof.Given two setsAandB, we say thatAandBare comparable if we have either A Ď BorB Ď A, and that they cross if they are not comparable but satisfyA X B ‰ H. For each vertexv, letC v be the core ofv, i.e., the set of pessimistsithat have at least two distinct actions available inv. We now define the game core as the set of subsets of Π that are included in some vertex core, i.e., the setC “ Ť vPV 2 C v . Our proof relies on the following argument: the size of the game core is bounded by the game size. § Proposition 23. We have |C| ď G. Proof.We have|C| ď ř v ˇ ˇ 2 C v ˇ ˇ “ ř v 2 |C v | .For eachv, there are at least 2 |C v | action profiles possible, hence the space required to represent the transition function is at least this sum.đ We now count separately the anchored sets in the game core, and those outside. In the game core. The number of setsA P Cthat are anchored is bounded by|C|. By Proposition 23, that quantity is smaller than or equal to the game size G. Outside of the game core. Let us first notice the following. § Proposition 24. Let A and B be two crossing anchored sets. Then, we have AX B P C. Proof. Leth A ,h B P Hbe two histories such that Λph A q “ Aand Λph B q “ B. None of those histories is a prefix of the other one: otherwise, by Property 2, we would have Λph A q ĎΛph B q or Λph B q Ď Λph A q, i.e. the sets A and B would be comparable, and thus would not cross. Let nowhbe the longest common prefix ofh A andh B : the historyhhas then two distinct childrenh ̄avandh ̄a 1 v 1 such thath ̄avis a prefix ofh A andh ̄a 1 v 1 is a prefix ofh B . By Property 2, we have A Ď Λph ̄avq and B Ď Λph ̄a 1 v 1 q, hence AX B Ď Λph ̄avqX Λph ̄a 1 v 1 q. Let theni P AXB. By Properties 4, playeriis necessarily a pessimist, and by Property 5 we necessarily havea i ‰ a 1 i . Thus, playeribelongs to the core of the vertexlastphq. Which proves the inclusion AX B Ď C lastphq .đ Let us now call critical set a setC ĎΠ such thatC R C, butCztiu P Cfor every player i.We then get the following result. § Proposition 25. LetAandBbe two anchored sets. If there is a critical setCwith C Ď AX B, then the sets A and B are comparable. Proof. Since we haveH P C, the setCis nonempty. The setsAandBare therefore either crossing or comparable. But if they were crossing, we would have AX B P C, and therefore C P C, which is false. Therefore, they are comparable.đ 14Algorithms for Equilibria in Concurrent Stopping Games Consequently, for every critical setC, there can be at mostpdistinct anchored sets containingC. On the other hand, there are at most|C|pcritical sets (to choose a critical set, one must choose a core setC 1 and then a playerisuch thatC 1 Y tiu R C). Consequently, there are at most |C|p 2 ď Gp 2 anchored sets outside the core. Conclusion. There are at most G`Gp 2 “ p 2 ` 1qG anchored sets, as desired.đ 4.5 A finite-memory strategy profile The labelling Λ provides us with the fundamental structure from which we can construct a finite-memory strategy profile. Tool box: memoryless strategies Before we proceed to the lemma, we recall one lemma from a recent work [7], that shows that if one player deviates in a way that can be observed by the other players, then the other players can form a team and punish the deviator using a memoryless randomised strategy. Earlier works [11,2] had considered concurrent games where players can form coalitions, but assumed that the players in a coalition are allowed to correlate their random choices, which makes it possible to reduce them to one meta-player; that is not the case in this setting. § Lemma 26 (App. B.1). For every playeriand vertexv, the value at vertexv, written val v p ̄σq “ inf ̄σ ́i sup σ i X i ` ̄σ ́i ,σ i ̆ , whereσ i and ̄σ ́i range over strategies from vertexv, is realised by a memoryless strategy profile. We also note a well-known result from the result from MDP literature that states that against a memoryless strategy profile, positional strategies are optimal. §Lemma 27 (Positional strategy for one player). Let ̄σ ́i be a memoryless strategy profile. Then, the supremum sup σ i X i p ̄σ ́i ,σ i q is realised by a positional strategy. The construction §Lemma 28 (App. B.3). There exists a finite-memory strategy profile ̄σ ‹ equivalent to ̄σ, with at most p`p 2 ` 1qG memory states. Proof sketch.We construct from ̄σand Λ a memory structure with the statespunish i , for each playeri, andanchor A , for each anchored setA. By Lemma 22, we have at most p`p 2 ` 1qG states. The initial state is anchor Π . Each memory state corresponds to a memoryless strategy until the memory is updated. In the statepunish i , all players follow the strategy profile ̄σ i , where, for each playeri, we let ̄σ i ́i be the memoryless punishing strategy from Lemma 26 and where σ i i is an arbitrary memoryless strategy. At memory stateanchor A , we define the choice function. For every historyh P H, we define its absolute rankRphqas the maximumi-rank ofh, foriranging over Λphq, with the conventionRphq “0 when Λphq “ H. For memory stateanchor A and vertexvwe pick a historyh v A P Hwith last vertexv, of minimal absolute rank. At stateanchor A , fromveach player i outputs the distribution σ i ph v A q. Finally, let us define the update function. From the statepunish i , the memory always remains in the statepunish i . From the stateanchor A , when seeing an edgepv, ̄a,wq, if there is a playerisuch thata i R Supppσ i ph v A q, then the memory switches topunish i . Otherwise, it switches to anchor Λph v A ̄awq . Léonard Brice, Thomas A. Henzinger, K. S. Thejaswini15 We show in the appendix that this strategy profile is an XRSE and is equivalent to ̄σ.đ 4.6 Conclusion § Theorem 29. The constrained existence problem for XRSE in a concurrent stopping game is NP-complete. Proof.Hardness is already known [8]. As for easiness, by Lemma 28, we know that there exists an XRSE satisfying the specified constraints if and only if there is a finite-memory one, using at mostp`p 2 `1qGmemory states. Such a strategy profile ̄σ ‹ can be guessed in polynomial time: what remains to be proven is that we can check in polynomial time that the generated risk measures satisfy the constraints, and that it is an XRSE. The strategy profile ̄σ ‹ induces a Markov chain. The profile ̄z “ Xp ̄σqcan be computed by computing the set of terminals that are reached with positive probability, by standard reachability algorithms. Then, for each playeri, the strategy profile ̄σ ‹ ́i induces an MDP. Deciding whether playerihas a profitable deviation in ̄σ ‹ amounts to deciding whether they can ensure reaching the setT ‹ “ t P T | μ i ptq ą z i uwith positive probability (if playeriis an optimist) or almost surely (if playeriis a pessimist). Both questions can be answered with standard polynomial-time algorithms [4, Section 10.6.1].đ 5 Discussion We have seen two different routes to circumvent the undecidability of the constrained existence of Nash equilibria in concurrent stopping games [25]. The first keeps the solution concept fixed and relaxes exactness: our algorithm decides the approximate problem in time exponential in the game and polynomial in the bit-size ofε, with no restrictions on the memory of the players, and is accompanied by aPSPACElower bound already in turn-based games. The second keeps exactness and changes the players’ risk attitude, replacing expected payoff by an extreme measure; for this notion the constrained existence problem remainsNP-complete, even under concurrency. In both cases, a first limitation is that our algorithms are valid only in stopping games. The approximate algorithm, in particular, relies heavily on that hypothesis, and decidability of the approximate problem in general concurrent games remains open. A second limitation is the complexity gap the we leave for that approximate problem, which is now known to be PSPACE-hard and in the classEXPTIME: a polynomial-space algorithm, if it exists, would have to resort to completely different techniques. Finally, we believe that a central question for future works is the exploration of equilibrium notions for which the constrained existence problem is decidable, with no restrictions on the strategies. So far, XRSEs are the only such notion, but constitute a strong idealisation of the players’ preferences, as they do not consider the probability distribution of payoffs at all—only its support. Variants of XRSEs could be considered: for example, their subgame-perfect version, where players maximise their risk measure after every possible history and not only in the whole game. But the literature also suggests less extreme risk measures, such as the value at risk (VaR), which can be seen as a generalisation of the pessimistic risk measure, where the players have some tolerance parameterpand can ignore bad payoffs occurring with probability lesser thanp. Decidability of the constrained existence problem of equilibria defined from that notion would then open new possibilities for the algorithmic study of equilibria in stochastic games. 16Algorithms for Equilibria in Concurrent Stopping Games References 1 Agarwal Alekh, Nan Jiang, Sham M. Kakade, and Sun Wen. Reinforcement Learning: Theory and Algorithms. https://rltheorybook.github.io/, 2021. 2Rajeev Alur, Thomas A. Henzinger, and Orna Kupferman. Alternating-time temporal logic. J. ACM, 49(5):672–713, September 2002. doi:10.1145/585265.585270. 3Ali Asadi, Léonard Brice, Krishnendu Chatterjee, and K. S. Thejaswini.ε-stationary nash equilibria in multi-player stochastic graph games. In 45th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2025, BITS Pilani, K K Birla Goa Campus, India, December 17-19, 2025, volume 360 of LIPIcs, pages 9:1–9:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2025. URL:https://doi.org/ 10.4230/LIPIcs.FSTTCS.2025.9, doi:10.4230/LIPICS.FSTTCS.2025.9. 4 Christel Baier and Joost-Pieter Katoen. Principles of Model Checking. The MIT Press, 2008. 5Calin Belta, Antonio Bicchi, Magnus Egerstedt, Emilio Frazzoli, Eric Klavins, and George J. Pappas. Symbolic planning and control of robot motion [grand challenges of robotics]. IEEE Robotics & Automation Magazine, 14(1):61–70, 2007. doi:10.1109/MRA.2007.339624. 6Patricia Bouyer, Romain Brenguier, Nicolas Markey, and Michael Ummels. Pure nash equilibria in concurrent deterministic games. Log. Methods Comput. Sci., 11(2), 2015.doi: 10.2168/LMCS-11(2:9)2015. 7Léonard Brice, Thomas A. Henzinger, Alipasha Montaseri, Ali Shafiee, and K. S. Thejaswini. Randomise alone, reach as a team. In Proceedings of the 38th International Conference on Computer Aided Verification (CAV 2026), Lecture Notes in Computer Science, Portugal, 2026. Springer. To appear, extended version available at https://doi.org/10.48550/arXiv.2603.07094. 8Léonard Brice, Thomas A. Henzinger, and K. S. Thejaswini. Finding Equilibria: Simpler for Pessimists, Simplest for Optimists. In 50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025), volume 345, pages 30:1–30:18, 2025.doi: 10.4230/LIPIcs.MFCS.2025.30. 9John F. Canny. Some algebraic and geometric computations in PSPACE. In Janos Simon, editor, Proceedings of the 20th Annual ACM Symposium on Theory of Computing, May 2-4, 1988, Chicago, Illinois, USA, pages 460–467. ACM, 1988. doi:10.1145/62212.62257. 10Krishnendu Chatterjee, Rupak Majumdar, and Marcin Jurdzinski. On Nash equilibria in stochastic games. In Computer Science Logic, 18th International Workshop, CSL 2004, volume 3210 of Lecture Notes in Computer Science, pages 26–40. Springer, 2004.doi: 10.1007/978-3-540-30124-0\_6. 11 Luca de Alfaro and Thomas A. Henzinger. Concurrent omega-regular games. In Proceedings of the 15th Annual IEEE Symposium on Logic in Computer Science, LICS ’00, page 141, USA, 2000. IEEE Computer Society. 12Luca de Alfaro, Thomas A. Henzinger, and Ranjit Jhala. Compositional methods for probabilistic systems. In CONCUR 2001 — Concurrency Theory, pages 351–365, Berlin, Heidelberg, 2001. Springer Berlin Heidelberg. 13Luca de Alfaro, Thomas A. Henzinger, and Orna Kupferman. Concurrent reachability games. Theoretical Computer Science, 386(3):188–217, 2007. Expressiveness in Concurrency. doi:10.1016/j.tcs.2007.07.008. 14 Kousha Etessami, Marta Kwiatkowska, Moshe Vardi, and Mihalis Yannakakis. Multi-objective model checking of markov decision processes. Logical Methods in Computer Science, Volume 4, Issue 4, 11 2008. doi:10.2168/LMCS-4(4:8)2008. 15Vojtěch Forejt, Marta Kwiatkowska, Gethin Norman, and David Parker. Automated Verification Techniques for Probabilistic Systems, pages 53–113. Springer Berlin Heidelberg, Berlin, Heidelberg, 2011. doi:10.1007/978-3-642-21455-4_3. 16Julian Gutierrez, Muhammad Najib, Giuseppe Perelli, and Michael J. Wooldridge. Automated temporal equilibrium analysis: Verification and synthesis of multi-player games. Artif. Intell., 287:103353, 2020. URL:https://doi.org/10.1016/j.artint.2020.103353,doi:10.1016/J. ARTINT.2020.103353. Léonard Brice, Thomas A. Henzinger, K. S. Thejaswini17 17Kristoffer Arnsfelt Hansen and Steffan Christ Sølvsten.DR-completeness of stationary nash equilibria in perfect information stochastic games. In 45th International Symposium on Mathematical Foundations of Computer Science, MFCS 2020, volume 170 of LIPIcs, pages 45:1–45:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL:https://doi.org/ 10.4230/LIPIcs.MFCS.2020.45. 18 Marius Kloetzer and Calin Belta. A fully automated framework for control of linear systems from temporal logic specifications. IEEE Trans. Autom. Control., 53(1):287–297, 2008.doi: 10.1109/TAC.2007.914952. 19 Claude Lefèvre. Optimal control of a birth and death epidemic process. Operations Research, 29(5):971–982, 1981. URL: http://w.jstor.org/stable/170234. 20Martin L. Puterman. Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley Series in Probability and Statistics. Wiley, 1994. doi:10.1002/9780470316887. 21Dawei Shi, Robert J Elliott, and Tongwen Chen. On finite-state stochastic modeling and secure estimation of cyber-physical systems. IEEE Transactions on Automatic Control, 62(1):65–80, 2016. 22Florent Teichteil-Königsbuch, Ugur Kuter, and Guillaume Infantes. Incremental plan aggregation for generating policies in MDPs. In Proceedings of the 9th International Conference on Autonomous Agents and Multiagent Systems: Volume 1 - Volume 1, AAMAS ’10, page 1231–1238. International Foundation for Autonomous Agents and Multiagent Systems, 2010. 23Michael Ummels. Stochastic multiplayer games: theory and algorithms. PhD thesis, RWTH Aachen, Germany, January 2010. 24Michael Ummels and Dominik Wojtczak. The complexity of nash equilibria in limit-average games. In Joost-Pieter Katoen and Barbara König, editors, CONCUR 2011 - Concurrency Theory - 22nd International Conference, CONCUR 2011, Aachen, Germany, September 6-9, 2011. Proceedings, volume 6901 of Lecture Notes in Computer Science, pages 482–496. Springer, 2011. doi:10.1007/978-3-642-23217-6\_32. 25Michael Ummels and Dominik Wojtczak. The Complexity of Nash Equilibria in Stochastic Multiplayer Games. Logical Methods in Computer Science, Volume 7, Issue 3, September 2011. URL: https://lmcs.episciences.org/1209, doi:10.2168/LMCS-7(3:20)2011. A Appendix for Section 3 A.1 Proof of Lemma 6 §Lemma 6 (App. A.1). Let ̄σbe a Nash equilibrium in the gameG. Letδ ą0, and letk such thatλ k ď δ 4R . Then, there exists aδ-Nash equilibrium with memory horizonkNwhere each player has an expected payoff that is at most different by δ2. Proof. Let us build the strategy profile ̄σ 1 as follows. On every history h of length at most kN , we define ̄σ 1 phq “ ̄σphq. Let nowhbe a history of lengthkN. For every historyh 1 of which the history h is a prefix, we define ̄σ 1 ph 1 q arbitrarily. We know that there exists a memoryless strategy profile ̄τ h such that for every terminal vertext, we haveP lastphq ̄τ p3tq “ P ̄σ p3t | hq [14, Theorem 3.2]. But obtaining such exact strategies might not possible without correlated strategies. By construction, the strategy profile ̄σ 1 has memory horizonkN, and each playerihas the same expected payoff as in ̄σ. Let us prove that ̄σ 1 is a δ-NE. Let i be a player and let σ 2 i be a strategy for player i. We want: E i p ̄σ 1 ́i ,σ 2 i q ď E i p ̄σ 1 q` δ. Let us decompose: E i p ̄σ 1 ́i ,σ 2 i q “ P ̄σ 1 ́i ,σ 2 i pV ďkN TqE i p ̄σ 1 ́i ,σ 2 i | V ďkN Tq` P ̄σ 1 ́i ,σ 2 i pV kN`1 qE i p ̄σ 1 ́i ,σ 2 i | V kN`1 q. 18Algorithms for Equilibria in Concurrent Stopping Games Note that on every history of length at mostkN, the strategy profile ̄σ 1 behaves exactly as ̄σ. Therefore, the probabilities of reaching or avoiding terminal vertices within the first kN `1 steps are the same in the two strategy profiles. Similarly, assuming a terminal vertex is reached withinkN `1 steps, the expected payoff for playeriis the same. On the other hand, every expected payoff in the game G is smaller than or equal to R. Hence: E i p ̄σ 1 ́i ,σ 2 i q ď P ̄σ ́i ,σ 2 i pV ďkN TqE i p ̄σ ́i ,σ 2 i | V ďkN Tq` δ 2R R.(1) Let us now apply the same decomposition when following the strategy profile p ̄σ ́i ,σ 2 i q: E i p ̄σ ́i ,σ 2 i q “ P ̄σ ́i ,σ 2 i pV ďkN TqE i p ̄σ ́i ,σ 2 i | V ďkN Tq` P ̄σ 1 ́i ,σ 2 i pV kN`1 qE i p ̄σ ́i ,σ 2 i | V kN`1 q. And since every expected payoff is greater than or equal to ́R: E i p ̄σ ́i ,σ 2 i q ě P ̄σ ́i ,σ 2 i pV ďkN TqE i p ̄σ ́i ,σ 2 i | V ďkN Tq ́ δ 2R R. By injecting this in Equation (1), we obtain: E i p ̄σ 1 ́i ,σ 2 i q ď E i p ̄σ ́i ,σ 2 i q` δ 2 ` δ 2 “ E i p ̄σ ́i ,σ 2 i q` δ. Finally, since the strategy profile ̄σ is an NE, we obtain: E i p ̄σ 1 ́i ,σ 2 i q ď E i p ̄σq` δ “ E i p ̄σ 1 q` δ. The strategy profile ̄σ 1 is an δ-NE.đ A.2 Proof of Lemma 10 § Lemma 10 (App. A.2). For everykand eachv, the set X k pvqcontains all vectors of the form ̄χ ̄σ , where ̄σis a strategy profile fromvwith memory horizonk. Conversely, for every vector ̄χ PX k pvq, there exists a strategy profile ̄σfromvwith memory horizonksatisfying ̄χ ́ ̄χ ̄σ ď pk ` 1q R D . Proof. We proceed by induction on k. The casek “0. Consider first the casek “0: strategy profiles with memory horizon 0 are exactly the memoryless strategy profiles, hence if ̄σis a memoryless strategy profile from v, the cubeC P Ccontaining the vector ̄χ ̄σ is included in the set X 0 pvq. Conversely, every vector ̄χ PX 0 pvqis contained in a cubeC P Cthat also contains a characteristic vector ̄χ ̄σ where ̄σis a memoryless strategy profile: then, we have ̄χ ́ ̄χ ̄σ ď R D . Let us now prove that the statement holds for k ą 0. Fork ą0, the set X k pvqcontains the characteristic vectors. Let ̄σbe a strategy profile fromv, with memory horizonk. For every action profile ̄aavailable fromv, and for every w P V, the strategy profile ̄τ ̄aw :pw, ̄a 1 ,v 1 ..., ̄a k ,v k q ÞÑ ̄σpv, ̄a,w,...,v k qhas memory horizonk ́1, and by induction hypothesis we haveχ ̄aw “ χ ̄τ ̄aw P X k ́1 pwq. Then, for every i, we have: χ ̄σ ireg “ E i p ̄σq “ ÿ ̄aPAvpvq ÿ wPV ̃ ź jPΠ α aj ̧ ∆pv, ̄aqpwqE i p ̄τ ̄aw q, whereα aj “ σ j pvqpa j q. An analogous equality holds forχ ̄σ idev , hence the cube containing the vector ̄χ ̄σ is contained in the set X k pvq, and therefore we have χ ̄σ P X k pvq. Léonard Brice, Thomas A. Henzinger, K. S. Thejaswini19 Fork ą0, every vector in X k pvqis close to some characteristic vector. Conversely, let ̄χ PX k pvq, and letC P Cbe the cube containing ̄χ. Then, the cubeCalso contains a vector ̄χ 1 for which vectors ̄χ ̄aw and coefficientsα ia satisfying the equalities in Definition 9. By induction hypothesis, for each pairp ̄a,wq, there is a strategy profile ̄τ ̄aw with memory horizon k ́ 1 satisfying: › › › ̄χ ̄aw ́ ̄χ ̄τ ̄aw › › › ď k R D . Consider then the strategy profile ̄σ, defined byσ i paq “ α ia for each playeriand each action a, and that follows the strategy profile ̄σ ̄aw after having performed the action profile ̄a and seen the vertexw. That strategy profile has memory horizonk. Moreover, for everyi, we have: ˇ ˇ χ 1 ireg ́ χ ̄σ ireg ˇ ˇ “ ˇ ˇ ˇ ˇ ˇ ˇ ÿ ̄aPAvpvq ÿ wPV ∆pv, ̄aqpwq ̃ ź j α ja j ̧ ́ χ ̄aw ireg ́ χ ̄τ ̄aw ireg ̄ ˇ ˇ ˇ ˇ ˇ ˇ ď ÿ ̄aPAvpvq ÿ wPV ∆pv, ̄aqpwq ̃ ź j α ja j ̧ ˇ ˇ ˇ χ ̄aw ireg ́ χ ̄τ ̄aw ireg ˇ ˇ ˇ ď ÿ ̄aPAvpvq ÿ wPV ∆pv, ̄aqpwq ̃ ź j α ja j ̧ k R D “ k R D . Analogously, we get|χ 1 idev ́ χ ̄σ idev | ď k R D , and therefore ̄χ 1 ́ ̄χ ̄σ ď k R D . Finally, using the triangular inequality, we have: › › ̄χ ́ ̄χ ̄σ › › ď › › ̄χ ́ ̄χ 1 › › ` › › ̄χ 1 ́ ̄χ ̄σ › › ď R D ` k R D “ pk ` 1q R D , as desired.đ A.3 Proof of Lemma 11 § Lemma 11 (App. A.3). Given the gameG, a vertexvand a numberk, the set X k pvqcan be computed in exponential time. Proof.Each set X ℓ pvqis a union of cubes inC, and can therefore be described by the list of those cubes, which takes spaceOpD 2|Π| q, which grows exponentially with the instance size (note thatDis already exponential in the instance size—but that does not affect the result). Assuming X ℓ ́1 is known, computing the set X ℓ pvqcan be done by iterating all cubesC P C and all cubesC ̄aw PX ℓ ́1 pwqfor each pairp ̄a,wq, and then by checking whether there exist vectors ̄χ P Cand ̄χ ̄aw P C ̄aw satisfying the following sentence, written in the existential theory of the reals: ̈ ̋ ÿ aPAv i pvq α ia “ 1 ̨ ‚ ľ iPΠ ̈ ̋ χ ireg “ ÿ ̄aPAvpvq ÿ wPV ∆pv, ̄aqpwq ̃ ź j α ja j ̧ χ ̄aw ireg ̨ ‚ ľ iPΠ ľ a i PAv i pvq ̈ ̋ χ idev ě ÿ ̄a ́i PAv ́i pvq ÿ wPV ∆pv, ̄aqpwq ̃ ź j‰i α ja j ̧ χ ̄aw idev ̨ ‚ 20Algorithms for Equilibria in Concurrent Stopping Games x 1 ? x 1 ␣x 1 x 2 ? x 2 ␣x 2 . . . x n ␣x n φ . . . C 1 . . . t L : ̄ L 0 t K : E 0 t K : E 0 0.5 0.5 1 m Figure 2 A reduction from QBF ľ iPΠ ł a i PAv i pvq ̈ ̋ χ idev “ ÿ ̄a ́i PAv ́i pvq ÿ wPV ∆pv, ̄aqpwq ̃ ź j‰i α ja j ̧ χ ̄aw idev ̨ ‚ . This sentence has polynomial size (let us remember that each setAv i pvqis explicitly described in the instance, even though it may be exponential in the number of players), and the cubesCandC ̄aw are also described by a polynomial number of inequations. Since the existential theory of the reals is decidable inPSPACE[9], only polynomial space, and therefore exponential time, is needed to decide the existence of such a solution. The set X ℓ pvq can therefore be constructed from X ℓ ́1 in exponential time. By iterating that algorithm from ℓ “ 1 to ℓ “ k, we obtain an exponential-time algorithm computing the set X k pvq.đ A.4 Proof of Theorem 14 § Theorem 14 (App. A.4). The approximate constrained existence problem of NEs in stopping games isPSPACE-hard, even in turn-based stopping games. So is the approximated constrained existence problem of pure NEs. Proof.We proceed by reduction from thePSPACE-complete QSAT. Let us assume a formula φ “ Dx 1 @x 2 ...Dx n ́1 @x n Ź m i“1 C i , where each clauseC i is a conjunction of three literals over the variablesx 1 ,...,x n . We construct a gameGand an error termεsuch that if the formulaφis true, then there is a (pure) NE where the player Eve has expected payoff at least 1, and that if the formulaφis false, then there is noε-NE where Eve has expected payoff at least 1 ́ ε. The construction The construction is depicted by Figure 2. The gameGhas 2n`1 players, calledx 1 ,␣x 1 , . . . , x n ,␣x n , and Eve, denotedE. Intuitively, Eve tries to build a valuation satisfying all clauses; later on, for each clause, she is asked to select a literal that is satisfied by the generated valuation. Each literal player, on the other hand, will have a profitable deviation if and only if Eve wrongly claims that its negation is satisfied. On Figure 2, all omitted rewards are 1, and the terminal vertext K has been depicted twice for clarity. Round vertices are controlled Léonard Brice, Thomas A. Henzinger, K. S. Thejaswini21 by Eve, square vertices by literal players, and black vertices are stochastic: each player has only one action available. For each variablex k , we define three vertices denoted byx k ?,x k , and␣x k . If the variable x k is quantified existentially, then the vertexx k ? is controlled by Eve, and she chooses deterministically to move the game tox k or to␣x k . If it is quantified universally, then the vertex x k ? is stochastic: the game goes to x k or to ␣x k with probability 1 2 each. Each literal vertexL P tx k ,␣x k uis controlled by the playerL. There, that player can either go to the vertex t K , or (if k ă n) to the vertex x k`1 , or (if k “ n) to the vertex φ. The vertexφis stochastic: from there, the game goes with uniform probability distribution to the verticesC 1 ,...,C m . Each vertexC i is controlled by Eve, and from the vertexC i , Eve can reach the terminal vertices t L for all literals L of C i . In the terminal vertext K , every player gets payoff 1, except Eve, who gets payoff 0. In the terminal vertext L , every player gets payoff 1, except player ̄ L(the negation ofL), who gets payoff 0. The initial vertex is x 1 ?. We define ε “ 1 3ˆ2 n m`1 . If the formulaφis true, then there is a (pure) NE where Eve gets expected payoff 1. Let us assume that the formulaφis true: then, there exist mappingsf k :t0,1u k ́1 Ñ t0,1u, for each oddk, such that for every valuationνof the variablesx 2 ,x 3 ,...,x n , the valuation ν 1 that extendsνwithν 1 px k q “ f k px 1 ,...,x k ́1 qfor each evenksatisfies the conjunction Ź i C i . Let ̄σbe the strategy profile where the literal players never go to the vertext K , and where Eve plays according to the mappingsf k , i.e., after the historyhx k ?, goes deterministically to the vertexx k iff k pb 1 ,...,b k ́1 q “1 and to␣x k otherwise, whereb j “1 if the history hvisits the vertexx j and 0 otherwise. Then, when reaching a vertexC i after a historyh, that history defines a valuation of all variables, and by definition of the mappingsf k , that valuation satisfiesC i : Eve goes then deterministically to a terminal vertext L such that the literal L is satisfied. In this strategy profile, Eve has expected payoff 1, sine the vertext K is never reached. Therefore, she has no profitable deviation. As for every literal playerL, every play compatible with ̄σthat doe snot give playerLthe payoff 1, i.e. that reaches the terminal vertext ̄ L , defines a valuation that satisfies the literal ̄ L . Therefore, the vertexLis not visited, and player L has no profitable deviation. That strategy profile is a pure NE. If the formula φ is false, then there is no ε-NE where Eve gets expected payoff at least 1 ́ ε. Let ̄σbe a strategy profile where Eve gets expected payoff at least 1 ́ ε, and let us prove that it is not an ε-NE. In this strategy profile, the probability of reaching t K is less than ε. Let us define the mappingsf k :t0,1u k ́1 Ñ t0,1u, for each oddk, byf k pb 1 ,...,b k ́1 q “1 if and only if after the history that visits exactly the vertices x j such that b j “ 1, Eve goes to the vertexx k with probability at least 1 2 . Since the formulaφis false, there is at least one valuationνsuch that the corresponding valuationν 1 does not satisfy the conjunction Ź i C i , i.e., does not satisfy one specific clauseC i . Lethbe the history corresponding to that valuation, and that ends in the clause vertexC i : under the strategy profile ̄σ, that history is followed with probability at least p1 ́εq n 2 n m . Then, lett L be a terminal vertex that is reached with probability at least 1 3 . Along that play, player ̄ Lgets payoff 0. Since the valuationν does not satisfy the clauseC i , it does not satisfy the literalL, which means that the vertex ̄ Lhas been visited along the historyh. Then, by going to the vertext K , player ̄ Lhas a 22Algorithms for Equilibria in Concurrent Stopping Games deviation that is profitable by at least: p1 ́ εq n 3ˆ 2 n m ď 1 ́ ε 3ˆ 2 n m “ 1 ́ 1 3ˆ2 n m`1 3ˆ 2 n m “ 1 3ˆ 2 n m` 1 “ ε. Therefore, the strategy profile ̄σ is not an ε-NE.đ B Appendix for Section 4 B.1 Proof of Lemma 26 § Lemma 26 (App. B.1). For every playeriand vertexv, the value at vertexv, written val v p ̄σq “ inf ̄σ ́i sup σ i X i ` ̄σ ́i ,σ i ̆ , whereσ i and ̄σ ́i range over strategies from vertexv, is realised by a memoryless strategy profile. Proof. Let: z “ inf ̄σ ́i from v sup σ i X i ` ̄σ ́i ,σ i ̆ The infimum is realised, since extreme risk measure range over a finite set of values. Therefore, there exists a strategy ̄σ ́i such that for every strategyσ i , we haveX i p ̄σ ́i ,σ i q ď z. If playeriis an optimist, and since the game is stopping, this means that the coalition Πztiu has a strategy profile that guarantees almost-sure reachability of the settt P T:μ i ptq ď zu (where all players randomise independently). Then, by [7, Theorem 5], there exists a memoryless strategy profile with that property. Similarly, if playeriis a pessimist, the coalition Πztiuhas a strategy profile that guarantees that the settt P T:μ i ptq ď zuis reached with positive probability. Then, by [7, Theorem 1], there exists a memoryless strategy profile with that property.đ B.2 Proof of Lemma 21 § Lemma 21 (App B.2). There exists a labelling Λ :H Ñ2 Π that has the following properties: 1. we have Λpv 0 q “ Π; 2. for every history h and child h ̄av of h, we have Λph ̄avq Ď Λphq; 3. for every history h, all players in Λphq are anchorable at h; 4.for every historyhand every optimisti PΛphq, there is exactly one childh ̄avofhsuch that i P Λph ̄avq, and h ̄av has i-rank smaller than h; 5.for every historyhand every pessimisti PΛphq, for every actiona i P Supppσ i phqq, there is exactly one action profile ̄a ́i and one vertexv P Supppδplastphq, ̄aqqsuch that i P Λph ̄avq, and h ̄av has i-rank smaller than h. Proof.We construct the labelling Λ from the strategy ̄σ, and prove by an induction on the length of the histories that this function satisfies the properties required. Base case. Consider the historyv 0 . We define Λpv 0 q “Π. This trivially satisfies Property 1. For Property 3, observe that the definition of anchorability ensures that optimists get their optimistic expectationz i , while for pessimists, it requires that they have no profitable deviation. Therefore Property 3 follows since ̄σis an XRSE. We show that the labelling satisfies the rest of the properties in the next step of the proof. Léonard Brice, Thomas A. Henzinger, K. S. Thejaswini23 Induction step: Λphqis defined for a historyhSuppose the labelling Λ has been defined until a historyh, then we define it for all childrenh ̄aw. Since Λphqis defined until historyh and satisfies Properties 1-5, we know that all players in Λphqare anchorable. Since player i PΛphqis anchorable, we know from Lemma 20 that the historyhhas ani-rank. Recall that by the definition ofi-rank, if playeriis an optimist, there is a child that hasi-rank that isk ́1 and if playeriis a pessimist, for every actiona i P Supppσ i phqq, there is an action profile ̄a ́i P Suppp ̄σ ́i phqqand a vertexv P Suppp∆plastphq, ̄aqqsuch thath ̄avhasi-rank less than k. We first start by declaring Λph ̄awq “ Hfor each ̄aandw, and add a player to each extension one after another for each player as below. The playeriis an optimist. We then know from Lemma 20 there is a child that has i-rank that is k ́ 1. We pick such an extension and add player i to Λph ̄awq. The playeriis a pessimist. For every actiona i P Supppσ i phqq, there is an action profile ̄a ́i P Suppp ̄σ ́i phqqand a vertexv P Suppp∆plastphq, ̄aqqsuch thath ̄avhasi-rank less than k. We add player i to the set Λph ̄awq for exactly one extension h ̄av for each action a i . We now show that this label Λ satisfies the Properties 2-5. 2. From construction we already know that Property 2 is satisfied. 3.We prove Property 3 by first showing that everyi PΛph ̄awqis anchorable. Anyi PΛph ̄awq was added because the historyhhad a finitei-rank, and therefore by definition ofi-rank, it is anchorable. 4. Property 4 follows from construction of how optimists were added to Λph ̄awq. 5.Similarly, Property 5 follows from construction of how pessimists were added to Λph ̄awq. đ B.3 Proof of Lemma 28 § Lemma 28 (App. B.3). There exists a finite-memory strategy profile ̄σ ‹ equivalent to ̄σ, with at most p`p 2 ` 1qG memory states. Proof. We first define the strategy profile, then prove it is equivalent to ̄σ, and finally that it is an XRSE. Construction of the strategy profile ̄σ ‹ We construct from ̄σ and Λ a memory structure with the following states: for each player i, the state punish i ; for each anchored set A, the state anchor A . The initial state is anchor Π . By Lemma 22, we have at most p`p 2 ` 1qG states. Let us now define the choice functions. For each playeri, let ̄σ i ́i be the memoryless punishing strategy from Lemma 26. Letσ i i be an arbitrary memoryless strategy. In the state punish i , all players follow the strategy profile ̄σ i . For every history h P H, we define its absolute rank as Rphq “ max jPΛphq j-rank of history h, with the conventionRphq “0 when Λphq “ H. By Property 3, every playerj PΛphqis anchorable ath, and therefore has a finitej-rank by Lemma 20; henceRphq P N. For every anchored setAand every vertexvsuch that the setH A,v “ th P H |Λphq “ A and lastphq “ vu is nonempty, we fix a representativeh v A P arg min hPH A,v Rphq,which 24Algorithms for Equilibria in Concurrent Stopping Games exists sinceNis well-ordered, and we write ΦpA,vq “ Rph v A q. Representatives are needed only for the pairspA,vqthat are reachable under the update function defined below; the claim in the proof of Proposition 35 shows thatH A,v ‰ Hholds for all such pairs. On the remaining pairs, the choice functions are defined arbitrarily. Then we define the choice function foranchor A : when seeing a vertexv, each playerioutputs the distributionσ i ph v A q. Finally, let us define the update function. From the statepunish i , the memory always remains in the statepunish i . From the stateanchor A , when seeing an edgepv, ̄a,wq, if there is a playerjsuch thata j R Supppσ j ph v A q, then the memory switches topunish j . Otherwise, it switches to anchor Λph v A ̄awq . The strategy profile ̄σ ‹ is equivalent to ̄σ § Proposition 30. We have X i p ̄σ ‹ q “ z i . Let us recall that we had ̄z “ Xp ̄σq. Let i be a player, and let us prove that Xp ̄σ ‹ q “ z i . Whenever the strategy profile is in a memory stateanchor A withi P Aand see the vertex v, the players play the distribution ̄σph v A q. In a play where there is no deviation, the punish state is not entered. By construction, all terminals that are reachable are reached also by the original strategy ̄σ. For an optimisti, this implies thatX i p ̄σ ‹ q ď z i and for pessimists X i p ̄σq ě z i . The other direction of the proof is structured around these claims. Ź Claim 31 (Rank reduces). Leth P H, leth ̄awbe a child ofh, and letj PΛph ̄awq. Then j-rankph ̄awq ă j-rankphq. Proof.By Property 2, we havej PΛphq. Ifjis an optimist, then by Property 4 the history h ̄awis the unique child ofhwhose label containsj, and that child hasj-rank smaller than h. Ifjis a pessimist, thena j P Supppσ j phqq, and by Property 5, applied to the actiona j , the historyh ̄awis the unique child ofhwithjth actiona j whose label containsj; that child has j-rank smaller than h.Ÿ ŹClaim 32 (Payoffs at anchored terminals). Letc P Hbe a history ending in a terminal vertex t, and let i P Λpcq. Then μ i ptq “ z i . Proof. This claim follows from the definition of anchored sets and ranks.Ÿ In both cases of optimists and pessimists, we show that there is a positive probability of obtainingz i . Letibe a player. We construct, step by step, a play prefix compatible with ̄σ ‹ and of positive probability, visiting pairspA t ,v t qwithi P A t andH A t ,v t ‰ H, where the memory state at vertexv t isanchor A t . We initialise withpA 0 ,v 0 q “ pΠ,v 0 q, which satisfies those conditions by Property 1. (Assume v 0 R T.) Assume the pairpA t ,v t qhas been constructed withv t R T, and writeh t “ h v t A t . Ifi is an optimist, letc t “ h t ̄awbe the unique child ofh t whose label containsi, given by Property 4. Ifiis a pessimist, pick an actiona i P Supppσ i ph t q, and letc t “ h t ̄awbe the unique child ofh t withith actiona i whose label containsi, given by Property 5. In both cases, ̄a P Suppp ̄σph t q, which is exactly the support prescribed by ̄σ ‹ in the memory state anchor A t atv t , andw P Suppp∆pv t , ̄aqq: the edgepv t , ̄a,wqis taken with positive probability, no player leaves the prescribed support, and the memory is updated toanchor Λpc t q , with i P Λpc t q. The play stops att P T. The prefix built so far, a finite concatenation of positive- probability transitions, has positive probability, and by Claim 32 forc t , playerireceives the Léonard Brice, Thomas A. Henzinger, K. S. Thejaswini25 payoffz i . Otherwise, we setpA t`1 ,v t`1 q “ pΛpc t q,wq: the historyc t witnessesH A t`1 ,v t`1 ‰ H, and by minimality of the representativeh t`1 and Claim 31, we haveRph t`1 q ď Rpc t q ă Rph t q. The sequencepRph t q t is a strictly decreasing sequence of natural numbers: the construction therefore stops, after at mostRph 0 qsteps, at a terminal vertex where playeri receives the payoff z i . The strategy profile ̄σ ‹ is an XRSE. We split this part into two propositions and prove them in Propositions 34 and 35. We now state a claim that we use in Propositions 34 and 35. Throught the claim and the propositions, we write ρ A to be the memoryless strategy played at memory state anchor A by ̄σ ‹ . ŹClaim 33 (Post-deviation values are capped). Lethbe a ̄σ ‹ -compatible history whose memory state is anchor A at v “ lastphq, with i P A. We have (i)(optimist) if playeri P O, thenval i pwq ď z i for every joint action ̄awith ̄a ́i P Supppρ A ́i pvqq and every w P Suppp∆pv, ̄aqq; (i)(pessimist) ifi P P, then for every actiona i available to playeriatvthere exist a joint action ̄awith ̄a i “ a i and ̄a ́i P Supppρ A ́i pvqqand a successorw P Suppp∆pv, ̄aqqsuch that val i pwq ď z i . Proof.Supposehbe a ̄σ ‹ -compatible history whose memory state isanchor A atv “ lastphq, withi P A. Consider the candidate historyh v A whose last vertex isv, that was chosen to define the strategy at vertexv. Such ah v A is an anchorable history compatible with ̄σand Λph v A q “ A. We call this history h 1 “ h v A . We note the following statement that we use: if somew P Suppp∆pv, ̄aqqwith ̄a ́i P Suppp ̄σ ́i ph 1 q “ Supppρ A ́i pvqqhasval i pwq ą z i , then sinceval i pwqis the least value the opponents can enforce on i from w and ̄σ ́iæh 1 ̄aw is one such opponent profile, sup τ i X i p ̄σ ́iæh 1 ̄aw ,τ i q ě val i pwq ą z i , so player i has a strategy θ ̄aw i with X i p ̄σ ́iæh 1 ̄aw ,θ ̄aw i q ą z i . (i). Optimists. Consider some vertexwin the game as in the statement hasval i pwq ą z i , and letθ i be the corresponding strategy above. Consider the deviationτ i that agrees with ̄σ i alongh 1 , plays ̄a i atv, and followsθ i oncep ̄a,wqis realised. Underp ̄σ ́i ,τ i qthe history h 1 is reached with positive probability; atvthe opponents play ̄σ ́i ph 1 q, whose support is Supppρ A ́i pvqq, so the pairp ̄a ́i ,wqis realised with positive probability; and fromwplayeri secures a payoffą z i with positive probability. AsX i is the greatest payoff obtained with positive probability for optimists,X i p ̄σ ́i ,τ i q ą z i , contradicting that ̄σis an XRSE for optimists. Hence val i pwq ď z i . (i). Pessimists. Fix an available actiona i and suppose, for contradiction, that val i pwq ą z i for every realised pairp ̄a,wqwith ̄a “ pa i , ̄a ́i q, ̄a ́i P Suppp ̄σ ́i ph 1 qqand w P Suppp∆pv, ̄aqq. For each such pair pickθ ̄aw i as above, and letτ i playa i atvand then follow θ ̄aw i from p ̄a,wq. The pessimistic risk is the minimum of the realisable payoffs, so X i p ̄σ ́iæh 1 ,τ i q “ min p ̄a,wq X i p ̄σ ́iæh 1 ̄aw ,θ ̄aw i q ą z i , contradicting thatiis anchored ath 1 . Hence some vertexwthat is reached by ̄σhas val i pwq ď z i .Ÿ § Proposition 34. No optimist has a profitable deviation in ̄σ ‹ . 26Algorithms for Equilibria in Concurrent Stopping Games Proof.Let playeri P Obe an optimist and letσ 1 i be a deviation, withz 1 “ X i p ̄σ ‹ ́i ,σ 1 i q . Along any play compatible with ̄σ ‹ ́i the shared memory can only stay among states anchor A for a fixed A; move from anchor A to anchor B with B Ĺ A; move to punish i , and then remain there. Since the anchored sets strictly shrink along the second kind of step and Π is finite, and sinceGis stopping, every play stabilises either inpunish i or in someanchor A . AsX i equals the greatest payoff that playeriobtains with positive probability, it suffices to bound byz i the payoff of every play that occurs with positive probability under p ̄σ ‹ ́i ,σ 1 i q. If such a play never enterspunish i , then playerinever played outside its prescribed support, so the play is compatible with ̄σ ‹ itself; since we have shown Proposition 30, every payoff that ̄σ ‹ realises with positive probability is at most z i for the optimist i. If the play enterspunish i , letvbe the last vertex at which the memory is still an anchoring stateanchor A , and letv ̄awbe the step that triggers the switch: it meansiplayed the out- of-support action ̄a i while the opponents played withinSuppp ̄σ ́i ph v A q. Fromwonward the opponents follow the value-optimal punishment ̄σ :i ́i , so every continuation gives playeriat mostsup τ i X i ` p ̄σ :i ́i ,τ i q æw ̆ ď val i pwq , which is at mostz i by Claim 33(i). Hence this play, too, yields player i at most z i . In both cases z 1 ď z i , so σ 1 i is not a profitable deviation.đ § Proposition 35. No pessimist has a profitable deviation in ̄σ ‹ . Proof. Let i P P and let σ 1 i be a deviation; by Lemma 27 we may take σ 1 i positional on the support arena. We show that playeristill obtains a payoffď z i with positive probability, i.e.PM i p ̄σ ‹ ́i ,σ 1 i q ď z i , so the deviation does not raisei’s pessimistic value abovez i . By construction, and as in Proposition 34, along any play compatible with ̄σ ‹ ́i the shared memory stabilises in punish i or in some anchor A . A detectable deviation. Suppose that at some historyhcompatible with ̄σ ‹ , whose memory state isanchor A withi P Aatv “ lastphq, the strategyσ 1 i plays an actiona i R Supppρ A i pvqq, so the memory switches topunish i . By Claim 33(i) some successorwreached by this action satisfiesval i pwq ď z i ; thiswoccurs with positive probability, and fromwthe punishment ̄σ :i ́i guarantees, against every strategy of playeri, a positive-probability play of payoffď z i (Lemma 26, case (P)). Hence X i p ̄σ ‹ ́i ,σ 1 i q ď z i , and the deviation is not profitable. No detectable deviation. Otherwise, the strategyσ 1 i never leaves the prescribed support at an anchoring state carryingi: whenever the memory is in a stateanchor A withi P Aat a vertexv, every action played with positive probability byσ 1 i lies inSupppσ i ph v A q. The argument of Proposition 30 is used on the profilep ̄σ ‹ ́i ,σ 1 i q: at each such pairpanchor A ,vq, pick an actiona i played with positive probability byσ 1 i ; sincea i P Supppσ i ph v A q, Property 5 ensures that the unique childh v A ̄awwithi th actiona i whose label containsi, and its opponent part ̄a ́i lies inSuppp ̄σ ́i ph v A q, which is exactly the support played by ̄σ ‹ ́i . The corresponding edge is therefore taken with positive probability underp ̄σ ‹ ́i ,σ 1 i q, and the rank of the representatives strictly decreases as in the proof of Proposition 30. Hence, with positive probability, a terminal historycwithi PΛpcqis reached, at which playerireceives the payoff z i by Claim 32. Consequently, X i p ̄σ ‹ ́i ,σ 1 i q ď z i , and the deviation is not profitable. đ đ