Verification of Correlated Equilibria in Concurrent Reachability Games

TL;DR

This paper investigates the complexity of verifying correlated equilibria and subgame-perfect correlated equilibria in multiplayer games, revealing a surprising complexity separation and the impact of succinct input representations.

Contribution

It introduces subgame-perfect correlated equilibria in the context of formal verification and characterizes their computational complexity, including effects of succinct representations.

Findings

Correlated equilibria verification is P-complete.

Subgame-perfect correlated equilibria verification can be done in log-squared-space.

The complexity gap disappears with succinct Bayesian network inputs.

Abstract

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.