Senthil Rajasekaran ; Moshe Y. Vardi - Verifying Equilibria in Finite-Horizon Probabilistic Concurrent Game Systems

lmcs:15486 - Logical Methods in Computer Science, May 20, 2026, Volume 22, Issue 2 - https://doi.org/10.46298/lmcs-22(2:19)2026
Verifying Equilibria in Finite-Horizon Probabilistic Concurrent Game SystemsArticle

Authors: Senthil Rajasekaran ; Moshe Y. Vardi

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. Computing these equilibria from scratch is, however, 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.


Volume: Volume 22, Issue 2
Published on: May 20, 2026
Accepted on: April 8, 2026
Submitted on: April 10, 2025
Keywords: Computer Science and Game Theory, Logic in Computer Science

Consultation statistics

This page has been seen 4 times.
This article's PDF has been downloaded 2 times.