Nash Equilibrium and Bisimulation Invariance
Abstract
Game theory provides a well-established framework for the analysis of concurrent and multi-agent
systems. The basic idea is that concurrent processes (agents) can be understood as corresponding
to players in a game; plays represent the possible computation runs of the system; and strategies
define the behaviour of agents. Typically, strategies are modelled as functions from sequences of
system states to player actions. Analysing a system in such a way involves computing the set of
(Nash) equilibria in the game. However, we show that, with respect to the above model of
strategies---the standard model in the literature---bisimilarity does not preserve the existence of
Nash equilibria. Thus, two concurrent games which are behaviourally equivalent from a semantic
perspective, and which from a logical perspective satisfy the same temporal formulae, nevertheless
have fundamentally different properties from a game theoretic perspective. In this paper we
explore the issues raised by this discovery, and investigate three models of strategies with respect
to which the existence of Nash equilibria is preserved under bisimilarity. We also use some of
these models of strategies to provide new semantic foundations for logics for strategic reasoning,
and investigate restricted scenarios where bisimilarity can be shown to preserve the existence of
Nash equilibria with respect to the conventional model of strategies in the literature.