As part of an effort to apply the rigorous guarantees of formal verification to multi-agent systems, the field of equilibrium analysis, also called rational verification, studies equilibria in multiplayer games to reason about system-level properties such as safety and scalability. While most prior work focuses on deterministic settings, recent probabilistic extensions enable the use of richer equilibrium concepts. In this paper, we study one such equilibrium concept -- correlated equilibria -- and introduce a natural refinement -- subgame-perfect correlated equilibria -- in the context of the verification problem. We characterize the computational complexity of verifying such equilibria and show a somewhat surprising separation (under standard complexity-theoretic assumptions): despite being more general, correlated equilibria yield a strictly harder P-complete verification problem than the subgame-perfect correlated equilibria verification problem, which can be solved in log-squared-space. We further analyze the setting where inputs are given succinctly via Bayesian networks, as the study of succinct representations is an important direction to connect static complexity-theoretic analysis to real-world program representations, and show that this complexity gap disappears under such representations.

翻译：作为将形式化验证的严格保证应用于多智能体系统的一项努力，均衡分析领域（亦称理性验证）研究多人博弈中的均衡，以推理安全性和可扩展性等系统级属性。尽管大多数先前工作聚焦于确定性设定，近期概率性扩展使得更丰富的均衡概念得以应用。在本文中，我们研究一种此类均衡概念——相关均衡——并引入一种自然精炼——子博弈完美相关均衡——置于验证问题的背景下。我们刻画了验证此类均衡的计算复杂性，并展示了一个（在标准复杂性理论假设下）略显令人惊讶的分离：尽管更一般化，相关均衡导致的验证问题严格更难（P-完全），而子博弈完美相关均衡的验证问题可在对数平方空间内求解。我们进一步分析了通过贝叶斯网络以简洁方式给出输入的情形（因为简洁表示研究是连接静态复杂性分析与真实程序表示的重要方向），并证明在此类表示下该复杂性差距消失。