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完全的。这是一个极具反直觉的结果，因为子博弈完美均衡通常被视为纳什均衡的严格强化，且直观上被认为更为复杂。