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.

翻译：有限视界概率多智能体并发博弈系统（亦称有限多人随机博弈）是计算机科学中一种成熟的研究模型，其优势在于能够刻画涉及智能体在有限迭代次数（由有限视界决定）内进行策略交互的广泛现实场景。此类博弈的分析通常聚焦于评估（验证）与计算（综合/实现）哪些策略分布（表示各智能体行为的函数）构成均衡。两种最显著的均衡概念是纳什均衡与子博弈完美均衡，后者通常被视为前者的概念性精炼。然而，从头计算这些均衡往往在计算上不可行。因此，近年研究重心转向验证问题——即需评估给定策略分布是否满足均衡条件。本文证明：子博弈完美均衡的验证问题属于PSPACE，而纳什均衡的验证问题则为EXPTIME完全问题。这一结果高度反直觉，因为子博弈完美均衡通常被视为纳什均衡的严格强化，直觉上更为复杂。