Nash Equilibria in Finite-Horizon Multiagent Concurrent Games

TL;DR

This paper presents a novel approach for finding pure strategy Nash equilibria in finite-horizon multiagent concurrent games by leveraging safety games and lasso testing in Büchi automata, simplifying previous automata-based methods.

Contribution

It introduces a method that separates strategic from temporal reasoning using DFAs, enabling more efficient analysis of Nash equilibria in finite-horizon games.

Findings

The approach reduces the problem to safety games and lasso testing.

The complexity of the problem is characterized as PSPACE complete.

It offers a new automata-based framework for finite-horizon game analysis.

Abstract

The problem of finding pure strategy Nash equilibria in multiagent concurrent games with finite-horizon temporal goals has received some recent attention. Earlier work solved this problem through the use of Rabin automata. In this work, we take advantage of the finite-horizon nature of the agents' goals and show that checking for and finding pure strategy Nash equilibria can be done using a combination of safety games and lasso testing in B\"uchi automata. To separate strategic reasoning from temporal reasoning, we model agents' goals by deterministic finite-word automata (DFAs), since finite-horizon logics such as LTL\textsubscript{f} and LDL\textsubscript{f} are reasoned about through conversion to equivalent DFAs. This allow us characterize the complexity of the problem as PSPACE complete.