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.

翻译：近期多智能体系统领域的研究采用形式化方法中的技术与概念，为多个智能体战略性交互的复杂系统提供严格的理论分析与保证，由此催生了均衡分析这一研究方向。该领域通过复杂性理论的视角研究博弈论中的均衡概念。然而，多智能体系统作为复杂的数学对象，其精确定义颇具挑战性。为此，研究者常采用更具约束性的简化模型（虽易于建模却缺乏表达能力），或在分析中直接省略关键的复杂性理论结论。本文通过严谨对比分析显式模型（文献中常用模型的数学精确形式化表述）与电路模型（一种解决文献中现存问题的新颖模型）的复杂性理论结果，系统解决上述问题。通过全面分析两类模型中均衡分析最重要的两个判定问题（可实现性与验证问题）的上下界，我们证明了电路模型的有效性。该分析表明，显式模型及整个均衡分析文献中普遍存在的核心问题，均能在电路模型中得到妥善解决。