Verifying Equilibria in Finite-Horizon Probabilistic Concurrent Game Systems

TL;DR

This work analyzes the verification problem for equilibria in finite-horizon probabilistic multiagent concurrent games under a $b$-bounded concurrency model. It establishes a PSPACE upper bound for verifying subgame perfect equilibria by reducing the problem to hitting-probability computations in a constructed Markov chain, with careful treatment of finite-precision probabilities and linear-system representations. In contrast, it proves that verifying Nash equilibria is EXPTIME-complete by reducing the problem to solving an exponential-size MDP that captures unilateral deviations, and then demonstrates the reduction from an APSPACE-complete problem to prove hardness. The results reveal a surprising separation: verifying the stronger SPE can be easier (PSPACE) than verifying a Nash equilibrium (EXPTIME), with implications for the design of verification tools and the understanding of equilibrium concepts in probabilistic finite-horizon settings.

Abstract

Finite-horizon probabilistic multiagent concurrent game systems, also known as finite multiplayer stochastic games, are a well-studied model in computer science due to their ability to represent a wide range of real-world scenarios involving strategic interactions among agents over a finite amount of iterations (given by the finite-horizon). The analysis of these games typically focuses on evaluating (verifying) and computing (synthesizing/realizing) which strategy profiles (functions that represent the behavior of each agent) qualify as equilibria. The two most prominent equilibrium concepts are the Nash equilibrium and the subgame perfect equilibrium, with the latter considered a conceptual refinement of the former. However, computing these equilibria from scratch is often computationally infeasible. Therefore, recent attention has shifted to the verification problem, where a given strategy profile must be evaluated to determine whether it satisfies equilibrium conditions. In this paper, we demonstrate that the verification problem for subgame perfect equilibria lies in PSPACE, while for Nash equilibria, it is EXPTIME-complete. This is a highly counterintuitive result since subgame perfect equilibria are often seen as a strict strengthening of Nash equilibria and are intuitively seen as more complicated.

Figures (3)

• Figure 1: A description of the sections to follow.
• Figure 2: An illustration of Example \ref{['markovexamplehittingprobs']}. The entire figure represents the Markov Chain $\mathcal{C}$, which has two disconnected components: $\mathcal{C'}$ and the two non-target states $x$ and $y$. We wish to calculate the hitting probabilities for some state $c \in \mathcal{C'}$ by setting up a system of linear equations. If we set the hitting probabilities up in a naïve way, we get $h_x = h_y = \frac{1}{2}h_x + \frac{1}{2}h_y$, a pair of equations with an infinite number of solutions. Thus, the system of equations to solve for the hitting probabilities in $\mathcal{C}$ is underdetermined.
• Figure 3: The crucial mechanism of the reduction, Agent $n+1$'s first choice. The Agent can either choose the fixed payoff mechanism with $\alpha$, or start the probabilistic simulation of $M$ by the other $n$ agents with $\beta$ with the intention of reaching an accepting configuration. Since $M$ is an alternating Turing machine, it admits a computation tree. If Agent $n+1$ chooses $\beta$, the game proceeds by probabilistically sampling one of the branches in the computation tree. The numbers are chosen in such a way that if even one branch in the computation tree is nonaccepting (meaning $M$ is nonaccepting), Agent $n+1$ gets a better chance of reaching their goal through choosing $\alpha$ and taking the fixed payoff mechanism.

Theorems & Definitions (30)

• Definition 2.1
• Definition 2.2
• Definition 2.3
• Definition 2.4
• Definition 2.5
• Definition 2.6
• Definition 2.7
• Definition 2.8
• Definition 2.9
• Lemma 3.1