# PSPACE algorithm for SPEs in quantitative reachability games

We study n-player turn-based games played on a finite directed graph such that each player aims at satisfying a quantitative reachability objective. In this setting, each player wants to reach a subset of graph's vertices - called target set - "as soon as possible". Instead of the well-known notion of Nash equilibrium (NE) we focus on the notion of subgame perfect equilibrium (SPE). We are interested in the complexity class membership of the constrained existence problem for SPEs in games with quantitative reachability objectives. This problem can be expressed as follows: given an upper and a lower thresholds x, y in (N U {+infinity})^n, we want to determine if there exists an SPE such that the cost of each player to reach his target set (or not) along the outcome of this SPE is componentwise between those two thresholds. We show that this problem is PSPACE-complete.