Verification of Correlated Equilibria in Concurrent Reachability Games
For researchers in formal verification and multi-agent systems, this work provides complexity-theoretic insights into equilibrium verification, revealing a counterintuitive gap between correlated and subgame-perfect correlated equilibria.
The paper studies correlated equilibria in concurrent reachability games, introducing subgame-perfect correlated equilibria and characterizing their verification complexity. It shows that correlated equilibrium verification is P-complete, while subgame-perfect correlated equilibrium verification is in log-squared-space, a surprising separation that disappears under succinct representations.
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.