pith. sign in

arxiv: 2503.14690 · v8 · pith:UMPARBBSnew · submitted 2025-03-18 · 💻 cs.GT · cs.LO

Verifying Equilibria in Finite-Horizon Probabilistic Concurrent Game Systems

Senthil Rajasekaran , Moshe Y. Vardi This is my paper

Pith reviewed 2026-05-22 23:15 UTC · model grok-4.3

classification 💻 cs.GT cs.LO
keywords Nash equilibriumsubgame perfect equilibriumverificationprobabilistic gamesconcurrent gamescomplexityPSPACEEXPTIME
0
0 comments X

The pith

The verification problem for subgame perfect equilibria lies in PSPACE while for Nash equilibria it is EXPTIME-complete in finite-horizon probabilistic concurrent games.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper studies the verification of whether given strategy profiles form equilibria in finite-horizon probabilistic concurrent game systems. It establishes that subgame perfect equilibrium verification belongs to PSPACE. Nash equilibrium verification, however, is EXPTIME-complete. The result is counterintuitive because subgame perfect equilibria strengthen Nash equilibria, yet their verification appears easier.

Core claim

In finite-horizon probabilistic multiagent concurrent game systems, the verification problem for subgame perfect equilibria lies in PSPACE, while for Nash equilibria, it is EXPTIME-complete. This separation arises even though subgame perfect equilibria are a conceptual refinement of Nash equilibria.

What carries the argument

The complexity classification of the equilibrium verification problem for explicitly given strategy profiles in finite-horizon stochastic games.

Load-bearing premise

The finite-horizon restriction together with the explicit input encoding of strategy profiles enables the PSPACE membership for subgame perfect equilibrium verification.

What would settle it

An algorithm that verifies Nash equilibria in polynomial space for some family of these games, or a proof that SPE verification requires more than polynomial space.

Figures

Figures reproduced from arXiv: 2503.14690 by Moshe Y. Vardi, Senthil Rajasekaran.

Figure 1
Figure 1. Figure 1: A chart depiction of the outline with some figures intended to facilitate conceptual understanding. 3.2. Histories and Subgames. As outlined in Section 3.1, the first step to our approach is to guess a history h so that we can check whether π|h is a Nash equilibrium in G|h. Since [PITH_FULL_IMAGE:figures/full_fig_p010_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: An illustration of Example 3.4. The entire figure represents the Markov Chain C, which has two disconnected components: C ′ and the two non-target states x and y. We wish to calculate the hitting probabilities for some state c ∈ C′ by setting up a system of linear equations. If we set the hitting probabilities up in a na¨ıve way, we get hx = hy = 1 2 hx + 1 2 hy, a pair of equations with an infinite number… view at source ↗
Figure 3
Figure 3. Figure 3: The crucial mechanism of the reduction, Agent n + 1’s first choice. The Agent can either choose the fixed payoff mechanism with α, or start the probabilistic simulation of M by the other n agents with β with the intention of reaching an accepting configuration. Since M is an alternating Turing machine, it admits a computation tree. If Agent n+ 1 chooses β, the game proceeds by probabilistically sampling on… view at source ↗
Figure 4
Figure 4. Figure 4: A graphical depiction of the interactions between π and G. As mentioned before, we use the state space of the individual πi to track the ID of M. (1) The machine M has some ID, depicted by the top row of small cells. The head is currently over cell i, which is in blue. Cells i − 1 and i + 1 are depicted in green. The state of G is ⟨i, ∅⟩ ∈ V1, indicating that it is Agent i’s turn to select an action. To do… view at source ↗
read the original abstract

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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 3 minor

Summary. The manuscript studies the verification problem for strategy profiles in finite-horizon probabilistic concurrent game systems (stochastic games). It claims to establish that verifying whether a given strategy profile is a subgame-perfect equilibrium lies in PSPACE, while verifying Nash equilibrium is EXPTIME-complete. The finite-horizon restriction and the encoding of strategy profiles are central to obtaining the separation.

Significance. If the complexity bounds hold, the result is notable for separating the verification complexity of two equilibrium notions in the opposite direction from their logical strength (SPE refines NE). The finite-horizon setting and explicit strategy-profile input allow a PSPACE procedure for SPE that does not obviously extend to NE. Credit is due for targeting a clean complexity separation rather than approximation or synthesis.

minor comments (3)
  1. The abstract and introduction repeatedly describe the result as 'highly counterintuitive'; a brief paragraph in §1 or §2 explaining why the PSPACE algorithm for SPE does not immediately yield an EXPTIME algorithm for NE would help readers see where the separation arises.
  2. Notation for the game model (states, actions, transition probabilities, horizon length) should be collected in a single preliminary section with explicit definitions before the complexity arguments begin.
  3. The manuscript should state explicitly whether the PSPACE membership for SPE verification is shown by a direct algorithm or by reduction to a known PSPACE-complete problem; likewise for the EXPTIME-hardness of NE verification.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment of the significance of our complexity separation and for recommending minor revision. The finite-horizon restriction and explicit strategy-profile input are indeed central to the PSPACE procedure for SPE verification that does not extend to NE. No major comments were listed in the report.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper establishes complexity bounds (PSPACE for subgame-perfect equilibrium verification, EXPTIME-complete for Nash) via algorithmic constructions and reductions on finite-horizon stochastic games. No equations, definitions, or claims in the abstract reduce by construction to fitted parameters, self-citations, or renamed inputs; the results are standard complexity-theoretic statements whose proofs are externally checkable and independent of the target claims themselves.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The result rests on standard definitions of PSPACE and EXPTIME, the finite-horizon stochastic game model, and the usual encoding of strategy profiles as inputs; no free parameters or invented entities appear in the abstract.

axioms (2)
  • domain assumption Standard definitions of Nash equilibrium and subgame perfect equilibrium apply directly to finite-horizon probabilistic concurrent game systems.
    Invoked when stating the verification problems.
  • standard math PSPACE and EXPTIME are the relevant complexity classes for the decision problems.
    Used to classify the verification problems.

pith-pipeline@v0.9.0 · 5736 in / 1292 out tokens · 68096 ms · 2026-05-22T23:15:44.111724+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Modeling Concurrent Multi-Agent Systems

    cs.GT 2026-02 unverdicted novelty 7.0

    A novel circuit-based model for multi-agent systems yields complexity bounds on realizability and verification that address endemic issues in the explicit model and equilibrium analysis literature.

Reference graph

Works this paper leans on

15 extracted references · 15 canonical work pages · cited by 1 Pith paper

  1. [1]

    Nash equilibria in concurrent games with b¨ uchi objectives

    [BBMU11] Patricia Bouyer, Romain Brenguier, Nicolas Markey, and Michael Ummels. Nash equilibria in concurrent games with b¨ uchi objectives. InIARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2011). Schloss Dagstuhl- Leibniz-Zentrum fuer Informatik,

    work page 2011

  2. [2]

    [BKN+19] Nikhil Balaji, Stefan Kiefer, Petr Novotn´ y, Guillermo A

    doi:10.2168/ LMCS-11(2:9)2015. [BKN+19] Nikhil Balaji, Stefan Kiefer, Petr Novotn´ y, Guillermo A. P´ erez, and Mahsa Shirmohammadi. On the complexity of value iteration. In Christel Baier, Ioannis Chatzigiannakis, Paola Flocchini, and Stefano Leonardi, editors,46th International Colloquium on Automata, Languages, and Programming, ICALP 2019, July 9-12, 2...

    work page 2015

  3. [3]

    Bouyer, N

    [BMS14] P. Bouyer, N. Markey, and D. Stan. Mixed Nash equilibria in concurrent terminal-reward games. InProceedings of 34th International Conference on Foundation of Software Technology and Theoretical Computer Science, FSTTCS 2014, volume 29 ofLIPIcs, pages 351–363,

    work page 2014

  4. [4]

    The non-cooperative rational synthesis problem for subgame perfect equilibria and omega-regular objectives.CoRR, abs/2412.08547,

    [BRRvdB24] V´ eronique Bruy` ere, Jean-Fran¸ cois Raskin, Alexis Reynouard, and Marie van den Bogaard. The non-cooperative rational synthesis problem for subgame perfect equilibria and omega-regular objectives.CoRR, abs/2412.08547,

    work page arXiv

  5. [5]

    Rational verification for nash and subgame-perfect equilibria in graph games

    [BRvdB23] L´ eonard Brice, Jean-Fran¸ cois Raskin, and Marie van den Bogaard. Rational verification for nash and subgame-perfect equilibria in graph games. In J´ erˆ ome Leroux, Sylvain Lombardy, and David Peleg, editors,48th International Symposium on Mathematical Foundations of Computer Science, MFCS 2023, August 28 to September 1, 2023, Bordeaux, Franc...

    work page 2023

  6. [6]

    Schmerl, and Ashutosh Pandey

    [CGSP15] Javier C´ amara, David Garlan, Bradley R. Schmerl, and Ashutosh Pandey. Optimal planning for architecture-based self-adaptation via model checking of stochastic games. In Roger L. Wainwright, Juan Manuel Corchado, Alessio Bechini, and Jiman Hong, editors,Proceedings of the 30th Annual ACM Symposium on Applied Computing, Salamanca, Spain, April 13...

    work page 2015

  7. [7]

    Chandra and Larry J

    [CS76] Ashok K. Chandra and Larry J. Stockmeyer. Alternation. In17th Annual Symposium on Foundations of Computer Science (sfcs 1976), pages 98–108,

    work page 1976

  8. [9]

    [GNPW18] Julian Gutierrez, Muhammad Najib, Giuseppe Perelli, and Michael J

    URL: https://arxiv.org/abs/2107.09119. [GNPW18] Julian Gutierrez, Muhammad Najib, Giuseppe Perelli, and Michael J. Wooldridge. EVE: A tool for temporal equilibrium analysis. In Shuvendu K. Lahiri and Chao Wang, editors,Automated VERIFICATION IN FINITE-HORIZON PROBABILISTIC SYSTEMS 33 Technology for Verification and Analysis - 16th International Symposium,...

    work page arXiv 2018

  9. [10]

    Wooldridge

    [GPW17] Julian Gutierrez, Giuseppe Perelli, and Michael J. Wooldridge. Iterated games with LDL goals over finite traces. In Kate Larson, Michael Winikoff, Sanmay Das, and Edmund H. Durfee, editors,Proceedings of the 16th Conference on Autonomous Agents and MultiAgent Systems, AAMAS 2017, S˜ ao Paulo, Brazil, May 8-12, 2017, pages 696–704. ACM,

    work page 2017

  10. [11]

    [GV13] Giuseppe De Giacomo and Moshe Y

    URL: http://ethos.bl.uk/OrderDetails.do?uin=uk.bl.ethos.706789. [GV13] Giuseppe De Giacomo and Moshe Y. Vardi. Linear temporal logic and linear dynamic logic on finite traces. In Francesca Rossi, editor,IJCAI 2013, Proceedings of the 23rd International Joint Conference on Artificial Intelligence, Beijing, China, August 3-9, 2013, pages 854–

    work page 2013

  11. [12]

    Prism-games 3.0: Stochastic game verification with concurrency, equilibria and time

    [KNPS20] Marta Kwiatkowska, Gethin Norman, David Parker, and Gabriel Santos. Prism-games 3.0: Stochastic game verification with concurrency, equilibria and time. In Shuvendu K. Lahiri and Chao Wang, editors,Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II, volume 12225 ofLe...

    work page 2020

  12. [13]

    Nash (1950): Equilibrium Points in n-Person Games

    URL: https://www.pnas.org/content/36/1/48, arXiv:https: //www.pnas.org/content/36/1/48.full.pdf,doi:10.1073/pnas.36.1.48. [Nas51] John Nash. Non-cooperative games.Annals of Mathematics, 54:286–295,

    work page doi:10.1073/pnas.36.1.48

  13. [14]

    Multi-agent verification and control with probabilistic model checking

    [Par23] David Parker. Multi-agent verification and control with probabilistic model checking. In Quantitative Evaluation of Systems, 08 2023.doi:10.48550/arXiv.2308.02829. [PR89] Amir Pnueli and Roni Rosner. On the synthesis of a reactive module. InConference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages, Austin, Texa...

    work page doi:10.48550/arxiv.2308.02829 2023

  14. [15]

    doi:10.24963/ijcai.2023/32

    Main Track. doi:10.24963/ijcai.2023/32. [Ros92] R. Rosner.Modular Synthesis of Reactive Systems. PhD thesis, Weizmann Institute of Science,

    work page doi:10.24963/ijcai.2023/32 2023

  15. [16]

    Finite- horizon equilibria for neuro-symbolic concurrent stochastic games

    [YSD+22] Rui Yan, Gabriel Santos, Xiaoming Duan, David Parker, and Marta Kwiatkowska. Finite- horizon equilibria for neuro-symbolic concurrent stochastic games. InProceedings of Machine Learning Research, 05 2022.doi:10.48550/arXiv.2205.07546

    work page doi:10.48550/arxiv.2205.07546 2022