Verifying Equilibria in Finite-Horizon Probabilistic Concurrent Game Systems

Fuente: arXiv
Saved in:
Bibliographic Details
Main Authors: Rajasekaran, Senthil, Vardi, Moshe Y.
Format: Preprint
Published: 2025
Subjects:
Online Access:
Tags: Add Tag
No Tags, Be the first to tag this record!
_version_ 1866917534909857792
author Rajasekaran, Senthil
Vardi, Moshe Y.
author_facet Rajasekaran, Senthil
Vardi, Moshe Y.
contents 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.
format Preprint
id arxiv_https___arxiv_org_abs_2503_14690
institution arXiv
publishDate 2025
record_format arxiv
spellingShingle Verifying Equilibria in Finite-Horizon Probabilistic Concurrent Game Systems
Rajasekaran, Senthil
Vardi, Moshe Y.
Computer Science and Game Theory
Logic in Computer Science
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.
title Verifying Equilibria in Finite-Horizon Probabilistic Concurrent Game Systems
topic Computer Science and Game Theory
Logic in Computer Science
url https://arxiv.org/abs/2503.14690