has to occur

Nash Equilibrium and Bisimulation Invariance]Nash Equilibrium and Bisimulation Invariance

J. Gutierrez]Julian Gutierrez
Department of Computer Science, University of Oxford

P. Harrenstein]Paul Harrenstein
Department of Computer Science, University of Oxford

G. Perelli]Giuseppe Perelli
Department of Informatics, University of Leicester

M. Wooldridge]Michael Wooldridge
Department of Computer Science, University of Oxford

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 setting involves computing the set of (Nash) equilibria in
the concurrent game. However, we show that, with respect to the
above model of strategies (arguably, the “standard” model in the
computer science 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 logic formulae,
may  nevertheless have fundamentally different properties (solutions)
from a game theoretic perspective. Our aim in this paper is to
explore the issues raised by this discovery. After illustrating the
issue by way of a motivating example, we present three models of
strategies with respect to which the existence of Nash equilibria is
preserved under bisimilarity. We 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 computer science literature.

§ INTRODUCTION

The concept of bisimilarity plays a central role in both the
theory of concurrency [34, 28] and
logic [44, 28].  In the context of concurrency, bisimilar
systems are regarded as behaviourally equivalent—appearing to
have the same behaviour when interacting with an arbitrary
environment. From a logical/verification perspective, bisimilar
systems are known to satisfy the same temporal logic properties
with respect to languages such as LTL, CTL, or the
$\mu$-calculus [40, 14, 29].
These features, in turn, make it possible to verify
temporal logic properties of concurrent systems using
bisimulation-based approaches [42]. For example, temporal logic model
checking techniques [13] may be optimised by applying them to the smallest
bisimulation equivalent model of the system being analysed; or,
indeed, to any other model within the system's bisimulation
equivalence class. This is possible because the properties that one is
interested in checking are bisimulation invariant.

Model checking [13] is not the only verification technique
that can benefit from bisimulation invariance: consider abstraction
and refinement techniques [15, 16] (where a set of states is
either collapsed or broken down in order to build a somewhat simpler
set of states); coinduction methods [41] (which can be used to
check the correctness of an implementation with respect to a given
specification); or reduced BDD representations of a system [10]
(where isomorphic, and therefore bisimilar, subgraphs are merged,
thereby eliminating part of the initial state space of the
system). Bisimulation invariance is therefore a powerful and fundamental concept
in the formal analysis and verification of concurrent and multi-agent
systems, which plays an important role in many verification tools.

Game theory provides another important framework for the analysis and
verification of concurrent and multi-agent systems. Within this
framework, a concurrent/multi-agent system is viewed as a game, where
processes/agents correspond to players, system executions (that is,
computation runs) to plays, and individual process behaviours are
modelled as player strategies, which are used to resolve the possible
nondeterministic choices available to each player.

A widely-used model for strategies in concurrent games is to view a
strategy for a process/agent/player $i$ as a function $f_i$ which maps finite
histories $s_0,s_1,\ldots ,s_k$ of system states to actions
$f_i(s_0,s_1,\ldots,s_k)$ available to $i$ at
state $s_k$. (In what follows, we use the terms process, agent, and
player interchangeably.) We refer to this as the “conventional”
model of strategies, as it is the best-known and most widely-used
model in logic, AI, and computer science (and indeed in extensive form
games [37]).  For instance, specification languages such as
Alternating-time Temporal Logic (ATL [1]), and formal models
such as concurrent game structures [1] use this model of
strategies. If we model a concurrent/multi-agent system as a game in
this way, then the analysis and verification of the system reduces to
computing the set of (Nash) equilibria in the
game; in some cases, the analysis reduces to the computation of a
winning strategy in the game, that is, a strategy that ensures that
the players who follow such a plan will achieve their goal no matter
how the other players in the system play, i.e., against any
other possible counter-strategy.

Now, because bisimilar
systems are regarded as
behaviourally equivalent, and bisimilar systems satisfy the same set
of temporal logic properties, it is natural to ask whether the Nash
equilibria of bisimilar structures can be identified in a similar way; that is, we ask the
following question:

Is Nash equilibrium invariant under bisimilarity?

We show that, for the “conventional” model of strategies, the answer
to this question is, in general, no. More specifically, the answer
critically depends on precisely how players' strategies are
modelled. With the conventional model of strategies, we find the answer is
positive only for some two-player games, but negative in general
for games with more than two players. This means, for instance, that,
in the general case, bisimulation-based techniques cannot be used when
one is also reasoning about the Nash equilibria of concurrent systems
that are formally modelled as multi-player (concurrent) games.

For instance, given a concurrent and reactive system, represented as a
collection of individual system components, say $P_1,\ldots,P_n$, one
may want to know if a given temporal logic property, say $\phi$, is
satisfied by these system components whenever they choose to use
strategies that form an equilibrium, that is, we want to know whether
for some/every computation run $\rho\in \mathit{NE}(P_1,\ldots,P_n)$
we have $\rho\models\phi$, where $\mathit{NE}(P_1,\ldots,P_n)$ denotes
the set of all computation runs that may be generated as a result of
$P_1,\ldots,P_n$ selecting strategies that form a Nash equilibrium.
Because we are interested in concurrent systems, and bisimilarity is
one of the most important behavioural equivalences in
concurrency [33, 28, 17, 47], it is
highly desirable  that properties which hold in equilibrium are
sustained across all systems that are bisimilar to $P_1,\ldots,P_n$, meaning
that for every (temporal logic) property $\phi$ and every process
$P'_i$, if $P'_i$ is bisimilar to $P_i\in\{P_1,\ldots,P_n\}$, then
$\phi$ is satisfied in equilibrium by $P_1,\ldots P_i \ldots P_n$ if
and only if is also satisfied in equilibrium by
$P_1,\ldots P'_i \ldots,P_n$, the system in which $P_i$ is replaced by
$P'_i$, that is, across all bisimilar systems
to $P_1,\ldots,P_n$. This property, called invariance under
bisimilarity, has been widely used for decades for the semantic
analysis (e.g., for modular and compositional reasoning) and
formal verification (e.g., for temporal logic model checking) of
concurrent systems. Unfortunately, as shown here, and already
discussed in [22], the satisfaction of temporal logic
properties in equilibrium is not invariant under bisimilarity, thus
posing a verification challenge for the modular and compositional
reasoning of concurrent systems, since individual system components in
a concurrent system cannot be replaced by (behaviourally equivalent)
bisimilar ones, while preserving the temporal logic properties that
the overall system satisfies in equilibrium.  This is also
a problem from a synthesis point of view.  Indeed, a strategy for a
system component $P_i$ may not be a valid strategy for a bisimilar
system component $P'_i$.  As a consequence, the problem of building
strategies for individual processes in the concurrent
system $P_1,\ldots P_i \ldots P_n$ may not, in general, be the same as
building strategies for a bisimilar
system $P_1,\ldots P'_i \ldots P_n$, again, dashing any hope of
modular reasoning on concurrent systems.

Motivated by these observations—which bring together in a striking
way a fundamental concept in game theory and a fundamental concept in
logic/concurrency—the purpose of the present paper is to investigate
these issues in detail. We first present a motivating example, to
illustrate the basic point that using the conventional model of
strategies, bisimulation need not preserve Nash equilibria. We then
present three alternative models of strategies in which Nash
equilibria and their existence are preserved under bisimilarity.  We
also study the above question for different classes of systems, for
instance deterministic and nondeterministic ones, and explore
applications to logic. Specifically, we investigate the implications
of replacing the conventional model of strategies with some of the
models we propose in this paper in logics for strategic
reasoning [35, 12], in particular, the semantic
implications with respect to Strategy Logic (SL [35]).

We also show that, within the conventional model of strategies, Nash
equilibrium is preserved by bisimilarity in certain two-player games
as well as in the class of concurrent game structures that are induced
by iterated Boolean games [23], a framework that can be used
to reason about the strategic behaviour of AI, autonomous, and
multi-agent systems [48].
Our main invariance results are summarised in Table <ref>.

§.§ A Motivating Example

So far we have mentioned some cases where one needs or desires a
property to be invariant under bisimilarity. However, one may still
wonder why it is so important that the particular property of having a Nash equilibrium
is preserved under bisimilarity. One reason has its roots in
automated formal verification. To illustrate this, imagine that the
system of Figure <ref> is given as input to a
verification tool. It is likely that such a tool will try to perform
as many optimisations as possible to the system before any analysis is
performed. Perhaps the simplest of such optimisations—as is being done
by virtually every model checking tool—is to reduce the input system
by merging isomorphic subtrees.
This is done, e.g., when generating the ROBDD
representation of a system.  If such an optimisation is made,
the tool will construct the (bisimilar) system in
Figure <ref>.
(Observe that the subgraphs rooted at $s_1$ and $s'_1$ are isomorphic.)
However, with respect to the existence
of Nash equilibria, such a transformation is unsound in the
general case.

every ellipse node=[draw,inner xsep=3.5em,inner ysep=1.2em,fill=black!15!white,draw=black!15!white]
every circle node=[fill=white,draw,minimum size=1.6em,inner sep=0pt]

(0,0) node(0)
++ 	( 0:.9)	  	node[label=-90:$\bar p\bar q$,circle](v0)$s_0$
++	(  0:3)   	node[label=-90:$\bar p\bar q$,circle](v1)$s'_1$
+( 90:3)  	node[label=-90:$\bar p\bar q$,circle](w1)$s_1$
++( 0:5)  	node[label=-90:$\bar p     q$,circle](v3)$s_3$
+( 90:3)  	node[label=-90:$     p\bar q$,circle](v2)$s_2$
+(-90:4.5)	node[label=-90:$\bar p\bar q$,circle](v4)$s_4$

[-latex] (v0) –node[inner xsep=0pt, inner ysep=0pt, pos=.5,fill=white]()
\mwbactions{\aonetwooo}{\atwo}{\bthree}\\[-.2em]
\mwbactions{\aonethree}{\atwo}{\bthree}\\[-.2em]
\mwbactions{\bonetwooo}{\btwo}{\athree}\\[-.2em]
\mwbactions{\bonethree}{\btwo}{\athree}
\end{array}$ (v1);

[-latex] (v0) –node[inner xsep=0pt, inner ysep=0pt, pos=.5,fill=white]()
\mwbactions{\aonetwooo}{\btwo}{\athree}\\[-.2em]
\mwbactions{\aonethree}{\btwo}{\athree}\\[-.2em]
\mwbactions{\bonetwooo}{\atwo}{\bthree}\\[-.2em]
\mwbactions{\bonethree}{\atwo}{\bthree}
\end{array}$ (w1);

[-latex] (v0) to[bend right=25]node[inner xsep=0pt, inner ysep=0pt, pos=.545,fill=white]()
\mwbactions{\ast}{\atwo}{\athree}\\[-.2em]
% \mwbactions{\aonethree}{\atwo}{\athree}\\[-.2em]
% \mwbactions{\bonetwooo}{\btwo}{\bthree}\\[-.2em]
\mwbactions{\ast}{\btwo}{\bthree}
\end{array}$ (v4);

[-latex] (v1) –node[inner xsep=0pt, inner ysep=0pt, pos=.7,fill=white]().85$\begin{array}{l}\mwbactions{\aonetwooo}{\btwo}{\ast}\\[-.2em]\mwbactions{\bonetwooo}{\atwo}{\ast}\end{array}$ (v2);

[-latex] (v1) –node[inner xsep=0pt, inner ysep=0pt, pos=.7,fill=white]().85$\begin{array}{l}\mwbactions{\aonethree}{\ast}{\bthree}\\[-.2em]\mwbactions{\bonethree}{\ast}{\athree}\end{array}$ (v3);

[-latex] (w1) –node[inner xsep=0pt, inner ysep=0pt, pos=.7,fill=white]().85$\begin{array}{l}\mwbactions{\aonetwooo}{\btwo}{\ast}\\[-.2em]\mwbactions{\bonetwooo}{\atwo}{\ast}\end{array}$ (v2);

[-latex] (w1) –node[inner xsep=0pt, inner ysep=0pt, pos=.7,fill=white]().85$\begin{array}{l}\mwbactions{\aonethree}{\ast}{\bthree}\\[-.2em]\mwbactions{\bonethree}{\ast}{\athree}\end{array}$ (v3);

[-latex] (v1) to[bend right=17.5]node[inner xsep=0pt, inner ysep=0pt, pos=.45,fill=white,fill opacity=1]().85$\begin{array}{l}\mwbactions{\aonetwooo}{\atwo}{\ast}\\[-.2em]\mwbactions{\bonetwooo}{\btwo}{\ast}\\[-.2em]\mwbactions{\aonethree}{\ast}{\athree}\\[-.2em]\mwbactions{\bonethree}{\ast}{\bthree}\end{array}$ (v4);

[-latex] (w1) –node[inner xsep=0pt, inner ysep=0pt, pos=.565,fill=white,fill opacity=1]().85$\begin{array}{l}\mwbactions{a}{\atwo}{\ast}\\[-.2em]\mwbactions{\bonetwooo}{\btwo}{\ast}\\[-.2em]\mwbactions{\aonethree}{\ast}{\athree}\\[-.2em]\mwbactions{\bonethree}{\ast}{\bthree}\end{array}$ (v4);

[-latex] (0) – (v0);

[-latex] (v2.70-90) .. controls +(60-90:4em) and +(120-90:4em) .. node[pos=.5,fill=white,right,xshift=.5ex]()$\ast,\ast,\ast$ (v2.110-90);

[-latex] (v3.70-90) .. controls +(60-90:4em) and +(120-90:4em) .. node[pos=.5,fill=white,right,xshift=.5ex]()$\ast,\ast,\ast$ (v3.110-90);

[-latex] (v4.70-90) .. controls +(60-90:4em) and +(120-90:4em) .. node[pos=.5,fill=white,right,xshift=.5ex]()$\ast,\ast,\ast$ (v4.110-90);

The game $G_0$ on concurrent game structure $M_0$ with a Nash equilibrium.

For instance, suppose that the system in
Figure <ref> represents a 3-player game, where each
transition is labelled by the choices $x,y,z$ made by player $1$, $2$,
and $3$, respectively, and asterisk $\ast$ being a wildcard for any
action for the player in the respective position. Thus, whereas
players $1$ and $2$ can choose to play either $a$ or $b$ at each
state, player $3$ can choose between $a$, $b$, $a'$, or $b'$. The
states are labelled by valuations $xy$ over $\set{p,q}$,
where $\bar x$ indicates that $x$ is set to false. Assume that
player $1$ would like $p$ to be true sometime, that player $2$
would like $q$ to be true sometime, and that player $3$ desires
to prevent both player $1$ and player $2$ from achieving their goals.
Accordingly, their preferences/goals can, respectively, be formally
represented by the LTL formulae

\begin{align*}
\gamma_1	&	=	\sometime p,	&
\gamma_2	&	=	\sometime q,&
\text{and}	&&
\gamma_3	&	=	\always \neg(p\vee q),
\end{align*}

where, informally, $\sometime \phi$ means “eventually $\phi$ holds” and $\always \phi$ means “always $\phi$ holds”.
Moreover,  given these players' goals and the conventional model of
strategies, we will see later in Section <ref> that the system in
Figure <ref> has a Nash equilibrium, whereas  no Nash equilibria
exists in the
(bisimilar) concurrent system presented in Figure <ref>.

every ellipse node=[draw,inner xsep=3.5em,inner ysep=1.2em,fill=black!15!white,draw=black!15!white]
every circle node=[fill=white,draw,minimum size=1.6em,inner sep=0pt]

(0,0) node(0)
++ 	( 0:.9)	  node[label=-90:$\bar p\bar q$,circle](v0)$s_0$
++	(  20:3.5)  node[label=-90:$\bar p\bar q$,circle](v1)$s_1$
+( 20:4)  node[label=-90:$     p\bar q$,circle](v2)$s_2$
+(-20:4)  node[label=-90:$\bar p     q$,circle](v3)$s_3$
(0,.9) ++(-27.5:9)	node[label=-90:$\bar p\bar q$,circle](v4)$s_4$;

[-latex] (v0) –node[inner xsep=0pt, inner ysep=0pt,pos=.5,fill=white]().85$\begin{array}{l}\mwbactions{\ast}{\atwo}{\bthree}\\\mwbactions{\ast}{\btwo}{\athree}\end{array}$ (v1);

[-latex] (v1) –node[inner xsep=0pt, inner ysep=0pt,pos=.5,fill=white]().85$\begin{array}{l}\mwbactions{\aonetwooo}{\btwo}{\ast}\\\mwbactions{\bonetwooo}{\atwo}{\ast}\end{array}$ (v2);

[-latex] (v1) –node[inner xsep=0pt, inner ysep=0pt,pos=.5,fill=white]().85$\begin{array}{l}\mwbactions{\aonethree}{\ast}{\bthree}\\\mwbactions{\bonethree}{\ast}{\athree}\end{array}$ (v3);

[-latex] (v0) to[bend right=0]node[inner xsep=0pt, inner ysep=0pt,pos=.5,fill=white]().85$\begin{array}{l}
\mwbactions{\ast}{\atwo}{\athree}\\[-.2em]
% \mwbactions{\aonethree}{\atwo}{\athree}\\[-.2em]
% \mwbactions{\bonetwooo}{\btwo}{\bthree}\\[-.2em]
\mwbactions{\ast}{\btwo}{\bthree}
\end{array}$ (v4);

[-latex] (v1) to[bend right=0]node[inner xsep=0pt, inner ysep=0pt,pos=.5,fill=white]()1.85$\begin{array}{l}\mwbactions{\aonetwooo}{\atwo}{\ast}\\[-.2em]\mwbactions{\bonetwooo}{\btwo}{\ast}\\[-.2em]\mwbactions{\aonethree}{\ast}{\athree}\\[-.2em]\mwbactions{\bonethree}{\ast}{\bthree}\end{array}$ (v4);

[-latex] (0) – (v0);

[-latex] (v2.70-90) .. controls +(60-90:4em) and +(120-90:4em) .. node[pos=.5,fill=white,right,xshift=.5ex]()$\ast,\ast,\ast$ (v2.110-90);

[-latex] (v3.70-90) .. controls +(60-90:4em) and +(120-90:4em) .. node[pos=.5,fill=white,right,xshift=.5ex]()$\ast,\ast,\ast$ (v3.110-90);

[-latex] (v4.70-90) .. controls +(60-90:4em) and +(120-90:4em) .. node[pos=.5,fill=white,right,xshift=.5ex]()$\ast,\ast,\ast$ (v4.110-90);

The game $G_1$ on concurrent game structure $M_1$ without a Nash equilibrium.

This example illustrates a major issue when analysing (the existence of) Nash equilibria in the most widely used models of strategies and multi-player games in the computer science literature, namely, that even the simplest and most innocuous optimisations commonly used in automated verification are not necessarily sound with respect to game-theoretic analyses.

Because the problem is so fundamental, one may wonder whether bisimilarity is not the right behavioural equivalence for multi-player games, or whether Nash equilibrium is not the right solution concept for game-theoretic analyses of concurrent and multi-agent systems modelled as multi-player games. We will discuss these questions in more detail in Section <ref>, as we do not have a definite answer, but for now we would like to make a couple of observations. On the one hand, that our results also hold both for “alternating” (bisimilarity) relations, as defined in [3], which are intended to capture strategic behaviour in multi-player games, as well as for trace equivalence, as defined in CSP [9], an equivalence much weaker than bisimilarity. On the other hand, that our negative results also hold for solution concepts stronger than Nash equilibrium, e.g., for strong and subgame-perfect Nash equilibria, suggesting that the problem is not a particular defect of Nash equilibrium. Indeed, we think that the issue underlying the mismatch between bisimilarity and Nash equilibrium lies elsewhere. We will propose a very general solution to this problem, that is, a way to reconcile bisimilarity and Nash equilibrium, based on a new definition of strategy in a multi-player game. To do this, some concepts and definitions have to be introduced first.

§ PRELIMINARIES

We begin by introducing the main notational conventions, models, and
technical concepts used in this

§.§ Sets

Given any set $S=\set{s,q,r,\ldots}$, we use
$S^*$, $S^\omega$, and $S^+$ for, respectively, the sets of finite, infinite, and non-empty finite sequences of elements in $S$.
$w_1\in S^*$
and $w_2$ is any other (finite or
infinite) sequence, we write $w_1w_2$ for their concatenation. The
empty sequence is denoted by $\epsilon.$

§.§ Concurrent Game Structures

We use the model of concurrent game structures, which are well-established in the logic and computer science literatures (see, for instance, [1]).
A concurrent game structure (CGS) is a tuple $M=(\Ag,\AP,\Ac,\States,s^0_M,\valf,\transf)$, where
$\Ag=\set{1,\dots,n}$ is a set of players or agents, $\AP$ a set of propositional variables, $\Ac$ is a set of actions, $\States$ is a set of states containing a unique initial state $s^0_M$.
With each player $i\in\Ag$ and each state $s\in\states$, we associate a non-empty set $\Ac_i(s)$ of feasible actions that, intuitively, $i$ can perform when in state $s$.
By a direction or decision we understand a profile of actions $\direction=(\action_1,\dots,\action_n)$ in $\actions\times\dots\times\actions$ and we let $\Dir$ denote the set of directions. A direction $\direction=(\action_1,\dots,\action_n)$ is legal at state $s$ if $a_i\in\Ac_i(s)$ for every player $i$.
Unless stated otherwise, by “direction” we will henceforth generally mean “legal direction”.
Furthermore, $\valf\colon\states\to 2^{\AP}$ is a labelling function, associating with every state $s$ a valuation $v\in 2^\AP$.
Finally, $\delta$ is a deterministic transition function, which
associates with each state $s$ and every legal direction $\direction=(a_1,\dots,a_n)$ at $s$ a state $\delta(s,a_1,\dots,a_n)$.
As such $\delta$

characterises the behaviour of the system when $\direction=(\action_1,\dots,\action_n)$ is performed at state $\state$.

§.§.§ Computations, Runs, and Traces

The possible behaviours exhibited by a CGS can be described at at
least three different levels of abstraction. In what follows, we
distinguish between computations, runs, and
traces.  Computations carry the most information, while traces
carry the least, in the sense that every computation induces a unique
run and every run induces a unique trace, but not necessarily the
other way round. The distinctions we make between computations,
runs, and traces may appear to be insignificant, but are in fact central in
our analysis of bisimilarity and Nash equilibrium.

A state $\state'$ is accessible from another state $\state$
whenever there is some $\direction=(\action_1,\dots,\action_n)$ such
that $\direction$ is legal at $\state$ and
$\delta(s,\action_1,\dots,\action_n)=\state'$.  For easy readability
we then also write $s\transarrow{\direction} s'$.  An
(infinite) computation is then an infinite sequence of
directions $\computation=\direction_0,\direction_1,\direction_2,\dots$
such that there are states $s_0,s_1,\dots$ with $s_0=s^0_M$ and
$ Observe that, having assumed the transition function $\transf$ to be
complete and deterministic, in every concurrent game model the
states $s_0,s_1,\dots$ in the above definition always exist and are
unique.  A finite computation is any finite prefix of a
computation $\fincomputation$. We also allow a finite computation to
be the empty sequence $\epsilon$ of directions.

The sets of infinite and finite computations are denoted by $\computations_M$ and $\fincomputations_M$, respectively.

We also use $\transf^{*}(s, \direction_{0}, \direction_{1}, \ldots \direction_{k})$ to denote the unique state that is reached from the state $s$ after applying the computation $\direction_{0}, \direction_{1}, \ldots \direction_{k}$.

An (infinite) run is an infinite sequence $\run=\state_0,\state_1,\state_2\dots$ of states of sequentially accessible states, with $s_0=s^0_M$.
We say that run $s_0,\dots,s_k$ is induced by computation $d_0,\dots,d_{k-1}$ if $	s_0\transarrow{\direction_0}s_1\transarrow{\direction_1}s_2\transarrow{\direction_2}\cdots$ and $s_0=s^0_M$.
Thus, every computation induces a unique run and every run is induced by at least one computation.

By a finite run or (finite) history we mean a finite prefix of a run.
The sets of infinite and finite runs are denoted by $\runs_M$ and $\finruns_M$, respectively.

An (infinite) trace is a sequence $\trace=v_0,v_1,v_2,\dots$ of
valuations such that there is a run $\run=s_0,s_1,s_2,\dots$
in $\runs_M$ such that $v_k=\lambda(s_k)$ for every $k\ge 0$, that is,
$\trace=\valf(s_0),\valf(s_1),\valf(s_2),\dots$.  In that case we
say that trace $\trace$ is induced by run $\run$, and if $\run$
is induced by computation $\computation$, also that $\trace$ is
induced by $\computation$.

By a finite trace we
mean a finite prefix of a trace.  We denote the sets of finite and
infinite traces of a concurrent game structure $M$ by $\fintraces_M$
and $\traces_M$, respectively.

We use $\run_M(\computation)$ to denote the run induced by a computation $\computation$ in CGS $M$, and write $\finrun_M(\computation)$ if $\computation$ is finite on the understanding that $\finrun_M(\epsilon)=s_M^0$.
Also, if $\run=s_0,s_1,s_2,\dots$ is a run, by $\trace_M(\run)$ we denote the trace $\valf(s_0),\valf(s_1),\valf(s_2),\dots$, and similarly for finite runs $\finrun\in\finruns_M$. Finally, $\trace_M(\run_M(\computation))$ is abbreviated as $\trace_M(\computation)$. When no confusion is likely, we omit the subscript $M$ and the qualification `finite'.

§.§ Bisimilarity

One of the most important behavioural/observational equivalences in concurrency is bisimilarity, which is usually defined over Kripke structures or labelled transition systems (see, e.g., [34, 28]). However, the equivalence can be uniformly defined for general concurrent game structures, where decisions/directions play the role of, for instance, actions in transition systems.
Formally, let $M=(\AP,\Ag,\Ac,\States,s^0_{M},\valf,\transf)$ and $M'=(\AP,\Ag,\Ac,\States',s^0_{M'},\valf',\transf')$ be two concurrent game structures.

A bisimulation, denoted by $\Bisimilar$,

between states $s^*\in\States$ and $t^*\in\States'$ is a non-empty binary
relation $\Bisim \subseteq \States \times \States'$, such that $s^* \mathrel{\Bisim} t^*$ and for all $s,s'\in\States$, $t,t'\in\States'$, and $d\in\Dir$:

* $s\mathrel{\Bisim} t$ implies $\valf(s)=\valf'(t)$,

* $s\mathrel{\Bisim} t$ and $s\transarrow{\direction}s'$ implies $t\transarrow{\direction}t''$ for some $t''\in\States'$ with $s'\mathrel{\Bisim}t''$,

* $s\mathrel{\Bisim} t$ and $t\transarrow{\direction}t'$ implies $s\transarrow{\direction}s''$ for some $s''\in\States$ with $s''\mathrel{\Bisim}t'$.

Then, if there is a bisimulation between two states $s^*$ and $t^*$, we say that they are bisimilar and write $s^*\Bisimilar t^*$ in such a case. We also say that concurrent game structures $M$ and $M'$ are bisimilar (in symbols $M\Bisimilar M'$) if $s^0_{M} \Bisimilar s^0_{M'}$.

Since the transition functions of concurrent game structures, as defined, are deterministic, we have
the following simple but useful facts.

We say that runs $\run=s_0,s_1,\dots$ and $\run'=s'_0,s_1',\dots$  are statewise bisimilar (in symbols $\run\pairwisebisim\run'$) if $s_k\sim s'_k$ for every $k\ge 0$.

Both bisimilarity and statewise bisimilarity are equivalence relations, which is a standard result in the literature (see, for instance, [18, 5, 34]).

We find, moreover, that the sets of (finite) computations as well as the sets of (finite) traces of two bisimilar concurrent game structures are identical. In order to see this, the following simple auxiliary result is useful.

Let $M\sim M'$, $s,s'\in\States$ and $t,t'\in\States'$, and $\direction$ a direction. Then,
$s\sim t$, $s\transarrow{\direction} s'$, and $t\transarrow{\direction} t'$ together imply $s'\sim t'$.

Assume $s\sim t$, $s\transarrow{\direction} s'$, and $t\transarrow{\direction} t'$. As $M\sim M'$, there is a $t''\in\States$ such that $t\transarrow{\direction} t''$ and $s'\sim t''$. Since the transition function is deterministic, moreover, it follows that $t''=t'$. Hence, $s'\sim t'$, as desired.

Using this observation we also have the following result.

Let $M$ and $M'$ be bisimilar concurrent game structures. Then,

*  $\computations_M=\computations_{M'}$ and $\fincomputations_M=\fincomputations_{M'}$,

*  $\mathwordbox{\traces_M=\traces_{M'}}{{\computations_M=\computations_{M'}}
}$ and $\mathwordbox{\fintraces_M=\fintraces_{M'}}{\computations_M=\computations_{M'}}$.

For part <ref>, let $\computation=d_0,d_1,\dots,d_2,\dots$ be a computation in $\computations_M$ and $s_0,s_1,s_2,\dots$ the states in $\states_M$
such that $s_0\xtransarrow{d_0}s_1\xtransarrow{d_1}s_2\xtransarrow{d_2}\cdots$. We show, by induction on $k$, that there are states $t_0,t_1,t_2,\dots$ in $\states_{M'}$ such that
$t_0\xtransarrow{d_0}t_1\xtransarrow{d_1}t_2\xtransarrow{d_2}\cdots$, where $t_0=s^0_{M'}$.
It suffices to prove by induction on $k$ that for every $k\ge 0$ there is a $t_{k+1}$ such that $t_0\xtransarrow{d_0}\dots\xtransarrow{d_k}t_{k+1}$ and $s_{k+1}\bisim t_{k+1}$.
For $k=0$, we have $t_0=s_{M'}^0$. Then, observe that, by definition, $s_0=s_M^0$ and, as $M\bisim M'$, it immediately follows that $s_0\bisim t_0$
and that there is a $t_{1}$ such that $t_0\xtransarrow{d_0}t_1$ and $s_1\bisim t_1$.
For the induction step, we may assume that  there are $t_0,\dots,t_k$ with $s_{M'}^0=t_0\xtransarrow{d_0}\dots\xtransarrow{d_{k-1}}t_{k}$ and $s_k\bisim t_k$. By bisimilarity of $M$ and $M'$ we then immediately obtain that there is a $t_{k+1}$ such that $t_0\xtransarrow{d_0}\dots\xtransarrow{d_{k-1}}t_k\xtransarrow{d_k}t_{k+1}$. By Lemma <ref> it then follows that $s_{k+1}\bisim t_{k+1}$.
Hence, $\computations_M\subseteq\computations_{M'}$.
As the inclusion in the opposite direction is proven by an analogous argument, we may conclude that $\computations_M=\computations_{M'}$. It also follows that $\fincomputations_M=\fincomputations_{M'}$, the latter being defined as the finite prefixes of $\computations_M$ and $\computations_{M'}$, respectively.

Observe that from the argument in part <ref> it also follows that $\run_M(\computation)\statewisebisim\run_{M'}(\computation)$ for every $\computation\in\computations_{M}=\computations_{M'}$.
For part <ref>, consider an arbitrary trace $\trace\in\traces_M$. Then, there is a computation $\computation\in\computations_M$ such that $\trace_M(\computation)=\trace$. By part <ref>, also $\computation\in\computations_{M'}$. Moreover, $\run_M(\computation)\statewisebisim\run_{M'}(\computation)$. By the definition of (statewise) bisimilarity it then follows that $\trace=\trace_M(\computation)=\trace_{M'}(\computation)$. Accordingly, $\traces_M\subseteq\traces_{M'}$ and the inclusion in the opposite direction ensues by an analogous argument. We then conclude that $\fintraces_M=\fintraces_{M'}$, the latter being defined as the finite prefixes of $\traces_M$ and $\traces_{M'}$, respectively.

Moreover, every (finite) computation $\computation$ gives rise to statewise bisimilar (finite) runs and identical (finite) traces in bisimilar concurrent game structures.

Let $M$ and $M'$ be bisimilar concurrent game structures and $\computation\in\computations_M$ and $\computation'\in\fincomputations_M$. Then,

*  $\run_M(\computation)\statewisebisim\run_{M'}(\computation)$ and $\finrun_{M}(\computation')\statewisebisim\finrun_{M'}(\computation')$,

*  $\mathwordbox{\trace_M(\computation)}{\run_M(\computation)}=\mathwordbox[l]{\trace_{M'}(\computation)}{\run_{M'}(\computation)}$
and $\mathwordbox{\fintrace_{M}(\computation')}{\finrun_{M}(\computation')}=\mathwordbox{\fintrace_{M'}(\computation')}{\finrun_{M'}(\computation')}$.

For part <ref>, first observe that by virtue of Lemma <ref>, we also have that $\computation\in\computations_{M'}$ and $\fincomputation\in\fincomputations_{M'}$.
Let $\computation=d_0,d_1,d_2,\dots$,
$\run_M(\computation)=s_0,s_1,s_2,\dots$, and
We prove by induction on $k$ that $s_k\bisim t_k$ for every $k\ge 0$.
If $k=0$, then $s_0=s^0_M\bisim s^0_{M'}=t_0$. For the induction step,
we may assume that $s_k\bisim t_k$. Then, $s_k\xtransarrow{d_k}s_{k+1}$ and
$t_k\xtransarrow{d_k}t_{k+1}$. Lemma <ref> now yields $s_{k+1}\bisim t_{k+1}$, as desired.
The argument for the second part of <ref> proceeds by an analogous argument.

Part <ref> then follows almost immediately from part <ref>.
Let $\run_M(\computation)=s_0,s_1,s_2,\dots$ and $\run_{M'}(\computation)=t_0,t_1,t_2,\dots$. Now observe that for every $k\ge0$ we have that $\evalf_M(s_k)=\evalf_{M'}(t_k)$.
Accordingly, $\trace_M(\computation)=\trace_{M'}(\computation)$. For $\computation'$ a similar argument yields the result.

However, as runs are sequences of states and the states of different concurrent game structures $M$ and $M'$ may be distinct, even if they are bisimilar, no identification of their sets $\runs_M$ and $\runs_{M'}$  of runs can generally be made.

§ GAMES ON CONCURRENT GAME STRUCTURES

Concurrent game structures specify the actions the players can take at
each state and which states are reached if they all concurrently
decide on an action. In game theoretic terms, these structures loosely
correspond to what are called game forms.
A full understanding of the game-theoretic aspects of the system and the
strategic behaviour of its constituent players—and therefore which computations/runs/traces will be generated in equilibrium—also essentially depends on what goals the players desire to
achieve and on what strategies they may adopt in pursuit of these
goals. We therefore augment concurrent game structures with
preferences and strategies for the players. In this way CGSs define fully fledged strategic games and as such they are amenable to game theoretic analysis by standard solution concepts, among which Nash equilibrium is arguably the most prominent.

§.§ Strategies and Strategy Profiles

Based on the distinction between computations, runs, and traces, we can also distinguish three types of strategy: computation-based, run-based, and trace-based strategies.
The importance of these distinctions is additionally corroborated by Bouyer et al. [6, 7], who show how the specific model of strategies adopted affects the computational complexity of some standard decision problems related to multi-agent systems.

A computation-based strategy for a player $i$ in a concurrent game structure $M$ is a function

\[
\]

such that $f_i^{\mathit{comp}}(\fincomputation)\in\Ac_i(s_{k})$ for every finite $\fincomputation\in\fincomputations_M$ with $\finrun_M(\fincomputation)=s_0,\dots,s_k$.

Thus, in particular, $f_i^{\mathit{comp}}(\epsilon)\in\Ac_i(s^0_M)$, where $\epsilon$ is the empty sequence of directions.

Similarly, a run-based strategy for player $i$ is a

\[
\]

where $f_i^{\mathit{run}}(s_0,\dots,s_k)\in\Ac_i(s_k)$ for every finite run $(s_0,\dots,s_k)\in\finruns_M$.
Finally, a trace-based strategy for $i$ is a function

\[
\]

such that $f_i^{\mathit{trace}}(\fintrace)\in\Ac_i(s_k)$ for every trace $\fintrace\in\fintraces_M$ and every run $\finrun=s_0,\dots,s_k$ such that $\trace=\valf(s_0),\dots,\valf(s_k)$.

A computation-based strategy profile is then a tuple
$\stratprof=(\strategy_1,\dots,\strategy_n)$ that associates with each
player $i$ a computation-based strategy $f_i$. Run-based and
trace-based strategy profiles are defined analogously.

Every computation-based strategy profile $f=(f_1,\dots,f_n)$ induces a unique computation

\[
\computation_M(f)=d_0,d_1,d_2,\dots
\]

in $M$ that is defined inductively as follows:

\begin{align*}
% s_0		&	=	s^0_M&
d_0		&	=	(f_1(\epsilon),\dots,f_n(\epsilon))\\
% s_{k+1}	&	=	\transf(s_k,d_k)&
d_{k+1}	&	=	(f_1(d_0,\dots,d_{k}), \ldots,f_n(d_0,\dots,d_{k})).
\end{align*}

A run-based strategy profile $f=(f_1,\dots,f_n)$ defines a unique computation $\computation_M(f)=d_0,d_1,d_2,\dots$ in a similar manner:

\begin{align*}
% s_0		&	=	s^0_M&
d_0		&	=	(f_1(s^0_M),\dots,f_n(s^0_M))\text{, and}\\
% s_{k+1}	&	=	\transf(s_k,d_k)&
% d_{k+1}	&	=	(f_1(s_0,\dots, s_{k+1}),\dots,f_n(s_0,\dots,s_{k+1}))\text,\\
d_{k+1}	&	=	(f_1(\finrun(d_0,\dots,d_k)),\dots,f_n(\finrun(d_0,\dots,d_k))\text.
\end{align*}

Finally, the computation $\computation_M(f)$ defined by a trace-based strategy profile $f$ is given by

\begin{align*}
% s_0		&	=	s^0_M&
d_0		&	=	(f_1(\valf(s^0_M)),\dots,f_n(\valf(s^0_M)))\\
% s_{k+1}	&	=	\transf(s_k,d_k)&
% d_{k+1}	&	=	\scalebox{.95}[1]{$(f_1(\valf(s_0),\dots, \valf(s_{k+1})), \dots,f_n(\valf(s_0),\dots,\valf(s_{k+1})))$}\text,\\
d_{k+1}	&	=	\scalebox{1}[1]{$(f_1(\trace(d_0,\dots,d_k)), \dots,f_n(\trace(d_0,\dots,d_k))$}\text.
\end{align*}

If $M$ is clear from the context, we usually omit the subscript in $\computation_M(f)$.

For $f=(f_1,\dots,f_n)$ a profile of computation-based, run-based, or trace-based strategies,
we write with a slight abuse of notation  $\run(f_1,\dots,f_n)$ for $\run(\computation(f_1,\dots,f_n))$ and $\trace(f_1,\dots,f_n)$ for $\trace(\run(f_1,\dots,f_n))$.

As the computations of bisimilar concurrent games structures coincide (Lemma <ref>), we can now establish that a
player's computation-based strategies coincide in bisimilar
concurrent game structures. Moreover, the computations induced by them will be identical.
Also, from the coincidence of traces between bisimilar concurrent game structures (Lemma <ref>), we can establish also trace-based strategies coincide in bisimilar concurrent game structures.

Let $M$ and $M'$ be bisimilar concurrent game structures and $i$ a player.
Then, every computation-based  strategy for $i$ in $M$ is also a computation-based strategy for $i$ in $M'$, and every trace-based  strategy for $i$ in $M$ is also a trace-based strategy for $i$ in $M'$. 	Moreover, for every computation-based profile $f$ for $M$ we have that $\computation_M(f)=\computation_{M'}(f)$, and for every trace-based profile $g$ that $\computation_M(g)=\computation_{M'}(g)$.

First, let $f_i$ be a computation-based strategy for $i$ in $M$. We show that $f_i$ is also a computation-based strategy for $i$ in $M'$. To this end, consider an arbitrary $\fincomputation\in\fincomputations_{M'}$. Let $\finrun_{M'}(\fincomputation)=t_0,\dots,t_k$.
It suffices to prove that $f_i(\fincomputation)\in\actions_i(t_k)$.
To see this, first observe that by Lemma <ref> also $\fincomputation\in\fincomputations_M$ and let $\finrun_M(\fincomputation)=s_0,\dots,s_k$.
In virtue of Lemma <ref>, then $s_k\bisim t_k$.
Moreover, because $f_i$ is a computation-based strategy for $i$ in $M$, we have $f_i(\fincomputation)\in\actions_i(s_k)$. Now consider any legal direction $d_{k}=(a_1,\dots,a_n)$ at $s_k$ with $a_i=f_i(\fincomputation)$.
Then, there is some state $s_{k+1}\in\states_M$ such that $s_k\xtransarrow{d_k}s_{k+1}$. As $s_k\bisim t_k$, moreover, there is also a state $t_{k+1}\in\states_{M'}$ such that $t_k\xtransarrow{d_k}t_{k+1}$. Accordingly, $d_{k}$ is legal at $t_k$ in $M'$ and in particular $a_i=f_i(\fincomputation)\in\actions_i(t_k)$ as desired.

The case if $g_i$ is a trace-based strategy for $i$ in $M$ is similar. We then have to prove that $g_i$ is also a trace-based strategy for $i$ in $M'$ as well. To this end, consider an arbitrary finite trace $\fintrace\in\fintraces_{M'}$ and run $\finrun=t_0,\dots,t_k$ such that $\fintrace=\valf_{M'}(t_0),\dots,\valf_{M'}(t_k)$. It then suffices to prove that $g_i(\fintrace)\in\actions_i(t_k)$. We may assume that $\finrun$ is induced by a computation $\fincomputation\in\fincomputations_{M'}$, that is, $\finrun=\finrun_{M'}(\fincomputation)$. By Lemma <ref> we have $\fincomputation\in\fincomputations_M$ and by Lemma <ref> both $\finrun_M(\fincomputation)\statewisebisim\finrun_{M'}(\fincomputation)$ and
Let $\finrun_M(\fincomputation)=s_0,\dots,s_k$. Hence, $s_k\bisim t_k$. As $g_i$ is a run-based strategy for $i$ in $M$ we have $g_i(\fintrace)\in\actions_i(s_k)$.
Let, furthermore, $d=(a_1,\dots,a_k)$ be a legal direction at $s_k$ with $a_i=g_i(\fintrace)$.
Then, there is some state $s_{k+1}\in\states_M$ such that $s_k\xtransarrow{d_k}s_{k+1}$. As $s_k\bisim t_k$, there is also a state $t_{k+1}\in\states_{M'}$ such that $t_k\xtransarrow{d_k}t_{k+1}$. Accordingly, $d_{k}$ is legal at $t_k$ in $M'$ and in particular $a_i=g_i(\fintrace)\in\actions_i(t_k)$.

For the second part of the lemma, let $f=(f_1,\dots,f_n)$ be a computation-based strategy profile in $M$. Then, $f$ is a computation-based strategy profile in $M'$ as well. Let $\computation_M(f)=d_0,d_1,d_2,\dots$
and $\computation_{M'}(f)=d'_0,d'_1,d'_2,\dots$. We show by induction on $k$ that for every $k\ge0$ we have $d_k=d'_k$. For $k=0$, immediately,
For the induction step we may assume that $d_0,\dots,d_k=d_0',\dots,d'_k$. Hence,

\begin{align*}
d_{k+1}		=	(f_1(d_0,\dots,d_k),\dots,f_n(d_0,\dots,d_k))
=	(f_1(d'_0,\dots,d'_k),\dots,f_n(d'_0,\dots,d'_k))
=	d'_{k+1}\text.
\end{align*}

Finally, let $g=(g_1,\dots,g_n)$ be a trace-based strategy profile. Again we let $\computation_M(f)=d_0,d_1,d_2,\dots$
and $\computation_{M'}(f)=d'_0,d'_1,d'_2,\dots$ and show by induction on $k$ that for every $k\ge0$ we have that $d_k=d'_k$.
If $k=0$, observe that having assumed $M\bisim M'$ also $s^0_M=s^0_{M'}$.
Accordingly, $\evalf_M(s_M^0)=\evalf_{M'}(s^0_{M'})$ and, hence,

\begin{align*}
d_{0}		=	(g_1(\evalf_M(s_M^0)),\dots,g_n(\evalf_M(s_M^0))
=	(g_1(\evalf_{M'}(s^0_{M'})),\dots,g_n(\evalf_{M'}(s^0_{M'})))
=	d'_{k+1}\text.
\end{align*}

For the induction step, we may assume that $d_0,\dots,d_k=d'_0,\dots,d'_k$ and by Lemma <ref>, moreover, $\fintrace_{M}(d_0,\dots,d_k)=\fintrace_{M'}(d'_0,\dots,d'_k)$.
Now the following equations hold:

\begin{align*}
d_{k+1}	&	=	(g_1(\fintrace_M(d_0,\dots,d_k)),\dots,g_n(\fintrace_{M}(d_0,\dots,d_k)))\\
&	=	(g_1(\fintrace_{M'}(d'_0,\dots,d'_k)),\dots,g_n(\fintrace_{M'}(d'_0,\dots,d'_k)))\\
&	=	d'_{k+1}\text,
\end{align*}

which concludes the proof.

With the states of bisimilar structures possibly being
distinct, however, a statement  analogous to Lemma <ref> cannot
be shown to hold for run-based strategies.

§.§ Preferences and Goals

We assume the agents of a concurrent game structure to have preferences on basis of which they choose their strategies.

Formally, we specify the preferences of a player $i$ of a CGS $M$
as a subset $\goalset_i$ of computations,
that is, $\goalset_i \subseteq \computations_M$ and refer
to $\goalset_i$ as $i$'s goal set. Player $i$ is then
understood to (strictly) prefer computations in $\goalset_i$ to
those not in $\goalset_i$ and to be indifferent
otherwise. Accordingly, each player's preferences are dichotomous,
only distinguishing between the preferred computations in $\goalset_i$
and the not preferred ones not in $\goalset_i$.  Formally, player $i$
is said to weakly prefer computation $\computation$ to
computation $\computation'$ if $\computation\in\goalset_i$
whenever $\computation'\in\goalset_i$, and to strictly prefer
$\computation$ to $\computation'$ if $i$ weakly prefers $\computation$
to $\computation'$ but not the other way round.  If $i$ both weakly
prefers $\computation$ to $\computation'$ and weakly
prefers $\computation'$ to $\computation$, player $i$ is said to be
indifferent between $\computation$ and $\computation'$.

Our choice to assume the players' preferences to be computation-based preferences—that is, to model their goals as sets of
computations rather than, say, sets of runs or sets of
traces—is for technical convenience and flexibility. Recall that
every set of runs induces a set of computations, namely the set of
computations that give rise to the same runs, and similarly for every
set of traces. Thus, we say that a goal
set $\goalset_i\subseteq\computations_M$ is run-based if for
any two computations $\computation$ and $\computation'$ with
$\run(\computation)=\run(\computation')$ we have that
$\computation\in\goalset_i$ if and only if
$\computation'\in\goalset$. Similarly, $\goalset_i$ is said to be
trace-based whenever
$\trace(\computation)=\trace(\computation')$ implies
$\computation\in\goalset_i$ if and only if
$\computation'\in\goalset_i$. In other words, in our setting, formally,
run-based goals are computation-based goals closed under induced runs, and
trace-based goals are computation-based goals closed
under induced traces.

[We do not directly consider sets of runs or sets of traces as
possible models of players' preferences in this paper—formally, they are induced sets of computations. Accordingly, when talking about preferences,
we need not make the distinction between `run-based' (`trace-based') and
`run-invariant' (`trace-invariant') as we do for strategies. Our run-based
preferences and trace-based preferences can with as much justification be
referred to as run-invariant preferences and trace-invariant preferences,

Sometimes—as we did in the example in the introduction—players' goals are specified by temporal logic formulae [18].
As the satisfaction of goals only depends on traces, they will
directly correspond to trace-based goals, given our formalisation of
goals and preferences.

§.§ Games and Nash Equilibrium

With the above definitions in place, we are now in a position to
define a game on a concurrent game structure $M$ (also called a CGS-game) with
$\agents=\set{1,\dots,n}$ as a

\[
% ,\strategies_1,\dots\strategies_n
\]

where, for each player $i$ in $M$, the
set $\goalset_i\subseteq\computations_M$ is a goal set
specifying $i$'s dichotomous preferences over the computations in $M$.

In a CGS-game the players can all play either computation-based strategies,  run-based strategies, or trace-based strategies.

For each such choice of type of strategies, with the set of players and their preferences specified,
every CGS-game defines a strategic game in the standard game-theoretic sense.
Observe that the set of strategies is infinite in general.
Thus the game-theoretic solution concept of Nash equilibrium becomes available for the analysis of games on concurrent game structures.
If $f=(f_1,\dots,f_n)$ is a strategy profile and $g_i$ a strategy for player $i$, we write $(f_{-i},g_i)$ for the strategy profile
which is identical to $f$ except that $i$'s strategy is replaced by $g_i$.
Formally, given a CGS-game, we  say that a profile $\strategy=(\strategy_1,\dots,\strategy_n)$ of computation-based strategies is a Nash equilibrium in computation-based strategies (or computation-based equilibrium) if, for every player $i$ and every computation-based  strategy $g_i$ available to $i$,

\[
\text{
% $\computation(f_1,\dots,g_i,\dots,f_n)\in\goalset_i$
% $\computation(f_1,\dots,f_n)\in\goalset_i$.
\]

The concepts of Nash equilibrium in run-based strategies and Nash equilibrium in trace-based strategies are defined analogously, where, importantly, the strategies in $f_{-i}$ and $g_i$ are required to be of the same type, that is, either they are all run-based or they are all trace-based.
If $\computation(f)\notin\goalset_i$ whereas $\computation(f_{-i},g_i)\in\goalset_i$, we also say that player $i$ would like to deviate from $f$ (and play $g_i$ instead). Thus, a run-based profile $f$ is a run-based equilibrium whenever no player would like to deviate from it and play some run-based strategy different from $f_i$. Similarly, a trace-based profile $f$ is a trace-based equilibrium if no player likes to deviate and play another trace-based strategy.

We say that a computation $\computation$, run $\run$, or a trace $\trace$ is sustained by a Nash equilibrium $\strategy=(\strategy_1,\dots,\strategy_n)$ (of any type) whenever $\computation=\computation(\strategy)$, $\run=\run(\strategy)$, and $\trace=\trace(\strategy)$, respectively. We also refer to a computation, run, or trace that is sustained by a Nash equilibrium as an equilibrium computation, equilibrium run, and equilibrium trace, respectively.

Computation-based equilibrium is a weaker notion than run-based
equilibrium, in the sense that if $f$ is a run-based equilibrium there
is also a corresponding computation-based equilibrium, but not
necessarily the other way round. Run-based equilibrium, in turn, is in
a similar way a weaker concept than trace-based equilibrium.
As computation-based, run-based, and trace-based strategies are
set-theoretically of different types, a comparison cannot be made
directly. To make the comparison precise, we therefore identify
two subclasses of computation-based strategies, run-invariant strategies and trace-invariant strategies, that characterise the behaviour of, respectively, run-based and trace-based strategies.

We say that a computation-based strategy $f_i\colon\fincomputations_M\to\actions_i$ is run-invariant in CGS $M$ whenever  $\finrun_M(\fincomputation)=\finrun_M(\fincomputation')$ implies $f_i(\fincomputation)=f_i(\fincomputation')$, for all computations $\fincomputation,\fincomputation'\in\fincomputations_M$.
Similarly, $f_i$ is trace-invariant in $M$ whenever  $\fintrace_M(\fincomputation)=\fintrace_M(\fincomputation')$ implies $f_i(\fincomputation)=f_i(\fincomputation')$, for all
Observe that thus a strategy $f_i$ being trace-invariant implies $f_i$ being run-invariant, but not necessarily the other way around.

We observe that there are one-to-one correspondences between run-based strategies on the one hand and run-invariant computation-based strategies on the other, and similarly between trace-based strategies and trace-invariant computation-based strategies.
Let $f_i\colon\finruns_M\to\actions$ be a run-based strategy. Then define $\check f_i\colon\fincomputations_M\to\actions$ as the computation-based strategy such that for every finite computation $\fincomputation\in\fincomputations_M$ we have
\check f_i(\fincomputation)=f_i(\finrun_M(\fincomputation)).
A similar statment holds if $g_i\colon\fintraces_M\to\actions$ is a trace-based strategy. Then, define $\dcheck g_i\colon\fincomputations\to\actions_i$ as the computation-based strategy such that for every finite computation $\fincomputation\in\fincomputations_M$ we have
\dcheck g_i(\fincomputation)=g_i(\fintrace_M(\fincomputation)).

For run-based strategies $f_i$ and trace-based strategies $g_i$, the mapping that transforms $f_i$ into $\check f_i$ and the mapping that transforms $g_i$ into $\dcheck g_i$ are both one-to-one.

Let $f_i$ a run-based strategy. We first show that $\check f_i$ is run-invariant.
To this end, let $\fincomputation,\fincomputation'\in\fincomputations_M$ be computations such that $\finrun_M(\fincomputation)=\finrun_M(\fincomputation')$. Then,

\[
\check f_i(\fincomputation)
=	f_i(\finrun_M(\fincomputation))
=	f_i(\finrun_M(\fincomputation'))
= \check f_i(\fincomputation')\text.
\]

To show that the mapping is onto, let $g_i$ be an arbitrary run-invariant strategy.
Now define run-based strategy $\hat g_i$ such that, for every run $\finrun\in\finruns_M$
and $\fincomputation\in\fincomputations_M$ with $\finrun=\finrun_M(\fincomputation)$ we have
$\hat g_i(\finrun)=g_i(\fincomputation)$.
Observe that $\hat g_i$ is well-defined since, , by run-invariance of $g_i$, for all $\fincomputation,\fincomputation'\in\fincomputations_M$ with $\finrun_M(\fincomputation)=\finrun_M(\fincomputation')=\finrun$ we have that $g_i(\fincomputation)=g_i(\fincomputation')$.

Finally, to see that the mapping is injective, let $f_i$ and $f'_i$ be two distinct run-based strategies. Then, there is a run $\finrun\in\finruns_M$ such that $f_i(\finrun)\neq f'_i(\finrun)$. We may assume the existence of a computation $\fincomputation\in\fincomputations_M$ such that $\finrun_M(\fincomputation)=\finrun$. Then,

\[
\check f_i(\fincomputation)
=	f_i(\finrun_M(\fincomputation))
=	f_i(\finrun)
\neq f'_i(\finrun)
=	f'_i(\finrun_M(\fincomputation))
= 	\check f_i(\fincomputation)\text,
\]

as desired. This concludes the proof.

Furthermore, each profile of run-invariant strategies induces the same computation in a concurrent game structure as its run-based counterpart. A similar remark applies to trace-invariant and trace-based profiles.

Let $f=(f_1,\dots,f_n)$ be a run-based profile and $g=(g_1,\dots,g_n)$ a trace-based profile. Then,

\begin{align*}
\computation_M(f_1,\dots,f_n)&=\computation_M(\check f_1,\dots,\check f_n)
\computation_M(f_1,\dots,f_n)&=\computation_M(\dcheck f_1,\dots,\dcheck f_n)\text.
\end{align*}

Let $\computation_M(f_1,\dots,f_n)=d_0,d_1,d_2,\dots$
and $\computation_M(\check f_1,\dots,\check f_n)=d'_0,d'_1,d'_2,\dots$.
We prove by induction on $k$ that $d_0,\dots,d_k=d'_0,\dots,d'_k$ for every $k\ge 0$.

If $k=0$, recall that $\finrun_M(\epsilon)=s_M^0$. Hence,

\[
(\check f_1(\epsilon),\dots,\check f_n(\epsilon))
\]

For the induction step, we may assume that $d_0,\dots,d_k=d'_0,\dots,d'_k$.
Now the following equalities hold.

\begin{align*}
&	=_{\phantom{i.h.}}
\\
(\check f_1(d_0,\dots,d_k),\dots,\check f_n(d_0,\dots,d_k))
\\
(\check f_1(d'_0,\dots,d'_k),\dots,\check f_n(d'_0,\dots,d'_k))
\\
\end{align*}

We may conclude that $d_0,\dots,d_{k+1}=d'_0,\dots,d'_{k+1}$.

The argument for trace-based and trace-invariant strategies runs along analogous lines, mutatis mutandis.

We say that a computation-based profile $f=(f_1,\dots,f_n)$ is a run-invariant equilibrium in a CGS-game if $f$ is run-invariant and no player $i$ wishes to deviate from $f$ and play another run-invariant strategy $f'_i$.
Similarly, a computation-based profile $f=(f_1,\dots,f_n)$ is a trace-invariant equilibrium in a CGS-game if $f$ is trace-invariant and no player $i$ wishes to deviate from $f$ and play another trace-invariant strategy $f'_i$.
As an immediate consequence of Lemmas <ref> and <ref> we have the following corollary.

Let $f=(f_1,\dots,f_n)$ and $g=(g_1,\dots,g_n)$ be a run-based profile, respectively, a trace-based profile in a CGS-game $G=(M,\goalset_1,\dots,\goalset_n)$ based on $M$. Then,

* $f$ is a run-based equilibriumtrace-based equilibrium if and only if  $\check f$ is a run-invariant equilibriumtrace-invariant equilibrium,

* $g$ is a trace-based equilibrium if and only if  $\dcheck g$ is a trace-invariant equilibrium.

For the run-based case, the following equivalences hold by virtue of Lemmas <ref> and <ref>:

\begin{align*}
&	\text{$f$ is not a run-based equilibrium in $G$}\\
&	\text{iff}\quad \text{$\computation_M(f)\notin\goalset_i$ and $\computation_{M}(f_{-i},f'_i)\in\goalset_i$ for some run-based strategy~$f'_i$ for some player~$i$}\\
& 	\text{iff}\quad \text{$\computation_M(\check f)\notin\goalset_i$ and $\computation_{M}(\check f_{-i},\check f'_i)\in\goalset_i$ for some run-based strategy~$f'_i$ for some player~$i$}\\
& 	\text{iff}\quad \text{$\computation_M(\check f)\notin\goalset_i$ and $\computation_{M}(\check f_{-i},f''_i)\in\goalset_i$ for some run-invariant strategy~$f''_i$ for some player~$i$}\\
&	\text{iff}\quad\text{$\check f$ is not a run-invariant equilibrium in $G$}
\end{align*}

The proof of the second part is by an analogous argument, mutatis mutandis.

Computation-based strategies grant a player more strategic flexibility than do run-invariant strategies. A similar remark applies to run-invariant strategies and trace-invariant strategies. Still, we find that, if a player $i$ wishes to deviate from a computation-based profile $f$ and play another computation-based strategy, $i$ would also like to deviate by playing a run-invariant or even a trace-invariant strategy. This insight underlies the following result.[The situation can be compared to the relation between equilibria in pure and mixed (or randomised) strategies in game theory. There every equilibrium in pure strategies is also an equilibrium in mixed strategies, because, if a player wishes to deviate from a mixed profile, she wishes to deviate by playing a pure, that is, not randomised, strategy.]

Let $f=(f_1,\dots,f_n)$ be a run-invariant profile and $g=(g_1,\dots,g_n)$ a trace-invariant profile in CGS-game $G=(M,\goalset_1,\dots,\goalset_n)$ based on $M$. Then,

*   $f$ is a run-invariant equilibrium$g$ is a trace-invariant equilibrium if and only if $f$ is a computation-based equilibrium$g$ is a computation-based equilibrium,

*  $g$ is a trace-invariant equilibrium if and only if $g$ is a computation-based equilibrium.

For part <ref>, first assume that $f$ is a run-invariant equilibrium in $G$.
For a contradiction assume moreover that $f$ is not a computation-based equilibrium.
Then, there is a player $i$ and a computation-based strategy $f'_i$ such that $\computation_M(f)\notin\goalset_i$ whereas
Let $\computation_M(f_{-i},f'_i)=d'_0,d'_1,d'_2,\dots$.
Observe that $f'_i$ need not be run-invariant.
We therefore define strategy $f''_i$ for player $i$ such that $f''_i(\epsilon)=f'_i(\epsilon)$ and,
for all finite computations $d_0,\dots,d_k$,

\[
\begin{cases}
f'_i(d'_0,\dots,d'_k)	&	\text{if $\finrun_M(d_0,\dots,d_k)=\finrun_M(d'_0,\dots,d'_k)$,}\\
f_i(d_0,\dots,d_k)	&	\text{otherwise.}
\end{cases}
\]

As $f_i$ is run-invariant, this definition guarantees that $f''_i$ is run-invariant as well.
Let $\computation_M(f_{-i},f''_i)=d_0'',d_2'',d_2'',\dots$. We prove by induction
on $k$ that $d'_0,\dots,d'_k=d''_0,\dots,d''_k$, for every $k\ge 0$, and hence that $\computation_M(f_{-i},f'_i)=\computation_M(f_{-i},f''_i)$.
If $k=0$, we immediately obtain that

\begin{align*}
&	=	(f_1(\epsilon),\dots,f'_i(\epsilon),\dots,f_n(\epsilon))
=	(f_1(\epsilon),\dots,f''_i(\epsilon),\dots,f_n(\epsilon))
% &	=	(f_1(\finrun(\epsilon)),\dots,f'_i(\epsilon),\dots,f_n(\finrun(\epsilon)))\\
% &	=	(\check f_1(\epsilon),\dots,f'_i(\epsilon),\dots,f_n(\epsilon))\\
=	\direction''_0\text.
\end{align*}

For the induction step, we may assume that $d'_0,\dots,d'_k=d''_0,\dots,d''_k$.

and the following equalities hold:

\begin{align*}
&		=_{\phantom{i.h.}}	(f_1(d_1',\dots,d_k'),\dots,f'_i(d_1',\dots,d_k'),\dots,f_n(d_1',\dots,d_k'))
\\&		=_{\phantom{i.h.}}	(f_1(d_1',\dots,d_k'),\dots,f''_i(d_1'',\dots,d_k''),\dots,f_n(d_1',\dots,d_k'))
\\&		=_{{i.h.}}			(f_1(d_1'',\dots,d_k''),\dots,f''_i(d_1'',\dots,d_k''),\dots,f_n(d_1'',\dots,d_k''))
% \\&		=_{\phantom{i.h.}}	(f_1(d_1'',\dots,d_k''),\dots,f''_i(d_1'',\dots,d_k''),\dots,f_n(d_1'',\dots,d_k''))
\\&		=_{\phantom{i.h.}} 	d''_{k+1}\text.
\end{align*}

Observe that the second equality holds by virtue of the definition of $f''_i$ and $\finrun_M(d'_0,\dots,d'_k) = \finrun_M(d''_0,\dots,d''_k)$.
It would follow that $\computation_M(f_{-i},f''_i)\in\goalset_i$ as well, and, as $f''_i$ is run-invariant, moreover that $f$ is not a run-invariant equilibrium, a contradiction.

For the opposite direction, assume for contraposition that $f$ is not a run-invariant equilibrium. Then, there is some player $i$
who would like to deviate  from $f$ and play some run-invariant strategy $f'_i$. As run-invariant strategies are strategy-based by definition,
it follows that $f$ is not a computation-based equilibrium either.

Part <ref> follows by an analogous argument, mutatis mutandis.

Theorem <ref> does not preclude the existence of computation-based equilibria that fail to be run-invariant or trace-invariant, that is, the three equilibrium concepts—computation-based, run-invariant, and trace-invariant equilibrium—are not equivalent. However, they can be ordered with respect to how restrictive they are, that is, with respect to the sets of profiles they exclude as solutions.

Let $f=(f_1,\dots,f_n)$ be a computation-based profile in some CGS-game $G=(M,\goalset_1,\dots,\goalset_n)$ based on $M$. Then,

* [l]$f$ is a run-invariant equilibrium$f$ is a trace-invariant equilibrium implies $f$ is a computation-based equilibrium,

* $f$ is a trace-invariant equilibrium implies $f$ is a run-invariant equilibrium.

Merely observe that if $f$ is a run-invariant equilibrium, it is also a run-invariant profile. If $f$ is moreover trace-invariant it is also run-invariant. The result then immediately follows from Theorem <ref>.

On basis of the findings in this section, we may with justification claim that every trace-based equilibrium corresponds to a run-based equilibrium, and that every run-based equilibrium corresponds with some computation-based equilibrium, even if the converses of these statements do not generally hold.

§ INVARIANCE OF NASH EQUILIBRIA UNDER BISIMILARITY

From a computational point of view, one may expect games based on bisimilar concurrent game structures and with identical players' preferences to exhibit similar properties, in particular with respect to their Nash equilibria.
We find that that this is indeed the case for games with
computation-based strategies as well as for games with trace-based
Recall that (finite) computations and (finite) traces
are unaffected by (state-splitting and state-merging) operations on CGSs that preserve bisimilarity (Lemma <ref>).
As a consequence the sets of computation-based strategies and trace-based strategies available to an again are the same in bisimilar CGSs (Lemma <ref>), providing the intuitive basis for these observations.

For games with run-based strategies the situation is
considerably more complicated. Here, a key observation is that, by contrast
to computation-based and trace-based strategies, there need not be a
natural one-to-one mapping between the sets of run-based
strategies in bisimilar concurrent game models. By restricting attention to
so-called bisimulation-invariant run-based strategies, however, we
find that order can be restored.

§.§ Invariance under Bisimilarity and Preference Types

We are primarily interested in the
Nash equilibria of games that are the same up to bisimilarity of the
underlying concurrent game structures. The Nash equilibria of a game, however, essentially depend on the players' preferences. Accordingly, the Nash equilibria of two bisimilar CGS-games can only be meaningfully compared if we also
we assume that the players' preferences in these two games are identical. We
formalised players' preferences as sets of computations, and, due to
Lemma <ref>, this enables a
straightforward comparison of players' goal sets across bisimilar
concurrent game structures.

In Section <ref>, we also distinguished run-based
and trace-based preferences, that is, goal sets closed under
computations that induce the same runs and traces, respectively. We
are also interested in the invariance of the existence of Nash equilibria
in games on bisimilar concurrent game structures
where the players' preferences games are what we will call congruent, that is, both the same and of the same type in both games.

For computation-based and
trace-based preferences the issue of congruence is moot.
Observe that for
bisimilar concurrent game structures $M$ and $M'$, if a goal
set $\goalset_i$ is computation-based in $M$, then it is also
computation-based in $M'$. Due to
Lemma <ref>, the same holds
for trace-based preferences.

every ellipse node=[draw,inner xsep=3.5em,inner ysep=1.2em,fill=black!15!white,draw=black!15!white]
every circle node=[fill=white,draw,minimum size=1.6em,inner sep=0pt]

(0,-3)	node();
(7.8,3.25)	node();

(0,0) node(0)
++ 	( 0:.9)	  node[label=-90:$p$,circle](v0)$s_0$

+ (.8*6,.8*3)  node[label=-90:$p$,circle](v1)$s_1$

+ (.8*6,.8*0) node[label=-90:$p$,circle](v3)$s_2$
+ (.8*6,.8*-3) node[label=-90:$\bar p$,circle](v4)$s_3$

[-latex] (v0) –node[pos=.55,fill=white]()$\begin{array}{l}a,a\end{array}$ (v1);

[-latex] (v0) –node[pos=.55,fill=white]()$\begin{array}{l}a,b\\b,a\end{array}$ (v3);
[-latex] (v0) –node[pos=.55,fill=white]()$\begin{array}{l}b,b\end{array}$  (v4);

[-latex] (0) – (v0);

[-latex] (v1.70-90) .. controls +(60-90:4em) and +(120-90:4em) .. node[pos=.5,fill=white,right,xshift=.5ex]()$\ast,\ast$ (v1.110-90);

[-latex] (v3.70-90) .. controls +(60-90:4em) and +(120-90:4em) .. node[pos=.5,fill=white,right,xshift=.5ex]()$\ast,\ast$ (v3.110-90);

[-latex] (v4.70-90) .. controls +(60-90:4em) and +(120-90:4em) .. node[pos=.5,fill=white,right,xshift=.5ex]()$\ast,\ast$ (v4.110-90);

every ellipse node=[draw,inner xsep=3.5em,inner ysep=1.2em,fill=black!15!white,draw=black!15!white]
every circle node=[fill=white,draw,minimum size=1.6em,inner sep=0pt]

(0,-3)	node();
(7.8,3.25)	node();

(0,0) node(0)
++ 	( 0:.9)	  node[label=-90:$p$,circle](v0)$t_0$

+ (.8*6,.8*3)  node[label=-90:$p$,circle](v1)$t_1$

+ (.8*6,.8*0) node[label=-90:$p$,circle](v3)$t_2$
+ (.8*6,.8*-3) node[label=-90:$\bar p$,circle](v4)$t_3$

[-latex] (v0) –node[pos=.55,fill=white]()$\begin{array}{l}a,a\\a,b\end{array}$ (v1);

[-latex] (v0) –node[pos=.55,fill=white]()$\begin{array}{l}b,a\end{array}$ (v3);
[-latex] (v0) –node[pos=.55,fill=white]()$\begin{array}{l}b,b\end{array}$  (v4);

[-latex] (0) – (v0);

[-latex] (v1.70-90) .. controls +(60-90:4em) and +(120-90:4em) .. node[pos=.5,fill=white,right,xshift=.5ex]()$\ast,\ast$ (v1.110-90);

[-latex] (v3.70-90) .. controls +(60-90:4em) and +(120-90:4em) .. node[pos=.5,fill=white,right,xshift=.5ex]()$\ast,\ast$ (v3.110-90);

[-latex] (v4.70-90) .. controls +(60-90:4em) and +(120-90:4em) .. node[pos=.5,fill=white,right,xshift=.5ex]()$\ast,\ast$ (v4.110-90);

Two games $G_2$ (left) and $G_3$ (right) based on $M_2$ and $M_3$, respectively, showing that run-based preferences may not be preserved across bisimilar systems.

This preservation of preference type under bisimilarity, however, does
not extend to run-based preferences. To see this, consider
Figure <ref> and let the goal
set $\goalset_i$ of some player $i$ be given by all
computations $\computation=d_0,d_1,d_2,\dots$ with $d_0=(a,a)$.
obviously, $\goalset_i$ is run-based in the game $G_2$ based on $M_2$ on the left, but not in the game $G_3$ based on $M_3$ to the right.

To see the latter, consider any computation $\computation'=d'_0,d_1',d_2',\dots$ with $d'_0=(a,b)$.
Then, $\computation'\notin\goalset_i$, but, nevertheless, in $G_3$ we have $\run_{M_3}(\computation)=\run_{M_3}(\computation')$.
By contrast, the goal set given by all
computations $\computation=d_0,d_1,d_2,\dots$ such that $d_0\neq(b,b)$ is
run-based in both games.

§.§ Computation-based Strategies

If strategies are computation-based, players can have their actions
depend on virtually all information that is available in the
system. In an important sense full transparency prevails and different
actions can be chosen on bisimilar states provided that the
computations that led to them are different. Moreover, the strategies
available to players in bisimilar concurrent game structures are
identical. Thus we obtain our first main result.

Let $G=(M,\goalset_1,\dots,\goalset_n)$ and $G'=(M',\goalset_1,\dots,\goalset_n)$ be games on bisimilar concurrent game structures $M$ and $M'$, respectively, and let  $f=(f_1,\dots,f_n)$ be a computation-based profile.
Then, $f$ is a Nash equilibrium in computation-based strategies in $G$ if and only if $f$ is a Nash equilibrium in computation-based strategies in $G'$.

First assume

for contraposition that $f=(f_1,\dots,f_n)$ is not a Nash equilibrium in computation-based strategies in $M'$.
Then, there is a player $i$ and a strategy $g_i$ for $i$ in $M'$ such that $\computation_{M'}(f)\notin\goalset_i$ and $\computation_{M'}( f_{-i},g_i)\in\goalset_i$.
Observe that, as the computation-based strategies of players in bisimilar structures coincide (cf., Lemma <ref>), $f$ is also a strategy profile in $M$ and $g_i$ a strategy for $i$ in $M$.
Moreover, recall that the computations induced by the same strategy profile in different but bisimilar structures are identical (cf., second part of Lemma <ref>). This yields $\computation_{M}(f)=\computation_{M'}(f)$
and $\computation_{M}(f_{-i},g_i)=\computation_{M'}(f_{-i},g_i)$.
Accordingly, $\computation_{M}(f)\notin\goalset_i$ whereas
We may conclude that $f$ is not a computation-based equilibrium in $M$ either. The opposite direction follows by an analogous argument.

Theorem <ref> holds for computation-based preferences. As run-based preferences and trace-based preferences  are computation-based preferences of a special kind, the result immediately extends to games in which the players' preferences are run-based in both games or trace-based preferences in both games.

As a consequence of Theorem <ref>, moreover, we find that sustenance of runs and traces by computation-based equilibrium is also preserved under bisimilarity.

Let $G=(M,\goalset_1,\dots,\goalset_n)$ and $G'=(M',\goalset_1,\dots,\goalset_n)$ be games on bisimilar concurrent game structures $M$ and $M'$, respectively, $\computation\in\computations_{M}$, and $\trace\in\traces_M$.

*  $\computation$  is sustained by computation-based equilibrium in $G$ if and only if $\computation$  is sustained by a computation-based equilibrium in $G'$.

*  $\trace$ is sustained by a computation-based equilibrium in $G$ if and only if $\trace$ is sustained by a computation-based equilibrium in $G'$.

Recall that by Lemma <ref>, we have that $\computation\in\computations_{M'}$ and $\trace\in\traces_{M'}$.
For part <ref>, let $\computation_M(f)=\computation$, where $f$ is a computation-based equilibrium in $G'$. Then, by Theorem <ref>, profile $f$ is a computation-based equilibrium in $G'$ as well. By virtue of Lemma <ref>, moreover,
$\computation_M(f)=\computation_{M'}(f)$, which gives the result. The implication in the other direction follows by the same argument mutatis mutandis.

The argument for part <ref> runs along analogous lines. First assume that $\trace$ is sustained by computation-based equilibrium $f$, that is, $\trace=\trace_M(f)$.
By Theorem <ref>, we have that $f$ is a computation-based equilibrium in $G'$ as well.
Now consider $\computation_M(f)$. By Lemma <ref> then  $\computation_{M'}(f)=\computation_M(f)$. Lemma <ref> then yields $\trace_M(\computation_M(f))=\trace_{M'}(\computation_{M'}(f))$. It thus follows that $\trace$ is sustained by $f$, a computation based Nash equilibrium, in $G'$.
The argument in the opposite direction is analogous, giving the result.

§.§ Trace-based Strategies

As we saw in Lemma <ref>, the sets of (finite) traces of two bisimilar concurrent game structures coincide. Lemma <ref> shows that the same holds for the trace-based strategies that are available to the players.
As a consequence,
we can directly compare their trace-based Nash-equilibria. We find that, like computation-based equilibria, trace-based Nash equilibria are preserved in  CGS-games based on bisimilar concurrent game structures.

Let $G=(M,\goalset_1,\dots,\goalset_n)$ and
$G'=(M',\goalset_1,\dots,\goalset_n)$ be games on bisimilar
concurrent game structures $M$ and $M'$, respectively, and
$f=(f_1,\dots,f_n)$ be a trace-based strategy profile.
Then, $f$ is a Nash equilibrium in trace-based strategies in $G$ if
and only if $f$ is a Nash equilibrium in trace-based strategies
in $G'$.

The proof is analogous to the one for Theorem <ref> for the computation-based case.
First assume

for contraposition that $f=(f_1,\dots,f_n)$ is not a Nash equilibrium in trace-based strategies in $M'$.
Then, there is a player $i$ and a trace-based strategy $g_i$ for $i$ in $M'$ such that $\computation(f)\notin\goalset_i$ and $\computation( f_{-i},g_i)\in\goalset_i$.
Observe that, as the trace-based strategies of players in bisimilar structures coincide (cf., Lemma <ref>),
we have that $f$ is also a trace-based strategy profile in $M$ and $g_i$ a trace-based strategy for $i$ in $M$.
By the second part of Lemma <ref>, moreover, $\computation_{M}(f)=\computation_{M'}(f)$
and $\computation_{M}(f_{-i},g_i)=\computation_{M'}(f_{-i},g_i)$.
Accordingly, $\computation_{M}(f)\notin\goalset_i$ whereas
We may conclude that $f$ is not a trace-based equilibrium in $M$ either. The opposite direction follows by an analogous argument.

Like Theorem <ref>, this result is for computation-based preferences in general, and as such immediately extends
to the case in which the players' preferences are stipulated to be run-based in both games or trace-based in both games. Theorem <ref> has further the following result as an immediate consequence, which is analogous to Corollary <ref>.

Let $G=(M,\goalset_1,\dots,\goalset_n)$ and $G'=(M',\goalset_1,\dots,\goalset_n)$ be games on bisimilar concurrent game structures $M$ and $M'$, respectively, $\computation\in\computations_{M}$, and $\trace\in\traces_M$.

*  $\computation$  is sustained by trace-based equilibrium in $G$ if and only if $\computation$  is sustained by a trace-based equilibrium in $G'$.

*  $\trace$ is sustained by a trace-based equilibrium in $G$ if and only if $\trace$ is sustained by a trace-based equilibrium in $G'$.

The proof is analogous to the one for Corollary <ref>.

§.§ Run-based Strategies

The positive results obtained using computation-based and trace-based
strategies are now followed by a negative result, already
mentioned in the introduction of the paper, which establishes that
Nash equilibria in run-based strategies—the most widely-used
strategy model in logic, computer science, and AI—are not preserved by
bisimilarity. Previously we observed that the players'
run-based strategies cannot straightforwardly be identified across two
different concurrent game structures, even if they are
bisimilar. We would therefore have to establish a correspondence
between the run-based strategies in the one game and the run-based
strategies in the other in an arguably ad hoc way. To cut this Gordian
knot, we therefore show in this section the stronger result that the
very existence of run-based equilibria is not preserved under
bisimilarity.  That is, we can have two bisimilar concurrent game
structures, say $M$ and $M'$, on which we base two games $G$
and $G'$ with congruent preferences, such that $G$ has a Nash equilibrium and $G'$
does not.

The existence of run-based Nash equilibria is not preserved under bisimilarity. That is, there are games $(M,\goalset_1,\dots,\goalset_n)$
and $(M',\goalset_1,\dots,\goalset_n)$ on bisimilar concurrent game structures $M$ and $M'$ such that a  Nash equilibrium in run-based strategies exists in $G$ but not in $G'$.

To see that the above statement holds,
consider again the three-player game $G_0$ on the concurrent game structure $M_0$ in Figure <ref>. Assume, as before, that player $1$'s goal set $\goalset_1$ is given by those computations $\computation$ such that $\trace_{M_0}(\computation)=v_0,v_1,v_2,\dots,$ implies $p\in v_k$ for some $k\ge 0$. Similarly, $\goalset_2$ consists of all computations $\computation$ with $\trace_{M_0}(\computation)=v_0,v_1,v_2,\dots$ and $q\in v_k$ for some $k\ge 0$ and $\goalset_3$ by those computations $\computation$ with $\trace_{M_0}(\computation)=v_0,v_1,v_2,\dots$ and $v_k=\emptyset$ for all $k\ge0$. Recall that, consequently, the preferences of players $1$, $2$, and $3$ are trace-based and can be represented by the LTL formulas  $	\gamma_1=	\sometime p$,
$\gamma_2		=	\sometime q$, and
$ 	\gamma_3		=	\always \neg(p\vee q)$, respectively.

Let $f^*_1$ and $f^*_2$ be any run-based strategies for players $1$ and $2$ such that $f^*_1(s_0)=f^*_2(s_0)=a$. Let, furthermore, player $3$'s run-based strategy $f^*_3$ be such that

\[
\text{
$f^*_3(s_0)		=	a$,\quad
$f^*_3(s_0,s_1)		= 	a'$,\quad and \quad
$f^*_3(s_0,s'_1)		=	b$.}
\]

Let $f^*=(f^*_1,f^*_2,f^*_3)$ and observe that $\run_{M_0}(f^*)=s_0,s_4,s_4,s_4,\dots$. Accordingly, player $3$ has her goal achieved and does not want to deviate from $f^*$. Players $1$ and $2$ do not have their goals achieved, but do not want to deviate from $f^*$ either. To see this, let $g_1$ be any run-based strategy for $1$ such that $g_1(s_0)=b$; observe that this is required for any meaningful deviation from $f^*$ by $1$. Then $\run_{M_0}(g_1,f^*_2,f^*_3)=s_0,s_1,s_3,s_3,s_3,\dots$ or
$\run_{M_0}(g_1,f^*_2,f^*_3)=s_0,s_1,s_4,s_4,s_4,\dots$, depending on whether $f^*_2(s_0,s_1)=b$ or $f^*_2(s_0,s_1)=a$, respectively. In either case, player $1$ does not get his goal achieved and it follows that he does not want to deviate from $f^*$. An analogous argument—notice that the roles of player $1$ and $2$ are symmetric—shows that player $2$ does not want to deviate from $f^*$ either. We may thus conclude that $f^*$ is a run-based equilibrium in $G_0$.

Now, consider the game $G_1$ on concurrent game structure $M_1$ in Figure <ref> with the players' preferences as in $M_0$. It is easy to check that $M_0$ and $M_1$ are bisimilar. Still, there is no run-based equilibrium in $G_1$. To see this, consider an arbitrary run-based strategy profile $f=(f_1,f_2,f_3)$.

First, assume that $\run_{M_1}(f)=s_0,s_1,s_2,s_2,s_2,\dots$. Then, player $1$ gets his goal achieved and  players $2$ and $3$ do not. If $f_1(s_0,s_1)=a$ then $f_3(s_0,s_1)=b$ and player $3$ would like to deviate and play a strategy $g_3$ with $g_3(s_0,s_1)=a$. On the other hand, if $f_1(s_0,s_1)=b$, player $3$ would like to deviate and play a strategy $g_3$ with $g_3(s_0,s_1)=b$.

Player $3$ would similarly like to deviate from $f$ if we assume that $\run_{M_1}(f)=s_0,s_1,s_3,s_3,s_3\dots$, in whose case it is player $2$ who gets his goal achieved.

Now, assume that $\run_{M_1}(f)=s_0,s_1,s_4,s_4,s_4\dots$. In this case player $3$ does get her goal achieved, but players $1$ and $2$ do not. However, player $1$ would like to deviate and play a strategy $g_1$ with $g_1(s_0,s_1)=b$ or $g_1(s_0,s_1)=a$, depending on whether $f_3(s_0,s_1)=a$ or $f_3(s_0,s_1)=b$;
in a similar fashion, player $2$ would like to deviate and play a strategy $g_2$ with $g_2(s_0,s_1)=b$ if $f_1(s_0,s_1)=a'$, and to one with $g_2(s_0,s_1)=a$ if $f_1(s_0,s_1)=b'$.

Finally, assume that $\run_{M_1}(f)=s_0,s_4,s_4,s_4,\dots$. Then, neither player $1$ nor player $2$ gets his goal achieved. Now either $f_3(s_0,s_1)\in\set{a,b}$ or $f_3(s_0,s_1)\in\set{a',b'}$. If the former, player $1$ would like to deviate and play a strategy $g_1$ with $g_1(s_0)\neq f_1(s_0)$ and $g_1(s_0,s_1)\neq f_3(s_0,s_1)$. If the latter, player $2$ would like to deviate and play a strategy $g_2$ with $g_2(s_0)\neq f_2(s_0)$ and either $g_2(s_0,s_1)=b$ if $f_3(s_0,s_1)=a'$ or $g_2(s_0,s_1)=a$ if $f_3(s_0,s_1)=b'$.
We can then conclude that the CGS-game $G_1$ does not have any run-based Nash equilibria.

The main idea behind this counter-example is that in $G_0$ player $3$
could distinguish which player deviates from $f^*$ if the state
reached after the first round is not $s_4$: if that state is $s_1$, it
was player $1$ who deviated, otherwise player $2$. By choosing
either $a'$ or $b'$ at $s_1$, and either $a$ or $b$ at $s'_1$,
player $3$ can guarantee that neither player $1$ nor player $2$ gets
his goal achieved (“punish” them) and thus deter them from deviating
from $f^*$. This possibility to punish deviations from $f^*$ by players $1$
and $2$ in a single strategy is not available in the game on $M_1$:
choosing from $a$ and $b$ will induce a deviation by player $1$,
choosing from $a'$ and $b'$ one by player $2$.

Observe that the games $G_0$ and $G_1$ do not constitute a
counter-example against either the preservation under bisimilarity of
computation-based equilibria or the preservation of trace-based
equilibria. The reasons why such games fail to do so, however, are different. For the setting of computation-based strategies, player $3$
can still distinguish and “punish” the deviating player in $G_1$
as $(a,b,a)$ and $(b,a,a)$ are different directions and player $3$ can
still have his action at $s_1$ depend on which of these is played
at $s_0$. By contrast, if we assume trace-based strategies, player $3$
has to choose the same action at both $s_1$ and $s'_1$ in $G_0$. As a
consequence, and contrarily to computation-based equilibria,
trace-based equilibria exist in neither $G_0$ nor $G_1$.
Please check this last remark.

Also note that the goal sets $\goalset_1$, $\goalset_2$, and $\goalset_3$ are run-based as well as computation-based both in $G_1$ and $G_2$. Accordingly, the counter-example also applies to settings wherein the players' preferences are assumed to be finer-grained in these two ways.

Observe at this point that $s_1$ and $s'_1$ are bisimilar states. Yet,
players are allowed to have run-based strategies
(which depend on state histories only) that choose different actions
at bisimilar states. The above counter-example shows how this relative
richness of strategies
makes a crucial difference. This raises the question as to whether we
actually want players to adopt run-based strategies in which they choose
different actions at bisimilar states. This observation leads us to the next

§.§ Bisimulation-invariant Run-based Strategies

Bisimilarity formally captures an informal concept of observational
indistinguishability on the part of an external observer of the
system. Now, the players in a concurrent game structure are in
essentially the same situation as an external observer if they are
assumed to be only able to observe the behaviour of the other players,
without knowing their internal structure or their interaction.

Drawing on this idea of indistinguishability, it is natural that
players cannot distinguish statewise bisimilar runs and, as a
consequence, can only adopt strategies that choose the same action at
runs that are statewise bisimilar. The situation is comparable to the
one in extensive games of imperfect information, in which players are
required to choose the same action in histories that are in the same
information set, that is, histories that cannot be distinguished (cf., e.g.,
[37, 32]).

To make this idea formally precise, we say that a run-based strategy
$f_i$ is bisimulation-invariant if $f_i(\finrun)=f_i(\finrun')$
for all histories $\finrun$ and $\finrun'$ that are statewise

The concept of Nash equilibrium is then similarly restricted to
bisimulation-invariant strategies. A profile
$\stratprof=(\strategy_1,\dots,\strategy_n)$ of
bisimulation-invariant strategies is a Nash equilibrium
in bisimulation-invariant strategies (or a
bisimulation-invariant equilibrium) in a game
$(M,\goalset_1,\dots,\goalset_n)$ if for all players $i$ and every
bisimulation-invariant strategy $g_i$ for $i$,

\[
\scalebox{1}[1]{$\trace(f_{-i},g_i)\in\goalset_i$ implies
% $\trace(f_1,\dots,f_n)\in\goalset_i$.
\]

That is, $f$ is a bisimulation-invariant equilibrium if no player wishes to deviate from $f$ by playing a different bisimulation-invariant strategy.
In contrast to the situation for general run-based strategies, we
find that computations and traces that are sustained by a
bisimulation-invariant Nash equilibrium are preserved by
bisimulation. We show this by establishing a one-to-one correspondence
between the bisimulation-invariant strategies available to the players
in two bisimilar structures.

Based on the concept of state-wise bisimilarity, we associate with
every bisimulation-invariant strategy $f_i$ for player $i$ in
concurrent game structure $M$, another bisimulation-invariant
strategy $\tilde f_i$ for player $i$ in any bisimilar concurrent game
structure $M'$ such that for all $\finrun\in\finruns_{M'}$ and

\[
\scalebox{.97}[1]{
$\tilde f_i(\finrun)
\quad if $f_i(\finrun')=a$ for some $\finrun'\in\finruns_M$ with $\finrun\pairwisebisim\finrun'$.
\]

Transitivity of $\pairwisebisim$ guarantees that $\tilde f_i$ is well
defined. To see this, observe that for all $\pi',\pi''\in\finruns_M$
with $\pi'\pairwisebisim \pi$ and $\pi''\pairwisebisim\pi$,

we have $\pi'\pairwisebisim\pi''$.
Having assumed that $f_i$ is bisimulation-invariant, then
$f_i(\pi')=f_i(\pi'')$. By very much the same argument, $\tilde f_i$
bisimulation-invariant, if $f_i$ is.

Let $M$ and $M'$ be bisimilar concurrent game structures and let $f_i$ be a bisimulation-invariant strategy for player $i$ in $M$. Then, $\tilde f_i$ is a bisimulation-invariant strategy in $M'$.

Consider two statewise bisimilar runs $\finrun,\finrun'\in\finruns_{M'}$, that is, $\finrun\pairwisebisim\finrun'$. Then, there are computations $\fincomputation,\fincomputation'\in\fincomputations_{M'}$ such that $\finrun_{M'}(\fincomputation)=\finrun$ and $\finrun_{M'}(\fincomputation')=\finrun'$.
By Lemma <ref>, we have  $\finrun_{M}(\fincomputation)\pairwisebisim\finrun_{M'}(\fincomputation)$ and $\finrun_{M}(\fincomputation')\pairwisebisim\finrun_{M'}(\fincomputation')$.
Now, transitivity of $\statewisebisim$ yields $\finrun_{M}(\fincomputation)\statewisebisim\finrun_{M}(\fincomputation')$.
Having assumed that $f_i$ is bisimulation-invariant, we obtain that
$f_i(\finrun_{M}(\fincomputation))=f_i(\finrun_M(\fincomputation'))$. Finally, we may conclude that $\tilde f_i(\finrun)=\tilde f_i(\finrun')$, as desired.

Moreover, it is easily appreciated that the mapping that transforms a strategy $f_i$ into
strategy $\tilde f_i$ is one-to-one. We will find that this is an essential property for bisimulation-invariant equilibria to be preserved under bisimilarity.

For a profile of bisimulation-invariant strategies $f=(f_1,\dots,f_n)$
in $M$ we denote $\tilde f=(\tilde f_1,\dots,\tilde f_n)$.  We then
find that profiles $f$ and $\tilde f$ of bisimulation-invariant
strategies induce identical computations.

Let $M$ and $M'$ be bisimilar concurrent game structures, $f=(f_1,\dots,f_n)$ a bisimulation-invariant strategy profile. Then,
$\computation_M(f)=\computation_{M'}(\tilde f)$.

Let $\computation_M(f)=d_0,d_1,d_2,\dots$ and $\computation_{M'}(\tilde f)=d'_0,d'_1,d'_2,\dots$. We prove by induction on $k$ that $d_k=d'_k$ for every $k\ge 0$. If $k=0$, we have $d_0=(f_1(s^0_M),\dots,f_n(s^0_M))$. Observe that, as $M\bisim M'$ also $s^0_M\bisim s^0_{M'}$ and, hence, $f_i(s^0_M)=\tilde f_i(s^0_{M'})$. Therefore,

\[
(\tilde f_1(s^0_{M'}),\dots,\tilde f_n(s^0_{M'}))
\]

For the induction step, we may assume that $d_0,\dots,d_k=d'_0,\dots,d_k'$.
By Lemma <ref>, then $\finrun_M(d_0,\dots,d_k)\statewisebisim\finrun_{M'}(d_0',\dots,d_k')$. Accordingly, for every player $i$ we have that $f_i(\finrun_M(d_0,\dots,d_k))=\tilde f_i(\finrun_{M'}(d'_0,\dots,d'_k))$.
It thus follows that

\begin{align*}
&	=
(\tilde f_1(\finrun_{M'}(d'_0,\dots,d_k')),\dots,\tilde f_n(\finrun_{M'}(d'_0,\dots,d_k')))\\
&	=
&	=
\end{align*}

This concludes the proof.

We are now in a position to state an equilibrium preservation theorem
for bisimulation-invariant strategies in a similar way as we were able
to obtain Theorem <ref>, the analogous result
for computation-based and trace-based strategies.

Let $G=(M,\goalset_1,\dots,\goalset_n)$ and
$G'=(M',\goalset_1,\dots,\goalset_n)$ be games on bisimilar
concurrent game structures $M$ and $M'$, respectively.
Then, $f$ is a bisimulation-invariant equilibrium in $G$ if and only if $\tilde
f$ is a bisimulation-invariant equilibrium in $G'$.

First assume

for contraposition  that $\tilde f=(\tilde f_1,\dots,\tilde f_n)$ is not a Nash equilibrium in bisimulation-invariant strategies in $G'$.
Then, there is a player $i$ and a bisimulation-invariant strategy $g_i$ for $i$ in $M'$ such that $\computation_{M'}(\tilde f)\notin\goalset_i$ and $\computation_{M'}(\tilde f_{-i},g_i)\in\goalset_i$.

As the mapping that transforms a strategy $f_i$ into
strategy $\tilde f_i$ is one-to-one, there is a bisimulation-invariant strategy $f'_i$ for $i$ in $M$ with $\tilde f'_i= g_i$.
Accordingly, $\computation_{M'}(\tilde f_{-i},\tilde f'_i)\in\goalset_i$. Lemma <ref> then yields that $\computation_M(f_{-i},f'_i)\in\goalset_i$ and $\computation_M(f)\notin\goalset_i$. As $f'_i$ is bisimulation-invariant, it follows that $f$ is not an equilibrium in bisimulation-invariant strategies in $G$.

The proof in the opposite direction runs along analogous lines.

As an immediate corollary of Theorem <ref>, it follows that the property of a computation or trace to be sustained by a bisimulation-invariant equilibria is also preserved  under bisimilarity.

Let $G=(M,\goalset_1,\dots,\goalset_n)$ and $G'=(M',\goalset_1,\dots,\goalset_n)$ be  games on bisimilar concurrent game structures $M$ and $M'$, respectively.
Then, for every computation $\computation\in\computations_M=\computations_{M'}$ and every trace $\trace\in\traces_{M}=\traces_{M'}$,

*  $\computation$  is sustained by a bisimulation invariant equilibrium in $G$ if and only if $\computation$ is sustained by a  bisimulation-invariant equilibrium in $G'$.

$\trace$ is sustained by a bisimulation-invariant equilibrium in $G$ if and only if $\trace$ is sustained by a bisimulation-invariant equilibrium in $G'$.

For part <ref>, assume that $\computation_M(f)=\computation$. Then in virtue of Lemma <ref> also $\computation_{M'}(\tilde f)=\computation$.
by Theorem <ref> we have that profile $f$ is a Nash equilibrium in bisimulation-invariant strategies in $G$ if and only if $\tilde f$ is a Nash equilibrium in bisimulation-invariant strategies in $G'$, which gives the result.

The argument for part <ref> runs along analogous lines. First assume that $\trace$ is sustained by bisimulation-invariant Nash equilibrium $f$. Let $\computation=\computation_{M}(f)$. Then, $\trace=\trace_{M}(\computation)$. By Theorem <ref>, moreover, $\tilde f$ is a bisimulation-invariant Nash equilibrium in $G'$. An application of Lemma <ref> yields $\computation_M(\tilde f)=\computation_M(f)$. By Lemma <ref> then $\trace_M(\computation)=\trace_{M'}(\computation)$. It follows that $\trace$ is sustained by $\tilde f$, a bisimulation-invariant Nash equilibrium, in $G'$.
The argument in the opposite direction is analogous, giving the result.

§ SPECIAL CASES

In the previous section we provided results about the preservation of
a given Nash equilibrium under bisimilarity, specifically, as long as we
do not consider run-based strategies or goals. In this
section we study two important special scenarios where
this is not the case.

Firstly, consider the scenario where we have two-player games with
run-based strategies and trace-based goals. This is an important
special case since run-based strategies, as we emphasised in the
introduction, are the “conventional” model of strategies used in
logics such as ATL$^*$ or SL, as well as in systems represented as concurrent
game structures. In particular, we show that with respect to
two-player games with run-based strategies and trace-based goals
(which include temporal logic goals), the
setting coincides with the one with bisimulation-invariant strategies
and trace-based goals, for which the preservation of Nash equilibria
under bisimilarity holds. A key observation in this case is that in
two-player games the existence of Nash equilibria can be characterised
in terms of the existence of certain winning strategies, which are
preserved across bisimilar systems.

Secondly, we also study the scenario where concurrent game structures are restricted to those that are induced by iterated Boolean games [23] and Reactive Modules games [48], two frameworks for the strategic analysis of AI and multi-agent systems, in particular, using model checking techniques.
[For instance, Reactive Modules games provide a game semantics to formal specification languages such as Reactive Modules [2], which is widely used in model checking tools,
such as MOCHA [4] and PRISM [31].]
In this case, we show that bisimulation-invariant strategies also
coincide with run-based strategies, and therefore, that the positive
results for bisimulation-invariant strategies presented in the
previous section also transfer to this special case.

§.§ Two-Player Games

This section concerns the preservation under bisimilarity of Nash equilibria under bisimulation in two-player games. We deal with the cases in which the players' preferences are computation-based, trace-based, and run-based separately.

§.§.§ Computation-based Preferences

The counter-example against the preservation of the existence of Nash equilibria in Section <ref> involved three players. We find that, if preferences are computation-based, the example can be adapted so as to involve only two players, which gives rise to the following result.

every ellipse node=[draw,inner xsep=3.5em,inner ysep=1.2em,fill=black!15!white,draw=black!15!white]
every circle node=[fill=white,draw,minimum size=1.6em,inner sep=0pt]

(0,0) node(0)
++ 	( 0:.9)	  	node[label=-90:$\bar p\bar q$,circle](v0)$s_0$
++	(  0:3)   	node[label=-90:$\bar p\bar q$,circle](v1)$s_1'$
+( 90:3)  	node[label=-90:$\bar p\bar q$,circle](w1)$s_1$
++( 0:5)  	node[label=-90:$\bar p     q$,circle](v3)$s_3$
+( 90:3)  	node[label=-90:$     p\bar q$,circle](v2)$s_2$
+(-90:4.5)	node[label=-90:$\bar p\bar q$,circle](v4)$s_4$

[-latex] (v0) –node[inner xsep=0pt, inner ysep=0pt, pos=.5,fill=white]()
\mwbactionstwo{c}{a}{\bthree}
% \\[-.2em]
% \mwbactionstwo{c}{a}{\bthree}\\[-.2em]
% \mwbactionstwo{\bonetwooo}{\btwo}{\athree}\\[-.2em]
% \mwbactionstwo{\bonethree}{\btwo}{\athree}
\end{array}$ (v1);

[-latex] (v0) –node[inner xsep=0pt, inner ysep=0pt, pos=.5,fill=white]()
\mwbactionstwo{b}{a}{\athree}
% \\[-.2em]
% \mwbactionstwo{a}{}{\athree}\\[-.2em]
% \mwbactionstwo{\bonetwooo}{\atwo}{\bthree}\\[-.2em]
% \mwbactionstwo{\bonethree}{\atwo}{\bthree}
\end{array}$ (w1);

[-latex] (v0) to[bend right=25]node[inner xsep=0pt, inner ysep=0pt, pos=.545,fill=white]()
\mwbactionstwo{a}{a}{\athree}
% \\[-.2em]
% \mwbactionstwo{\aonethree}{\atwo}{\athree}\\[-.2em]
% \mwbactionstwo{\bonetwooo}{\btwo}{\bthree}\\[-.2em]
% \mwbactionstwo{\ast}{\btwo}{\bthree}
\end{array}$ (v4);

[-latex] (v1) –node[inner xsep=0pt, inner ysep=0pt, pos=.7,fill=white]().85$\begin{array}{l}\mwbactionstwo{a}{b}{\ast}\\[-.2em]\mwbactionstwo{\bonetwooo}{\atwo}{\ast}\end{array}$ (v2);

[-latex] (v1) –node[inner xsep=0pt, inner ysep=0pt, pos=.7,fill=white]().85$\begin{array}{l}\mwbactionstwo{a}{b'}{\bthree}\\[-.2em]\mwbactionstwo{b}{a'}{\athree}\end{array}$ (v3);

[-latex] (w1) –node[inner xsep=0pt, inner ysep=0pt, pos=.7,fill=white]().85$\begin{array}{l}\mwbactionstwo{a}{b}{\ast}\\[-.2em]\mwbactionstwo{\bonetwooo}{\atwo}{\ast}\end{array}$ (v2);

[-latex] (w1) –node[inner xsep=0pt, inner ysep=0pt, pos=.7,fill=white]().85$\begin{array}{l}\mwbactionstwo{a}{b'}{\bthree}\\[-.2em]\mwbactionstwo{b}{a'}{\athree}\end{array}$ (v3);

[-latex] (v1) to[bend right=17.5]node[inner xsep=0pt, inner ysep=0pt, pos=.45,fill=white,fill opacity=1]().85$\begin{array}{l}\mwbactionstwo{a}{a}{\ast}\\[-.2em]\mwbactionstwo{a}{a'}{\ast}\\[-.2em]\mwbactionstwo{b}{b}{\athree}\\[-.2em]\mwbactionstwo{b}{b'}{\bthree}\end{array}$ (v4);

[-latex] (w1) –node[inner xsep=0pt, inner ysep=0pt, pos=.565,fill=white,fill opacity=1]().85$\begin{array}{l}\mwbactionstwo{a}{a}{\ast}\\[-.2em]\mwbactionstwo{a}{a'}{\ast}\\[-.2em]\mwbactionstwo{b}{b}{\athree}\\[-.2em]\mwbactionstwo{b}{b'}{\bthree}\end{array}$ (v4);

[-latex] (0) – (v0);

[-latex] (v2.70-90) .. controls +(60-90:4em) and +(120-90:4em) .. node[pos=.5,fill=white,right,xshift=.5ex]()$\ast,\ast,\ast$ (v2.110-90);

[-latex] (v3.70-90) .. controls +(60-90:4em) and +(120-90:4em) .. node[pos=.5,fill=white,right,xshift=.5ex]()$\ast,\ast,\ast$ (v3.110-90);

[-latex] (v4.70-90) .. controls +(60-90:4em) and +(120-90:4em) .. node[pos=.5,fill=white,right,xshift=.5ex]()$\ast,\ast,\ast$ (v4.110-90);

The concurrent game structure $M_4$ underlying the game $G_4$.

every ellipse node=[draw,inner xsep=3.5em,inner ysep=1.2em,fill=black!15!white,draw=black!15!white]
every circle node=[fill=white,draw,minimum size=1.6em,inner sep=0pt]

(0,0) node(0)
++ 	( 0:.9)	  node[label=-90:$\bar p\bar q$,circle](v0)$s_0$
++	(  20:3.5)  node[label=-90:$\bar p\bar q$,circle](v1)$s_1$
+( 20:4)  node[label=-90:$     p\bar q$,circle](v2)$s_2$
+(-20:4)  node[label=-90:$\bar p     q$,circle](v3)$s_3$
(0,.9) ++(-27.5:9)	node[label=-90:$\bar p\bar q$,circle](v4)$s_4$;

[-latex] (v0) –node[inner xsep=0pt, inner ysep=0pt,pos=.5,fill=white]().85$\begin{array}{l}\mwbactionstwo{b}{a}{\bthree}\\\mwbactionstwo{c}{a}{\athree}\end{array}$ (v1);

[-latex] (v1) –node[inner xsep=0pt, inner ysep=0pt,pos=.5,fill=white]().85$\begin{array}{l}\mwbactionstwo{a}{b}{\ast}\\\mwbactionstwo{b}{a}{\ast}\end{array}$ (v2);

[-latex] (v1) –node[inner xsep=0pt, inner ysep=0pt,pos=.5,fill=white]().85$\begin{array}{l}\mwbactionstwo{a}{b'}{\bthree}\\\mwbactionstwo{b}{a'}{\athree}\end{array}$ (v3);

[-latex] (v0) to[bend right=0]node[inner xsep=0pt, inner ysep=0pt,pos=.5,fill=white]().85$\begin{array}{l}
\mwbactionstwo{a}{a}{\athree}
% \\[-.2em]
% \mwbactionstwo{\aonethree}{\atwo}{\athree}\\[-.2em]
% \mwbactionstwo{\bonetwooo}{\btwo}{\bthree}\\[-.2em]
% \mwbactionstwo{\ast}{\btwo}{\bthree}
\end{array}$ (v4);

[-latex] (v1) to[bend right=0]node[inner xsep=0pt, inner ysep=0pt,pos=.5,fill=white]()1.85$\begin{array}{l}\mwbactionstwo{a}{a}{\ast}\\[-.2em]\mwbactionstwo{a}{a'}{\ast}\\[-.2em]\mwbactionstwo{b}{b}{\athree}\\[-.2em]\mwbactionstwo{b}{b'}{\bthree}\end{array}$ (v4);

[-latex] (0) – (v0);

[-latex] (v2.70-90) .. controls +(60-90:4em) and +(120-90:4em) .. node[pos=.5,fill=white,right,xshift=.5ex]()$\ast,\ast,\ast$ (v2.110-90);

[-latex] (v3.70-90) .. controls +(60-90:4em) and +(120-90:4em) .. node[pos=.5,fill=white,right,xshift=.5ex]()$\ast,\ast,\ast$ (v3.110-90);

[-latex] (v4.70-90) .. controls +(60-90:4em) and +(120-90:4em) .. node[pos=.5,fill=white,right,xshift=.5ex]()$\ast,\ast,\ast$ (v4.110-90);

The concurrent game structure $M_5$ underlying the game $G_5$.

There are two-player games $(M,\goalset_1,\goalset_2)$
and $(M',\goalset_1,\goalset_2)$ on bisimilar concurrent game structures $M$ and $M'$ with $\goalset_1$ and $\goalset_2$ computation-based such that a run-based Nash equilibrium exists in $G$ but not in $G'$.

Consider the concurrent game structures $M_4$ and $M_5$ depicted in Figures <ref> and <ref>, respectively.
Observe that
$\actions_1(s_0)=\set{a,b,c}$ and $\actions_1(s)=\set{a,b}$ at all states $s$ distinct from $s_0$, and that
$\actions_2(s_0)=\set{a}$ and $\actions_2(s)=\set{a,a',b,b'}$ at all states $s$ distinct from $s_0$.
We define the games $G_4=(M_4,\goalset_1,\goalset_2)$ and $G_5=(M_5,\goalset_1,\goalset_2)$ by letting
$\goalset_1$ contain exactly those computations $\computation=d_0,d_1,d_2,\dots$
such that either $d_0=(b,a)$ and $d_1\in\set{(a,b),(b,a)}$ or $d_0=(c,a)$ and $d_1\in\set{(a,b'),(b,a')}$, and
letting $\goalset_2$ consist precisely of those computations $\computation=d_0,d_1,d_2,\dots$ such that
$d_0=(a,a)$ or $d_1\in\set{(a,a),(a,a'),(b,b),(b,b')}$. By an argument analogous to that presented in Section <ref>, it can then be appreciated that $G_4$ has a run-based equilibrium, whereas $G_5$ has not.

To see the former, observe that any run-based profile $f^*=(f^*_1,f^*_2)$ will be an equilibrium if
$f^*_1(s_0)=f^*_2(s_0)=a$, $f^*_2(s_1)\in\set{a',b'}$, and $f^*_2(s_1')\in\set{a,b}$. For every strategy $g_1$ for player $1$, we then have $\computation_{M_4}(g_1,f^*_2)\notin\goalset_1$, whereas $\computation_{M_4}(f^*_1,f^*_2)\in\goalset_2$.

To see that $G_5$ has no run-based equilibrium, first let $f=(f_1,f_2)$ be a run-based profile such that $\computation_{M_5}(f_1,f_2)\notin\goalset_1$.
Then, if $f_2(s_0,s_1)=a$, player $1$ would like to deviate and play a strategy $g_1$ with $g_1(s_0)=g_1(s_0,s_1)=b$; if $f_2(s_0,s_1)=a'$, to deviate and play a strategy $g'_1$ with
$g'_1(s_0)=c$ and $g'_1(s_0,s_1)=b$; if $f_2(s_0,s_1)=b$ to deviate and play a strategy $g''_1$ with $g''_1(s_0)=b$ and $g''_1(s_0,s_1)=a$; and, finally, if $f_2(s_0,s_1)=b'$ to deviate and play a strategy $g'''_1$ with $g'''_1(s_0)=c$ and $g'''_1(s_0,s_1)=a$. On the other hand, if $\computation_{M_3}(f_1,f_2)\notin\goalset_2$, it must be the case that $f_1(s_0)\in\set{b,c}$. Observe, however, that player $2$ would then like to deviate and play any strategy $g_2$ with $g_2(s_0,s_1)=a$ if $f_1(s_0,s_1)=a$ and to a strategy $g'_2$ with $g'_2(s_0,s_1)=b$ if $f_1(s_0,s_1)=b$. As, furthermore, $\goalset_1$ and $\goalset_2$ are disjoint, that is, the goals players $1$ and $2$ cannot simultaneously be satisfied, it follows that $G_5$ has no run-based equilibria.

§.§.§ Run-based Preferences

We now address the preservation (of the existence) of Nash equilibria in two-player CGS-games where both preferences and strategies are run-based.
In contrast to our findings in the previous section, we find that,
under a natural closure restriction on the players' preferences, we are able to obtain a positive result.
Our proof relies on the equivalence of run-based profiles and run-invariant profiles as expounded in Section <ref>.

As already noted above, run-based strategies cannot generally be identified directly across  bisimilar CGS-games. The reason for this complication is that runs are sequences of states, and the sets of states of the two CGS-games need not coincide. In Section <ref>, we saw, however, how run-based strategies correspond to run-invariant strategies, which are computation-based by definition.  Lemma <ref>, moreover, allows us to compare computation-based strategies, even if they may be run-invariant in the one model but not in the other.

Let $f=(f_1,f_2)$ be a given run-invariant equilibrium  in a CGS-game $G=(M,\goalset_1,\goalset_2)$ based on $M$ and let $G'=(M',\goalset_1,\goalset_2)$ be a CGS-game based on a concurrent game structure $M'$ bisimilar to $M$.
We  define
a (computation-based) profile $f^K=(f^K_1,f^K_2)$ that is a run-invariant equilibrium in both $G$ and $G'$.
To prove that $f^K=(f^K_1,f^K_2)$ is a run-invariant equilibrium if $f=(f_1,f_2)$ is,
we exploit a characterisation of Nash equilibria in terms of winning strategies.
[Winning strategies have also been used to characterise the existence of Nash equilibria in other two-player games with binary outcomes—see, e.g., [22, 27].]
We say that a run-invariant strategy $f_i$ for player $i$ is winning against player $j$ whenever $\computation_M(f_i,f_j)\notin\goalset_j$ for all run-invariant strategies $f_j$ of player $j$. We then have the following lemma, which is independent of the type of preferences that players have.

Let $G=(M,\goalset_1,\goalset_2)$ be a game. Then, a profile
$f=(f_1,f_2)$ is a run-invariant equilibrium if and only if

*  $\computation_M(f_1,f_2)\notin\goalset_1$ implies that $f_2$ is a winning strategy against player $1$, and

*  $\computation_M(f_1,f_2)\notin\goalset_2$ implies that $f_1$ is a winning strategy against player $2$.

For the “if” direction assume for contraposition that $f=(f_1,f_2)$ is not a run-invariant equilibrium. Then, either $\computation_M(f_1,f_2)\notin\goalset_1$ and $\computation_M(g_1,f_2)\in\goalset_1$ for some run-invariant strategy $g_1$ for player $1$, or $\computation_M(f_1,f_2)\notin\goalset_2$ and $\computation_M(f_1,g_2)\in\goalset_2$ for some run-invariant strategy $g_2$ for player $2$. If the former, $f_2$ is not winning against player $1$, refuting <ref>. If the latter, $f_1$ is not winning  against player $2$, which refutes <ref>.

The opposite direction is also by contraposition. Assume that either <ref> or <ref> is not satisfied. Without loss of generality we may assume the former.
Then, $\computation_M(f_1,f_2)\notin\goalset_1$ and $f_2$ is not a winning strategy against player $1$. Accordingly, there is some run-invariant strategy $g_1$ for player $1$ such that $\computation_{M}(g_1,f_2)\in\goalset_1$ and it follows that $f=(f_1,f_2)$ is not a run-invariant equilibrium.

In order to have a formally convenient characterisation of the goal sets $\goalset_1$ and $\goalset_2$ to be run-based in two bisimilar CGS-games and to define the profile $f^K=(f^K_1,f^K_2)$, we furthermore introduce the following notations and auxiliary concepts.
For a concurrent game structure $M$ and finite computations $\fincomputation,\fincomputation'\in\fincomputations_M$, we write $\computation\equiv_M\computation'$ if $\finrun_M(\computation)=\finrun_M(\computation)$.
Furthermore, we  say that finite computations $\fincomputation$ and $\fincomputation'$
are finitely congruent in $M$ and $M'$, in symbols $\fincomputation\equiv_{K_{M,M'}} \fincomputation'$, whenever there are (not necessarily distinct) intermediate computations $\fincomputation_0,\dots,\fincomputation_m$ such that

* $\mathwordbox[l]{\fincomputation  }{\fincomputation_j}=\fincomputation_0$,

* $\mathwordbox[l]{\fincomputation' }{\fincomputation_j}=\fincomputation_m$, and

* $\mathwordbox[l]{\fincomputation_j}{\fincomputation_j}\equiv_M \fincomputation_{j+1}$ or
$\fincomputation_j\equiv_{M'} \fincomputation_{j+1}$, for every $0\le j<m$.

As $\equiv_M$ and $\equiv_{M'}$ are equivalence relations, we may assume that here
$\equiv_M$ and $\equiv_{M'}$ alternate and  $\computation_j\equiv_M\computation_{j+1}$ if $j$ is even, and $\computation_j\equiv_{M'}\computation_{j+1}$ if $j$ is odd.
We will generally omit the subscript in $K_{M,M'}$ when $M$ and $M'$ are clear from the context.
For an example, see again Figure <ref>.
Consider the (one-step) computations $\fincomputation_1=(a,a)$, $\fincomputation_2=(a,b)$, $\fincomputation_3=(b,a)$, and
$\fincomputation_4=(b,b)$. Then, $\fincomputation_1\equiv_{M_2,M_3}\fincomputation_3$, because $\fincomputation_1\equiv_{M_3}\fincomputation_2$ and $\fincomputation_2\equiv_{M_2}\fincomputation_3$. On the other hand, some reflection reveals that $\fincomputation_1\not\equiv_{K_{M_1,M_2}}\fincomputation_4$.
It is worth noting that finite congruence of two computations implies statewise bisimilarity of the runs induced, that is, $\fincomputation\equiv_{K_{M,M'}}\fincomputation'$ implies

Let $M$ and $M'$ be two bisimilar concurrent game structures and $\fincomputation=d_0,\dots,d_k$ and $\fincomputation'=d'_0,\dots,d'_k$. Then,
$\fincomputation\equiv_{K_{M,M'}}\fincomputation'$ implies $\finrun_M(\fincomputation)\statewisebisim\finrun_{M}(\fincomputation')$.

Assume $\fincomputation\equiv_{K_{M,M'}}\fincomputation'$.
Then there are $\fincomputation_0,\dots,\fincomputation_m$ such that
$\fincomputation_m=\fincomputation'$, and, for all $0\le \ell<m$,
$\finrun_M(\fincomputation_\ell)=\finrun_M(\fincomputation_{\ell+1})$ if $\ell$ is even
$\finrun_{M'}(\fincomputation_\ell)=\finrun_{M'}(\fincomputation_{\ell+1})$ if $\ell$ is odd.
We assume that $m$ is even; the case where $m$ is odd follows by the same argument mutatis mutandis.

By virtue of Lemma <ref>-<ref>,
we have $\finrun_M(\fincomputation_\ell)\statewisebisim\finrun_{M'}(\fincomputation_\ell)$ for every $0\le \ell<m$. Hence,

\[
\finrun_M(\fincomputation_0)
\finrun_{M}(\fincomputation_1)
\statewisebisim
\finrun_{M'}(\fincomputation_1)
% \finrun_{M'}(\fincomputation_2)
% \statewisebisim
% \finrun_{M}(\fincomputation_2)
% =
\cdots
\finrun_{M'}(\fincomputation_{m-1})
\statewisebisim
\finrun_{M}(\fincomputation_{m-1})
\finrun_{M}(\fincomputation_{m})\text.
\]

As obviously $\finrun_M(\fincomputation_\ell)=\finrun_M(\fincomputation_{\ell+1})$
and $\finrun_{M'}(\fincomputation_\ell)=\finrun_{M'}(\fincomputation_{\ell+1})$
imply, respectively,
and $\finrun_{M'}(\fincomputation_\ell)\statewisebisim\finrun_{M'}(\fincomputation_{\ell+1})$,

\[
\finrun_M(\fincomputation_0)
\statewisebisim
\finrun_{M}(\fincomputation_1)
\statewisebisim
\finrun_{M'}(\fincomputation_1)
\statewisebisim
% \finrun_{M'}(\fincomputation_2)
% \statewisebisim
% \finrun_{M}(\fincomputation_2)
% =
\cdots
\statewisebisim
\finrun_{M'}(\fincomputation_{m-1})
\statewisebisim
\finrun_{M}(\fincomputation_{m-1})
\statewisebisim
\finrun_{M}(\fincomputation_{m})\text.
\]

By transitivity of $\statewisebisim$ we may conclude that $\finrun_M(\fincomputation)\statewisebisim\finrun_M(\fincomputation)$.

For bisimilar concurrent game structures $M$ and $M'$, we say that
a computation-based strategy $f$ is ${K_{M,M'}}$-invariant if  $\fincomputation\equiv_{K_{M,M'}}\fincomputation'$ implies $f(\fincomputation)=f(\fincomputation')$, for all finite computations $\fincomputation,\fincomputation'\in\fincomputations_M$.
We find that $K_{M,M'}$-invariance exactly captures the concept of a strategy that is run-invariant in two  bisimilar concurrent game structures.

Let $M$ and $M'$ be bisimilar concurrent game structures and $f_i$ a computation-based strategy for player $i$. Then, $f_i$ is $K_{M,M'}$-invariant if and only if $f_i$ is run-invariant in both $M$ and $M'$.

For the “only if”-direction, assume that $f_i$ is $K_{M,M'}$-invariant and consider arbitrary $\fincomputation,\fincomputation'\in\fincomputations_M$ such that $\finrun_M(\fincomputation)=\finrun_M(\fincomputation')$, that is,
$\fincomputation\equiv_M\fincomputation'$. By $K_{M,M'}$-invariance of $f_i$ then immediately
$f_i(\fincomputation)=f_i(\fincomputation')$. Accordingly, $f_i$ is run-invariant in $M$. The argument for $f_i$ being run-invariant in $M'$ is analogous.

For the “if”-direction, assume that $f_i$ is run-invariant in both $M$ and $M'$, and consider arbitrary $\fincomputation,\fincomputation'\in\fincomputations$ such that
$\fincomputation\equiv_K\fincomputation'$. Then, we may assume that there are $\fincomputation_0,\dots,\fincomputation_m$ such that

\[
\fincomputation=
\fincomputation_0 \equiv_M
\fincomputation_1 \equiv_{M'}
\fincomputation_2 \equiv_M
\dots
\equiv_{M'}
\fincomputation_m
\fincomputation'\text.
\]

Having assumed that $f_i$ is run-invariant in both $M$ and $M'$, then also

\[
f_i(\fincomputation_0) =
f_i(\fincomputation_1) =
f_i(\fincomputation_2) =
\dots
\]

from which follows that $f_i$ is $K_{M,M'}$-invariant.

As we have argued in Section <ref>, for the question whether the Nash equilibria across two bisimilar CGS-games are preserved to make sense, the players' preferences in the two games have to be congruent, that is, they have to be the same and of the same type in both games.
In this section we deal with run-based preferences. We have already seen in Section <ref>, that identity of a player's computation-based preferences in two CGSs does not guarantee their being congruent as run-based preferences. By imposing an additional closedness restriction, however, we find that a computation-based goal set can be guaranteed to be run-based in two CGS-games based on bisimilar concurrent game structures $M$ and $M'$.
Accordingly, call a goal set $\goalset_i$ $K_{M,M'}$-closed if for all computations $\computation=d_0,d_1,d_2,\dots$ and $\computation'=d'_0,d'_1,d_2',\dots$, we have that $\computation\in\goalset_i$
implies $\computation'\in\goalset_i$ whenever
$d_0,\dots,d_k\equiv_{K_{M,M'}} d_0',\dots,d_k'$ for all $k\ge 0$.

Let $G=(M,\goalset_1,\dots,\goalset_n)$ and $G'=(M',\goalset_1,\dots,\goalset_n)$ be CGS-games on bisimilar concurrent game structures $M$ and $M'$, and $\goalset_i$ is $K_{M,M'}$-closed for some player $i$. Then, $\goalset_i$ is run-based in both $M$ and $M'$.

Assume that $\goalset_i$ is $K_{M,M'}$-invariant and consider arbitrary infinite computations $\computation=d_0,d_1,d_2,\dots$ and $\computation'=d'_0,d'_1,d'_2,\dots$ such that $\run_M(\computation)=\run_M(\computation')$.
Also assume that $\computation\in\goalset_i$.
Let $\run_M(\computation)=s_0,s_1,s_2,\dots$ and $\run_M(\computation')=t_0,t_1,t_2,\dots$.
Then, for every $k\ge 0$, we also have

\[
\finrun_M(d_0,\dots,d_k)=s_0,\dots,s_{k+1}=t_0,\dots,t_{k+1}=\finrun_M(d'_0,\dots,d_k')\text.
\]

Having assumed $\goalset_i$ to be $K_{M,M'}$-invariant, it follows that $\computation'\in\goalset_i$, as desired.

For the remainder, let $G=(M,\Gamma_1,\Gamma_2)$ and $G'=(M',\Gamma_1,\Gamma_2)$ be two two-player CGS-games  based on bisimilar concurrent game structures $M$ and $M'$ such that both $\goalset_1$ and $\goalset_2$ are $K_{M,M'}$-closed (and thus, in particular, run-based). We prove that if there is a run-invariant equilibrium in $M$, then there is also a $K$-invariant profile that is a run-invariant equilibrium in $M$.

We construct for
a given strategy profile $f=(f_1,f_2)$ that is run-invariant in $M$ a $K_{M,M'}$-invariant profile $f^K=(f^K_1,f^K_2)$ such that

* $\computation_M(f_1,f_2)=\computation_M(f^K_1,f^K_2)$,

* if $f_1$ is a winning strategy against player $2$, then so is $f^K_1$,

* if $f_2$ is a winning strategy against player $1$, then so is $f^K_2$.

On basis of Lemma <ref> we may then conclude that $f^K$ corresponds to a run-invariant equilibrium in $M$. Having defined $f^K$ formally as a computation-based profile, by Theorem <ref> it follows that $f^K$ is also a computation-based equilibrium in $G'$. Finally, because $f^K$ is $K_{M,M'}$-invariant, we know that it furthermore corresponds to a run-invariant equilibrium in both $M$ and $M'$.

[draw=white] (1,-3) rectangle (9.5,4);
every ellipse node=[draw,inner xsep=3.5em,inner ysep=1.2em,fill=black!15!white,draw=black!15!white]
every circle node=[fill=white,draw,minimum size=1em,inner sep=0pt]

(0,-3)	node();
(7.8,3.25)	node();

(0,0) node(0)
++ 	( 0:.9)	  node[label=-90:$p$,circle](v0)          $ $
+  (.5*6,.7*3)  node[label=-90:$p$,circle](v1)     $ $
+  (.5*6,.7*0) node[label=-90:$p$,circle](v3)      $ $
+  (.5*6,.7*-3) node[label=-90:$p$,circle](v4)$ $
++ (.5*6,.35*3)node(vv0)      $ $
+  (.6*6,.7*3)  node[label=-90:$p$,circle](vv1)     $ $
+  (.6*6,.7*0) node[label=-90:$p$,circle](vv3)      $ $
+  (.6*6,.7*-3) node[label=-90:$\bar p$,circle](vv4)$ $

[-latex] (v0) –node[pos=.55,fill=white]()$\begin{array}{l}a,a\end{array}$ (v1);
[-latex] (v0) –node[pos=.55,fill=white]()$\begin{array}{l}a,b\\b,a\end{array}$ (v3);
[-latex] (v0) –node[pos=.55,fill=white]()$\begin{array}{l}b,b\end{array}$  (v4);

[-latex] (v1) –node[pos=.7,fill=white]()$a,a$      (vv1);
[-latex] (v1) –node[pos=.7,fill=white]()$a,b$ (vv3);
[-latex] (v1) –node[pos=.7,fill=white]()$a,c$      (vv4);
[-latex] (v3) –node[pos=.7,fill=white]()$a,a$      (vv1);
[-latex] (v3) –node[pos=.7,fill=white]()$a,b$ (vv3);
[-latex] (v3) –node[pos=.7,fill=white]()$a,c$      (vv4);

[-latex] (0) – (v0);

[-latex] (vv1.70-90) .. controls +(60-90:4em) and +(120-90:4em) .. node[pos=.5,fill=white,right,xshift=.5ex]()$\ast,\ast$ (vv1.110-90);
[-latex] (vv3.70-90) .. controls +(60-90:4em) and +(120-90:4em) .. node[pos=.5,fill=white,right,xshift=.5ex]()$\ast,\ast$ (vv3.110-90);
[-latex] (vv4.70-90) .. controls +(60-90:4em) and +(120-90:4em) .. node[pos=.5,fill=white,right,xshift=.5ex]()$\ast,\ast$ (vv4.110-90);
[-latex] (v4.70-90) .. controls +(60-90:4em) and +(120-90:4em) .. node[pos=.5,fill=white,right,xshift=.5ex]()$\ast,\ast$ (v4.110-90);

[draw=white] (-.5,-3) rectangle (8,4);

every ellipse node=[draw,inner xsep=3.5em,inner ysep=1.2em,fill=black!15!white,draw=black!15!white]
every circle node=[fill=white,draw,minimum size=1em,inner sep=0pt]

(0,-3)	node();
(7.8,3.25)	node();

(0,0) node(0)
++ 	( 0:.9)	  node[label=-90:$p$,circle](v0)          $ $
+  (.5*6,.7*3)  node[label=-90:$p$,circle](v1)     $ $
+  (.5*6,.7*0) node[label=-90:$p$,circle](v3)      $ $
+  (.5*6,.7*-3) node[label=-90:$p$,circle](v4)$ $
++ (.5*6,.35*3)node(vv0)      $ $
+  (.6*6,.7*3)  node[label=-90:$p$,circle](vv1)     $ $
+  (.6*6,.7*0) node[label=-90:$p$,circle](vv3)      $ $
+  (.6*6,.7*-3) node[label=-90:$\bar p$,circle](vv4)$ $

[-latex] (v0) –node[pos=.55,fill=white]()$\begin{array}{l}a,a\\a,b\end{array}$ (v1);
[-latex] (v0) –node[pos=.55,fill=white]()$\begin{array}{l}b,a\end{array}$ (v3);
[-latex] (v0) –node[pos=.55,fill=white]()$\begin{array}{l}b,b\end{array}$  (v4);

[-latex] (v1) –node[pos=.7,fill=white]()$a,a$      (vv1);
[-latex] (v1) –node[pos=.7,fill=white]()$a,b$ (vv3);
[-latex] (v1) –node[pos=.7,fill=white]()$a,c$      (vv4);
[-latex] (v3) –node[pos=.7,fill=white]()$a,a$      (vv1);
[-latex] (v3) –node[pos=.7,fill=white]()$a,b$ (vv3);
[-latex] (v3) –node[pos=.7,fill=white]()$a,c$      (vv4);

[-latex] (0) – (v0);

[-latex] (vv1.70-90) .. controls +(60-90:4em) and +(120-90:4em) .. node[pos=.5,fill=white,right,xshift=.5ex]()$\ast,\ast$ (vv1.110-90);
[-latex] (vv3.70-90) .. controls +(60-90:4em) and +(120-90:4em) .. node[pos=.5,fill=white,right,xshift=.5ex]()$\ast,\ast$ (vv3.110-90);
[-latex] (vv4.70-90) .. controls +(60-90:4em) and +(120-90:4em) .. node[pos=.5,fill=white,right,xshift=.5ex]()$\ast,\ast$ (vv4.110-90);
[-latex] (v4.70-90) .. controls +(60-90:4em) and +(120-90:4em) .. node[pos=.5,fill=white,right,xshift=.5ex]()$\ast,\ast$ (v4.110-90);

Two games $G_6$ (left) and $G_7$ (right) based on $M_6$ and $M_7$, respectively.

For an example consider the games $G_6$ and $G_7$ depicted in Figure <ref>.
The underlying concurrent game structures $M_6$ and $M_7$ only differ with respect to direction $(a,b)$ at the
initial state and their bisimilarity is easily established.
Assume that the goal of player $1$ is to see $p$ false at some point in the future, that is,

\[
\goalset_1=\set{d_0,d_1,d_2,\dots\in\computations\midd \text{$d_0\in\set{(a,a),(a,b),(b,a)}$ and $d_1=(a,c)$} }\text,
\]

and that player $2$ tries to prevent this, that is, $\Gamma_2=\computations\setminus\Gamma_1$.
Observe that defined thus, the players' preferences are run-based in both $G_6$ and $G_7$.
Concentrating on $G_6$ first, define the run-invariant strategy profile $f=(f_1,f_2)$, such that,

\begin{align*}
f_1(\epsilon)	&	=	b	&
f_1(a,a)		&	=	a	&
f_1(a,b)		&	=	a	&
f_1(b,a) 		&	=	a\\
f_2(\epsilon)	&	=	b	&
f_2(a,a)		&	=	a	&
f_2(a,b)		&	=	b	&
f_2(b,a) 		&	=	b
\end{align*}

We find that $f=(f_1,f_2)$ is a run-invariant equilibrium in $G_6$.
Observe, however, that $f=(f_1,f_2)$ is not run-invariant in $G_7$, as $f_2(a,a)\neq f_2(a,b)$ even though
Accordingly, $f=(f_1,f_2)$ fails as a $K_{M_6,M_7}$-invariant equilibrium.
Let $g_2$ be defined such that,

\begin{align*}
g_2(\epsilon)	&	=	b	&
g_2(a,a)		&	=	b	&
g_2(a,b)		&	=	b	&
g_2(b,a) 		&	=	b
\end{align*}

Then, $(f_1,g_2)$ is readily seen to be a $K_{M_6,M_7}$-invariant equilibrium in $G_6$.
We will find that under the conditions specified, this is no coincidence and that $K$-invariant equilibria can be
constructed from run-invariant equilibria in a systematic fashion.

We first define the strategy profile $f^K=(f_1^K,f^K_2)$.
The underlying idea is to carefully choose for each finite computation $d_0,\dots,d_k$
from the equivalence class of $d_0,\dots,d_k$  under $\equiv_{K_{M,M'}}$, and set
$f_2^K(d_0,\dots,d_k)=f_2(\fincomputation^{d_0,\dots,d_k}_{f_2})$, respectively.
This guarantees that $f^K=(f^K_1,f^K_2)$ is $K_{M,M'}$-invariant.
Here we give priority to prefixes of $\computation(f_1,f_2)$, that is if
$\computation(f_1,f_2)=d'_0,d'_1,d'_2,\dots$ and $d'_0,\dots,d'_k\equiv_{K_{M,M'}}d_0,\dots,d_k$,
then $\fincomputation_{f_1}^{d_0,\dots,d_k}=\fincomputation_{f_2}^{d_0,\dots,d_k}=d'_0\dots,d_k'$.
In a similar way, we also choose $\fincomputation^{d_0,\dots,d_k}_{f_1}$
so as to preserve the two players' punishment strategies.
This guarantees that $f^K=(f^K_1,f^K_2)$ is an equilibrium, as it inherits this property from $f=(f_1,f_2)$.[The precise definition is rather involved, and the reader may want to skip to page theorem:runbased_runbased_1, where the main theorem of the section is stated and proven.]
To do so we assume a well-ordering of the action sets $\actions_1$ and $\actions_2$ of players $1$ and $2$, respectively. 		Then, for all finite computations $\fincomputation=d_0,\dots,d_k$ in $\fincomputations_M$, we define inductively and simultaneously computations $\fincomputation_{f_1}^{d_0,\dots,d_k}$
$\fincomputation_{f_2}^{d_0,\dots,d_k}$ as follows.
For $\fincomputation=\epsilon$ we have
\fincomputation^\epsilon_{f_1}							=	\fincomputation^\epsilon_{f_2}	=\epsilon,
and, for $\fincomputation=d_0,\dots,d_{k+1}$,

\begin{align*}
\fincomputation_{f_1}^{d_0,\dots,d_k,d_{k+1}}		& 	=	d'_0,\dots,d'_k,(x_1,x_2)
\\
% &\text{and}&&
\fincomputation_{f_2}^{d_0,\dots,d_k,d_{k+1}}		&	=	d''_0,\dots,d''_k,(y_1,y_2),
\end{align*}

$\fincomputation_{f_2}^{d_0,\dots,d_k}=d''_0,\dots,d''_k$, and

$(i.1)$ $x_1=f_1(d'_0,\dots,d'_k)$ and $x_2=f_2(d'_0,\dots,d'_k)$, if

\[d'_0,\dots,d'_k,(f_1(d'_0,\dots,d'_k),f_2(d'_0,\dots,d'_k))\equiv_{K}d_0,\dots,d_k,d_{k+1}\text,
\]

$(i.2)$ $y_1=f_1(d''_0,\dots,d''_k)$ and $y_2=f_2(d''_0,\dots,d''_k)$, if

\[d''_0,\dots,d''_k,(f_1(d''_0,\dots,d''_k),f_2(d''_0,\dots,d''_k))\equiv_{K}d_0,\dots,d_k,d_{k+1}\text,
\]

$(ii.1)$ $x_1=f_1({d'_0,\dots,d'_k})$ and $x_2$ is the least action available to player $2$ such that

\[
\]

if such an action $x_2$ exists and $(i.1)$ does not apply,

$(ii.2)$ $y_2=f_2({d''_0,\dots,d''_k})$ and $y_1$ is the least action available to player $1$ such that

\[
\]

if such an action $y_1$ exists and $(i.2)$ does not apply,

$(iii.1)$ $x_1$ and $x_2$ are the least actions available to players $1$ and $2$, respectively,  such that $d'_0,\dots,d'_k,(x_1,x_2)\equiv_{K}d_0,\dots,d_k,d_{k+1}$, if neither $(i.1)$ nor $(ii.1)$ apply,

$(iii.2)$ $y_1$ and $y_2$ are the least actions available to players $1$ and $2$, respectively,  such that $d''_0,\dots,d''_k,(x_1,x_2)\equiv_{K}d_0,\dots,d_k,d_{k+1}$, if neither $(i.2)$ nor $(ii.2)$ apply,

Observe that the actions $x_1$ and $x_2$ in the definition above always exist. The reason for this is that, if $d_0,\dots,d_k\equiv_{K_{M,M'}}d'_0,\dots,d'_k$,  by Lemma <ref> also $\finrun_M(d_0,\dots,d_k)\statewisebisim\finrun_M(d'_0,\dots,d'_k)$.
Let $\finrun(d_0,\dots,d_k)=s_0,\dots,s_k$,
$\finrun(d'_0,\dots,d'_k)=s'_0,\dots,s'_k$, and
Then, obviously, $a_1$ and $a_2$ are available to players $1$ and $2$ respectively at state $s'_k$. As $s_k\bisim s'_k$, that should also be the case at $s_k$. A similar argument applies to the case where $d_0,\dots,d_k\equiv_{K_{M,M'}}d''_0,\dots,d''_k$.

We now define strategies $f^K_1$ and $f^K_2$ such that, for all finite computations $\fincomputation=d_0,\dots,d_k$ in $\fincomputations_M$,

\begin{align*}
f^K_1(d_0,\dots,d_k)	&= f_1(\fincomputation_{f_1}^{d_0,\dots,d_k})
f^K_2(d_0,\dots,d_k)	&=f_2(\fincomputation_{f_2}^{d_0,\dots,d_k})\text.
\end{align*}

To illustrate how $f^K=(f_1^K,f_2^K)$ is constructed from $f=(f_1,f_2)$, recall the games $M_6$ and $G_7$
in Figure <ref>, and assume that actions for both players are ordered alphabetically.
For the empty computation $\epsilon$, we have

\begin{align*}
f^K_1(\epsilon) &	=	f_1(\fincomputation_{f_1}^\epsilon) =	f_1(\epsilon) = b	& \text{and}&&
f^K_2(\epsilon) &	=	f_2(\fincomputation_{f_2}^\epsilon) =	f_2(\epsilon) = b
\end{align*}

Now consider the finite computations of length one.
For computation $(b,b)$, we find that $(b,b)\equiv_{K_{M_6,M_7}}(f_1(\fincomputation^\epsilon_{f_1}),f_2(\fincomputation^\epsilon_{f_1}))$.
Now case $(i.1)$ applies and we obtain $\fincomputation_{f_1}^{(b,b)}=(b,b)$.
Similarly, $\fincomputation_{f_2}^{(b,b)}=(b,b)$.
For the other one-step computations $(x_1,x_2)\in\set{(a,a),(a,b),(b,a)}$, we find that

First consider $(a,a)$, and to determine $\fincomputation^{(a,a)}_{f_1}$, first
observe that
$d_0,\dots,d_k=\epsilon$, and $d_{k+1}=(a,a)$.
Now, for $x_1=f_1(\epsilon)=b$ we have

\[
=				(b,a)
\equiv_{M_6} 	(a,b)
\equiv_{M_7} 	(a,a)\text.
\]

Accordingly, $(x_1,a)\equiv_{M_6,M_7}(a,a)=d_{k+1}$, and case $(ii.1)$ applies.
With $a$ being moreover player $2$'s alphabetically least action, we may therefore conclude that
\fincomputation_{f_1}^{(a,a)}	=
% \fincomputation_{f_1}^{(a,b)}	=
% \fincomputation_{f_1}^{(b,a)} 	=
In a similar way we obtain
\fincomputation_{f_1}^{(a,b)}	=
\fincomputation_{f_1}^{(b,a)} 	=
as well as
\fincomputation_{f_2}^{(a,a)}	=
\fincomputation_{f_2}^{(a,b)}	=
\fincomputation_{f_2}^{(b,a)} 	=

\[
\begin{array}{l@{\;\;=\;\;}l@{\;\;=\;\;}l@{\;\;=\;\;}l@{\quad\quad\quad}l@{\;\;=\;\;}l@{\;\;=\;\;}l@{\;\;=\;\;}l}
f_1^K(a,a)	   &	 f_1(\fincomputation_{f_1}^{(a,a)})	& f_1(b,a)	&	a	&		f_2^K(a,a)	&		f_2(\fincomputation_{f_2}^{(a,a)})		& f_2(a,b)	&	b	\\[8pt]
f_1^K(a,b)	   &	 f_1(\fincomputation_{f_1}^{(a,b)})	& f_1(b,a)	&	a	&		f_2^K(a,b)	&		f_2(\fincomputation_{f_2}^{(a,b)})		& f_2(a,b)	&	b	\\[8pt]
f_1^K(b,a)	   &	 f_1(\fincomputation_{f_1}^{(b,a)})	& f_1(b,a)	&	a	&		f_2^K(b,a)	&		f_2(\fincomputation_{f_2}^{(b,a)})		& f_2(a,b)	&	b	\\[8pt]
f_1^K(b,b)	   &	 f_1(\fincomputation_{f_1}^{(b,b)})	& f_1(b,b)	&	b	&		f_2^K(b,b)	&		f_2(\fincomputation_{f_2}^{(b,b)})		& f_2(b,b)	&	b
\end{array}
\]

We thus find that $f^K=(f_1^K,f_2^K)$ coincides with the $K_{M_6,M_7}$-invariant equilibrium $(f_1,g_2)$
that we identified above.

The definition of strategies $f_1^K$ and $f_2^K$ ensures that $f^K=(f^K_1,f^K_2)$ is ${K}_{M,M'}$-invariant.

Let $\fincomputation=d_0,\dots,d_k$ be s finite computation in $\fincomputations_M$. Then, for $i=1,2$,

\[
d_0,\dots,d_k\mathrel{\equiv_{K}} \fincomputation_{f_i}^{d_0,\dots,d_k}\text.
\]

Accordingly, $f^K=(f^K_1,f^K_2)$ is ${K}_{M,M'}$-invariant.

Strategies $f^K_1$ and $f^K_2$ have been defined so as to be $K$-invariant. The claim then follows by induction on the length of $\fincomputation$.
Let $i=1$; the case for $i=2$ is analogous.
If the length of $\fincomputation$ is $0$, we have $\fincomputation=\fincomputation_{f_1}^\epsilon=\epsilon$, and it immediately follows that $\fincomputation\equiv_K\fincomputation_{f_1}^\epsilon$.

For the induction step, let $\fincomputation=d_0,\dots,d_k,d_{k+1}$ and assume that
$d_0,\dots,d_k\mathrel{\equiv_{K}} \fincomputation_{f_1}^{d_0,\dots,d_k}$.
Let $\fincomputation_{f_1}^{d_0,\dots,d_{k+1}}$ be denoted by $d'_0,\dots,d'_{k},d'_{k+1}$ where $d'_{k+1}=(x_1,x_2)$.
There are three possibilities.

First, assume that $d'_0,\dots,d'_k,(f_1(d'_0,\dots,d'_k),f_2(d'_0,\dots,d'_k))\equiv_{K}d_0,\dots,d_k,d_{k+1}$.
Then, clause $(i.1)$ applies and we have $x_1=f_1(d'_0,\dots,d'_k)$ and $x_2=f_2(d'_0,\dots,d'_k)$.
It then follows that $d'_0,\dots,d_k',d_{k+1}'\equiv_K d_0,\dots,d_k,d_{k+1}$.

Second, assume that
$d'_0,\dots,d'_k,(f_1(d'_0,\dots,d'_k),y_2)\equiv_{K}d_0,\dots,d_k,d_{k+1}$ for some action $y_2\in\actions_2$, but $d'_0,\dots,d'_k,(f_1(d'_0,\dots,d'_k),f_2(d'_0,\dots,d'_k))\not\equiv_{K}d_0,\dots,d_k,d_{k+1}$.
Then clause $(ii.1)$ applies and we have that $x_1=f_1(d'_0,\dots,d'_k)$ and $x_2$ is the least action available to player $2$ such that $d'_0,\dots,d'_k,(f_1(d'_0,\dots,d'_k),y_2)\equiv_{K}d_0,\dots,d_k,d_{k+1}$.
Again, it immediately follows that $d'_0,\dots,d_k',d_{k+1}'\equiv_K d_0,\dots,d_k,d_{k+1}$.

Finally, assume that neither of the above, then clause $(iii.1)$ applies and we have that $x_1$ and $x_2$ are the least actions available to players $1$ and $2$  such that $d'_0,\dots,d'_k,(x_1,x_2)\equiv_{K}d_0,\dots,d_{k+1}$. As such actions exist, we conclude that $d'_0,\dots,d_k',d_{k+1}'\equiv_K d_0,\dots,d_k,d_{k+1}$.

We are now in a position to prove the following crucial lemmas.[The proofs of these two lemmas extend over a couple of pages and the reader may skip to page page:cont_1, where the running text continues.]

Let $f=(f_1,f_2)$ be a run-invariant strategy profile
for concurrent game structure $M$ and $f^K$ defined as above. Then,

Let us use the following notations:
$\fincomputation_M(f_1,f_2)					=	d_0,d_1,\dots$;
$\fincomputation(f^K_1, f^K_2)				=	d^K_0,d^K_1,\dots$;
$\fincomputation_{f_1}^{d_0,\dots,d_k}		=	d_0',d_1',\dots$;
$\fincomputation_{f_2}^{d_0,\dots,d_k}		=	d_0'',d''_1,\dots$;

where, for every $k\ge 0$,

\begin{align*}
d_k	&	= (a_1^k,a_2^k),
d^K_k	&	= (b_1^k,b_2^k),
d'_k	&	= (x^k_1,x_2^k),
d''_k	&	=	(y^k_1,y^k_2)\text.
\end{align*}

It then suffices to prove by induction on $k$ that for every $k\ge0$, we have

\[
d_k = d^K_k = d'_k =d''_k\text.
\]

For $k=0$, let $d_0=(a_1^0,a_2^0)$ and $d^K_0=(b_1,b_2)$. Then,

\[
=	f_1(\epsilon)
=	f_1(\fincomputation^\epsilon_{f_1})
=	f_1^K(\epsilon)
=   b_1^0
\text.
\]

In a similar way we find that $a_2^0=b_2^0$, and hence $d_0=d_0^K$.
Because both $f_1(\epsilon)=a_1^0$ and $f_2(\epsilon)=a_2^0$, we also have $d'_0=d_0$, and, a fortiori, $d'_0\equiv_K d_0$.
Hence, clause $(i.1)$ applies and therefore $d'_0=(f_1(\epsilon),f_2(\epsilon))=(a_1^0,a_2^0)=d_0$.
In a similar way we can establish that $d''_0=d_0$.

For the induction step, we may assume that

\[
\mathwordbox{=}{===}
\mathwordbox{=}{===}
\mathwordbox{=}{===}
\tag{\emph{i.h.}}
\]

\[
% =
% f_1(\fincomputation_{f_1}^{d_0,\dots,d_k})
\]

Observe that the third equality holds because
\fincomputation_{f_1}^{d_0,\dots,d_k}
For player $2$, the following equalities hold:

\[
% =
% f_2(\fincomputation_{f_2}^{d_0,\dots,d_k})
\]

Now the third equality holds since $d''_0,\dots,d''_k
\fincomputation_{f_2}^{d_0,\dots,d_k}

Finally, by the induction hypothesis,
From the above, we already had
$ and $
Hence, $(f_1(d'_0,\dots,d'_k),f_2(d''_0,\dots,d''_k))=d^{k+1}$.
It follows that,
In particular,