Senthil Rajasekaran

Senthil Rajasekaran, Moshe Y. Vardi

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.

Senthil Rajasekaran, Moshe Y. Vardi

Recent work in the field of multi-agent systems has sought to use techniques and concepts from the field of formal methods to provide rigorous theoretical analysis and guarantees on complex systems where multiple agents strategically interact, leading to the creation of the field of equilibrium analysis, which studies equilibria concepts from the field of game theory through a complexity-theoretic lens. Multi-agent systems, however, are complex mathematical objects, and, therefore, defining them in a precise mathematical manner is non-trivial. As a result, researchers often considered more restrictive models that are easier to model but lack expressive power or simply omit critical complexity-theoretic results in their analysis. This paper addresses this problem by carefully analyzing and contrasting complexity-theoretic results in the explicit model, a mathematically precise formulation of the models commonly used in the literature, and the circuit-based model, a novel model that addresses the problems found in the literature. The utility of the circuit-based model is demonstrated through a comprehensive analysis that considers upper and lower bounds for the realizability and verification problems, the two most important decision problems in equilibrium analysis, for both models. By conducting this analysis, we see that problematic issues that are endemic to the explicit model and the equilibrium analysis literature as a whole are adequately handled by the circuit-based model.

Senthil Rajasekaran, Jean-François Raskin, Moshe Y. Vardi

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.