The Complexity of Subgame Perfect Equilibria in Quantitative Reachability Games

TL;DR

This paper investigates the computational complexity of subgame perfect equilibria in multiplayer quantitative reachability games, proving the problem is PSPACE-complete and introducing a new iterative algorithm for characterizing SPE outcomes.

Contribution

It establishes the PSPACE-completeness of the constrained existence problem for SPE in these games and proposes a novel fixpoint-based algorithm for outcome characterization.

Findings

The constrained existence problem for SPE is PSPACE-complete.

A new iterative algorithm constructs a finite graph representing SPE outcomes.

The algorithm's complexity aligns with PSPACE, confirming the problem's computational difficulty.

Abstract

We study multiplayer quantitative reachability games played on a finite directed graph, where the objective of each player is to reach his target set of vertices as quickly as possible. Instead of the well-known notion of Nash equilibrium (NE), we focus on the notion of subgame perfect equilibrium (SPE), a refinement of NE well-suited in the framework of games played on graphs. It is known that there always exists an SPE in quantitative reachability games and that the constrained existence problem is decidable. We here prove that this problem is PSPACE-complete. To obtain this result, we propose a new algorithm that iteratively builds a set of constraints characterizing the set of SPE outcomes in quantitative reachability games. This set of constraints is obtained by iterating an operator that reinforces the constraints up to obtaining a fixpoint. With this fixpoint, the set of SPE outcomes can be represented by a finite graph of size at most exponential. A careful inspection of the computation allows us to establish PSPACE membership.

Tables

Table 1. Table 1. The different steps of the algorithm computing λ ∗ superscript 𝜆 \lambda^{*} for the extended game of Figure  2

Region	$\{1,2\}$	$\left\{2\right\}$							$\varnothing$
	$v$	$v_0$	$v_1$	$v_6$	$v_7$	$v_3$	$v_4$	$v_5$	$v_0$	$v_1$	$v_6$	$v_7$	$v_3$	$v_4$
${\lambda }^0={\lambda }^1$	0	0	$+\infty$	$+\infty$	$+\infty$	$+\infty$	$+\infty$	$+\infty$	$+\infty$	$+\infty$	$+\infty$	$+\infty$	$+\infty$	$+\infty$
${\lambda }^2={\lambda }^3$	0	0	$3$	$2$	1	$+\infty$	$+\infty$	$+\infty$	$+\infty$	$+\infty$	$+\infty$	$+\infty$	$+\infty$	$+\infty$
${\lambda }^4$	0	0	3	2	1	$+\infty$	$+\infty$	$+\infty$	$+\infty$	3	2	1	$+\infty$	$+\infty$
${\lambda }^5={\lambda }^{\ast }$	0	0	3	2	1	$+\infty$	$+\infty$	$+\infty$	4	3	2	1	$+\infty$	$+\infty$

Equations

$${\mathrm{Cost}}_i^{\prime }(\rho )=1-\frac{1}{{\mathrm{Cost}}_i(\rho )+1}\text{ if }{\mathrm{Cost}}_i(\rho )<+\infty ,\text{ and }{\mathrm{Cost}}_i^{\prime }(\rho )=1\text{ otherwise.}$$

$$I_k\subseteq I_{k+1}\text{mbox}forallk\in \mathbb{N}.$$

$$J_1<J_2<\cdots <J_N.$$

$$\pi [\ell ]\pi [\ell +1]\dots \pi [m]$$

$${\rho }^X=(v_0,\varnothing )(v_1,\varnothing )(v_6,\varnothing )(v_7,\varnothing ){((v_2,\Pi )(v_0,\Pi )(v_1,\Pi )(v_6,\Pi )(v_7,\Pi ))}^{\omega }$$

$${\mathrm{Cost}}_i({\rho }_{\ge n})\le \lambda ({\rho }_n).$$

$$\rho =(v_0,\varnothing )(v_1,\varnothing )(v_6,\varnothing )(v_7,\varnothing ){((v_2,\Pi )(v_0,\Pi )(v_1,\Pi )(v_6,\Pi )(v_7,\Pi ))}^{\omega }$$

$${\lambda }^0(v)=\{\begin{array}{ll}0& \text{if }i\in I(v)\\ +\infty & \text{otherwise}.\end{array}$$

$${\lambda }^{k+1}(v)=\{\begin{array}{ll}0& \text{if }i\in I(v)\\ 1+\underset{\begin{array}{c}(v,v^{\prime })\in E^X\end{array}}{\min }\sup \{{\mathrm{Cost}}_i(\rho )\mid \rho \in {\Lambda }^k(v^{\prime })\}& \text{otherwise}\end{array}$$

$${\lambda }^{k+1}(v)={\lambda }^k(v).$$

$${\lambda }^{k_n^{\ast }+m}(v)={\lambda }^{k_n^{\ast }}(v),$$

$${\lambda }^{k^{\ast }+m}(v)={\lambda }^{k^{\ast }}(v).$$

$${\lambda }^{k+1}(v)\le {\lambda }^k(v).$$

$${\Lambda }^{k+1}(v^{\prime })\subseteq {\Lambda }^k(v^{\prime }).$$

$${\lambda }^{k+1}(v)=1+\underset{\begin{array}{c}(v,v^{\prime })\in E^X\end{array}}{\min }\sup \{{\mathrm{Cost}}_i(\rho )\mid \rho \in {\Lambda }^k(v^{\prime })\}.$$

$${\lambda }^{k+1}(v)\ge 1+\underset{\begin{array}{c}(v,v^{\prime })\in E^X\end{array}}{\min }\sup \{{\mathrm{Cost}}_i(\rho )\mid \rho \in {\Lambda }^{k+1}(v^{\prime })\}={\lambda }^{k+2}(v).$$

$$\rho \in {\Lambda }^k(v).$$

$$\begin{array}[]{ccc}\operatorname{Cost}_{j}(\rho_{\geq m})>\lambda^{t}(\rho_{m})&\text{and}&\operatorname{Cost}_{j}(\rho_{\geq m})\leq\lambda^{t-1}(\rho_{m}).\end{array}$$

$$⟨{\sigma }_{\upharpoonright h}{⟩}_v\in {\Lambda }^k(v).$$

$${\mathrm{Cost}}_i({\rho }_{\ge n})>{\lambda }^{k+1}({\rho }_n).$$

$${\mathrm{Cost}}_i({\rho }_{\ge n})\le {\lambda }^k({\rho }_n).$$

$${\lambda }^{k+1}({\rho }_n)<+\infty \text{, }{\lambda }^k({\rho }_n)\ne 0\text{ and }{\lambda }^{k+1}({\rho }_n)\ne 0.$$

$${\lambda }^{k+1}({\rho }_n)=1+\underset{\begin{array}{c}({\rho }_n,v^{\prime })\in E^X\end{array}}{\min }\sup \{{\mathrm{Cost}}_i({\rho }^{\prime })\mid {\rho }^{\prime }\in {\Lambda }^k(v^{\prime })\}.$$

$${\lambda }^{k+1}({\rho }_n)-1=\sup \{{\mathrm{Cost}}_i({\rho }^{\prime })\mid {\rho }^{\prime }\in {\Lambda }^k(v^{\prime })\}.$$

$${\mathrm{Cost}}_i(h^{\prime }⟨{\tau }_i,{\sigma }_{-i|h^{\prime }}{⟩}_{{\rho }_n})$$

$$={\mathrm{Cost}}_i(h^{\prime }{\rho }_n⟨{\sigma }_{\upharpoonright h^{\prime }{\rho }_n}{⟩}_{v^{\prime }})$$

$$=|h^{\prime }{\rho }_n{v}^{\prime }|+{\mathrm{Cost}}_i(⟨{\sigma }_{\upharpoonright h^{\prime }{\rho }_n}{⟩}_{v^{\prime }})$$

$$\le |h^{\prime }{\rho }_n{v}^{\prime }|+{\lambda }^{k+1}({\rho }_n)-1$$

$$<|h^{\prime }{\rho }_n|+{\mathrm{Cost}}_i({\rho }_{\ge n})$$

$$={\mathrm{Cost}}_i(h^{\prime }⟨{\sigma }_{\upharpoonright h^{\prime }}{⟩}_{{\rho }_n})$$

$${\Lambda }^{\ast }(v)\ne \varnothing \text{ for all }v\in {\mathrm{Succ}}^{\ast }(x_0).$$

$${\mathrm{Cost}}_i({\rho }_{i,v^{\prime }})=\max \{{\mathrm{Cost}}_i({\rho }^{\prime })\mid {\rho }^{\prime }\in {\Lambda }^{\ast }(v^{\prime })\}$$

$$⟨{\sigma }_{\upharpoonright hv}{⟩}_{v^{\prime }}={\rho }_{i,v^{\prime }}$$

Full text

Introduction

While two-player zero-sum games played on graphs are the most studied model to formalize and solve the reactive synthesis problem [PR89], recent work has considered non-zero-sum extensions of this mathematical framework, see e.g. [CHJ06, FKL10, BRS14, KPV14, BRS15, BPRS16, CFGR16, BPRS17, BJP*+*18], see also the surveys [GU08, BCH*+*16, Bru17]. In the zero-sum game approach, the system and the environment are considered as monolithic and fully adversarial entities. Unfortunately, both assumptions may turn to be too strong. First, the reactive system may be composed of several components that execute concurrently and have their own purpose. So, it is natural to model such systems with multiplayer games with each player having his own objective. Second, the environment usually has its own objective too, and this objective is usually not the negation of the objective of the reactive system as postulated in the zero-sum case. Therefore, there are instances of the reactive synthesis problem for which no solution exists in the zero-sum setting, i.e. no winning strategy for the system against a completely antagonistic environment, while there exists a strategy for the system which enforces the desired properties against all rational behaviors of the environment pursuing its own objective.

While the central solution concept in zero-sum games is the notion of winning strategy, it is well known that this solution concept is not sufficient to reason about non-zero-sum games. In non-zero-sum games, notions of equilibria are used to reason about the rational behavior of players. The celebrated notion of Nash equilibrium (NE) [Nas50] is one of the most studied. A profile of strategies is an NE if no player has an incentive to deviate, i.e. change his strategy and obtain a better reward, when this player knows that the other players will be playing their respective strategies in the profile. A well-known weakness of NEs in sequential games, which include infinite duration games played on graphs, is that they are subject to non-credible threats: decisions in subgames that are irrational and used to threaten the other players and oblige them to follow a given behavior. To avoid this problem, the concept of subgame perfect equilibrium (SPE) has been proposed, see e.g. [Osb04]. In the framework of systems subject to bugs, this means that the players will keep playing rationally in all situations, i.e. when no bug occurs and after any bug’s occurrence. SPEs are NEs with the additional property that they are also NEs in all subgames of the original game. While it is now quite well understood how to handle NEs algorithmically in games played on graphs [Umm08, UW11, BDS13, CFGR16], this is not the case for SPEs.

Contributions

In this paper, we provide an algorithm to decide in polynomial space the constrained existence problem for SPEs in quantitative reachability games. A quantitative reachability game is played by $n$ players on a finite graph in which each player has his own reachability objective. The objective of each player is to reach his target set of vertices as quickly as possible. In a series of papers, it has been shown that SPEs always exist in quantitative reachability games [BBDG12], and that the set of outcomes of SPEs in a quantitative reachability game is a regular language which is effectively constructible [BBMR15]. As a consequence of the latter result, the constrained existence problem for SPEs is decidable. The previously mentioned results use the property that for quantitative reachability games, SPEs coincide with weak SPEs and very weak SPEs [BBMR15]. Weak (resp. very weak) SPE must be resistant to unilateral deviations of one player that differ from the original one on a finite number of histories only (resp. on the initial vertex only).

Unfortunately, the proof in [BBMR15] that establishes the regularity of the set of possible outcomes of SPEs in quantitative reachability games exploits a well-quasi order for proving termination and it cannot be used to obtain a good upper bound on the complexity for the algorithm. Here, we propose a new algorithm and we show that this set of outcomes can be represented using an automaton of size at most exponential. It follows that the constrained existence problem for SPEs can be decided in PSPACE. We also provide a matching lower-bound showing that this problem is PSPACE-complete.

Our new algorithm iteratively builds a set of constraints that exactly characterizes the set of SPEs in quantitative reachability games. This set of constraints is obtained by iterating an operator that reinforces the constraints up to obtaining a fixpoint. A careful inspection of the computation allows us to establish PSPACE membership.

Related work

Algorithms to reason on NEs in graph games are studied in [Umm08] for $\omega$-regular objectives and in [UW11, BDS13] for quantitative objectives. Algorithms to reason on SPEs are given in [Umm06] for $\omega$-regular objectives. Quantitative reachability objectives are not $\omega$-regular objectives. Reasoning about NEs and SPEs for $\omega$-regular specifications can also be done using strategy logics [CHP10, MMV10].

Other notions of rationality and their use for reactive synthesis have been studied in the literature: rational synthesis in cooperative [FKL10] and adversarial [KPV14] setting, and their algorithmic complexity has been studied in [CFGR16]. Extensions with imperfect information have been investigated in [FGR18]. Synthesis rules based on the notion of admissible strategies have been studied in [Ber07, BRS14, BRS15, BPRS16, BPRS17, BJP*+*18].

The restricted class of deviating strategies used in very weak SPEs is a well-known notion that for instance appears in [Kuh53] with the one-step deviation property. Weak SPEs and very weak SPEs are equivalent notions, but there are games for which there exists a weak SPE but no SPE [BBMR15, SV03]. Nevertheless, (very) weak SPEs and SPEs are equivalent for quantitative reachability games, an important property used in the proofs of [BBMR15] and of this paper. The equivalence between SPEs and very weak SPEs is also implicitly used as a proof technique in a continuous setting in [FL83] and in a lower-semicontinuous setting in [FKM*+*10].

In [BRPR17], general conditions are given that guarantee the existence of a weak SPE. It follows that there always exists a weak SPE for games where players use a prefix-independent payoff function. The computational complexity of the constraint existence problem for weak SPEs in games with $\omega$-regular objectives is studied in [BBGR18a]. In [BBGT19], the authors focus on relevant SPEs in qualitative and quantitative reachability games where a relevant SPE is either an SPE with cost profile as low as possible, or an SPE which maximizes the social welfare (both maximizes the number of players who reach their target set and minimize the sum of the costs of these players), or is Pareto optimal in the set of all SPE cost profiles. Notice that the obtained complexity results are based on the labeling technique proposed in our paper and that they are the same with or without lower bounds on the cost profiles.

Fixpoint techniques are used several papers to establish the existence of (weak) SPEs in some classes of games like [FKM*+*10, BBMR15, BRPR17, BBGR18a]. However they cannot be used in our context to get the PSPACE complexity result.

Structure of the paper

In Section 1, we recall the notions of $n$-player graph games and (very weak/weak) SPEs, we introduce the notion of extendend games and we state the studied constrained existence problem. In Section 2, we provide a way to characterize the set of plays that are outcomes of SPEs and give an algorithm to construct this set. This algorithm relies on the computation of a sequence of labeling functions ${(\lambda_{k})}_{k\in\mathbb{N}}$ until reaching a fixpoint $\lambda^{*}$ such that the plays which are $\lambda^{*}$-consistent are exactly the plays which are outcomes of SPEs. In Section 3, given a labeling function $\lambda$, we introduce the notion of counter graph in which infinite paths correspond to $\lambda$-consistent plays. We also show that such a counter graph has an exponential size. In Section 4, using counter graphs, we prove the PSPACE-easiness of the constrained existence problem. We then prove the PSPACE-hardness of this problem. A conclusion is provided in the last section.

This article is an extended version of an article that appeared in the Proceedings of CONCUR 2019 [BBG*+*19]. All results are proved while most of those proofs were omitted or very briefly sketched in the CONCUR Proceedings.

1. Preliminaries

In this section, we recall the notions of quantitative reachability game and subgame perfect equilibrium. We also state the problem studied in this paper and our main result.

1.1. Quantitative reachability games

An arena is a tuple $G=(\Pi,V,{(V_{i})}_{i\in\Pi},E)$ where $\Pi=\{1,2,\ldots,n\}$ is a finite set of $n$ players, $V$ is a finite set of vertices with $|V|\geq 2$, ${(V_{i})}_{i\in\Pi}$ is a partition of $V$ between the players, and $E\subseteq V\times V$ is a set of edges such that for all $v\in V$ there exists $v^{\prime}\in V$ such that $(v,v^{\prime})\in E$. Without loss of generality, we suppose that $|\Pi|\leq|V|$.

A play in $G$ is an infinite sequence of vertices $\rho=\rho_{0}\rho_{1}\ldots$ such that for all $k\in\mathbb{N}$111Throughout this document we assume that $\mathbb{N}$ contains [math], i.e., $\mathbb{N}=\{0,1,2,\ldots\}.$, $(\rho_{k},\rho_{k+1})\in E$. A history is a finite sequence $h=h_{0}h_{1}\ldots h_{k}$ with $k\in\mathbb{N}$ defined similarly. The length $|h|$ of $h$ is the number $k$ of its edges. We denote the set of plays by $\operatorname{Plays}$ and the set of histories by $\operatorname{Hist}$ (when it is necessary, we use notation $\operatorname{Plays}_{G}$ and $\operatorname{Hist}_{G}$ to recall the underlying arena $G$). Moreover, the set $\operatorname{Hist}_{i}$ is the set of histories such that their last vertex $v$ is a vertex of player $i$, i.e. $v\in V_{i}$.

Given a play $\rho=\rho_{0}\rho_{1}\ldots\in\operatorname{Plays}$ and $k\in\mathbb{N}$, the prefix $\rho_{0}\rho_{1}\ldots\rho_{k}$ of $\rho$ is denoted by $\rho_{\leq k}$ and its suffix $\rho_{k}\rho_{k+1}\ldots$ is denoted by $\rho_{\geq k}$. A play $\rho$ is called a lasso if it is of the form $\rho=h\ell^{\omega}$ with $h\ell\in\operatorname{Hist}$. Notice that $\ell$ is not necessary a simple cycle.

Given an arena $G$, we denote by $\operatorname{Succ}(v)=\{v^{\prime}\mid(v,v^{\prime})\in E\}$ the set of successors of $v$, for $v\in V$, and by $\operatorname{Succ}^{*}$ the transitive closure of $\operatorname{Succ}$.

A quantitative game $\mathcal{G}=(G,{(\operatorname{Cost}_{i})}_{i\in\Pi})$ is an arena equipped with a cost function profile $\operatorname{Cost}={(\operatorname{Cost}_{i})}_{i\in\Pi}$ such that each function $\operatorname{Cost}_{i}:\operatorname{Plays}\rightarrow\mathbb{R}\cup\{+\infty\}$ assigns a cost to each play. In a quantitative game $\mathcal{G}$, an initial vertex $v_{0}\in V$ is often fixed, and we call $(\mathcal{G},v_{0})$ an initialized game. A play (resp. a history) of $(\mathcal{G},v_{0})$ is then a play (resp. a history) of $\mathcal{G}$ starting in $v_{0}$. The set of such plays (resp. histories) is denoted by $\operatorname{Plays}(v_{0})$ (resp. $\operatorname{Hist}(v_{0})$). We also use notation $\operatorname{Hist}_{i}(v_{0})$ when these histories end in a vertex $v\in V_{i}$.

In this article we are interested in quantitative reachability games such that each player has a target set of vertices that he wants to reach. The cost to pay is equal to the number of edges to reach the target set, and each player aims at minimizing his cost.

{defi}

[Quantitative reachability game] A quantitative reachability game is a tuple $\mathcal{G}=(G,{(F_{i})}_{i\in\Pi},{(\operatorname{Cost}_{i})}_{i\in\Pi})$ such that

• •

$G$ is an arena;

• •

for each $i\in\Pi$, $F_{i}\subseteq V$ is the target set of player $i$;

• •

for each $i\in\Pi$ and each $\rho=\rho_{0}\rho_{1}\ldots\in\operatorname{Plays}$, $\operatorname{Cost}_{i}(\rho)$ is equal to the least index $k$ such that $\rho_{k}\in F_{i}$, and to $+\infty$ if no such index exists.

In the rest of this document, we simply call such a game a reachability game. Notice that the cost function used for reachability games can be supposed to be continuous in the following sense [BBDG12]. With $V$ endowed with the discrete topology and $V^{\omega}$ with the product topology, a sequence of plays ${(\rho_{n})}_{n\in\mathbb{N}}$ converges to $\rho$ if every prefix of $\rho$ is a prefix of all $\rho_{n}$ except, possibly, finitely many of them. A cost function $\operatorname{Cost}_{i}$ is continuous if whenever $\lim_{n\rightarrow+\infty}\rho_{n}=\rho$, we have that $\lim_{n\rightarrow+\infty}\operatorname{Cost}_{i}(\rho_{n})=\operatorname{Cost}_{i}(\rho)$. In reachability games, the function $\operatorname{Cost}_{i}$ can be transformed into a continuous one as follows:

[TABLE]

Notice that for the problem we study both cost functions ${(\operatorname{Cost}_{i})}_{i\in\Pi}$ or ${(\operatorname{Cost}^{\prime}_{i})}_{i\in\Pi}$ are equivalent. Therefore throughout this paper we use both functions indifferently.

Given a quantitative game $\mathcal{G}$, a strategy of a player $i\in\Pi$ is a function $\sigma_{i}:\operatorname{Hist}_{i}\rightarrow V$. This function assigns to each history $hv$, with $v\in V_{i}$, a vertex $v^{\prime}$ such that $(v,v^{\prime})\in E$. In an initialized game $(\mathcal{G},v_{0})$, $\sigma_{i}$ needs only to be defined for histories starting in $v_{0}$. A play $\rho=\rho_{0}\rho_{1}\ldots$ is consistent with $\sigma_{i}$ if for all $\rho_{k}\in V_{i}$ we have that $\sigma_{i}(\rho_{0}\ldots\rho_{k})=\rho_{k+1}$. A strategy $\sigma_{i}$ is positional if it only depends on the last vertex of the history, i.e., $\sigma_{i}(hv)=\sigma_{i}(v)$ for all $hv\in\operatorname{Hist}_{i}$. It is finite-memory if it can be encoded by a finite-state machine.

Given a quantitative game $\mathcal{G}$, a strategy profile is a tuple $\sigma={(\sigma_{i})}_{i\in\Pi}$ of strategies, one for each player. It is called positional (resp. finite-memory) if for all $i\in\Pi$, $\sigma_{i}$ is positional (resp. finite-memory). Given an initialized game $(\mathcal{G},v_{0})$ and a strategy profile $\sigma$, there exists an unique play from $v_{0}$ that is consistent with each strategy $\sigma_{i}$. We call this play the outcome of $\sigma$ and it is denoted by $\langle\sigma\rangle_{v_{0}}$. Let $c={(c_{i})}_{i\in\Pi}\in{(\mathbb{N}\cup\{+\infty\})}^{|\Pi|}$, we say that $\sigma$ is a strategy profile with cost $c$ or that $\langle\sigma\rangle_{v_{0}}$ has cost $c$ if $c_{i}=\operatorname{Cost}_{i}(\langle\sigma\rangle_{v_{0}})$ for all $i\in\Pi$.

1.2. Solution concepts and constraint problem

In the multiplayer game setting, the solution concepts usually studied are equilibria (see [GU08]). We here recall the concepts of Nash equilibrium and subgame perfect equilibrium.

Let $\sigma={(\sigma_{i})}_{i\in\Pi}$ be a strategy profile in an initialized game $(\mathcal{G},v_{0})$. When we highlight the role of player $i$, we denote $\sigma$ by $(\sigma_{i},\sigma_{-i})$ where $\sigma_{-i}$ is the profile ${(\sigma_{j})}_{j\in\Pi\setminus\{i\}}$. A strategy $\sigma^{\prime}_{i}\neq\sigma_{i}$ is a deviating strategy of player $i$, and it is a profitable deviation for him if $\operatorname{Cost}_{i}(\langle\sigma\rangle_{v_{0}})>\operatorname{Cost}_{i}(\langle\sigma^{\prime}_{i},\sigma_{-i}\rangle_{v_{0}})$. Hence a deviating strategy is profitable for player $i$ if it leads to a smaller cost for him when the other players stick to their own strategy.

The notion of Nash equilibrium is classical: a strategy profile $\sigma$ in an initialized game $(\mathcal{G},v_{0})$ is a Nash equilibrium (NE) if no player has an incentive to deviate unilaterally from his strategy, i.e. no player has a profitable deviation. Formally, $\sigma$ is an NE if for each $i\in\Pi$ and each deviating strategy $\sigma^{\prime}_{i}$ of player $i$, we have $\operatorname{Cost}_{i}(\langle\sigma\rangle_{v_{0}})\leq\operatorname{Cost}_{i}(\langle\sigma^{\prime}_{i},\sigma_{-i}\rangle_{v_{0}})$.

When considering games played on graphs, a useful refinement of NE is the concept of subgame perfect equilibrium (SPE) which is a strategy profile being an NE in each subgame. It is well-known that contrarily to NEs, SPEs avoid non-credible threats [GU08]. Formally, given a quantitative game ${\mathcal{G}}=(G,\operatorname{Cost})$, an initial vertex $v_{0}$, and a history $hv\in\operatorname{Hist}(v_{0})$, the initialized game $(\mathcal{G}_{\restriction h},v)$ is called a subgame of $(\mathcal{G},v_{0})$ such that $\mathcal{G}_{\restriction h}=(G,\operatorname{Cost}_{\restriction h})$ and $\operatorname{Cost}_{i\restriction h}(\rho)=\operatorname{Cost}_{i}(h\rho)$ for all $i\in\Pi$ and $\rho\in V^{\omega}$. Notice that $(\mathcal{G},v_{0})$ is subgame of itself. Moreover if $\sigma_{i}$ is a strategy for player $i$ in $(\mathcal{G},v_{0})$, then $\sigma_{i\restriction h}$ denotes the strategy in $(\mathcal{G}_{\restriction h},v)$ such that for all histories $h^{\prime}\in\operatorname{Hist}_{i}(v)$, $\sigma_{i\restriction h}(h^{\prime})=\sigma_{i}(hh^{\prime})$. Similarly, from a strategy profile $\sigma$ in $(\mathcal{G},v_{0})$, we derive the strategy profile $\sigma_{\restriction h}$ in $(\mathcal{G}_{\restriction h},v)$.

{defi}

[Subgame perfect equilibrium] Let $(\mathcal{G},v_{0})$ be an initialized game. A strategy profile $\sigma$ is a subgame perfect equilibrium in $(\mathcal{G},v_{0})$ if for all $hv\in\operatorname{Hist}(v_{0})$, $\sigma_{\restriction h}$ is an NE in $(\mathcal{G}_{\restriction h},v)$.

It is proved in [BBDG12] that there always exists an SPE in reachability games.

{thmC}

[[BBDG12]] There exists an SPE in each initialized reachability game.

In this paper, we are interested in solving the following constraint problem.

{defi}

[Constraint problem] Given ($\mathcal{G},v_{0})$ an initialized reachability game and two threshold vectors $x,y\in{(\mathbb{N}\cup\{+\infty\})}^{|\Pi|}$, the constraint problem is to decide whether there exists an SPE in $(\mathcal{G},v_{0})$ with cost $c$ such that $x\leq c\leq y$, that is, $x_{i}\leq c_{i}\leq y_{i}$ for all $i\in\Pi$.

Our main result is the following one:

Theorem 1**.**

The constraint problem for initialized reachability games is PSPACE-complete.

The remaining part of the paper is devoted to the proof of this result. Let us first illustrate the introduced concepts with an example.

{exa}

A reachability game $\mathcal{G}=(G,{(F_{i})}_{i\in\Pi},{(\operatorname{Cost}_{i})}_{i\in\Pi})$ with two players is depicted in Figure 1. The circle vertices are owned by player $1$ whereas the square vertices are owned by player $2$. The target sets of both players are respectively equal to $F_{1}=\{v_{2}\}$ (grey vertex), $F_{2}=\{v_{2},v_{5}\}$ (double circled vertices).

The positional strategy profile $\sigma=(\sigma_{1},\sigma_{2})$ is depicted by double arrows, its outcome in $({\mathcal{G}},v_{0})$ is equal to $\langle\sigma\rangle_{v_{0}}={(v_{0}v_{1}v_{6}v_{7}v_{2})}^{\omega}$ with cost $(4,4)$. Let us explain that $\sigma$ is an NE. Player 1 reaches his target set as soon as possible and has thus no incentive to deviate. Player 2 has no profitable deviation that allows him to reach $v_{5}$. For instance if he uses a deviating positional strategy $\sigma^{\prime}_{2}$ such that $\sigma^{\prime}_{2}(v_{0})=v_{4}$, then the outcome of $(\sigma_{1},\sigma^{\prime}_{2})$ is equal to ${(v_{0}v_{4})}^{\omega}$ with cost $(+\infty,+\infty)$ which is not profitable for player $2$.

One can verify that the strategy profile $\sigma$ is also an SPE. For instance in the subgame $(\mathcal{G}_{\restriction h},v_{5})$ with $h=v_{0}v_{4}$, we have $\rho=\langle\sigma_{\restriction h}\rangle_{v_{5}}=v_{5}v_{4}{(v_{0}v_{1}v_{6}v_{7}v_{2})}^{\omega}$ such that $\operatorname{Cost}_{\restriction h}(\rho)=\operatorname{Cost}(h\rho)=(8,2)$. In this subgame, with $\rho$, both players reach their target set as soon as possible and have thus no incentive to deviate.

Consider now the positional strategy profile $\sigma^{\prime}=(\sigma^{\prime}_{1},\sigma^{\prime}_{2})$ such that $\sigma^{\prime}_{1}(v_{4})=v_{0}$, $\sigma^{\prime}_{1}(v_{1})=v_{3}$, and $\sigma^{\prime}_{2}(v_{0})=v_{4}$. Its outcome in $({\mathcal{G}},v_{0})$ is equal to ${(v_{0}v_{4})}^{\omega}$ with cost $(+\infty,+\infty)$. Let us explain that $\sigma^{\prime}$ is an NE. On one hand, since player 2 never goes to $v_{1}$, player 1 has no incentive to deviate, as his target is only accessible from $v_{1}$. On the other hand, if player 2 deviates and chooses to go from $v_{0}$ to $v_{1}$, his cost is still $+\infty$ since player 1 goes to $v_{3}$. However, the strategy profile $\sigma^{\prime}$ is not an SPE. Indeed, it features a non-credible threat by player 1: consider the history $v_{0}v_{1}$ and the corresponding subgame $(\mathcal{G}_{\restriction v_{0}},v_{1})$. In that case, player 1 has an incentive to deviate to reach $v_{2}$ to yield a cost of $4$. Thus, the strategy profile $\sigma^{\prime}_{\restriction v_{0}}$ is not an NE in the subgame $(\mathcal{G}_{\restriction v_{0}},v_{1})$, and thus is not an SPE in $({\mathcal{G}},v_{0})$. ∎

1.3. Weak SPE, very weak SPE and extended game

In this section, we present two important tools that will be repeatedly used in the rest of this paper. First, we explain that in reachability games, the notion of SPE is equivalent to the simpler notion of very weak SPE. Second we present an extended version of a reachability game where the vertices are enriched with the set of players that have already visited their target sets along a history. Working with this extended game is essential to prove that the constraint problem for reachability games is in PSPACE.

We begin by recalling the concepts of weak and very weak SPE introduced in [BBMR15, BRPR17]. Let $(\mathcal{G},v_{0})$ be an initialized game and $\sigma={(\sigma_{i})}_{i\in\Pi}$ be a strategy profile. Given $i\in\Pi$, we say that a strategy $\sigma^{\prime}_{i}$ is finitely deviating from $\sigma_{i}$ if $\sigma^{\prime}_{i}$ and $\sigma_{i}$ only differ on a finite number of histories, and that $\sigma^{\prime}_{i}$ is one-shot deviating from $\sigma_{i}$ if $\sigma^{\prime}_{i}$ and $\sigma_{i}$ only differ on the initial vertex $v_{0}$. A strategy profile $\sigma$ is a weak NE (resp. very weak NE) in $(\mathcal{G},v_{0})$ if, for each player $i\in\Pi$, for each finitely deviating (resp. one-shot) strategy $\sigma^{\prime}_{i}$ of player $i$ from $\sigma_{i}$, we have $\operatorname{Cost}_{i}(\langle\sigma\rangle_{v_{0}})\leq\operatorname{Cost}_{i}(\langle\sigma^{\prime}_{i},\sigma_{-i}\rangle_{v_{0}})$. A strategy profile $\sigma$ is a weak SPE (resp. very weak SPE) in $(\mathcal{G},v_{0})$ if, for all $hv\in\operatorname{Hist}(v_{0})$, $\sigma_{\restriction h}$ is a weak (resp. very weak) NE in $(\mathcal{G}_{\restriction h},v)$.

From the given definitions, every SPE is a weak SPE, and every weak SPE is a very weak SPE. It is known that weak SPE and very weak SPE are equivalent notions and that there exist initialized games that have a weak SPE but no SPE; nevertheless, all three concepts are equivalent for initialized reachability games [BBMR15, BRPR17].

{propC}

[[BBMR15, BRPR17]] Let $({\mathcal{G}},v_{0})$ be an initialized reachability game and $\sigma$ be a strategy profile in $({\mathcal{G}},v_{0})$. Then $\sigma$ is an SPE if and only if $\sigma$ is a weak SPE if and only if $\sigma$ is a very weak SPE.

Let us now recall the notion of extended game for a given reachability game $\mathcal{G}$ (see e.g. [BBGR18a]). The vertices $(v,I)$ of the extended game store a vertex $v\in V$ as well as a subset $I\subseteq\Pi$ of players that have already visited their target sets.

{defi}

[Extended game] Let $\mathcal{G}=(G,{(F_{i})}_{i\in\Pi},{(\operatorname{Cost}_{i})}_{i\in\Pi})$ be a reachability game with an arena $G=(\Pi,V,{(V_{i})}_{i\in\Pi},E)$, and let $v_{0}$ be an initial vertex. The extended game of $\mathcal{G}$ is equal to $\operatorname{\mathcal{X}}=(X,{(F^{X}_{i})}_{i\in\Pi},{(\operatorname{Cost}^{X}_{i})}_{i\in\Pi})$ with the arena $X=(\Pi,V^{X},{(V^{X}_{i})}_{i\in\Pi},E^{X})$, such that:

• •

$V^{X}=V\times 2^{\Pi}$

• •

$((v,I),(v^{\prime},I^{\prime}))\in E^{X}$ if and only if $(v,v^{\prime})\in E$ and $I^{\prime}=I\cup\{i\in\Pi\mid v^{\prime}\in F_{i}\}$

• •

$(v,I)\in V^{X}_{i}$ if and only if $v\in V_{i}$

• •

$(v,I)\in F^{X}_{i}$ if and only if $i\in I$

• •

for each $\rho\in\operatorname{Plays}_{X}$, $\operatorname{Cost}^{X}_{i}(\rho)$ is equal to the least index $k$ such that $\rho_{k}\in F^{X}_{i}$, and to $+\infty$ if no such index exists.

The initialized extended game $(\operatorname{\mathcal{X}},x_{0})$ associated with the initialized game $({\mathcal{G}},v_{0})$ is such that $x_{0}=(v_{0},I_{0})$ with $I_{0}=\{i\in\Pi\mid v_{0}\in F_{i}\}$.

Notice the way each target set $F^{X}_{i}$ is defined: if $v\in F_{i}$, then $(v,I)\in F^{X}_{i}$ but also $(v^{\prime},I^{\prime})\in F^{X}_{i}$ for all $(v^{\prime},I^{\prime})\in\operatorname{Succ}^{*}(v,I)$. In the remaining part, to avoid heavy notations, each cost function $\operatorname{Cost}^{X}_{i}$ will be simply written as $\operatorname{Cost}_{i}$.

The extended game of the reachability game of Figure 1 is depicted in Figure 2. We will come back to this example at the end of this section.

Let us state some properties of the extended game. First, notice that for each $\rho=(v_{0},I_{0})(v_{1},I_{1})\ldots\in\operatorname{Plays}_{X}(x_{0})$, we have the next property called $I$-monotonicity:

[TABLE]

Second, given an initialized game $({\mathcal{G}},v_{0})$ and its extended game $({\operatorname{\mathcal{X}}},x_{0})$, there is a one-to-one correspondence between plays in $\operatorname{Plays}_{G}(v_{0})$ and plays in $\operatorname{Plays}_{X}(x_{0})$:

• •

from $\rho=\rho_{0}\rho_{1}\ldots\in\operatorname{Plays}_{G}(v_{0})$, we derive $\rho^{X}=(\rho_{0},I_{0})(\rho_{1},I_{1})\ldots\in\operatorname{Plays}_{X}(x_{0})$ such that $I_{k}$ is the set of players $i$ that have visited their target set $F_{i}$ along $\rho_{\leq k}$;

• •

from $\rho=(v_{0},I_{0})(v_{1},I_{1})\ldots\in\operatorname{Plays}_{X}(x_{0})$, we derive $\rho^{G}=v_{0}v_{1}\ldots\in\operatorname{Plays}_{G}(v_{0})$ such that the second components $I_{k}$, $k\in\mathbb{N}$, are omitted.

Third, given $\rho\in\operatorname{Plays}_{G}(v_{0})$, we have that $\operatorname{Cost}(\rho^{X})=\operatorname{Cost}(\rho)$, and conversely given $\rho\in\operatorname{Plays}_{X}(x_{0})$, we have that $\operatorname{Cost}(\rho^{G})=\operatorname{Cost}(\rho)$. It follows that outcomes of SPE can be equivalently studied in $({\mathcal{G}},v_{0})$ and in $({\operatorname{\mathcal{X}}},x_{0})$, as stated in the next lemma.

Lemma 2**.**

If $\rho$ is the outcome of an SPE in $({\mathcal{G}},v_{0})$, then $\rho^{X}$ is the outcome of an SPE in $({\operatorname{\mathcal{X}}},x_{0})$ with the same cost. Conversely, if $\rho$ is the outcome of an SPE in $({\operatorname{\mathcal{X}}},x_{0})$, then $\rho^{G}$ is the outcome of an SPE in $({\mathcal{G}},v_{0})$ with the same cost.

Notice that in the same way there is a one-to-one correspondence between strategies in $({\mathcal{G}},v_{0})$ and in its extended game $({\operatorname{\mathcal{X}}},x_{0})$. Thus Lemma 2 could be rephrased in term of SPEs instead of SPE outcomes. In Theorem 8, we see that outcome characterization is sufficient to deal with SPEs.

By construction, the arena $X$ of the initialized extended game is divided into different regions according to the players who have already visited their target set. Let us provide some useful notions with respect to this decomposition. (An illustrative example is given hereafter.) We will often use them in the following sections. Let $\mathcal{I}=\{I\subseteq\Pi\mid\text{there exists }v\in V\text{ such that }(v,I)\in\operatorname{Succ}^{*}(x_{0})\}$ be the set of sets $I$ accessible from the initial state $x_{0}$, and let $N=|\mathcal{I}|$ be its size. For $I,I^{\prime}\in\mathcal{I}$, if there exists $((v,I),(v^{\prime},I^{\prime}))\in E^{X}$, we say that $I^{\prime}$ is a successor of $I$ and we write $I^{\prime}\in\operatorname{Succ}(I)$. Given $I\in\mathcal{I}$, $X^{I}=(V^{I},E^{I})$ refers to the sub-arena of $X$ restricted to the vertices $\{(v,I)\in V^{X}\mid v\in V\}$. Hence $X^{I}$ has all its vertices with the same second component $I$. We say that $X^{I}$ is the region222In the rest of this paper, we indifferently call region either $X^{I}$, or $V^{I}$, or $I$. associated with $I$. Such a region $X^{I}$ is called a bottom region whenever $\operatorname{Succ}(I)=I$.

There exists a partial order on $\mathcal{I}$ such that $I<I^{\prime}$ if and only if $I^{\prime}\in\operatorname{Succ}^{*}(I)\setminus\{I\}$. We fix an arbitrary total order on $\mathcal{I}$ that extends this partial order $<$ as follows:

[TABLE]

(with $X^{J_{N}}$ a bottom region).333We use notation $J_{n}$, $n\in\{1,\ldots,N\}$, to avoid any confusion with the sets $I_{k}$ appearing in a play $\rho=(v_{0},I_{0})(v_{1},I_{1})\ldots$. With respect to this total order, given $n\in\{1,\ldots,N\}$, we denote by $X^{\geq J_{n}}=(V^{\geq J_{n}},E^{\geq J_{n}})$ the sub-arena of $X$ restricted to the vertices $\{(v,I)\in V^{X}\mid I\geq J_{n}\}$.

The total order given in (3) together with the $I$-monotonicity (see (2)) leads to the following lemma.

Lemma 3** (Region decomposition and section).**

Let $\pi$ be a path in the arena $X$ of the extended game $\operatorname{\mathcal{X}}$. Then there exists a region decomposition of $\pi$ as

[TABLE]

with $1\leq\ell\leq m\leq N$, such that for each $n$, $\ell\leq n\leq m$:

• •

$\pi[n]$* is a (possibly empty) path in $X$,*

• •

every vertex of $\pi[n]$ is of the form $(v,J_{n})$ for some $v\in V$.

Each path $\pi[n]$ is called a section. The last section $\pi[m]$ is infinite if and only if $\pi$ is infinite.

{exa}

Let us come back to the initialized game $(\mathcal{G},v_{0})$ of Figure 1. Its extended game $(\operatorname{\mathcal{X}},x_{0})$ is depicted in Figure 2 (only the part reachable from the initial vertex $x_{0}=(v_{0},\emptyset)$ is depicted; for the moment the reader should not consider the labeling indicated under the vertices). As we can see, the extended game is divided into three different regions: one region associated with $I=\emptyset$ that contains the initial vertex $x_{0}$, a second region associated with $I=\{2\}$, and a third bottom region associated with $I=\{1,2\}=\Pi$. Hence the set ${\mathcal{I}}=\{\emptyset,\{2\},\Pi\}$ is totally ordered as $J_{1}=\emptyset<J_{2}=\{2\}<J_{3}=\Pi$.

For all vertices $(v,I)$ of the region associated with $I=\{2\}$, we have $(v,I)\not\in F^{X}_{1}$ and $(v,I)\in F^{X}_{2}$, and for those of the region associated with $I=\Pi$, we have $(v,I)\in F^{X}_{1}\cap F^{X}_{2}$. The sub-arena $X^{\geq J_{2}}$ of $X$ is composed of all vertices $(v,I)$ such that $I=\{2\}$ or $I=\Pi$.

From the SPE $\sigma$ given in Example 1.2 with outcome $\rho={(v_{0}v_{1}v_{6}v_{7}v_{2})}^{\omega}\in\operatorname{Plays}_{G}(v_{0})$ and cost $(4,4)$, we derive the SPE outcome $\rho^{X}\in\operatorname{Plays}_{X}(x_{0})$ equal to

[TABLE]

with the same cost $(4,4)$. The region decomposition of $\rho^{X}$ is equal to $\rho^{X}[1]\rho^{X}[2]\rho^{X}[3]$ such that its second section $\rho^{X}[2]$ is empty, and its two other sections $\rho^{X}[1]$ and $\rho^{X}[3]$ are respectively equal to $(v_{0},\emptyset)(v_{1},\emptyset)(v_{6},\emptyset)(v_{7},\emptyset)$, and ${((v_{2},\Pi)(v_{0},\Pi)(v_{1},\Pi)(v_{6},\Pi)(v_{7},\Pi))}^{\omega}$. ∎

2. Characterization

In this section, given an initialized reachability game $({\mathcal{G}},v_{0})$, we characterize the set of plays that are outcomes of SPEs, and we provide an algorithm to construct this set. For this characterization, by Lemma 2, we can work on the extended game $({\operatorname{\mathcal{X}}},x_{0})$ instead of $({\mathcal{G}},v_{0})$. Moreover by Proposition 1.3, we can focus on very weak SPEs only since they are equivalent to SPEs. Such a characterization already appears in [BBMR15] however with a different algorithm that cannot be used to obtain good complexity upper bounds for the constraint problem.

All along this section, to avoid heavy notation when we refer to a vertex of $V^{X}$, we use notation $v$ (instead of $(u,I)$) and notation $I(v)$ means the second component $I$ of this vertex.

Our algorithm iteratively builds a set of constraints imposed by a labeling function $\lambda:V^{X}\rightarrow\mathbb{N}\cup\{+\infty\}$ such that the plays of the extended game satisfying those constraints are exactly the SPE outcomes. Let us provide a formal definition of such a function $\lambda$ with the constraints that it imposes on plays.

{defi}

[$\lambda$-consistent play] Let $\operatorname{\mathcal{X}}$ be the extended game of a reachability game $\mathcal{G}$, and $\lambda:V^{X}\rightarrow\mathbb{N}\cup\{+\infty\}$ be a labeling function. Given $v\in V^{X}$, for all plays $\rho\in\operatorname{Plays}_{X}(v)$, we say that $\rho=\rho_{0}\rho_{1}\ldots$ is $\lambda$-consistent if for all $n\in\mathbb{N}$ and $i\in\Pi$ such that $\rho_{n}\in V^{X}_{i}$:

[TABLE]

We denote by $\Lambda(v)$ the set of plays $\rho\in\operatorname{Plays}_{X}(v)$ that are $\lambda$-consistent.

Thus, a play $\rho$ is $\lambda$-consistent if for all its suffixes $\rho_{\geq n}$, if player $i$ owns $\rho_{n}$ then the number of edges to reach his target set $F^{X}_{i}$ along $\rho_{\geq n}$ is upper bounded by $\lambda(\rho_{n})$. Before going into the details of our algorithm, let us intuitively explain on an example how a well-chosen labeling function characterizes the set of SPE outcomes.

{exa}

We consider the initialized extended game $(\operatorname{\mathcal{X}},x_{0})$ of Figure 2, and a labeling function $\lambda$ whose values are indicated under each vertex.

If $v\in V^{X}_{i}$ is labeled by $\lambda(v)=c$, then if $c\in\mathbb{N}_{0}$, this means that player $i$ will only accept outcomes in $(\operatorname{\mathcal{X}},v)$ that reach his target set within $c$ steps, otherwise he would have a profitable deviation. If $\lambda(v)=0$, this means that player $i$ has already reached his target set (that is, $i\in I(v)$), and if $\lambda(v)=+\infty$, player $i$ has no profitable deviation whatever outcome is proposed to him.

In Example 1.3 was given the SPE outcome equal to

[TABLE]

and with cost $(4,4)$. We have $\lambda(v_{0},\emptyset)=4$ and player $2$ reaches his target set from $(v_{0},\emptyset)$ within exactly $4$ steps. For all vertices $v$ of the ending cycle of $\rho$, we have $\lambda(v)=0$ since both players belong to $I(v)=\Pi$. The constraints imposed by $\lambda$ on the other vertices of $\rho$ are respected too.

Recall now the strategy profile $\sigma^{\prime}$ with outcome $\rho^{\prime}={((v_{0},\emptyset)(v_{4},\emptyset))}^{\omega}$ described in Example 1.2. The outcome $\rho^{\prime}$ is not $\lambda$-consistent since player $2$ does not reach his target set, and so in particular does not reach it within $4$ steps. We already know that $\sigma^{\prime}$ is not an SPE from Example 1.2. In fact all the profiles that yield $\rho^{\prime}$ as an outcome are not SPEs.∎

Our algorithm roughly works as follows: the labeling function $\lambda$ that characterizes the set of SPE outcomes is obtained from an initial labeling function that imposes no constraints, by iterating an operator that reinforces the constraints step after step, up to obtaining a fixpoint which is the required function $\lambda$. Thus, if $\lambda^{k}$ is the labeling function computed at step $k$ and $\Lambda^{k}(v)$, $v\in V^{X}$, the related sets of $\lambda^{k}$-consistent plays beginning in $v$, initially we have $\Lambda^{0}(v)=\operatorname{Plays}_{X}(v)$, and step by step, the constraints imposed by $\lambda^{k}$ become stronger and the sets $\Lambda^{k}(v)$ become smaller, until a fixpoint is reached.

Initially, we want a labeling function $\lambda^{0}$ that imposes no constraint on the plays. We could define $\lambda^{0}$ as the constant function $+\infty$. We proceed a little bit differently. Indeed recall the definition of the target sets ${(F^{X}_{i})}_{i\in\Pi}$ in an extended game (see Definition 1.3): $v\in F^{X}_{i}$ if and only if $i\in I(v)$. Hence, given $\rho=\rho_{0}\rho_{1}\ldots$, once $\rho_{k}\in F^{X}_{i}$ for some $k\in\mathbb{N}$ then $\rho_{n}\in F^{X}_{i}$ for all $n\geq k$. It follows that for all $n\geq k$, $\operatorname{Cost}_{i}(\rho_{\geq n})=0$ and Inequality (4) is trivially true. (See also Example 2.) Therefore we define the labeling function $\lambda^{0}$ as follows.

{defi}

[Initial labeling] For all $v\in V^{X}$, let $i\in\Pi$ be such that $v\in V^{X}_{i}$,

[TABLE]

Lemma 4**.**

$\rho\in\Lambda_{0}(v)$* if and only if $\rho\in\operatorname{Plays}_{X}(v)$.*

Let us now explain how our algorithm computes the labeling functions $\lambda^{k}$, $k\geq 1$, and the related sets $\Lambda^{k}(v)$, $v\in V^{X}$. It works in a bottom-up manner, according to the total order $J_{1}<J_{2}<\cdots<J_{N}$ of $\mathcal{I}$ given in (3): it first iteratively updates the labeling function for all vertices $v$ of the arena $X^{J_{N}}$ until reaching a fixpoint in this arena, it then repeats this procedure in $X^{\geq J_{N-1}}$, $X^{\geq J_{N-2}}$, $\ldots$, $X^{\geq J_{1}}=X$. Hence, suppose that we currently treat the arena $X^{\geq J_{n}}$ and that we want to compute $\lambda^{k+1}$ from $\lambda^{k}$. We define the updated function $\lambda^{k+1}$ as follows (we use the convention that $1+(+\infty)=+\infty$).

{defi}

[Labeling update] Let $k\geq 0$ and suppose that we treat the arena $X^{\geq J_{n}}$, with $n\in\{1,\ldots,N\}$. For all $v\in V^{X}$,

• •

if $v\in V^{\geq J_{n}}$, let $i\in\Pi$ be such that $v\in V^{X}_{i}$, then

[TABLE]

• •

if $v\not\in V^{\geq J_{n}}$, then

[TABLE]

Let us provide some explanations. As this update concerns the arena $X^{\geq J_{n}}$, we keep $\lambda^{k+1}=\lambda^{k}$ outside of this arena. Suppose now that $v$ belongs to $X^{\geq J_{n}}$ and let $i$ be such that $v\in V^{X}_{i}$. We define $\lambda^{k+1}(v)=0$ whenever $i\in I(v)$ (as already explained for the definition of $\lambda^{0}$). When it is updated, the value $\lambda^{k+1}(v)$ represents what is the best cost that player $i$ can ensure for himself from $v$ with a “one-shot” choice by only taking into account plays of $\Lambda^{k}(v^{\prime})$ with $v^{\prime}\in\operatorname{Succ}(v)$.

Notice that it makes sense to run the algorithm in a bottom-up fashion according to the total ordering $J_{1}<\cdots<J_{N}$ since given a play $\rho=\rho_{0}\rho_{1}\ldots$, if $\rho_{0}$ is a vertex of $V^{\geq J_{n}}$, then for all $k\in\mathbb{N}$, $\rho_{k}$ is a vertex of $V^{\geq J_{n}}$ (by $I$-monotonicity). Moreover running the algorithm in this way is essential to prove that the constraint problem for reachability games is in PSPACE.

{exa}

We consider again the extended game $(\operatorname{\mathcal{X}},x_{0})$ of Figure 2 with the total order $J_{1}=\emptyset<J_{2}=\{2\}<J_{3}=J_{N}=\Pi$ of its set $\mathcal{I}$.

Let us illustrate Definition 4 on the arena $X^{\geq J_{2}}$. Let $k\geq 0$ and suppose that the labeling function $\lambda^{k}$ has been computed such that $\lambda^{k}(v_{0},J_{2})=0$, $\lambda^{k}(v,J_{2})=+\infty$ for every other vertex in region $X^{J_{2}}$ (notice that $\lambda^{k}$ is not the labeling function indicated in Figure 2). Let us show how to compute $\lambda^{k+1}(v_{1},J_{2})$. We need to compute $\sup\{\operatorname{Cost}_{1}(\rho)\mid\rho\in\Lambda^{k}(v^{\prime})\}$ for the two successors $v^{\prime}$ of $(v_{1},J_{2})$, that is, respectively $v^{\prime}=(v_{3},J_{2})$ and $v^{\prime}=(v_{6},J_{2})$. Recall that $\Lambda^{k}(v^{\prime})$ is the set of all plays $\lambda^{k}$-consistent from $v^{\prime}$. All the plays in $\Lambda^{k}(v_{6},J_{2})$ have cost $2$ for player $1$ and player $2$: indeed, they all first follow the history $(v_{6},J_{2}),(v_{7},J_{2}),(v_{2},J_{N})$. Thus, $\sup\{\operatorname{Cost}_{1}(\rho)\mid\rho\in\Lambda^{k}(v_{6},J_{2})\}=2$. On the other hand, as $\lambda^{k}(v_{3},J_{2})=+\infty$, the play $(v_{3},J_{2})(v_{0},J_{2}){(v_{4},J_{2})}^{\omega}$ is $\lambda^{k}$-consistent and belongs to $\Lambda^{k}(v_{3},J_{2})$. Thus, $\sup\{\operatorname{Cost}_{1}(\rho)\mid\rho\in\Lambda^{k}(v_{3},J_{2})\}=+\infty$. Hence, the minimum is attained with successor $(v_{6},J_{2})$, and $\lambda^{k+1}(v_{1},J_{2})=3$. ∎

We can now provide our algorithm (see Algorithm 1) that computes the sequence ${(\lambda^{k}(v))}_{k\in\mathbb{N}}$ until a fixpoint is reached (see Proposition 5 below). Initially, the labeling function is $\lambda^{0}$ (see Definition 2). For the next steps $k>0$, we begin with the bottom region $X^{J_{N}}$ of $\operatorname{\mathcal{X}}$ and update $\lambda^{k-1}$ to $\lambda^{k}$ as described in Definition 4. At some point, the values of $\lambda^{k}$ do not change anymore in $X^{J_{N}}$ and ${(\lambda^{k})}_{k\in\mathbb{N}}$ reaches locally (on $X^{J_{N}}$) a fixpoint (see again Proposition 5). Now, we consider the arena $X^{\geq J_{N-1}}$ and in the same way, we continue to update locally the values of $\lambda^{k}$ in $X^{\geq J_{N-1}}$. We repeat this procedure with arenas $X^{\geq J_{N-2}}$, $X^{\geq J_{N-3}}$, … until the arena $X^{\geq J_{1}}=X$ is completely processed. From the last computed $\lambda^{k}$, we derive the sets $\Lambda^{k}(v)$, $v\in V^{X}$, that we need for the characterization of outcomes of SPEs (see Theorem 8 below). An example illustrating the execution of this algorithm is given at the end of this section.

We now state that the sequence ${(\lambda^{k})}_{k\in\mathbb{N}}$ computed by this algorithm reaches a fixpoint — locally on each arena $X^{\geq J_{n}}$ and globally on $X$ — in the following meaning:

Proposition 5**.**

There exists a sequence of integers $0=k_{N}^{*}<k_{N-1}^{*}<\cdots<k_{1}^{*}=k^{*}$ such that

• •

Local fixpoint:* for all $J_{n}\in\mathcal{I}$, all $m\in\mathbb{N}$ and all $v\in V^{\geq J_{n}}$,*

[TABLE]

• •

Global fixpoint*: in particular, with $k^{*}=k_{1}^{*}$, for all $m\in\mathbb{N}$ and all $v\in V^{X}$,*

[TABLE]

The global fixpoint $\lambda^{k^{*}}$ is also simply denoted by $\lambda^{*}$, and each set $\Lambda^{k^{*}}(v),v\in V^{X}$, is denoted by $\Lambda^{*}(v)$.

Before proving Proposition 5, let us make some comments. This proposition indicates that Algorithm 1 terminates. Indeed for each $J_{n}\in\mathcal{I}$, taking the least index $k^{*}_{n}$ which makes Equality (5) true shows that the repeat loop is broken and the variable $n$ decremented by $1$. The value $n=0$ is eventually reached and the algorithm stops with the global fixpoint $\lambda^{*}$. Notice that the first local fixpoint is reached with $k_{N}^{*}=0$ because $X^{J_{N}}$ is a bottom region. To prove that the algorithm stops in a finite number of steps, we show that each region requires a finite number of steps to be treated. To do so, we rely on the fact that constraint values on vertices cannot increase from one step to another and that the set of constraint values can be seen as a well-quasi ordering. Thus a decreasing sequence in this set is stationary, and this means our algorithm reaches a fixpoint and terminates.

Proposition 5 also shows that when a local fixpoint is reached in the arena $X^{\geq J_{n+1}}$ and the algorithm updates the labeling function $\lambda^{k}$ in the arena $X^{\geq J_{n}}$, the values of $\lambda^{k}(v)$ do not change anymore for any $v\in V^{\geq J_{n+1}}$ but can still be modified for some $v\in V^{J_{n}}$. Recall also that outside of $X^{\geq J_{n}}$, the values of $\lambda^{k}(v)$ are still equal to the initial values $\lambda^{0}(v)$. These properties will be useful when we will prove that the constraint problem for reachability games is in PSPACE. They are summarized in the next lemma.

Lemma 6**.**

Let $k\in\mathbb{N}$ be a step of the algorithm and let $J_{n}$ with $n\in\{1,\ldots,N\}$. For all $v\in V^{J_{n}}$:

• •

if $k\leq k^{*}_{n+1}$, then $\lambda^{k+1}(v)=\lambda^{k}(v)=\lambda^{0}(v)$,

• •

if $k^{*}_{n}\leq k$, then $\lambda^{k+1}(v)=\lambda^{k}(v)=\lambda^{k^{*}_{n}}(v)$,

Hence the values of $\lambda^{k}(v)$ and $\lambda^{k+1}(v)$ may be different only when $k^{*}_{n+1}<k<k^{*}_{n}$. ∎

To prove Proposition 5, we have to prove that the sequences ${(\lambda^{k}(v))}_{k\in\mathbb{N}}$, with $v\in V^{X}$, are non increasing.

Lemma 7**.**

For all $v\in V^{X}$, the sequences ${(\lambda^{k}(v))}_{k\in\mathbb{N}}$ and ${(\Lambda^{k}(v))}_{k\in\mathbb{N}}$ are non increasing.

Proof 2.1**.**

Let us prove by induction on $k$ that for all $v\in V^{X}$

[TABLE]

We will get that $\Lambda^{k+1}(v)\subseteq\Lambda^{k}(v)$ by Definition 2.

First, recall that $\lambda^{k}(v)=0$ if and only if $i\in I(v)$, where $i$ is the player owning $v$. So, in this case, $\lambda^{k+1}(v)=\lambda^{k}(v)=0$ and assertion (6) is proved. It remains to prove this assertion when $i\not\in I(v)$.

For $k=0$, let $v\in V^{X}_{i}$ such that $i\not\in I(v)$, then $\lambda^{0}(v)=+\infty$ and obviously $\lambda^{1}(v)\leq\lambda^{0}(v)$.

Suppose that assertion (6) is true for $k$ and let us prove it for $k+1$. We know by induction hypothesis that for all $v^{\prime}\in V^{X}$, $\lambda^{k+1}(v^{\prime})\leq\lambda^{k}(v^{\prime})$, and thus also

[TABLE]

Let us prove that for all $v\in V^{X}_{i}$ such that $i\not\in I(v)$, $\lambda^{k+2}(v)\leq\lambda^{k+1}(v)$. If $\lambda^{k+2}(v)=\lambda^{k+1}(v)$ or $\lambda^{k+1}(v)=+\infty$, then the assertion is proved. Otherwise,

[TABLE]

By (7), it follows that

[TABLE]

And so, the assertion again holds.

We can now prove Proposition 5.

Proof 2.2** (Proof of Proposition 5).**

The base case is easily proved. Indeed, as $V^{J_{N}}$ is a bottom region, we have $\lambda_{1}(v)=\lambda_{0}(v)$ for all $v\in V^{J_{N}}$, and thus the local fixpoint is immediately reached on $V^{J_{N}}$. Hence with $k_{N}^{*}=0$, for all $m\in\mathbb{N}$ and all $v\in V^{J_{N}}$, $\lambda^{k_{N}^{*}+m}(v)=\lambda^{k_{N}^{*}}(v)$.

Let $J_{n}$ be an element of $\mathcal{I}$, with $n\in\{1,\ldots,N-1\}$. Suppose that a fixpoint has been reached in the arena $X^{\geq J_{n+1}}$ and that the labeling function $\lambda^{k}$ is udpated on the arena $X^{\geq J_{n}}$ as described in Definition 4. Recall (as already summarized in Lemma 6) that the previously computed values of $\lambda^{k}$ do no longer change on $X^{\geq J_{n+1}}$ (a local fixpoint is reached) and they do not change outside of $V^{\geq J_{n}}$ (by construction). However they can be modified on $X^{J_{n}}$. In this region $X^{J_{n}}$, there are $|V|$ sequences ${(\lambda^{k}(v))}_{k\in\mathbb{N}}$, $v\in V^{J_{n}}$, since the vertices $v$ are of the form $v=(u,J_{n})$ where $J_{n}$ is fixed. These sequences are non increasing by Lemma 7. As the component-wise ordering over ${(\mathbb{N}\cup\{+\infty\})}^{|V|}$ is a well-quasi-ordering, there exists a natural number $k^{*}_{n}$ that we choose as small as possible such that for all $v\in V^{J_{n}}$, $\lambda^{k_{n}^{*}+1}(v)=\lambda^{k_{n}^{*}}(v)$. This equality also holds for all $v\in V^{\geq J_{n}}$ (and not only for $V^{J_{n}}$), and it follows that for all $m\in\mathbb{N}$ and all $v\in V^{\geq J_{n}}$, $\lambda^{k_{n}^{*}+m}(v)=\lambda^{k_{n}^{*}}(v)$.

Notice that when $n$ is decremented in Algorithm 1, $k$ is incremented at least once showing that the sequence $0<k_{N}^{*}<k_{N-1}^{*}<\cdots<k_{1}^{*}=k^{*}$ is strictly increasing.

Finally, the last arena processed by the algorithm is $X^{\geq J_{1}}=X$. So with $k^{*}=k^{*}_{1}$, we have that for all $v\in V$ and all $m\in\mathbb{N}$, $\lambda^{k^{*}+m}(v)=\lambda^{k^{*}}(v)$.

We are ready to state how we characterize plays that are outcomes of SPEs. This is possible with the global fixpoint computed by Algorithm 1.

Theorem 8** (Characterization).**

Let $(\mathcal{G},v_{0})$ be an initialized quantitative game and $(\operatorname{\mathcal{X}},x_{0})$ be its initialized extended game. Let $\rho^{0}$ be a play in $\operatorname{Plays}_{X}(x_{0})$. Then $\rho^{0}$ is the outcome of an SPE in $(\operatorname{\mathcal{X}},x_{0})$ if and only if $\rho^{0}\in\Lambda^{*}(x_{0})$.

Notice that this theorem also provides a characterization of the outcomes of SPEs in $(\mathcal{G},v_{0})$ by Lemma 2.

The two implications of Theorem 8 respectively follow from Proposition 11 and Proposition 12 given below. We first need to establish an important property satisfied by the sets $\Lambda^{k}(v)$: when for some player $i$, the costs $\operatorname{Cost}_{i}(\rho)$ associated with the plays $\rho$ in $\Lambda^{k}(v)$ are unbounded, there actually exists some play in this set that has an infinite cost. In other terms, either $\Lambda^{k}(v)$ contains at least one play $\rho$ with an infinite cost $\operatorname{Cost}_{i}(\rho)$ or there exists a constant $c\in\mathbb{N}$ such that $\operatorname{Cost}_{i}(\rho)\leq c$ for all $\rho\in\Lambda^{k}(v)$.

Proposition 9**.**

For every $k\in\mathbb{N}$, for every $v\in V^{X}$ and for every $i\in\Pi$, the following implication holds: if $\sup\{\operatorname{Cost}_{i}(\rho)\mid\rho\in\Lambda^{k}(v)\}=+\infty$, then there exists a play $\rho\in\Lambda^{k}(v)$ such that $\operatorname{Cost}_{i}(\rho)=+\infty$.

Proof 2.3**.**

We assume that $\sup\{\operatorname{Cost}_{i}(\rho)\mid\rho\in\Lambda^{k}(v)\}=+\infty$, that is, for all $n\in\mathbb{N}$, there exists $\rho^{n}\in\Lambda^{k}(v)$ such that $\operatorname{Cost}_{i}(\rho^{n})>n$. By König’s lemma, there exist ${(\rho^{n_{\ell}})}_{\ell\in\mathbb{N}}$ a subsequence of ${(\rho^{n})}_{n\in\mathbb{N}}$ and $\rho\in\operatorname{Plays}_{X}(v)$ such that $\rho=\lim_{\ell\rightarrow+\infty}\rho^{n_{\ell}}$. Moreover, $\operatorname{Cost}_{i}(\rho)=+\infty$ as $\operatorname{Cost}_{i}$ can be transformed into a continuous function ([BBDG12], see also (1), page 1). Let us prove that

[TABLE]

This will establish Proposition 9.

We prove by induction on $t$ with $0\leq t\leq k$ that $\rho\in\Lambda^{t}(v)$. If $t=0$, then $\Lambda^{0}(v)=\operatorname{Plays}_{X}(v)$ by Lemma 4. As $\rho=\lim_{\ell\rightarrow+\infty}\rho^{n_{\ell}}\in\operatorname{Plays}_{X}(v)$, it follows that $\rho\in\Lambda^{0}(v)$.

Let $t>0$ and assume that the assertion is true for $t-1<k$. Suppose by contradiction that $\rho\not\in\Lambda^{t}(v)$. For all $\ell\in\mathbb{N}$, as $\rho^{n_{\ell}}\in\Lambda^{k}(v)$, we have $\rho^{n_{\ell}}\in\Lambda^{t}(v)$ by Lemma 7. Moreover by induction hypothesis we have $\rho\in\Lambda^{t-1}(v)$. From $\rho\in\Lambda^{t-1}(v)\setminus\Lambda^{t}(v)$, it follows that there exists $m\in\mathbb{N}$ and $j\in\Pi$ with $\rho_{m}\in V_{j}$ such that

[TABLE]

In particular, $\lambda^{t}(\rho_{m})<\lambda^{t-1}(\rho_{m})$ and thus $\lambda^{t}(\rho_{m})<+\infty$, and player $j$ does not reach his target set along $\pi=\rho_{0}\ldots\rho_{m}\ldots\rho_{m+\lambda^{t}(\rho_{m})}$. We choose $n_{\ell}$ large enough such that $\rho$ and $\rho^{n_{\ell}}$ share a common prefix of length at least $|\pi|$. As $\operatorname{Cost}_{j}(\rho_{\geq m})>\lambda^{t}(\rho_{m})$, it follows that $\operatorname{Cost}_{j}(\rho^{\ell_{n}}_{\geq m})>\lambda^{t}(\rho_{m})$. We can conclude that $\rho^{n_{\ell}}\not\in\Lambda^{t}(v)$ which leads to a contradiction.

The next corollary is a direct consequence of Proposition 9 with the convention that the max belongs to $\mathbb{N}\cup\{+\infty\}$.

Corollary 10**.**

$\sup\{\operatorname{Cost}_{i}(\rho)\mid\rho\in\Lambda^{k}(v)\}=\max\{\operatorname{Cost}_{i}(\rho)\mid\rho\in\Lambda^{k}(v)\}$.

The two implications of Theorem 8 are proved in the following Propositions 11 and 12. Notice that in Proposition 11, we derive the additional property that $\Lambda^{*}(v)\neq\emptyset$, for all $v\in\operatorname{Succ}^{*}(x_{0})$. This is necessary to prove Proposition 12.

Proposition 11**.**

If $\sigma$ is an SPE in $(\operatorname{\mathcal{X}},x_{0})$ then for all $v\in\operatorname{Succ}^{*}(x_{0})$, $\Lambda^{*}(v)\neq\emptyset$ and $\langle\sigma\rangle_{x_{0}}\in\Lambda^{*}(x_{0})$.

Proof 2.4**.**

Suppose that $\sigma$ is an SPE in $(\operatorname{\mathcal{X}},x_{0})$ and let us prove by induction on $k$ that for all $k\in\mathbb{N}$ and all $hv\in\operatorname{Hist}_{X}(x_{0})$,

[TABLE]

For case $k=0$, this is true by definition of $\Lambda^{0}(v)$ and Lemma 4.

Suppose that this assertion is satisfied for $k\geq 0$ and by contradiction, assume that there exists $hv\in\operatorname{Hist}_{X}(x_{0})$ such that $\langle\sigma_{\restriction h}\rangle_{v}\not\in\Lambda^{k+1}(v)$. Let $\rho=\langle\sigma_{\restriction h}\rangle_{v}$, by Definition 2, it means that there exist $n\in\mathbb{N}$ and $i\in\Pi$ such that $\rho_{n}\in V_{i}$ and

[TABLE]

But by induction hypothesis, we know that

[TABLE]

It follows by (8) and (9) that $\lambda^{k+1}(\rho_{n})<\lambda^{k}(\rho_{n})$ and that

[TABLE]

In regards of Definition 4, these three relations allow us to conclude that

[TABLE]

Let $v^{\prime}\in V$ be such that

[TABLE]

Let $h^{\prime}=h\rho_{0}\ldots\rho_{n-1}\in\operatorname{Hist}_{X}(x_{0})$, and let us define the one-shot deviating strategy $\tau_{i}$ from $\sigma_{i\restriction h^{\prime}}$ such that $\tau_{i}(\rho_{n})=v^{\prime}$. Let us prove that $\tau_{i}$ is a one-shot profitable deviation for player $i$ in $(\operatorname{\mathcal{X}}_{\restriction h^{\prime}},\rho_{n})$.

[TABLE]

This proves that $\sigma$ is not a very weak SPE and so not an SPE by Proposition 1.3, which is a contradiction. This concludes the proof.

Proposition 12**.**

Let $\rho^{0}\in\Lambda^{*}(x_{0})$, then $\rho^{0}$ is the outcome of an SPE in $(\operatorname{\mathcal{X}},x_{0})$.

Proof 2.5**.**

By Theorem 1.2, there exists an SPE in $(\operatorname{\mathcal{X}},x_{0})$ and thus, by Proposition 11:

[TABLE]

Let $\rho^{0}\in\Lambda^{*}(x_{0})$ and let us show how to construct a very weak SPE $\sigma$ (and so an SPE by Proposition 1.3) with outcome $\rho^{0}$ in $(\operatorname{\mathcal{X}},x_{0})$. We define $\sigma$ step by step by induction on the subgames of $(\operatorname{\mathcal{X}},x_{0})$. We first partially build $\sigma$ such as it produces $\rho^{0}$, i.e., $\langle\sigma\rangle_{x_{0}}=\rho^{0}$. Now, we define a set of plays which is useful to define $\sigma$ in the subgames. For all $(i,v^{\prime})$ such that $(v,v^{\prime})\in E^{X}$ with $v,v^{\prime}\in\operatorname{Succ}^{*}(x_{0})$ and $v\in V^{X}_{i}$, we take $\rho_{i,v^{\prime}}\in\Lambda^{*}(v^{\prime})$ such that:

[TABLE]

Notice that such a play exists by (11) and Corollary 10. The construction of $\sigma$ is done by induction as follows. Consider $hvv^{\prime}\in\operatorname{Hist}_{X}(x_{0})$ with $v\in V^{X}_{i}$ such that $\langle\sigma_{\restriction h}\rangle_{v}$ is already defined but not yet $\langle\sigma_{\restriction hv}\rangle_{v^{\prime}}$. We extend the definition of $\sigma$ as follows:

[TABLE]

Let us prove that $\sigma$ is a very weak SPE. Consider the subgame $(\operatorname{\mathcal{X}}_{\restriction h},v)$ for a given $hv\in\operatorname{Hist}_{X}(x_{0})$ with $v\in V^{X}_{i}$ and the one-shot deviating strategy $\sigma^{\prime}_{i}$ from $\sigma_{i|h}$ such that $\sigma^{\prime}_{i}(v)=v^{\prime}$. By construction, there exists $\rho_{j,u}$ and $\rho_{i,v^{\prime}}$ as defined previously and $g\in\operatorname{Hist}_{X}(x_{0})$ such that $h\langle\sigma_{\restriction h}\rangle_{v}=g\rho_{j,u}$ and $\langle\sigma_{\restriction hv}\rangle_{v^{\prime}}=\rho_{i,v^{\prime}}$.

We prove that $\sigma^{\prime}_{i}$ is not a one-shot profitable deviation by proving that $\operatorname{Cost}_{i}(h\langle\sigma_{\restriction h}\rangle_{v})\leq\operatorname{Cost}_{i}(hv\langle\sigma_{\restriction hv}\rangle_{v^{\prime}})$. If $i\in I(v)$, then obviously $\operatorname{Cost}_{i}(h\langle\sigma_{\restriction h}\rangle_{v})=\operatorname{Cost}_{i}(hv\langle\sigma_{\restriction hv}\rangle_{v^{\prime}})$. Otherwise $i\not\in I(v)$. We have that $\rho=\langle\sigma_{\restriction h}\rangle_{v}$ is suffix of $\rho_{j,u}$, that is, $\rho=\rho_{j,u,\geq n}$ for some $n\in\mathbb{N}$ and that $\rho_{j,u}\in\Lambda^{*}(u)=\Lambda^{k^{*}}(u)=\Lambda^{k^{*}+1}(u)$ (by (12) and the fixpoint). It follows that:

[TABLE]

Thus we have that

[TABLE]

This concludes the proof.

{exa}

Let us come back to the running example of Figure 2 and illustrate Proposition 5. The different steps of Algorithm 1 are given in Table 1. The columns indicate the vertices according to their region, respectively $\Pi$, $\{2\}$, and $\emptyset$. Notice that for the region $\Pi$, we only write one column $v$ as for all vertices $(v,\Pi)$ the value of $\lambda$ is equal to 0 all along the algorithm.

Recall that $J_{1}=\emptyset<J_{2}=\{2\}<J_{3}=\Pi=\{1,2\}$. The algorithm begins with the arena $X^{J_{3}}$. A local fixpoint ($\lambda^{1}=\lambda^{0}$) is immediately reached because all vertices belong to the target set of both players in $X^{J_{3}}$. Thus the first local fixpoint is reached with $k_{3}^{*}=0$.

The algorithm then treats the arena $X^{\geq J_{2}}$. By Lemma 6, it is enough to consider the region $X^{J_{2}}$. Let us explain how to compute $\lambda^{2}(v)$ from $\lambda^{1}(v)$ on this region. For $v=(v_{7},\{2\})$, we have that $\lambda^{2}(v)=1+\min_{(v,v^{\prime})\in E^{X}}\sup\{\operatorname{Cost}_{1}(\rho)\mid\rho\in\Lambda^{1}(v^{\prime})\}$. As the unique successor of $v$ is $(v_{2},\{1,2\})$, all $\lambda^{1}$-consistent plays beginning in this successor have cost [math] for player $1$. So, we have that $\lambda^{2}(v)=1$. For the computation of $\lambda^{2}(v_{6},\{2\})$, the same argument holds since $(v_{6},\{2\})$ has the unique successor $(v_{7},\{2\})$. The vertex $(v_{1},\{2\})$ has two successors: $(v_{6},\{2\})$ and $(v_{3},\{2\})$.444The computation of $\lambda^{2}(v_{1},\{2\})$ was already explained in Example 2. Again, we know that all $\lambda^{1}$-consistent plays beginning in $(v_{6},\{2\})$ have cost $2$ for player $1$. From $(v_{3},\{2\})$ however, one can easily check that the play $(v_{3},\{2\})(v_{0},\{2\}){((v_{4},\{2\}))}^{\omega}$ is $\lambda^{1}$-consistent and has cost $+\infty$ for player 1. Thus, we obtain that $\lambda^{2}(v_{1},\{2\})=3$. For the other vertices of $X^{J_{2}}$, one can see that $\lambda^{2}(v)=\lambda^{1}(v)$.

Finally, we can check that the local fixed point is reached in the arena $X^{\geq J_{2}}$ (resp. $X^{\geq J_{1}}$) with $\lambda^{3}=\lambda^{2}$ (resp. $\lambda^{6}=\lambda^{5}=\lambda^{*}$). Therefore the respective fixpoints are reached with $k^{*}_{2}=2$ and $k^{*}_{1}=5$. The labeling function indicated in Figure 2 is the one of $\lambda^{*}$. ∎

3. Counter graph

In the previous section, we have introduced the concept of labeling function $\lambda$ and the constraints that it imposes on plays. We have also proposed an algorithm that computes a sequence of labeling functions ${(\lambda^{k})}_{k\in\mathbb{N}}$ until reaching a fixpoint $\lambda^{*}$ such that the plays that are $\lambda^{*}$-consistent are exactly the SPE outcomes. In this section, given a labeling function $\lambda$, we introduce the concept of counter graph such that its infinite paths coincide with the plays that are $\lambda$-consistent. We then show that the counter graph associated with the fixpoint function $\lambda^{*}$ has an exponential size, an essential step to prove PSPACE membership of the constraint problem.

For the entire section, we fix a reachability game $\mathcal{G}=(G,{(F_{i})}_{i\in\Pi},{(\operatorname{Cost}_{i})}_{i\in\Pi})$ with an arena $G=(\Pi,V,{(V_{i})}_{i\in\Pi},E)$, and $v_{0}$ an initial vertex. Let $\operatorname{\mathcal{X}}=(X,{(F^{X}_{i})}_{i\in\Pi},{(\operatorname{Cost}_{i})}_{i\in\Pi})$ with the arena $X=(\Pi,V^{X},{(V^{X}_{i})}_{i\in\Pi},E^{X})$ be its associated extended game. Furthermore, when we speak about a play $\rho$ we always mean a play in the extended game $\operatorname{\mathcal{X}}$.

A labeling function $\lambda$ give constraints on costs of plays from each vertex in $X$, albeit only for the player that owns this vertex. However, by the property of $\lambda$-consistence, constraints for a player carry over all the successive vertices, whether they belong to him or not. In order to check efficiently this property, we introduce the counter graph to keep track explicitly of the accumulation of constraints for all players at each step of a play. Let us first fix some notation.

{defi}

[Restriction and maximal finite range] Let $\lambda:V^{X}\rightarrow\mathbb{N}\cup\{+\infty\}$ be a labeling function.

• •

We consider restrictions of $\lambda$ to sub-arenas of $V^{X}$ as follows. Let $n\in\{1,\ldots,N\}$, we denote by $\lambda_{n}:V^{J_{n}}\rightarrow\mathbb{N}\cup\{+\infty\}$ the restriction of $\lambda$ to $V^{J_{n}}$. Similarly we denote by $\lambda_{\geq n}$ (resp. $\lambda_{>n}$) the restriction of $\lambda$ to $V^{\geq J_{n}}$ (resp. $V^{>J_{n}}$).

• •

The maximal finite range of $\lambda$, denoted by $\mathrm{mR}(\lambda)$, is equal to

[TABLE]

with the convention that $\mathrm{mR}(\lambda)=0$ if $\lambda$ is the constant function $+\infty$. We also extend this notion to restrictions of $\lambda$ with the convention that $\mathrm{mR}(\lambda_{>n})=0$ if $J_{n}$ is a bottom region.

Notice that in the definition of maximal finite range, we only consider the finite values of $\lambda$ (and not the value $+\infty$).

{defi}

[Counter Graph] Let $\lambda:V^{X}\to\mathbb{N}\cup\{+\infty\}$ be a labeling function. Let $\mathcal{K}:=\{0,\dots,K\}\cup\{+\infty\}$ with $K=\mathrm{mR}(\lambda){}{}$. The counter graph $\mathbb{C}(\lambda)$ for $\mathcal{G}$ and $\lambda$ is equal to $\mathbb{C}(\lambda)=(\Pi,V^{C},{(V^{C}_{i})}_{i\in\Pi},E^{C})$, such that:

• •

$V^{C}=V^{X}\times\mathcal{K}^{|\Pi|}$

• •

$(v,{(c_{i})}_{i\in\Pi})\in V^{C}_{j}$ if and only if $v\in V^{X}_{j}$

• •

$((v,{(c_{i})}_{i\in\Pi}),(v^{\prime},{(c^{\prime}_{i})}_{i\in\Pi}))\in E^{C}$ if and only if:

• –

$(v,v^{\prime})\in E^{X}$, and

• –

for every $i\in\Pi$

[TABLE]

Intuitively, the counter graph is constructed such that once a value $\lambda(v)$ is finite for a vertex $v\in V^{X}_{i}$ along a play in $\operatorname{\mathcal{X}}$, the corresponding path in $\mathbb{C}(\lambda)$ keeps track of the induced constraint by (i) decrementing the counter value $c_{i}$ for the concerned player $i$ by $1$ at every step, (ii) updating this counter if a stronger constraint for player $i$ is encountered by visiting a vertex $v^{\prime}$ with a smaller value $\lambda(v^{\prime})$, and (iii) setting the counter $c_{i}$ to [math] if player $i$ has reached his target set.

Note that in the counter graph, there may be some vertices with no outgoing edges. Indeed, consider a vertex $(v,{(c_{i})}_{i\in\Pi})\in V^{C}$ such that $c_{j}=1$ for some player $j$. By construction of $\mathbb{C}(\lambda)$, the only outgoing edges from $(v,{(c_{i})}_{i\in\Pi})$ must link to vertices $(v^{\prime},{(c^{\prime}_{i})}_{i\in\Pi})$ such that $(v,v^{\prime})\in E^{X}$, $c^{\prime}_{j}=0$ and $j\in I(v^{\prime})$ (as in Definition 3 the two other cases require that $c_{j}>1$). However, it may be the case that no successor $v^{\prime}$ of $v$ in $X$ is such that $j\in I(v^{\prime})$.

Note as well that for each vertex $v\in V^{X}$, there exist many different vertices $(v,{(c_{i})}_{i\in\Pi})$ in $\mathbb{C}(\lambda)$, one for each counter values profile. However, the intended goal of the counter graph is to monitor explicitly the constraints accumulated by each player along a play in $\operatorname{\mathcal{X}}$ regarding the function $\lambda$. Thus, we will only consider paths in $\mathbb{C}(\lambda)$ that start in vertices $(v,{(c_{i})}_{i\in\Pi})$ such that the counter values correspond indeed to the constraint at the beginning of a play in $\operatorname{\mathcal{X}}$ regarding $\lambda$:

{defi}

[Starting vertex in $\mathbb{C}(\lambda)$] Let $v\in V^{X}$. We distinguish one vertex $v^{C}=(v,{(c_{i})}_{i\in\Pi})$ in $V^{C}$, such that for every $i\in\Pi$:

[TABLE]

We call $v^{C}$ the starting vertex associated with $v$, and denote by $\mathrm{SV}(\lambda)$ the set of all starting vertices in $\mathbb{C}(\lambda)$.

{exa}

Recall the extended game $(\operatorname{\mathcal{X}},x_{0})$ of Figure 2, and the labeling function $\lambda$ whose values are indicated under each vertex. In Figure 3, we illustrate a part of the counter graph $\mathbb{C}(\lambda)$. In Example 2, we have shown that the play

[TABLE]

was $\lambda$-consistent. Let us show that there is a corresponding infinite path $\pi$ that starts in ${(v_{0},\emptyset)}^{C}=(v_{0},\emptyset,(+\infty,4))$ in $\mathbb{C}(\lambda)$. Following Definition 3, we see that in $\mathbb{C}(\lambda)$, there exists an edge between $(v_{0},\emptyset,(+\infty,4))$ and $(v_{1},\emptyset,(3,3))$ and that

[TABLE]

with

[TABLE]

Come back now to the play $\rho^{\prime}={((v_{0},\emptyset)(v_{4},\emptyset))}^{\omega}$ described in Example 2, which is not $\lambda$-consistent. From ${(v_{0},\emptyset)}^{C}=(v_{0},\emptyset,(+\infty,4))$, there is an edge to $(v_{4},\emptyset,(+\infty,3))$, then to $(v_{0},\emptyset,(+\infty,2))$ and to $(v_{4},\emptyset,(+\infty,1))$. For the latter vertex, there is no outgoing edge back to $(v_{0},\emptyset,(+\infty,0))$ because $2\notin I(v_{0},\emptyset)$. Therefore there is no infinite path starting in ${(v_{0},\emptyset)}^{C}$ in $\mathbb{C}(\lambda)$ that corresponds to $\rho^{\prime}$.∎

There exists a correspondence between $\lambda$-consistent plays in $\operatorname{\mathcal{X}}$ and infinite paths from starting vertices in $\mathbb{C}(\lambda)$ in the following way. On one hand, every play $\rho$ in $\operatorname{\mathcal{X}}$ that is not $\lambda$-consistent does not appear in the counter graph: the first constraint regarding $\lambda$ that is violated along $\rho$ is reflected by a vertex in $\mathbb{C}(\lambda)$ with a counter value getting to $1$ and no outgoing edges. On the other hand, $\lambda$-consistent plays in $\operatorname{\mathcal{X}}$ have a corresponding infinite path in the counter graph $\mathbb{C}(\lambda)$. We call valid paths the infinite paths of $\mathbb{C}(\lambda)$. This correspondence is formalized in the two following lemmas:

Lemma 13**.**

Let $\rho=\rho_{0}\rho_{1}\ldots$ be a $\lambda$-consistent play in $\operatorname{Plays}_{X}(v)$. Then there exists an associated infinite path $\pi=\pi_{0}\pi_{1}\ldots$ in $\mathbb{C}(\lambda)$ such that:

• •

$\pi_{0}=v^{C}$,

• •

$\rho$* is the projection of $\pi$ on $V^{X}$, that is, $\pi_{n}$ is of the form $(v^{\prime},{(c^{\prime}_{i})}_{i\in\Pi})$ with $v^{\prime}=\rho_{n}$, for every $n\in\mathbb{N}$.*

Proof 3.1**.**

Let $v\in V^{X}$ and $\rho$ be a play in $\operatorname{\mathcal{X}}$ such that $\rho\in\Lambda(v)$ and $\rho_{0}=v$. We build the corresponding infinite path $\pi$ in $\mathbb{C}(\lambda)$ iteratively as follows: Let $\pi_{0}:=v^{C}$. Let $n\in\mathbb{N}$, $n\geq 1$. Suppose that $\pi_{<n}$ has been already constructed, we show how to choose $\pi_{n}$. Suppose $\pi_{n-1}=(v^{\prime},{(c^{\prime}_{i})}_{i\in\Pi})$. Then $\pi_{n}:=(v^{\prime\prime},{(c^{\prime\prime}_{i})}_{i\in\Pi})$, where:

• •

$v^{\prime\prime}=\rho_{n}$,

• •

for every $i\in\Pi$:

[TABLE]

Let us show that $((v^{\prime},{(c^{\prime}_{i})}_{i\in\Pi}),(v^{\prime\prime},{(c^{\prime\prime}_{i})}_{i\in\Pi}))\in E^{C}$. As $\rho$ is a play in $\operatorname{\mathcal{X}}$, we clearly have $(v^{\prime},v^{\prime\prime})\in E^{X}$. Assume now, towards contradiction, that $((v^{\prime},{(c^{\prime}_{i})}_{i\in\Pi}),(v^{\prime\prime},{(c^{\prime\prime}_{i})}_{i\in\Pi}))\notin E^{C}$, that is, there is no outgoing edge from vertex $(v^{\prime},{(c^{\prime}_{i})}_{i\in\Pi})$ in the counter graph. By Definition 3, this means that there exists a player $i$ such that $c^{\prime}_{i}=1$ and $i\notin I(v^{\prime\prime})$.

As $c^{\prime}_{i}=1$, by Definition 3 and construction of $\pi_{0}\ldots\pi_{n-1}$, there must exist a largest index $m\leq n-1$ such that $\rho_{m}\in V^{X}_{i}$, $\lambda(\rho_{m})=d$ with $d>0$ and such that the counter value for player $i$ decreases by exactly $1$ at each step from vertex $\pi_{m}$ until reaching value $c^{\prime}_{i}=1$ at vertex $\pi_{n-1}=v^{\prime}$. Since $\rho$ is $\lambda$-consistent, player $i$ visits his target set along $\rho$ in at most $d$ steps, thus at most at vertex $v^{\prime\prime}$, and thus $i\in I(v^{\prime\prime})$, which is a contradiction.

Lemma 14**.**

Let $v^{C}=(v,{(c_{i})}_{i\in\Pi})$ be a starting vertex in $\mathrm{SV}(\lambda)$. Let $\pi=\pi_{0}\pi_{1}\ldots$ be an infinite path in $\mathbb{C}(\lambda)$ such that $\pi_{0}=v^{C}$. Then there exists a corresponding play $\rho=\rho_{0}\rho_{1}\ldots$ in $\operatorname{\mathcal{X}}$ such that:

• •

$\rho$* is $\lambda$-consistent,*

• •

$\rho$* is the projection of $\pi$ on $V^{X}$, that is, $\rho_{n}=v^{\prime}$ with $\pi_{n}=(v^{\prime},{(c^{\prime}_{i})}_{i\in\Pi})$, for every $n\in\mathbb{N}$.*

Proof 3.2**.**

Let $v^{C}=(v,{(c_{i})}_{i\in\Pi})$ be a starting vertex in $\mathrm{SV}(\lambda)$. Let $\pi$ be an infinite path in $\mathbb{C}(\lambda)$ such that $\pi_{0}=v^{C}$. Let $\rho$ be the projection of $\pi$ on $V^{X}$, that is, $\rho_{n}=v^{\prime}$ with $\pi_{n}=(v^{\prime},{(c^{\prime}_{i})}_{i\in\Pi})$, for every $n\in\mathbb{N}$.

• •

Clearly, $\rho$ is a play in $\operatorname{\mathcal{X}}$: by construction of $\mathbb{C}(\lambda)$, there exists an edge between two vertices $(v,{(c_{i})}_{i\in\Pi})$ and $(v^{\prime},{(c^{\prime}_{i})}_{i\in\Pi})$ in $\mathbb{C}(\lambda)$ only if $(v,v^{\prime})$ is an edge in $E^{X}$.

• •

Furthermore, the play $\rho$ is $\lambda$-consistent: Assume, towards contradiction, that it is not. Thus, there exists $n\in\mathbb{N}$ and $i\in\Pi$ such that $\rho_{n}\in V^{X}_{i}$ and

[TABLE]

Consider now $\pi_{n}$ and the value $c_{i}$ of the counter for player $i$ at this vertex. Since $\rho_{n}\in V^{X}_{i}$, we know that $c_{i}\leq\lambda(\rho_{n})$. From this vertex, the counter value for player $i$ decreases at least by $1$ at each step along $\pi_{\geq n}$. and hits the value [math] before $\lambda(\rho_{n})$ steps. However, this means that in $\rho_{\geq n}$, player $i$ visits his target set sooner than expected, which is a contradiction with (14).

Since the edge relation $E^{C}$ in the counter graph respects the edge relation $E^{X}$ in the extended game, the region decomposition of path in $\operatorname{\mathcal{X}}$ given in Lemma 3 can also be applied to a path in $\mathbb{C}(\lambda)$. We will often use such path region decompositions in the proofs of this section.

In order to prove the PSPACE membership for the constraint problem, we need to show that the counter graph $\mathbb{C}(\lambda^{*})$, with $\lambda^{*}$ the fixpoint function computed by Algorithm 1, has an exponential size. To this end, as the size of $|\mathbb{C}(\lambda^{*})|$ of $\mathbb{C}(\lambda^{*})$ is equal to $|V|\cdot 2^{|\Pi|}\cdot{(K+2)}^{|\Pi|}$ with $K=\mathrm{mR}(\lambda^{*})$ defined in Definition 3, it is enough to show an exponential upper bound on $K$. We proceed in two steps: First, with the next proposition, given a labeling function $\lambda$ and its restriction $\lambda_{\geq\ell}$ to $V^{\geq\ell}$, we exhibit a bound on the supremum of the cost of $\lambda$-consistent plays for each player, in terms of the maximal finite range $\mathrm{mR}(\lambda_{\geq\ell})$. Second, we consider the actual sequence of functions ${(\lambda^{k})}_{k\in\mathbb{N}}$ defined in Definitions 2 and 4, as implemented by Algorithm 1. With Theorem 18, we show that $\mathrm{mR}(\lambda^{*})$ is bounded by an exponential in the size of the original game $\mathcal{G}$. The proof is by induction on $k$ and uses Proposition 15.

Proposition 15** (Bound on finite supremum).**

Let $\lambda$ be a labeling function. Let $v\in V^{X}$ such that $I(v)=J_{\ell}$ with $\ell\in\{1,\ldots,N\}$. Let $c\in\mathbb{N}\cup\{+\infty\}$ be such that $\sup~{}\{\operatorname{Cost}_{i}(\rho)\mid\rho\in\Lambda(v)\}=c$. If $c<+\infty$, then

[TABLE]

Moreover, in both cases $c=+\infty$ and $c<+\infty$, there exists a valid path $\pi$ in $\mathbb{C}(\lambda)$ starting in $v^{C}$ that is a lasso $hg^{\omega}$ with the length of $hg$ bounded by $2\cdot|\mathbb{C}(\lambda)|$ and such that its corresponding play $\rho$ in $\operatorname{\mathcal{X}}$ belongs to $\Lambda(v)$ and has its cost $\operatorname{Cost}_{i}(\rho)$ equal to $c$.

Before proving Proposition 15, we need the following technical lemma:

Lemma 16**.**

Let $v^{C}$ be a starting vertex in $\mathrm{SV}(\lambda$) associated with $v\in V^{X}$ such that $I(v)=J_{\ell}$. Let $\pi$ be a finite prefix of a valid path in $\mathbb{C}(\lambda)$ such that:

• •

$\pi_{0}=v^{C}$,

• •

$\pi$* does not contain any cycle.*

Then,

[TABLE]

Proof 3.3** (Proof sketch).**

The proof of this lemma is quite technical, so we give here the main ideas and refer to the full proof hereafter for more details.

Let $\pi$ be a finite prefix of a valid path in $\mathbb{C}(\lambda)$ as in the statement. Let $\pi[\ell]\dots\pi[m]$ be its region decomposition according to Lemma 3, graphically represented in Figure 4. Let $\rho$ be the corresponding path in $\operatorname{\mathcal{X}}$ and $\rho[\ell]\dots\rho[m]$ be its region decomposition. Let us consider a fixed non-empty section $\pi[n]$.

Suppose first that the counter values at ${\pi[n]}_{0}$ are either [math] or $+\infty$. Let us prove that along $\pi[n]$, there can be at most $|V|$ steps before reaching a vertex with a finite positive value of $\lambda$:

• •

assume there is a cycle in the corresponding section $\rho[n]$ in $\operatorname{\mathcal{X}}$ such that from ${\rho[n]}_{0}$ and along the cycle, all the values of $\lambda$ are either [math] or $+\infty$,

• •

by construction of $\mathbb{C}(\lambda)$, the counter values in the corresponding prefix of $\pi[n]$ remain fixed for each vertex of this prefix: as no value of $\lambda$ is positive and finite, no counter value can be decremented,

• •

thus, the cycle in $\rho[n]$ is also a cycle in $\pi[n]$ which is impossible by hypothesis,

• •

thus there is no such cycle in $\rho[n]$, and as there are at most $|V|$ vertices in region $X^{J_{n}}$, $\rho[n]$ can have a prefix of length at most $|V|$ with only values [math] or $+\infty$ for $\lambda$, implying that this is also the case for $\pi[n]$.

Therefore, we can decompose $\pi[n]$ into a (possibly empty) prefix of length at most $|V|$, and a (possibly empty) suffix where at least one counter value $c^{\prime}_{i}$, for some $i$, is a positive finite value in its first vertex $v^{\prime}$. This frontier between prefix and suffix of $\pi[n]$ is represented by a vertical double bar $\|$ with caption $\infty\to c$ in Figure 4. This value $c^{\prime}_{i}$ is bounded by $\mathrm{mR}(\lambda_{n})$, the maximal finite range of $\lambda_{n}$. From there, as the corresponding $\rho$ is $\lambda$-consistent, player $i$ reaches his target set in at most $c^{\prime}_{i}$ steps, and $\rho$ enters a new region, which means that the section $\pi[n]$ is over. So, in that case, the length of $\pi[n]$ can be bounded by $|V|+\mathrm{mR}(\lambda_{n})$.

Suppose now that at vertex ${\pi[n]}_{0}$, there exists a counter value $c_{i}$ for some player $i$ that is neither [math] nor $+\infty$. This means that there was a constraint for player $i$ initialized in a previous section $\pi[n^{\prime}]$, with $n^{\prime}<n$, that has carried over to ${\pi[n]}_{0}$, via decrements of at least $1$ per step. We know that the initial finite counter value is bounded by $\mathrm{mR}(\lambda_{n^{\prime}})$, and appeared before the end of section $\pi[n^{\prime}]$. Thus the length from the end of section $\pi[n^{\prime}]$ to the end of section $\pi[n]$ is bounded by $\mathrm{mR}(\lambda_{n^{\prime}})$, as again, once the counter value attains [math] for player $i$, the path $\pi$ has entered the next section.

Therefore, considering the possible cases for each section, we can bound the total length of $\pi$ as follows:

[TABLE]

Finally, remark that by $I$-monotonicity, it is actually the case that only (and at most) $|\Pi|$ different non-empty sections can appear in the decomposition of $\pi$. Furthermore, for each $n\in\{\ell+1,\ldots,N\}$, we have

[TABLE]

by Definition 3. Thus, we have the following bound:

[TABLE]

which is the bound stated in Lemma 16.

Proof 3.4** (Proof of Lemma 16).**

Let $v^{C}$ be a starting vertex in $\mathrm{SV}(\lambda$). Let $\pi$ be a finite prefix of a valid path in $\mathbb{C}(\lambda)$ such that:

• •

$\pi_{0}=v^{C}$,

• •

$\pi$* does not contain any cycle.*

The following proof is quite technical, thus we alleviate some of the difficulties by proving a first upper bound on the length of finite paths without cycles in $\mathbb{C}(\lambda)$, then by showing how to obtain the desired bound. The main idea is to bound iteratively the length of prefixes of $\pi$, adding at each step of the reasoning the section for the next region traversed by $\pi$.

Let $\pi^{\prime}$ be a valid path in $\mathbb{C}(\lambda)$ such that $\pi$ is a prefix of $\pi^{\prime}$. By Lemma 3, we know that there exist two natural numbers $\ell,m^{\prime}\leq N$ and $m^{\prime}-\ell$ (possibly empty) paths $\pi^{\prime\ell},\dots,\pi^{\prime m^{\prime}}$ in $\mathbb{C}(\lambda)$ such that:

• •

$\pi^{\prime}=\pi^{\prime}[\ell]\dots\pi^{\prime}[m^{\prime}]$,

• •

for each $\ell\leq j\leq m^{\prime}$, each vertex in $\pi^{\prime}[n]$ is of the form $(w,{(c_{i})}_{i\in\Pi})$ with $I(w)=J_{j}$.

The finite path $\pi$ is a finite prefix of $\pi^{\prime}$. Thus there exists a natural number $m\leq m^{\prime}$ and $m-\ell$ (possibly empty) paths $\pi[\ell],\dots,\pi[{m^{\prime}}]$ in $\mathbb{C}(\lambda)$ such that:

• •

$\pi=\pi[\ell]\dots\pi[{m}]$,

• •

for each $\ell\leq j<m$, $\pi[j]=\pi^{\prime}[j]$,

• •

$\pi[m]$* if a finite prefix of $\pi^{\prime}[{m}]$.*

By Lemma 14, there exist a corresponding $\lambda$-consistent play $\rho^{\prime}$ in $\operatorname{\mathcal{X}}$ and a corresponding history $\rho$. Furthermore, since $\pi$ contains no cycle, the sections $\pi[n]$ do not either.

We first treat the case where $m<m^{\prime}$.

We first bound the length of the first section $\pi[\ell]$. Recall that since ${\pi[\ell]}_{0}=v^{C}\in\mathrm{SV}(\lambda)$, we have that $v^{C}=(v,{(c_{i})}_{i\in\Pi})$ with $c_{i}=0$ if $i\in J_{\ell}$, $c_{i}=\lambda(v)$ if $v\in V_{i}$ and $c_{i}=+\infty$ otherwise.

Suppose $0<\lambda(v)<+\infty$. In that case, we know that along $\rho^{\prime}$, which is $\lambda$-consistent, player $i$ reaches his target after at most $\lambda(v)$ steps. Thus, there exists $n\leq m^{\prime}$, $n\neq\ell$ such that $I(\rho_{\lambda(v)})=J_{n}$, $J_{\ell}\subsetneq J_{n}$, and $\pi_{\lambda(v)}$ belongs to section $\pi[n]$. This means that section $\pi[\ell]$ is shorter than $\lambda(v)$. Since $I(v)=J_{\ell}$, we have that $\lambda(v)\leq\mathrm{mR}(\lambda_{\ell})$, and thus $|\pi[\ell]|\leq\mathrm{mR}(\lambda_{\ell})$.

Suppose now that $\lambda(v)=0$ or $\lambda(v)=+\infty$. The counter values at $v^{C}$ are thus either [math] or $+\infty$. Along $\pi^{\prime}$, they can stay stable for at most $|V|$ steps (see Proof sketch of Lemma 16). Otherwise, the cycle induced in $\rho^{\prime}$ is also a cycle in $\pi^{\prime}$ as the counter values are fixed. If $\pi^{\prime}_{|V|+1}$ is in section $\pi^{\prime}[n]$ with $n>\ell$, then we immediately get that $|\pi[\ell]|\leq|V|$. If $\pi^{\prime}_{|V|+1}$ is in section $\pi^{\prime}[\ell]$, then it means that a counter value for some player $i$ has become finite along the first $|V|+1$ vertices of $\pi^{\prime}[\ell]$. Let $t$ be the first index it does so along $\pi^{\prime}[\ell]$. By the same argument as in the previous case, we know that from ${\pi^{\prime}[\ell]}_{t}$, there is at most $\mathrm{mR}(\lambda_{\ell})$ vertices before entering the next section of $\pi^{\prime}$. Thus, we obtain that:

[TABLE]

If $\ell=m$, we can already conclude that:

[TABLE]

Suppose now that $\ell<m$. We show that for each $n>\ell$, we have:

[TABLE]

Let $n=\ell+1$. We assume $\pi[n]$ is not empty, otherwise its length is [math]. Consider now ${\pi[n]}_{0}$.

Suppose there exists a player $i$ such that his counter value $c_{i}$ at ${\pi[n]}_{0}=(w,J_{n},{(c_{i})}_{i\in\Pi})$ is a finite non-zero value. If $w\not\in V_{i}$, it means that the counter value has decreased since a vertex $(w^{\prime},{(c^{\prime}_{i})}_{i\in\Pi})$ in the previous section $\pi[{\ell}]$ such that $w^{\prime}\in V_{i}$ and $c^{\prime}_{i}=\lambda(w)$. Thus, the length of the path from this vertex $(w^{\prime},{(c^{\prime}_{i})}_{i\in\Pi})$ to the next section $\pi[{n+1}]$ is smaller or equal than $\lambda(w^{\prime})$. In particular, the whole section $\pi[n]$ is “covered” by this path. Therefore, we can conclude that $|\pi[n]|\leq\lambda(w^{\prime})\leq\mathrm{mR}(\lambda_{\ell})$. Since we already know that $|\pi[\ell]|\leq|V|+\mathrm{mR}(\lambda_{\ell})$, we obtain that:

[TABLE]

If $w\in V_{i}$, it means that either the counter value $c_{i}$ is equal to $\lambda(w)$ or has decreased since a vertex $(w^{\prime},{(c^{\prime}_{i})}_{i\in\Pi})$ in the previous section $\pi[{\ell}]$ such that $w^{\prime}\in V_{i}$ and $c^{\prime}_{i}=\lambda(w^{\prime})$. Thus, we have that $c_{i}\leq\mathrm{mR}(\lambda_{n})$ or $c_{i}\leq\mathrm{mR}(\lambda_{\ell})$, and, in turn, $|\pi[n]|\leq\mathrm{mR}(\lambda_{n})$ or $|\pi[n]|\leq\mathrm{mR}(\lambda_{n})$. Therefore, we can conclude that:

[TABLE]

Suppose now that for every player $i$, his counter value $c_{i}$ at ${\pi[n]}_{0}=(w,{(c_{i})}_{i\in\Pi})$ is either [math] or $+\infty$. In that case, we are in a similar case than for section $\pi[\ell]$, thus we can conclude that $|\pi[n]|\leq|v|+\mathrm{mR}(\lambda_{n})$. Thus, we have indeed:

[TABLE]

and also

[TABLE]

If $m=\ell+1$, we are done.

Suppose now that $m>\ell+1$. Let $n$ be such that $\ell+1<n\leq m$. Assume that for each $n^{\prime}<n$, it holds that

[TABLE]

We assume $\pi[n]$ is not empty, otherwise its length is [math]. Consider now ${\pi[n]}_{0}$.

Suppose there exists a player $i$ such that his counter value $c_{i}$ at ${\pi[n]}_{0}=(w,{(c_{i})}_{i\in\Pi})$ is a finite non-zero value. If $w\not\in V_{i}$, it means that the counter value has decreased since a vertex $(w^{\prime},{(c^{\prime}_{i})}_{i\in\Pi})$ in a previous section $\pi[{n^{\prime}}]$ such that $w^{\prime}\in V_{i}$ and $c^{\prime}_{i}=\lambda(w^{\prime})$. Thus, the length of the path from this vertex $(w^{\prime},{(c^{\prime}_{i})}_{i\in\Pi})$ to the next section $\pi[{n+1}]$ is smaller or equal than $\lambda(w^{\prime})$. In particular, the whole sections from $\pi[{n^{\prime}+1}]$ to $\pi[n]$ are “covered” by this path. Therefore, we can conclude that $|\pi[{n^{\prime}+1}]\dots\pi[n]|\leq\lambda(w^{\prime})\leq\mathrm{mR}(\lambda_{n^{\prime}})$. Since we already know that:

[TABLE]

we obtain that:

[TABLE]

If $w\in V_{i}$, it means that either the counter value $c_{i}$ is equal to $\lambda(w)$ or has decreased since a vertex $(w^{\prime},{(c^{\prime}_{i})}_{i\in\Pi})$ in a previous section $\pi[{n^{\prime}}]$ such that $w^{\prime}\in V_{i}$ and $c^{\prime}_{i}=\lambda(w^{\prime})$. Thus, we have that $c_{i}\leq\mathrm{mR}(\lambda_{n})$ or $c_{i}\leq\mathrm{mR}(\lambda_{n^{\prime}})$, and, in turn, $|\pi[n]|\leq\mathrm{mR}(\lambda_{n})$ or $|\pi[n]|\leq\mathrm{mR}(\lambda_{n^{\prime}})$.

If $|\pi[n]|\leq\mathrm{mR}(\lambda_{n})$, we can conclude that:

[TABLE]

If $|\pi[n]|\leq\mathrm{mR}(\lambda_{n^{\prime}})$, we can conclude that:

[TABLE]

Suppose now that for every player $i$, his counter value $c_{i}$ at ${\pi[n]}_{0}=(w,{(c_{i})}_{i\in\Pi})$ is either [math] or $+\infty$. In that case, we are in a similar case than for section $\pi[\ell]$, thus we can conclude that $|\pi[n]|\leq|v|+\mathrm{mR}(\lambda_{n})$. Thus, we have indeed:

[TABLE]

and thus finally:

[TABLE]

Assume now that $m=m^{\prime}$. In that case, we cannot rely on the section $\pi^{\prime m}$ to be finite, as the play $\rho^{\prime}$ never reaches another region. However, in this situation, it is guaranteed that the counter values in $\pi^{\prime m}$ are fixed and are equal to either [math] or $+\infty$: indeed, a finite counter value would imply that some player $i$ such that $i\not\in J_{m}$ reaches his target in $\rho^{\prime}$ exactly when his counter value becomes [math] in $\pi^{\prime}$. But $\pi^{\prime m}$ is the last section of $\rho^{\prime}$, thus no new region is reached after $J_{m}$ and no new player can visit his target set than the players $i\in J_{m}$. Therefore, finite prefix of $\pi^{\prime m}$ that contains no cycle has its length bounded by $|V|$. Thus, we can conclude:

[TABLE]

In fact, the bound given above can be slightly changed to give the desired bound. Indeed, the bound above relies on the fact that $m\leq N$ and covers the case where a path traverses every region from $J_{\ell}$ to $J_{N}$. In all generality, the number $N$ of different regions can be exponential in the number $|\Pi|$ of players. However, by the $I$-monotonicity property, we know that a path can actually traverse at most $|\Pi|$ regions. Thus, in the region decomposition of a path, only (and at most) $|\Pi|$ sections are relevant and of length greater than [math]. Therefore, we can define a subsequence of indices ${(n_{r})}_{r\leq|\pi|}$, with $n_{1}=\ell$, such that in fact $\pi=\pi[{n_{1}}]\dots\pi[{n_{|\Pi|}}]$. Hence, we obtain the following bound on the length $t$ of $\pi$:

[TABLE]

Finally, as for every $r\leq|\pi|$, $r>1$, we have $\mathrm{mR}(\lambda_{n_{r}})\leq\max\{\mathrm{mR}(\lambda_{j})\mid J_{j}>J_{\ell},|J_{j}|=|J_{n_{r}}|\}$, we obtain the desired bound:

[TABLE]

We are now ready to prove Proposition 15.

Proof 3.5** (Proof of Proposition 15).**

Let $v\in V^{X}$ with $I(v)=J_{\ell}$ and $i\in\Pi$. Let $c\in\mathbb{N}\cup\{+\infty\}$ be such that $\sup~{}\{\operatorname{Cost}_{i}(\rho)\mid\rho\in\Lambda(v)\}=c$. Consider $\rho\in\Lambda^{k}(v)$ such that $\operatorname{Cost}_{i}(\rho)=c$. Notice that such a play always exists by Corollary 10. Consider also $\pi$ the valid path in $\mathbb{C}(\lambda)$ that starts in $v^{C}$ and corresponds to $\rho$.

Suppose first that $c<+\infty$ and let us prove that

[TABLE]

If $i\in J_{\ell}$, then $c=0$, as every play starting in $v$ has a cost [math] for player $i$. Hence (15) trivially holds.

Suppose now that $i\notin J_{\ell}$. As player $i$ eventually reaches his target set along $\rho$, this means that $\rho$ eventually leaves region $J_{\ell}$ and eventually reaches another region $J_{n}$ such that $i\in J_{n}$. Consider the prefix $\rho_{\leq c}$ of $\rho$ of length $c$. Let $\pi_{\leq c}:=\pi_{\leq c}[\ell]\dots\pi_{\leq c}[m]$ be the prefix of $\pi$ and its region decomposition such that $\pi_{\leq c}$ is associated with $\rho_{\leq c}$. Notice that $\pi_{\leq c}[m]$ consists only of one vertex corresponding to $\rho_{c}$, and that for every $n<m$, we have $i\notin J_{n}$.

Suppose that $\pi_{\leq c}$ contains a cycle. By construction of $\mathbb{C}(\lambda)$, this cycle is included in one single section $\pi_{\leq c}[n]$, where $n<m$ (as $\pi_{\leq c}[m]$ contains only one vertex), and thus $i\notin J_{n}$. Consider the infinite path $\pi^{\prime}$ in $\mathbb{C}(\lambda)$ that follows $\pi_{\leq c}$ until the cycle and then repeats the cycle forever. By Lemma 14, there exists a $\lambda$-consistent play $\rho^{\prime}$ in $\operatorname{\mathcal{X}}$ corresponding to $\pi^{\prime}$. We have $\operatorname{Cost}_{i}(\rho^{\prime})=+\infty$ for player $i$, as $\rho^{\prime}$ never reaches a region where player $i$ visits his target set. This is a contradiction with the fact that $\sup~{}\{\operatorname{Cost}_{i}(\rho)\mid\rho\in\Lambda(v)\}=c$ is finite.

Therefore $\pi_{\leq c}$ contains no cycle, and by Lemma 16,

[TABLE]

Since $|\pi_{\leq c}|=c=\operatorname{Cost}_{i}(\rho)$, we obtain Inequality (15).

Let us now prove the second part of Proposition 15 for both cases $c<+\infty$ and $c=+\infty$. Given the valid path $\pi$, we consider the first occurrence of a cycle in $\pi$. We then construct the infinite path $\pi^{\prime}$ in $\mathbb{C}(\lambda)$ that follows $\pi$ until this cycle and then repeats it forever. Then $\pi^{\prime}$ is a lasso $hg^{\omega}$ with the length $|hg|$ bounded by $2\cdot|\mathbb{C}(\lambda)|$. Clearly if $c=+\infty$, then the corresponding play $\rho^{\prime}$ in $\operatorname{\mathcal{X}}$ belongs to $\Lambda(v)$ and has a cost $\operatorname{Cost}_{i}(\rho^{\prime})$ equal to $\operatorname{Cost}_{i}(\rho)=+\infty$. If $c<+\infty$, we know by the first part of the proof that $\pi_{\leq c}$ contains no cycle and thus is prefix of $h$. Therefore we also have that the corresponding play $\rho^{\prime}$ has cost $\operatorname{Cost}_{i}(\rho^{\prime})=\operatorname{Cost}_{i}(\rho)=c$.

Remark 17**.**

In the proof of Proposition 15 and Lemma 16, we consider paths $\pi$ in the counter graph $\mathbb{C}(\lambda)$ that starts in a vertex $v$ such that $I(v)=J_{\ell}$. This means that such paths only visit vertices of regions $V^{J_{j}}$ such that $j\in\{\ell,\ell+1,\ldots,N\}$. There are therefore paths in the counter graph restricted $V^{\geq J_{\ell}}$ that we denote by $\mathbb{C}(\lambda_{\geq\ell})$.

We now come back to the labeling functions ${(\lambda^{k})}_{k\in\mathbb{N}}$ computed by Algorithm 1. Recall that this algorithm works in a bottom-up manner (see Proposition 5): it first computes the local fixpoint $\lambda^{k_{N}^{*}}$ on region $V^{J_{N}}$, then the local fixpoint $\lambda^{k_{N-1}^{*}}$ on $V^{\geq J_{N-1}}$, …, until finally computing the global fixpoint $\lambda^{*}$ on $V^{\geq J_{1}}=V^{X}$. Recall also that when the algorithm computes the local fixpoint in the arena $X^{\geq J_{n}}$, the values of $\lambda^{k}(v)$ may only change in the region $V^{J_{n}}$ (Lemma 6). We are now ready to show an exponential bound (in the size of $\mathcal{G}$) on the maximal finite ranges $\mathrm{mR}(\lambda^{k^{*}_{\ell}}_{\ell})$ for each region $X^{J_{\ell}}$ and $\mathrm{mR}(\lambda^{k^{*}_{\ell}}_{\geq\ell})$ for each arena $X^{\geq J_{\ell}}$. With $\ell=1$, we get that $\mathrm{mR}(\lambda^{*})$ is of exponential size, and thus also the size of the counter graph.

Theorem 18** (Bound on maximal finite range).**

For each $\ell\in\{1,\dots,N\}$, we have

[TABLE]

and also:

[TABLE]

In particular for the global fixpoint $\lambda^{*}$ we have

[TABLE]

Proof 3.6**.**

The proof is done by a double induction: First, we exploit the fact that Algorithm 1 treats every region one after the other, following the total order on regions in reverse. That is, to compute the values of the fixpoint function $\lambda^{*}$ over $V^{X}$, Algorithm 1 computes first the values of $\lambda^{*}$ on region $V^{J_{N}}$, then on region $V^{J_{N-1}}$ etc…until finally on region $V^{J_{1}}$. Thus, we follow this order to prove the local bounds on $\mathrm{mR}(\lambda^{k^{*}_{\ell}}_{\ell})$, starting by $\mathrm{mR}(\lambda^{k^{*}_{N}}_{N})$ and making our way up to $\mathrm{mR}(\lambda^{k^{*}_{1}}_{1})$, assuming for each region $V^{J_{\ell}}$ such that $\ell<N$ that the bound is true for every region already treated by Algorithm 1. Second, given a non-bottom region $V^{J_{\ell}}$ and assuming the bound is true for every already treated region, we proceed to show the local bound for $V^{J_{\ell}}$ by induction on the number $k$ of steps in the computation, which corresponds to the values of function $\lambda^{k}$ in the sequence of functions leading to the fixpoint, up to step $k^{*}_{\ell}$, where the values stabilize on region $V^{\ell}$.

Let us now detail the proof. It is structured into several parts.

Part 1.

We begin with some notations and basic properties. We introduce a useful notation: for each $\ell<N$ and each $k\in\mathbb{N}$, we define $\alpha(\lambda^{k},\ell)$ as follows555This sum appears in the statement of Proposition 15.:

[TABLE]

Let $\ell\leq N$ and $v\in V^{J_{\ell}}$. By Lemma 6, we know the following:

1. (1)

the values of $\lambda^{k+1}_{\ell}(v)$ and $\lambda^{k}_{\ell}(v)$ may differ only when $k^{*}_{\ell+1}<k<k^{*}_{\ell}$; 2. (2)

for $k\leq k^{*}_{\ell+1}$, we have $\lambda^{k}_{\ell}(v)=\lambda^{k+1}_{\ell}(v)=\lambda^{0}_{\ell}(v)$; 3. (3)

for $k\geq k^{*}_{\ell}$, we have $\lambda^{k}_{\ell}(v)=\lambda^{k+1}_{\ell}(v)=\lambda^{k^{*}_{\ell}}(v)$

By 3., we have that for each $\ell<N$, and for $k\geq k^{*}_{\ell+1}$, we have $\mathrm{mR}(\lambda^{k}_{\ell+1})=\mathrm{mR}(\lambda^{k^{*}_{\ell+1}}_{\ell+1})$. Thus, for $k\geq k^{*}_{\ell+1}$, we also have

[TABLE]

Part 2.

Let $\ell<N$ and assume $J_{\ell}$ is not a bottom region. We start by proving, this time by induction on the number $k$ of algorithm steps, a bound on $\mathrm{mR}(\lambda^{k}_{\ell})$. Note, by Lemma 6 recalled above, that the only relevant steps for region $J_{\ell}$ are the steps $k$, where $k^{*}_{\ell+1}\leq k\leq k^{*}_{\ell}$. Let us show, for each such $k$, that:

[TABLE]

where $\mathrm{Dom}(\lambda^{k}_{\ell})=\{v\in V^{J_{\ell}}~{}|~{}\lambda^{k}_{\ell}(v)\neq 0,\lambda^{k}_{\ell}(v)\neq+\infty\}$.

• •

Base case: Assume $k=k^{*}_{\ell+1}$. By Lemma 6, we know that $\lambda^{k}_{\ell}=\lambda^{0}_{\ell}$. Thus, $\mathrm{mR}(\lambda^{k}_{\ell})=\mathrm{mR}(\lambda^{0}_{\ell})=0$. Furthermore, $\mathrm{Dom}(\lambda^{k}_{\ell})=\mathrm{Dom}(\lambda^{0}_{\ell})=\emptyset$, thus $\sum^{|\mathrm{Dom}(\lambda^{k}_{\ell})|}_{i=0}2^{i}=1$. Clearly, Equation (17) is satisfied.

• •

General case: Let now $k$ be such that $k^{*}_{\ell+1}\leq k<k^{*}_{\ell}$. Assume that Equation (17) holds for $k$. Let us show that

[TABLE]

We distinguish the two following subcases: $(a)$ when $\mathrm{Dom}(\lambda^{k+1}_{\ell})=\mathrm{Dom}(\lambda^{k}_{\ell})$, and $(b)$ when $\mathrm{Dom}(\lambda^{k+1}_{\ell})\neq\mathrm{Dom}(\lambda^{k}_{\ell})$.

• $(a)$

Assume $\mathrm{Dom}(\lambda^{k+1}_{\ell})=\mathrm{Dom}(\lambda^{k}_{\ell})$. We know by Lemma 7 that for each $v\in V^{J_{\ell}}$, $\lambda^{k+1}_{\ell}(v)\leq\lambda^{k}_{\ell}(v)$. Thus in the considered case we have:

[TABLE]

That is, Equation (18) holds.

• $(b)$

Assume $\mathrm{Dom}(\lambda^{k+1}_{\ell})\neq\mathrm{Dom}(\lambda^{k}_{\ell})$. Either we have $\mathrm{mR}(\lambda^{k+1}_{\ell})\leq\mathrm{mR}(\lambda^{k}_{\ell})$, and we can proceed as in subcase $(a)$, or we know that there exists $v\in V^{J_{\ell}}$ such that $\lambda^{k}_{\ell}(v)=+\infty$ and $\lambda^{k+1}_{\ell}(v)<+\infty$. Recall that by Definition 4 we have that

[TABLE]

Since $\lambda^{k+1}_{\ell}(v)\neq+\infty$, we know that $\sup\{\operatorname{Cost}_{i}(\rho)\mid\rho\in\Lambda^{k}(v^{\prime})\}$ is finite, for at least one successor $v^{\prime}$ of $v$. Thus, by Proposition 15, we obtain:

[TABLE]

Since $\mathrm{Dom}(\lambda^{k+1}_{\ell})\neq\mathrm{Dom}(\lambda^{k}_{\ell})$ by $(b)$ (thus indeed $|\mathrm{Dom}(\lambda^{k+1}_{\ell})|>|\mathrm{Dom}(\lambda^{k}_{\ell})$—), we have

[TABLE]

Hence, we have

[TABLE]

Finally, as this holds for any such $v\in V^{J_{\ell}}$, we obtain

[TABLE]

That is, Equation (18) holds for region $J_{\ell}$.

We proved that Equation (17) holds for each non-bottom region $J_{\ell}$ and each step $k$ such that $k^{*}_{\ell+1}\leq k\leq k^{*}_{\ell}$.

Part 3.

We can now come back to the induction on the regions $J_{\ell}$, following the order provided by Algorithm 1. Let us show that each $\ell\leq N$, we have

[TABLE]

• •

Base case: If $J_{\ell}$ is a bottom region, we have that $\mathrm{mR}(\lambda^{k^{*}_{\ell}}_{\ell})=0$ showing that (20) holds in this case and thus in particular when $\ell=N$.

• •

General case: Let $\ell<N$ and suppose $J_{\ell}$ is not a bottom region. Assume that, for each $j>\ell$, Inequality (20) holds. By (17), we know that

[TABLE]

Furthermore, as $|\mathrm{Dom}(\lambda^{k^{*}_{\ell}}_{\ell})|\leq|V|$, we have

[TABLE]

We turn now our attention towards the term $\alpha(\lambda^{k^{*}_{\ell+1}},\ell)$:

[TABLE]

By the induction hypothesis (20), we can bound each term $\mathrm{mR}(\lambda^{k^{*}_{j}}_{j})$ appearing in the above sum:

[TABLE]

Coming back to $\alpha(\lambda^{k^{*}_{\ell+1}},\ell)$ whose the number of terms in the sum can be bounded by $|\Pi|$, we get

[TABLE]

Hence we have, by combining (22) and (21):

[TABLE]

Hence, Equation (20) holds for region $J_{\ell}$.

Part 4.

We can now prove the three statements of Theorem 18. We obtain the first one from Inequality (20) by recalling that $|\Pi|\leq|V|$ and $|V|\geq 2$:

[TABLE]

This proves the first statement of Theorem 18.

For the second one, remark that $\mathrm{mR}(\lambda^{k^{*}_{\ell}}_{\geq\ell})=\max\{\mathrm{mR}(\lambda^{k^{*}_{j}}_{j})~{}|~{}J_{j}\geq J_{\ell}\}$ (since only regions already treated are considered). For each such $j\geq\ell$, we have $\mathrm{mR}(\lambda^{k^{*}_{j}}_{j})\leq\mathcal{O}\left(|V|^{(|V|+3|)(|\Pi\setminus J_{j}|+2)}\right)$ by (23) and thus $\mathrm{mR}(\lambda^{k^{*}_{j}}_{j})\leq\mathcal{O}\left(|V|^{(|V|+3|)(|\Pi|+2)}\right)$. It follows that $\mathrm{mR}(\lambda^{k^{*}_{\ell}}_{\geq\ell})\leq\mathcal{O}\left(|V|^{(|V|+3|)(|\Pi|+2)}\right)$.

*For the last statement, recall that $\mathrm{mR}(\lambda^{*})=\mathrm{mR}(\lambda^{k^{*}_{1}}_{\geq 1})$. Hence in particular we obtain $\mathrm{mR}(\lambda^{*})\leq\mathcal{O}\left(|V|^{(|V|+3|)(|\Pi|+2)}\right)$. *

The next corollary is a direct consequence of Theorem 18.

Corollary 19**.**

The counter graph $\mathbb{C}(\lambda^{*})$ has a size $|\mathbb{C}(\lambda^{*})|=|V|\cdot 2^{|\Pi|}\cdot{(\mathrm{mR}(\lambda^{*})+2)}^{|\Pi|}$ that is exponential in the size of the game $\mathcal{G}$.

We conclude this section with two other corollaries that will be useful in the next section.

Corollary 20**.**

For every $k\in\mathbb{N}$ and region $V^{J_{\ell}}$, we have

[TABLE]

and also

[TABLE]

Proof 3.7**.**

Assume, without loss of generality, that $J_{\ell}$ is not a bottom region (otherwise we immediately have $\mathrm{mR}(\lambda^{k}_{\ell})=0$ for every $k\in\mathbb{N}$). Let $k\in\mathbb{N}$. Again, by Lemma 6, if $k\leq k^{*}_{\ell+1}$, we already have $\mathrm{mR}(\lambda^{k}_{\ell})=0$, and if $k\geq k^{*}_{\ell}$, we have $\lambda^{k}_{\ell}(v)=\lambda^{k^{*}_{\ell}}(v)$. Thus we assume that $k^{*}_{\ell+1}<k\leq k^{*}_{\ell}$. Using the terminology of the proof of Theorem 18, we know, by (17) in its proof, that

[TABLE]

As $|\mathrm{Dom}(\lambda^{k}_{\ell})|\leq|V|$, we have

[TABLE]

From there, following the same steps (from Equation (21) onwards) as in the proof of Theorem 18 leads to the desired bound: $\mathrm{mR}(\lambda^{k}_{\ell})\leq\mathcal{O}\left(|V|^{(|V|+3)(|\Pi|+2)}\right)$.

Similarly, as $\mathrm{mR}(\lambda^{k}_{\geq\ell})=\max\{\mathrm{mR}(\lambda^{k}_{j})~{}|~{}j\geq\ell\}$, and as we just showed that $\mathrm{mR}(\lambda^{k}_{j})\leq\mathcal{O}\left(|V|^{(|V|+3|)(|\Pi|+2)}\right)$ for every $j$ and $k$, we immediately get

[TABLE]

Corollary 21**.**

Let $v\in V^{X}$ with $I(v)=J_{\ell}$ with $\ell\in\{1,\ldots N-1\}$. Let $k\in\mathbb{N}$. Suppose there exists $c\in\mathbb{N}$ such that $\sup~{}\{\operatorname{Cost}_{i}(\rho)\mid\rho\in\Lambda^{k}(v)\}=c$. Then, the following holds:

[TABLE]

Proof 3.8**.**

Let $v\in V^{X}$ with $I(v)=J_{\ell}$ and $k\in\mathbb{N}$. Suppose there exists $c\in\mathbb{N}$ such that $\sup~{}\{\operatorname{Cost}_{i}(\rho)\mid\rho\in\Lambda^{k}(v)\}=c$. If $J_{\ell}$ is a bottom region, then $c=0$, thus we assume from now on that $J_{\ell}$ is not a bottom region. Then, by Proposition 15, we know that:

[TABLE]

Using the terminology of the proof of Theorem 18, we have:

[TABLE]

As $|\mathrm{Dom}(\lambda^{k}_{\ell})|\leq|V|$, we obtain:

[TABLE]

From there, following the same steps (from Equation (21) onwards) as in the proof of Theorem 18 leads to the desired bound:

[TABLE]

4. PSPACE completeness

In this section, we prove Theorem 1. We first prove that the constraint problem is in PSPACE and then that it is PSPACE-hard.

4.1. PSPACE easiness

The purpose of this section is to prove that determining if, given a reachability game ($\mathcal{G}$,$v_{0}$) and two thresholds $x,y\in{(\mathbb{N}\cup\{+\infty\})}^{|\Pi|}$, there exists an SPE $\sigma$ in this game such that for all $i\in\Pi$, $x_{i}\leq\operatorname{Cost}_{i}(\langle\sigma\rangle_{v_{0}})\leq y_{i}$ can be done in PSPACE.

Proposition 22**.**

The constraint problem for initialized reachability games is in PSPACE.

Let us provide a high level sketch of the proof of our PSPACE procedure for this constraint problem. Thanks to Theorem 8, solving the constraint problem for a given game $({\mathcal{G}},v_{0})$ reduces in finding a $\lambda^{*}$-consistent play $\rho$ in $(\operatorname{\mathcal{X}},x_{0})$ satisfying the constraints. By Lemmas 13 and 14, the latter problem reduces in finding a valid path $\pi$ in the counter graph $\mathbb{C}(\lambda^{*})$ that satisfies the constraints. We will see that it suffices to decide the existence of such a valid path that is a lasso $hg^{\omega}$. As $\mathbb{C}(\lambda^{*})$ is exponential in the size of the input $\mathcal{G}$ (by Corollary 19), classical arguments using Savitch’s Theorem can thus be used to prove the PSPACE membership. Nevertheless, the detailed proof is more intricate for two reasons. The first reason is that the counter graph is constructed from the labeling function $\lambda^{*}$. We thus also have to prove that $\lambda^{*}$ can be computed in PSPACE. The second reason is that, a priori, although we know that the counter graph is of exponential size, we do not know explicitly its size. This is problematic when using classical NPSPACE algorithms that guess, vertex by vertex, some finite path in a graph of exponential size, where a counter bounded by the size of the graph is needed to guarantee the termination of the procedure. In order to overcome this, we also need a PSPACE procedure to obtain the actual size of $\mathbb{C}(\lambda^{*})$. Recall that the size $|\mathbb{C}(\lambda^{*})|$ is equal to $|V|\cdot 2^{|\Pi|}\cdot{(K+2)}^{|\Pi|}$ where $K=\mathrm{mR}(\lambda^{*})$. Hence to compute the size of the counter graph, we have to compute the actual value of $\mathrm{mR}(\lambda^{*})$.

The PSPACE procedure to compute $\lambda^{*}$ and $\mathrm{mR}(\lambda^{*})$ works by induction on $k$, the steps in the computation of the labeling function $\lambda^{*}$. Moreover, it exploits the structural evolution of the local fixpoints formalized in Proposition 5 and Lemma 6. Indeed recall that these local fixpoints are computed region by region, from $X^{J_{N}}$ to $X^{J_{1}}$, and that if $X^{J_{\ell}}$ is the currently treated region, then the values of $\lambda^{k+1}(v)$ are computed from $\lambda^{k}(v)$ for all $v\in V^{J_{\ell}}$ (those values remain unchanged for all $v$ outside of $V^{J_{\ell}}$). For the moment, suppose that we have at our disposal a PSPACE procedure to compute $\{\lambda^{k}(v)\mid v\in V^{J_{\ell}}\}$ and the maximal finite range $\mathrm{mR}(\lambda^{k}_{\geq\ell})$:

Proposition 23**.**

Given an initialized reachability game $(\mathcal{G},v_{0})$, for all $k\in\mathbb{N}$ and for all $J_{\ell}$, $\ell\in\{1,\ldots,N\}$, the set $\{\lambda^{k}(v)\mid v\in V^{J_{\ell}}\}$ and the maximal finite range $\mathrm{mR}(\lambda^{k}_{\geq\ell})$ can be computed in PSPACE.

Let us prove Proposition 22. The proof of Proposition 23 will be given just after.

Proof 4.1** (Proof of Proposition 22).**

Let $(\mathcal{G},v_{0})$ be an initialized reachability game and let $x,y\in{(\mathbb{N}\cup\{+\infty\})}^{|\Pi|}$ be two thresholds. Let $(\operatorname{\mathcal{X}},x_{0})$ be the extended game of $(\mathcal{G},v_{0})$, $\mathbb{C}(\lambda^{*})$ the counter graph constructed from the labeling function $\lambda^{*}$ and its maximal finite range $\mathrm{mR}(\lambda^{*})$.

We first prove that there exists an SPE in $(\mathcal{G},v_{0})$ such that its outcome $\rho$ satisfies the constraints $x_{i}\leq\operatorname{Cost}_{i}(\rho)\leq y_{i}$ for all $i\in\Pi$, if and only if, there exists a valid path in $\mathbb{C}(\lambda^{*})$ starting from the starting vertex $x_{0}^{C}$ associated with $x_{0}$ such that it is a lasso $hg^{\omega}$ with the length $|hg|$ bounded by $d+2\cdot|\mathbb{C}(\lambda^{*})|$ with

[TABLE]

and such that it also satisfies these constraints.

We already know by Theorem 8 and Lemmas 13-14 that the existence of an SPE outcome $\rho$ in $\mathcal{G}$ satisfying the constraints is equivalent to the existence of a valid path $\pi$ in $\mathbb{C}(\lambda^{*})$ satisfying these constraints. It remains to show that the latter path can be chosen as a lasso $hg^{\omega}$ with the announced length of $hg$. This lasso is constructed as follows. Consider the suffix $\pi_{\geq d}$ of $\pi$ and its region decomposition $\pi_{\geq d}[m]\pi_{\geq d}[m+1]\ldots\pi_{\geq d}[n]$. For all $\ell\in\{m,\ldots,n-1\}$, we remove all the cycles in section $\pi_{\geq d}[\ell]$ to get a simple path $\pi^{\prime}_{\ell}$, and from the last section $\pi_{\geq d}[n]$, we derive the infinite path $\pi^{\prime}_{n}$ formed of the first vertices of $\pi_{\geq d}[n]$ until a cycle is reached and then repeated forever. Notice that there is no other cycle in $\pi^{\prime}_{m}\pi^{\prime}_{m+1}\ldots\pi^{\prime}_{n}$ by the $I$-monotonicity property (2). The required lasso $hg^{\omega}$ is equal to the concatenation of the prefix $\pi_{\leq d}$ with the modified suffix $\pi^{\prime}_{m}\pi^{\prime}_{m+1}\ldots\pi^{\prime}_{n}$. By construction $\pi^{\prime}_{m}\ldots\pi^{\prime}_{n}$ is itself a lasso $h^{\prime}g^{\prime\omega}$ with $|h^{\prime}g^{\prime}|$ bounded by $2\cdot|\mathbb{C}(\lambda^{*})|$ and thus $|hg|$ is bounded by $d+2\cdot|\mathbb{C}(\lambda^{*})|$. Moreover, for all $i$, $\pi$ visits the target set of player $i$ if and only if $hg^{\omega}$ visits this set (maybe earlier if the visit is inside $\pi^{\prime}_{m}\ldots\pi^{\prime}_{n}$). By definition of $d$, the constraints imposed by $x_{i},y_{i}$, $i\in\Pi$, are simultaneously satisfied by $\pi$ and $hg^{\omega}$.

Let us now show how to get a PSPACE procedure for the constraint problem. As just explained, we have to guess a lasso $\pi=hg^{\omega}$ in $\mathbb{C}(\lambda^{*})$ that starts in $x_{0}^{C}$, satisfies the constraints, and such that $|hg|$ is bounded by

[TABLE]

We cannot guess $\pi$ entirely and we have to proceed region by region. Suppose that $I(x_{0})=J_{m}$ for some $m\in\{1,\ldots,N\}$, and consider the region decomposition $\pi[m]\pi[m+1]\ldots\pi[n]$ of $\pi$, where some sections $\pi[\ell]$ may be empty.

We guess successively the sections $\pi[m]$, $\pi[m+1]$ and so on. To guess $\pi[\ell]$ with $\ell\in\{m,\ldots,n\}$, assuming it is not empty, we guess one by one its vertices that all belong to the same region $V^{J_{\ell}}$. To guess such a vertex $(v^{\prime},{(c^{\prime}_{i})}_{i\in\Pi})$, we only have to keep its predecessor $(v,{(c_{i})}_{i\in\Pi})$ in memory and to know the value $\lambda^{*}(v^{\prime})$ (in a way to compute each $c^{\prime}_{i}$ from $c_{i}$). So, we need to know $\{\lambda^{*}(v)\mid v\in V^{J_{\ell}}\}$. By Proposition 23, we can compute this set in PSPACE. Once we move to another region in a way to guess the next section of $\pi$, we can forget this set and compute the new one. We also need to guess which vertex will be the first vertex of $g$.

Notice that any vertex of the counter graph can be encoded in polynomial size memory. Indeed it is composed of a vertex of $V$, a subset $I$ of $\Pi$, and $|\Pi|$ counter values that belong to $\{0,\ldots,\mathrm{mR}(\lambda^{*})\}\cup\{+\infty\}$ ($\mathrm{mR}(\lambda^{*})$ is at most exponential in the input by Theorem 18). Moreover the set $\{\lambda^{*}(v)\mid v\in V^{J_{\ell}}\}$ can also be encoded in polynomial size memory since it is composed of $|V|$ values that belong to $\{0,\ldots,\mathrm{mR}(\lambda^{*})\}\cup\{+\infty\}$.

Recall that the length $|hg|$ for the guessed lasso $\pi=hg^{\omega}$ cannot exceed constant $L$. We thus have to compute and store $L$. The computation in PSPACE of $L$ requires the computation of $|\mathbb{C}(\lambda^{*})|$, and thus in particular the computation of $\mathrm{mR}(\lambda^{*})$. This is possible thanks to Proposition 23. And it follows by Corollary 19 that $L$ can be stored in polynomial size memory. In addition to $L$, during the guessing of $\pi$, we also have a counter $C_{L}$ to count the current length of $\pi$, and for each player $i\in\Pi$ a counter $C_{i}$ keeping track of the current cost of player $i$ along $\pi$. As $C_{L}\leq L$ and $C_{i}\leq L$ for all $i$, all these counters can be also encoded in polynomial size memory.

Finally, we stop guessing $\pi$ when either its length exceeds $L$ or when its currently guessed vertex is equal to the first vertex of cycle $g$ for the second time. In the latter case, we check whether $\pi$ satisfies the constraints, that is, $x_{i}\leq C_{i}\leq y_{i}$ for all $i$. This completes the proof that the given procedure works in PSPACE.

Let us now prove Proposition 23. We proceed by induction on the steps in the computation of the labeling function $\lambda^{*}$ and, once a step $k$ is fixed, we proceed region by region, beginning with the bottom region $J_{N}$ and then proceeding bottom-up by following the total order $J_{1}<\cdots<J_{N}$. Let $X^{J_{\ell}}$ be a region, we aim at proving that the set $\{\lambda^{k+1}(v)\mid v\in V^{J_{\ell}}\}$ and the value $\mathrm{mR}(\lambda^{k+1}_{\geq\ell})$ are both computable in PSPACE (from the previous step $k$). To this aim consider Proposition 5 and especially Lemma 6. Let $k^{*}_{\ell}$ (resp. $k^{*}_{\ell+1}$) be the step where the local fixpoint is reached for region $X^{J_{\ell}}$ (resp. $X^{J_{\ell+1}}$). Recall that $k^{*}_{\ell+1}<k^{*}_{\ell}$ and that when $k\leq k^{*}_{\ell+1}$ (resp. $k\geq k^{*}_{\ell}$), we have that $\lambda^{k+1}(v)=\lambda^{k}(v)$, for each $v\in V^{J_{\ell}}$. The tricky case in when $k^{*}_{\ell+1}<k<k^{*}_{\ell}$. In the latter case, the computation of $\lambda^{k+1}(v)$ from $\lambda^{k}(v)$, for all $v\in V^{J_{n}}$, relies on the computation of the maximal cost, for the player who owns vertex $v$, of the plays of $\Lambda^{k}(v^{\prime})$, with $v^{\prime}\in\operatorname{Succ}(v)$ (see Definition 4). This will be possible with the same approach as in the proof of Proposition 22: to guess a lasso in the counter graph $\mathbb{C}(\lambda^{k})$ that realizes this maximal cost.

Proof 4.2** (Proof of Proposition 23).**

We proceed by induction on $k\in\mathbb{N}$.

Base case.

For $k=0$ we have to prove that for all $J_{\ell}$, $\ell\in\{1,\ldots,N\}$, the set $\{\lambda^{0}(v)\mid v\in V^{J_{\ell}}\}$ and the value $\mathrm{mR}(\lambda^{0}_{\geq\ell})$ can be both computed in PSPACE. Given $J_{\ell}$, thanks to Definition 2, we have that either $\lambda^{0}(v)=0$ if $v\in V_{i}^{X}$ and $i\in I(v)=J_{\ell}$ or $\lambda^{0}(v)=+\infty$ otherwise. Thus $\mathrm{mR}(\lambda^{0}_{\geq l})=0$. So, we clearly have a PSPACE procedure in this case.

General case.

Now, assume that for all $n$, $n\in\{0,\ldots,k\}$, and for all $J_{\ell}$, $\ell\in\{1,\ldots,N\}$, the set $\{\lambda^{n}(v)\mid v\in V^{J_{\ell}}\}$ and the value $\mathrm{mR}(\lambda^{n}_{\geq\ell})$ can be computed in PSPACE. Let us prove that it remains true for $n=k+1$, that is:

[TABLE]

We proceed by induction on the region $X^{J_{\ell}}$ (we thus use a double induction, one on the computation steps and the other one on the regions).

If $J_{\ell}=J_{N}$, then it is a bottom region. Then for all $v\in V^{J_{N}}$, $\lambda^{k+1}(v)=\lambda^{0}(v)$ and so $\{\lambda^{k+1}(v)\mid v\in V^{J_{N}}\}=\{\lambda^{0}(v)\mid v\in V^{J_{N}}\}$ (local fixpoint $k_{N}^{*}=0$ in Proposition 5). By induction hypothesis we know that this latter set can be computed in PSPACE. Moreover, we have that $\mathrm{mR}(\lambda^{k+1}_{\geq N})=\mathrm{mR}(\lambda^{k+1}_{N})=0$. Therefore Assertion (26) holds.

Now, let $J_{\ell}$ be a region different from $J_{N}$. If it is a bottom region, we have $\{\lambda^{k+1}(v)\mid v\in V^{J_{\ell}}\}=\{\lambda^{0}(v)\mid v\in V^{J_{\ell}}\}$ as for $J_{N}$. Moreover $\mathrm{mR}(\lambda^{k+1}_{\ell})=\mathrm{mR}(\lambda^{0}_{\ell})=0$ and then $\mathrm{mR}(\lambda^{k+1}_{\geq\ell})=\max\{\mathrm{mR}(\lambda^{k+1}_{\ell}),\mathrm{mR}(\lambda^{k+1}_{\geq\ell+1})\}=\mathrm{mR}(\lambda^{k+1}_{\geq\ell+1})$. Thus by induction hypothesis, $\{\lambda^{k+1}(v)\mid v\in V^{J_{\ell}}\}$ and $\mathrm{mR}(\lambda^{k+1}_{\geq\ell})$ can be computed in PSPACE and Assertion (26) holds.

Let us now suppose that $J_{\ell}$ is not a bottom region. We first recall Proposition 5 that states that Algorithm 1 reaches a local fixpoint for each region. Let $k^{*}_{\ell}$ (resp. $k^{*}_{\ell+1}$), the step after which the region $X^{J_{\ell}}$ (resp. $X^{J_{\ell+1}}$) has reached its local fixpoint. Recall that $k^{*}_{\ell+1}<k^{*}_{\ell}$. Let us now consider the three cases of Lemma 6.

• •

If $k\leq k^{*}_{\ell+1}$, then by Lemma 6, the region $X^{J_{\ell+1}}$ has not reached its local fixpoint yet. So, it implies that the labeling of the vertices of $V^{J_{\ell}}$ has not change since initialization. More formally, for all $v\in V^{J_{\ell}}$, $\lambda^{k+1}(v)=\lambda^{0}(v)$. Thus $\mathrm{mR}(\lambda^{k+1}_{\ell})=0$ and then $\mathrm{mR}(\lambda^{k+1}_{\geq\ell})=\mathrm{mR}(\lambda^{k+1}_{\geq\ell+1})$. So by induction hypothesis, both $\{\lambda^{k+1}(v)\mid v\in V^{J_{\ell}}\}$ and $\mathrm{mR}(\lambda^{k+1}_{\geq\ell})$ can be computed in PSPACE showing (26).

• •

If $k>k^{*}_{\ell}$, then by Lemma 6, the local fixpoint of region $X^{J_{\ell}}$ is reached, that is, $\{\lambda^{k+1}(v)\mid v\in V^{J_{\ell}}\}=\{\lambda^{k}(v)\mid v\in V^{J_{\ell}}\}$ and $\mathrm{mR}(\lambda^{k+1}_{\geq\ell})=\mathrm{mR}(\lambda^{k}_{\geq\ell})$ and (26) holds by induction hypothesis.

(Notice the little difference with the inequalities given in Lemma 6: we here consider case $k>k^{*}_{\ell}$ instead of case $k\geq k^{*}_{\ell}$ of Lemma 6. Indeed when $k=k^{*}_{\ell}$, we still need to compute $\lambda^{k+1}$ to realize that the fixpoint is effectively reached. This is thus postponed in the next case.)

• •

It remains to consider the case $k^{*}_{\ell+1}<k\leq k^{*}_{\ell}$, which is the most difficult one. In this case, either the values of $\lambda^{k}(v)$ and $\lambda^{k+1}(v)$ differ for some $v\in V^{J_{\ell}}$, or $k=k^{*}_{\ell}$ and we realize that the local fixpoint is effectively reached on $X^{J_{\ell}}$.

Let us first show that the set $\{\lambda^{k+1}(v)\mid v\in V^{J_{\ell}}\}$ can be computed in PSPACE. Given $v\in V^{J_{\ell}}$, if $v\in V_{i}^{X}$, then by Definition 4, $\lambda^{k+1}(v)$ is either equal to 0 (if $i\in J_{\ell}$) or it is computed from the values $\sup\{\operatorname{Cost}_{i}(\rho)\mid\rho\in\Lambda^{k}(v^{\prime})\}$, $v^{\prime}\in\operatorname{Succ}(v)$. Thus we have to show that each value $\sup\{\operatorname{Cost}_{i}(\rho)\mid\rho\in\Lambda^{k}(v^{\prime})\}$ can be computed in PSPACE.

To this aim, we use Proposition 15 stating that if

[TABLE]

then there exists a valid path $\pi=hg^{\omega}$ in $\mathbb{C}(\lambda^{k})$ starting in $v^{\prime C}$ that is a lasso with $|hg|$ bounded by $2\cdot|\mathbb{C}(\lambda^{k})|$ and such that its corresponding play $\rho$ in $\operatorname{\mathcal{X}}$ belongs to $\Lambda^{k}(v)$ and has its cost $\operatorname{Cost}_{i}(\rho)$ equal to $c$. Notice that we can restrict $\lambda^{k}$ to $\lambda^{k}_{\geq\ell}$ since any path beginning in $V^{J_{\ell}}$ only visits vertices of $V^{\geq J_{\ell}}$. We thus work in the counter graph $\mathbb{C}(\lambda^{k}_{\geq\ell})$ restricted to $V^{\geq\ell}$ (see Remark 17). We will guess such a lasso $\pi$ as done in the proof of Proposition 22. More precisely, as the value of $c$ is unknown, we will first test in PSPACE whether there exists such a lasso $\pi$ with cost $c=+\infty$. If yes, we are done, otherwise by considering increasing values $d\in\mathbb{N}$, we will test in PSPACE whether there exists a lasso $\pi$ with cost $\geq d$. The last value $d$ for which the answer is yes is the required cost $c$.

• –

Let us detail the case $c=+\infty$. Similarly to the proof of Proposition 22, we guess the lasso $\pi=hg^{\omega}$ by on one hand guessing the first vertex of its cycle $g$ and on the other hand guessing the sections $\pi[\ell],\pi[\ell+1],\dots$ of $\pi$, one by one, from the starting vertex $v^{\prime C}\in V^{J_{\ell}}$. Given $m\geq\ell$, section $\pi[m]$ is guessed vertex by vertex, where each vertex belongs to $V^{J_{m}}$. By induction hypothesis, we can compute the set $\{\lambda^{k}(u)\mid u\in V^{J_{m}}\}$ and the value $\mathrm{mR}(\lambda^{k}_{\geq m})$ in PSPACE, and by Corollary 20 the previous set and each vertex of the counter graph $\mathbb{C}(\lambda^{k}_{\geq\ell})$ can be encoded in polynomial size memory. Once $\pi[m]$ is guessed we can forget the set $\{\lambda^{k}(u)\mid u\in V^{J_{m}}\}$ and guess the next section of $\pi$.

Additionally, to check that the length of $hg$ does not exceed the constant $L=2\cdot|\mathbb{C}(\lambda^{k}_{\geq\ell})|$, we have to compute $\mathrm{mR}(\lambda^{k}_{\geq\ell})$ that can be done in PSPACE by induction hypothesis. Thus we can also compute $L$ in PSPACE and by Corollary 20 we can encode it in polynomial size memory. We also store a counter $C_{L}\leq L$ (which is initialized to [math] and incremented by 1 each time we guess a new vertex of $\pi$) and a boolean $C_{i}$ (which is equal to [math] as long as player $i$ does not visit his target set and is equal to $1$ after this visit).

We stop if either if $C_{L}>L$ or if we have found the lasso. In the latter case we check whether $C_{i}=0$ or not.

• –

Let us now proceed to the case $c<+\infty$. We check whether there exists a lasso $\pi=hg^{\omega}$ with $|hg|$ bounded by $L=2\cdot|\mathbb{C}(\lambda^{k}_{\geq\ell})|$ with cost (for player $i$) $\geq d$, for values $d=0,d=1,\ldots$, until the answer is no. The last value $d$ for which the answer is yes is equal to $c$.

We know by Corollary 21, that the size of $c$ cannot exceed an exponential in the size of the input. Thus each tested value $d$ can be encoded in polynomial size memory.

To check in PSPACE the existence of such a lasso with length of $hg$ bounded by $L$ with cost $\geq d$, we proceed exactly as for the case $c=+\infty$ except that instead of the boolean $C_{i}$ we keep a counter $C_{i}\leq L$ that keeps track of the cost of player $i$ for the lasso that we are guessing.

Notice that the depth of the recursion of the procedure is at most $|\Pi|$ by the $I$-monotonicity property (2) (any path crosses at most $|\Pi|$ regions). And at each recursion level, only a polynomial size information is stored. This concludes the proof that the set $\{\lambda^{k+1}(v)\mid v\in V^{J_{\ell}}\}$ can be computed in PSPACE.

To conclude the case $k^{*}_{\ell+1}<k\leq k^{*}_{\ell}$, it remains to prove that the value $\mathrm{mR}(\lambda^{k+1}_{\geq\ell})$ can also be computed in PSPACE. Clearly we can compute $\mathrm{mR}(\lambda^{k+1}_{\ell})$ in PSPACE as we now have $\{\lambda^{k+1}(v)\mid v\in V^{J_{\ell}}\}$ in memory and we can compute $\mathrm{mR}(\lambda^{k+1}_{\geq\ell+1})$ by induction hypothesis. Notice that both values can be encoded in polynomial memory size by Corollary 20. So, as $\mathrm{mR}(\lambda^{k+1}_{\geq\ell})=\max\{\mathrm{mR}(\lambda^{k+1}_{\ell}),\mathrm{mR}(\lambda^{k+1}_{\geq\ell+1})\}$, we can compute $\mathrm{mR}(\lambda^{k+1}_{\geq\ell})$ in PSPACE and Assertion (26) is proved.

4.2. PSPACE hardness

We now prove that the constraint problem is PSPACE-hard for quantitative reachability games.

Proposition 24**.**

The constraint problem for quantitative reachability games is PSPACE-hard.

The proof of this proposition is based on a polynomial reduction from the QBF problem which is PSPACE-complete. It is close to the proof given in [BBGR18b] for the PSPACE-hardness of the constraint problem for Boolean games with reachability objectives — either a player reaches his objective or not. The main difference is here to manipulate costs instead of considering qualitative reachability.

The QBF problem is to decide whether a fully quantified Boolean formula $\psi$ is true. The formula $\psi$ can be assumed to be in prenex normal form $Q_{1}x_{1}Q_{2}x_{2}\ldots Q_{m}x_{m}\,\phi(X)$ such that the quantifiers are alternating existential and universal quantifiers ($Q_{1}=\exists$, $Q_{2}=\forall$, $Q_{3}=\exists,\ldots$), $X=\{x_{1},x_{2},\ldots,x_{m}\}$ is the set of quantified variables, and $\phi(X)=C_{1}\wedge\ldots\wedge C_{n}$ is an unquantified Boolean formula over $X$ equal to the conjunction of the clauses $C_{1},\ldots,C_{n}$.

Such a formula $\psi$ is true if there exists a value of $x_{1}$ such that for all values of $x_{2}$, there exists a value of $x_{3}$ $\ldots$, such that the resulting valuation $\nu$ of all variables of $X$ evaluates $\phi(X)$ to true. Formally, for each odd (resp. even) $k$, $1\leq k\leq m$, let us denote by $f_{k}:{\{0,1\}}^{k-1}\rightarrow\{0,1\}$ (resp. $g_{k}:{\{0,1\}}^{k-1}\rightarrow\{0,1\}$) a valuation of variable $x_{k}$ given a valuation of previous variables $x_{1},\ldots,x_{k-1}$666Notice that $f_{1}:\emptyset\rightarrow\{0,1\}$.. Given theses sequences $f=f_{1},f_{3},\ldots$ and $g=g_{2},g_{4},\ldots$, let us denote by $\nu=\nu_{(f,g)}$ the valuation of all variables of $X$ such that $\nu(x_{1})=f_{1}$, $\nu(x_{2})=g_{2}(\nu(x_{1}))$, $\nu(x_{3})=f_{3}(\nu(x_{1})\nu(x_{2}))$, $\ldots$. Then

$\psi=Q_{1}x_{1}Q_{2}x_{2}\ldots Q_{m}x_{m}\,\phi(X)$ is true

if and only if

there exist $f=f_{1},f_{3},\ldots$ such that for all $g=g_{2},g_{4},\ldots$, the valuation $\nu_{f,g}$ evaluates $\phi(X)$ to true.

Proof 4.3** (Proof of Proposition 24).**

Let us detail a polynomial reduction from the QBF problem to the constraint problem for quantitative reachability games. Let $\psi=Q_{1}x_{1}Q_{2}x_{2}\ldots Q_{m}x_{m}\,\phi(X)$ with $\phi(X)=C_{1}\wedge\ldots\wedge C_{n}$ be a fully quantified Boolean formula in prenex normal form. We build the following quantitative reachability game $\mathcal{G}_{\psi}=(\Pi,V,{(V_{i})}_{i\in\Pi},E,{(\operatorname{Cost}_{i})}_{i\in\Pi},{(F_{i})}_{i\in\Pi})$ (see Figure 5):

• •

the set $V$ of vertices:

• –

for each variable $x_{k}\in X$ under quantifier $Q_{k}$, there exist vertices $x_{k}$, $\neg x_{k}$ and $q_{k}$;

• –

for each clause $C_{k}$, there exist vertices $c_{k}$ and $t_{k}$;

• –

there exists an additional vertex $t_{n+1}$;

• •

the set $E$ of edges:

• –

from each vertex $q_{k}$ there exist an edge to $x_{k}$ and an edge to $\neg x_{k}$;

• –

from each vertex $x_{k}$ and $\neg x_{k}$, there exists an edge to $q_{k+1}$, except for $k=m$ where this edge is to $c_{1}$;

• –

from each vertex $c_{k}$, there exist an edge to $t_{k}$ and an edge to $c_{k+1}$, except for $k=n$ where there exist an edge to $t_{n}$ and an edge to $t_{n+1}$;

• –

there exists a loop on each $t_{k}$;

• •

the set $\Pi$ of $n+2$ players:

• –

each player $i$, $1\leq i\leq n$, owns vertex $c_{i}$;

• –

player $n+1$ (resp. $n+2$) is the player who owns the vertices $q_{i}$ for each existential (resp. universal) quantifier $Q_{i}$;

• –

as all other vertices have only one outgoing edge, it does not matter which player owns them;

• •

each function $\operatorname{Cost}_{i}$ is associated with the target set $F_{i}$ defined as follows:

• –

for all $i$, $1\leq i\leq n$, $F_{i}=\{\ell\in V\mid\ell\text{ is a literal of clause }C_{i}\}\cup\{t_{i}\}$;

• –

$F_{n+1}=\{t_{n+1}\}$;

• –

$F_{n+2}=\{t_{1},\ldots,t_{n}\}$.

Remark 25**.**

(1) Notice that a sequence $f$ of functions $f_{k}:{\{0,1\}}^{k-1}\rightarrow\{0,1\}$, with $k$ odd, $1\leq k\leq m$, as presented above, can be translated into a strategy $\sigma_{n+1}$ of player $n+1$ in the initialized game $(\mathcal{G}_{\psi},q_{1})$, and conversely. Similarly, a sequence $g$ of functions $g_{k}:{\{0,1\}}^{k-1}\rightarrow\{0,1\}$, with $k$ even, $1\leq k\leq m$ is nothing else than a strategy $\sigma_{n+2}$ of player $n+2$. (2) Notice also that if $\rho$ is a play in $(\mathcal{G}_{\psi},q_{1})$, then $\operatorname{Cost}_{n+1}(\rho)<+\infty$ if and only if $\operatorname{Cost}_{n+2}(\rho)=+\infty$. Moreover, suppose that $\rho$ visits $t_{n+1}$, then for all $i$, $1\leq i\leq n$, $\operatorname{Cost}_{i}(\rho)\leq 2\cdot m$ if and only if for all $i$, $1\leq i\leq n$, $\rho$ visits a vertex that is a literal of $C_{i}$, and that is the case if and only if there is a valuation of all variables of $X$ that evaluates $\phi(X)$ to true.

Consider the game $\mathcal{G}_{\psi}$ and the bound $x=(2\cdot m,\ldots,2\cdot m,2\cdot m+n,+\infty)$. Both can be constructed from $\psi$ in polynomial time. Let us now show that $\psi$ is true if and only if there exists an SPE in $(\mathcal{G}_{\psi},q_{1})$ with cost $\leq x$.

$(\Rightarrow)$* Suppose that $\psi$ is true. Then there exists a sequence $f$ of functions $f_{k}:{\{0,1\}}^{k-1}\rightarrow\{0,1\}$, with $k$ odd, $1\leq k\leq m$, such that for all sequences $g$ of functions $g_{k}:{\{0,1\}}^{k-1}\rightarrow\{0,1\}$, with $k$ even, $1\leq k\leq m$, the valuation $\nu_{f,g}$ evaluates $\phi(X)$ to true. We define a strategy profile $\sigma$ as follows:*

• •

for player $n+1$, his strategy $\sigma_{n+1}$ is the strategy corresponding to the sequence $f$ (by Remark 25);

• •

for player $n+2$, his strategy is an arbitrary strategy $\sigma_{n+2}$; we denote by $g$ the corresponding sequence $g_{k}:{\{0,1\}}^{k-1}\rightarrow\{0,1\}$, with $k$ even, $1\leq k\leq m$ (by Remark 25);

• •

for each player $i$, $1\leq i\leq n$,

• –

if $hv\in\operatorname{Hist}_{i}(q_{1})$ with $v=c_{i}$, is consistent with $\sigma_{n+1}$, then $\sigma_{i}(hv)=c_{i+1}$ if $i\neq n$ and $t_{n+1}$ otherwise

• –

else $\sigma_{i}(hv)=t_{i}$.

Let us first prove that the play $\rho=\langle\sigma\rangle_{q_{1}}$ has a cost $\leq x=(2\cdot m,\ldots,2\cdot m,2\cdot m+n,+\infty)$. By hypothesis, the valuation $\nu_{f,g}$ evaluates $\phi(X)$ to true, that is, it evaluates all clauses $C_{i}$ to true. Hence by Remark 25, $\rho$ visits a vertex of $F_{i}$ for all $i$, $1\leq i\leq n$, and by definition of $\sigma$, $\rho$ eventually loops on $t_{n+1}$. It follows that $\operatorname{Cost}_{i}(\rho)\leq 2\cdot m$ for all $i$, $1\leq i\leq n$, $\operatorname{Cost}_{n+1}(\rho)\leq 2\cdot m+n$, and $\operatorname{Cost}_{n+2}(\rho)=+\infty$. Hence $\operatorname{Cost}(\rho)\leq x$.

Let us now prove that $\sigma$ is an SPE, that is, for each history $hv\in\operatorname{Hist}(q_{1})$, there is no one-shot deviating strategy in the subgame $(\mathcal{G}_{\psi\restriction h},v)$ that is profitable to the player who owns vertex $v$ (by Proposition 1.3). This is clearly true for all $v=t_{i}$, $1\leq i\leq n+1$, since $t_{i}$ has only one outgoing edge. For the other vertices $v$, we study two cases:

• •

$hv$* is consistent with $\sigma_{n+1}$: Notice that $hv$ is maybe not consistent with $\sigma_{n+2}$, but with another arbitrary strategy $\sigma^{\prime}_{n+2}$. Let $g^{\prime}$ be the sequence corresponding to $\sigma^{\prime}_{n+2}$ by Remark 25. By hypothesis, the valuation $\nu_{f,g^{\prime}}$ evaluates $\phi(X)$ to true. Hence as explained previously for $\langle\sigma\rangle_{q_{1}}$, the cost of play $\rho=h\langle\sigma_{\restriction h}\rangle_{v}$ is such that $\operatorname{Cost}_{i}(\rho)\leq 2\cdot m$ for all $i$, $1\leq i\leq n$, $\operatorname{Cost}_{n+1}(\rho)\leq 2\cdot m+n$, and $\operatorname{Cost}_{n+2}(\rho)=+\infty$. If $v$ belongs to player $i$, $1\leq i\leq n$, this player has no incentive to deviate since he has already visited his target set along $h$ and thus cannot decrease his cost. If $v$ belongs to player $n+1$, a one-shot deviation will lead to a play eventually looping on $t_{1}$ by definition of $\sigma$, thus leading to a cost $+\infty$ which is not profitable for player $n+1$. Finally if $v$ belongs to player $n+2$, a one-shot deviation will not decrease his cost by definition of $\sigma$ ($\sigma_{n+2}$ is arbitrary).*

• •

$hv$* is not consistent with $\sigma_{n+1}$: Suppose that $v=c_{k}$. Then by definition of $\sigma$, the play $h\langle\sigma_{\restriction h}\rangle_{v}$ eventually loops on $t_{k}$ leading to a cost $\leq 2\cdot m+k$ for player $k$. In fact, if player $k$ has already seen his target set along $hv$, using a one-shot deviation in the subgame $(\mathcal{G}_{\psi\restriction h},v)$ leads to the same cost for him. Otherwise, it leads to a cost equal to $+\infty$: indeed, deviating here means going to the state $c_{k+1}$ (or $t_{n+1}$ if $k=n$, which leads to a cost of $+\infty$ for player $n$), and since $hv$ is not consistent with $\sigma_{n+1}$, by definition of $\sigma_{k+1}$, player $k+1$ will choose to go to $t_{k+1}$. This player has thus no incentive to deviate.*

Suppose that $v=q_{k}$. Then by definition of $\sigma$, the play $\rho=h\langle\sigma_{\restriction h}\rangle_{v}$ eventually loops on $t_{1}$. It follows that $\operatorname{Cost}_{n+1}(\rho)=+\infty$ and $\operatorname{Cost}_{n+2}(\rho)=2\cdot m+1$. Due to the structure of the game graph, $2\cdot m+1$ is the smallest cost that player $n+2$ is able to obtain. So if $q_{k}\in V_{n+2}$, player $n+2$ has no incentive to deviate. And if $q_{k}\in V_{n+1}$, player $n+1$ could try to use a one-shot deviating strategy, however the resulting play still eventually loops on $t_{1}$.

This proves that $\sigma$ is an SPE and we already showed that its cost was bounded by $x$.

$(\Leftarrow)$* Suppose that there exists an SPE $\sigma$ in $(\mathcal{G}_{\psi},q_{1})$ with outcome $\rho$ such that $\operatorname{Cost}(\rho)\leq x$. In particular $\operatorname{Cost}_{n+1}(\rho)<+\infty$. By Remark 25, it follows that $\operatorname{Cost}_{n+2}(\rho)=+\infty$. We have to prove that $\psi$ is true. To this end, consider the sequence $f$ of functions $f_{k}:{\{0,1\}}^{k-1}\rightarrow\{0,1\}$, with $k$ odd, $1\leq k\leq m$, that corresponds to strategy $\sigma_{n+1}$ of player $n+1$ by Remark 25. Let us show that for all sequences $g$ of functions $g_{k}:{\{0,1\}}^{k-1}\rightarrow\{0,1\}$, with $k$ even, $1\leq k\leq m$, the valuation $\nu_{f,g}$ evaluates $\phi(X)$ to true.*

By contradiction assume that it is not the case for some sequence $g^{\prime}$ and consider the related strategy $\sigma^{\prime}_{n+2}$ of player $n+2$ by Remark 25. Notice that $\sigma^{\prime}_{n+2}$ is a finitely deviating strategy. Let us consider the outcome $\rho^{\prime}$ of the strategy profile $(\sigma^{\prime}_{n+2},\sigma_{-(n+2)})$ from $q_{1}$. As $\operatorname{Cost}_{n+2}(\rho)=+\infty$, we must have $\operatorname{Cost}_{n+2}(\rho^{\prime})=+\infty$, otherwise $\sigma^{\prime}_{n+2}$ is a profitable deviation for player $n+2$ whereas $\sigma$ is an SPE. It follows that $\operatorname{Cost}_{n+1}(\rho^{\prime})<+\infty$ by Remark 25, that is, $\rho^{\prime}$ eventually loops on $t_{n+1}$.

Now recall that the valuation $\nu_{f,g^{\prime}}$ evaluates $\phi(X)$ to false, which means that it evaluates some clause $C_{k}$ of $\phi(X)$ to false. Consider the history $hc_{k}<\rho^{\prime}$. As strategy $\sigma^{\prime}_{n+2}$ only acts on the left part of the underlying graph of $\mathcal{G}_{\psi}$, we have $\rho^{\prime}=\langle\sigma^{\prime}_{n+2},\sigma_{-(n+2)}\rangle_{q_{1}}=h\langle\sigma_{\restriction h}\rangle_{c_{k}}$. In the subgame $(\mathcal{G}_{\psi\restriction h},c_{k})$, the outcome of $\sigma_{\restriction h}$ gives a cost of $+\infty$ to player $k$ because $\rho^{\prime}=h\langle\sigma_{\restriction h}\rangle_{c_{k}}$ does not visit $t_{k}$ and $\nu_{f,g^{\prime}}$ evaluates $C_{k}$ to false. In this subgame, player $k$ has thus a profitable one-shot deviation that consists to move to $t_{k}$. It follows that $\sigma$ is not an SPE which is impossible. Then $\psi$ is true.

5. Conclusion

In this paper, we study multiplayer quantitative reachability games played on finite directed graphs, where the objective of each player is to reach a specified target set of vertices as quickly as possible. The players want to minimize their cost computed as the number of edges followed to reach their target set. For this class of games, we focus on the constraint existence problem for SPEs that is to decide whether there exists an SPE in which the cost of each player lies between two given bounds. It was known that there always exists an SPE in quantitative reachability games and that the constraint existence problem is decidable. We here prove that this problem is PSPACE-complete.

We summarize the main steps to obtain the PSPACE-membership:

1. (1)

Very weak SPEs are equivalent to SPEs for quantitative reachability games. This allows us to manipulate a simpler concept in our proofs and algorithm. 2. (2)

Instead of working with the original game, we work with its extended version such that the vertices of the game are enriched with the set of players that have already visited their target set. The original game and its extented game are equivalent with respect to SPE outcomes. 3. (3)

We provide a characterization of the set of plays that are SPE outcomes in the extended game as well as an algorithm to construct this set. This characterization makes use of a labeling function assigning an integer bound to each vertex. It imposes constraints on plays of the extended game such that the plays satisfying those constraints are exactly the SPE outcomes. Our algorithm builds this labeling as a fixpoint obtained iteratively from an initial labeling. We expect that this new concept of labeling will be helpful for studying SPEs for other classes of games. 4. (4)

Given the extended game and a labeling function, we construct the counter graph such that its infinite paths coincide with the plays that satisfy the constraints imposed by the labeling. Therefore when the labeling is the fixpoint computed by our algorithm, the infinite paths of the counter graph are exactly the SPE outcomes of the extended game. We establish the crucial property that this counter graph has an exponential size. 5. (5)

To establish the PSPACE membership of the constraint problem, a careful inspection of the computation shows that one can decide the existence of an infinite lasso of polynomial size in the counter graph that satisfies the bounds provided in the constraint problem.

The PSPACE-hardness of the constraint problem is easily obtained from the proof proposed for the constraint problem for qualitative reachability games.

Acknowledgments

We thank the anonymous reviewers for their helpful comments and feedback.