Truly Concurrent Bisimilarities are Game Equivalent

TL;DR

This paper introduces game-based methods for analyzing various truly concurrent bisimilarities, providing a unified framework for strongly, branching, pomset, step, and history-preserving bisimilarities.

Contribution

It develops novel game-theoretic approaches for truly concurrent bisimilarities, covering multiple variants and enhancing the analysis of concurrent systems.

Findings

Game frameworks for strongly truly concurrent bisimilarities

Game frameworks for branching truly concurrent bisimilarities

Unified approach for various bisimilarity types

Abstract

We design games for truly concurrent bisimilarities, including strongly truly concurrent bisimilarities and branching truly concurrent bisimilarities, such as pomset bisimilarities, step bisimilarities, history-preserving bisimilarities and hereditary history-preserving bisimilarities.

Equations

$$\{(C_1,f,C_2)|C_1\in \mathcal{C}({\mathcal{E}}_1),C_2\in \mathcal{C}({\mathcal{E}}_2),f:C_1\to C_2\text{ isomorphism}\}.$$

Full text

1 Introduction

Game theory has been widely used to interpret the nature of the world. The combination of game theory and (computational) logic [1] always exists two ways.

One is to give game theory a logic basis, such as game logic [2] [3] [4], game algebras [5] [6], algebras [7] for concurrent games [8] [9] [10].

the other is to use game theory to interpret computational logic, such as the well-known game semantics [11] [12] [13] [14] [15], in which game theory acts as a foundational semantics bases to understand the behaviors of computer programming language.

Recently, there are some work on interpreting bisimilarities by use of game theory [16] [17]. Following these work, we give truly concurrent bisimilarities a game theory interpretation. This work is organized as follows. In section 2, 3, 4, 5, we design games for pomset bisimilarites, step bisimilarities, history-preserving bisimilarities, and hereditary history-preserving bisimilarities, respectively. And finally, in section 6, we conclude this paper.

2 Games for Pomset Bisimulations

Definition 2.1** (Prime event structure with silent event([18])).**

Let $\Lambda$ be a fixed set of labels, ranged over $a,b,c,\cdots$ and $\tau$. A ($\Lambda$-labelled) prime event structure with silent event $\tau$ is a tuple $\mathcal{E}=\langle\mathbb{E},\leq,\sharp,\lambda\rangle$, where $\mathbb{E}$ is a denumerable set of events, including the silent event $\tau$. Let $\hat{\mathbb{E}}=\mathbb{E}\backslash\{\tau\}$, exactly excluding $\tau$, it is obvious that $\hat{\tau^{*}}=\epsilon$, where $\epsilon$ is the empty event. Let $\lambda:\mathbb{E}\rightarrow\Lambda$ be a labelling function and let $\lambda(\tau)=\tau$. And $\leq$, $\sharp$ are binary relations on $\mathbb{E}$, called causality and conflict respectively, such that:

$\leq$* is a partial order and $\lceil e\rceil=\{e^{\prime}\in\mathbb{E}|e^{\prime}\leq e\}$ is finite for all $e\in\mathbb{E}$. It is easy to see that $e\leq\tau^{*}\leq e^{\prime}=e\leq\tau\leq\cdots\leq\tau\leq e^{\prime}$, then $e\leq e^{\prime}$.* 2. 2.

$\sharp$* is irreflexive, symmetric and hereditary with respect to $\leq$, that is, for all $e,e^{\prime},e^{\prime\prime}\in\mathbb{E}$, if $e\sharp e^{\prime}\leq e^{\prime\prime}$, then $e\sharp e^{\prime\prime}$.*

Then, the concepts of consistency and concurrency can be drawn from the above definition:

$e,e^{\prime}\in\mathbb{E}$* are consistent, denoted as $e\frown e^{\prime}$, if $\neg(e\sharp e^{\prime})$. A subset $X\subseteq\mathbb{E}$ is called consistent, if $e\frown e^{\prime}$ for all $e,e^{\prime}\in X$.* 2. 2.

$e,e^{\prime}\in\mathbb{E}$* are concurrent, denoted as $e\parallel e^{\prime}$, if $\neg(e\leq e^{\prime})$, $\neg(e^{\prime}\leq e)$, and $\neg(e\sharp e^{\prime})$.*

Definition 2.2** (Configuration([18])).**

Let $\mathcal{E}$ be a PES. A (finite) configuration in $\mathcal{E}$ is a (finite) consistent subset of events $C\subseteq\mathcal{E}$, closed with respect to causality (i.e. $\lceil C\rceil=C$). The set of finite configurations of $\mathcal{E}$ is denoted by $\mathcal{C}(\mathcal{E})$. We let $\hat{C}=C\backslash\{\tau\}$.

A consistent subset of $X\subseteq\mathbb{E}$ of events can be seen as a pomset. Given $X,Y\subseteq\mathbb{E}$, $\hat{X}\sim\hat{Y}$ if $\hat{X}$ and $\hat{Y}$ are isomorphic as pomsets. In the following of the paper, we say $C_{1}\sim C_{2}$, we mean $\hat{C_{1}}\sim\hat{C_{2}}$.

2.1 Games for Strong Pomset Bisimulation

Definition 2.3** (Pomset transitions([18])).**

Let $\mathcal{E}$ be a PES and let $C\in\mathcal{C}(\mathcal{E})$, and $\emptyset\neq X\subseteq\mathbb{E}$, if $C\cap X=\emptyset$ and $C^{\prime}=C\cup X\in\mathcal{C}(\mathcal{E})$, then $C\xrightarrow{X}C^{\prime}$ is called a pomset transition from $C$ to $C^{\prime}$.

Definition 2.4** (Pomset bisimulation([18])).**

Let $\mathcal{E}_{1}$, $\mathcal{E}_{2}$ be PESs. A pomset bisimulation is a relation $R\subseteq\mathcal{C}(\mathcal{E}_{1})\times\mathcal{C}(\mathcal{E}_{2})$, such that if $(C_{1},C_{2})\in R$, and $C_{1}\xrightarrow{X_{1}}C_{1}^{\prime}$ then $C_{2}\xrightarrow{X_{2}}C_{2}^{\prime}$, with $X_{1}\subseteq\mathbb{E}_{1}$, $X_{2}\subseteq\mathbb{E}_{2}$, $X_{1}\sim X_{2}$ and $(C_{1}^{\prime},C_{2}^{\prime})\in R$, and vice-versa. We say that $\mathcal{E}_{1}$, $\mathcal{E}_{2}$ are pomset bisimilar, written $\mathcal{E}_{1}\sim_{p}\mathcal{E}_{2}$, if there exists a pomset bisimulation $R$, such that $(\emptyset,\emptyset)\in R$.

The Ehrenfeucht-Fraïssé game for strong pomset bisimulation, in which two players called Spoiler and Duplicator exist, is as follows.

Definition 2.5** (Game for pomset bisimulation).**

A (strong) pomset bisimulation game on $\mathbb{E}$ is played on an arena of Spoiler-owned configurations $[(C_{1},C_{2})]$ and Duplicator-owned configurations $\langle(C_{1},C_{2}),c\rangle$, where $(C_{1},C_{2})\in S\times S$ the set of positions, and $c\in A\times S$ the set of pending challenges, with:

• •

Spoiler moves from a configuration $[(C_{1},C_{2})]$ by:

selecting $C_{1}\xrightarrow{X_{1}}C_{1}^{\prime}$ and moving to $\langle(C_{1},C_{2}),(X_{1},C_{1}^{\prime})\rangle$ with $X_{1}\subseteq\mathbb{E}_{1}$, or 2. 2.

selecting $C_{2}\xrightarrow{X_{2}}C_{2}^{\prime}$ and moving to $\langle(C_{2},C_{1}),(X_{2},C_{2}^{\prime})\rangle$ with $X_{2}\subseteq\mathbb{E}_{2}$; 3. 3.

$X_{1}\sim X_{2}$;

• •

Duplicator responds from a configuration $\langle(C_{3},C_{4}),(X_{1},C_{3}^{\prime})$ by playing $C_{4}\xrightarrow{X_{2}}C_{4}^{\prime}$ and continuing in configuration $[(C_{3}^{\prime},C_{4}^{\prime})]$.

If games starting in a configuration $[(C_{1},C_{2})]$ is won by Duplicator, we write $C_{1}\equiv_{p}C_{2}$.

Theorem 2.6**.**

$C_{1}\sim_{p}C_{2}$* iff $C_{1}\equiv_{p}C_{2}$.*

2.2 Games for Branching Pomset Bisimulation

Definition 2.7** (Branching pomset bisimulation([18])).**

Assume a special termination predicate $\downarrow$, and let $\surd$ represent a state with $\surd\downarrow$. Let $\mathcal{E}_{1}$, $\mathcal{E}_{2}$ be PESs. A branching pomset bisimulation is a relation $R\subseteq\mathcal{C}(\mathcal{E}_{1})\times\mathcal{C}(\mathcal{E}_{2})$, such that:

if $(C_{1},C_{2})\in R$, and $C_{1}\xrightarrow{X}C_{1}^{\prime}$ then

• •

either $X\equiv\tau^{*}$, and $(C_{1}^{\prime},C_{2})\in R$;

• •

or there is a sequence of (zero or more) $\tau$-transitions $C_{2}\xrightarrow{\tau^{*}}C_{2}^{0}$, such that $(C_{1},C_{2}^{0})\in R$ and $C_{2}^{0}\xRightarrow{X}C_{2}^{\prime}$ with $(C_{1}^{\prime},C_{2}^{\prime})\in R$; 2. 2.

if $(C_{1},C_{2})\in R$, and $C_{2}\xrightarrow{X}C_{2}^{\prime}$ then

• •

either $X\equiv\tau^{*}$, and $(C_{1},C_{2}^{\prime})\in R$;

• •

or there is a sequence of (zero or more) $\tau$-transitions $C_{1}\xrightarrow{\tau^{*}}C_{1}^{0}$, such that $(C_{1}^{0},C_{2})\in R$ and $C_{1}^{0}\xRightarrow{X}C_{1}^{\prime}$ with $(C_{1}^{\prime},C_{2}^{\prime})\in R$; 3. 3.

if $(C_{1},C_{2})\in R$ and $C_{1}\downarrow$, then there is a sequence of (zero or more) $\tau$-transitions $C_{2}\xrightarrow{\tau^{*}}C_{2}^{0}$ such that $(C_{1},C_{2}^{0})\in R$ and $C_{2}^{0}\downarrow$; 4. 4.

if $(C_{1},C_{2})\in R$ and $C_{2}\downarrow$, then there is a sequence of (zero or more) $\tau$-transitions $C_{1}\xrightarrow{\tau^{*}}C_{1}^{0}$ such that $(C_{1}^{0},C_{2})\in R$ and $C_{1}^{0}\downarrow$.

We say that $\mathcal{E}_{1}$, $\mathcal{E}_{2}$ are branching pomset bisimilar, written $\mathcal{E}_{1}\approx_{bp}\mathcal{E}_{2}$, if there exists a branching pomset bisimulation $R$, such that $(\emptyset,\emptyset)\in R$.

The Ehrenfeucht-Fraïssé game for branching pomset bisimulation, in which two players called Spoiler and Duplicator exist, is as follows. Note that the game is limited to no occurrence of infinite $\tau$-loops.

Definition 2.8** (Game for branching pomset bisimulation).**

A limited branching pomset bisimulation game on $\mathbb{E}$ is played on an arena of Spoiler-owned configurations $[(C_{1},C_{2})]$ and Duplicator-owned configurations $\langle(C_{1},C_{2}),c\rangle$, where $(C_{1},C_{2})\in S\times S$ the set of positions, and $c\in A\times S$ the set of pending challenges, with:

• •

Spoiler moves from a configuration $[(C_{1},C_{2})]$ by:

selecting $C_{1}\xrightarrow{X}C_{1}^{\prime}$ and moving to $\langle(C_{1},C_{2}),(X,C_{1}^{\prime})\rangle$ with $X\subseteq\mathbb{E}$, or 2. 2.

selecting $C_{2}\xrightarrow{X}C_{2}^{\prime}$ and moving to $\langle(C_{2},C_{1}),(X,C_{2}^{\prime})\rangle$ with $X\subseteq\mathbb{E}$;

• •

Duplicator responds from a configuration $\langle(C_{3},C_{4}),(X,C_{3}^{\prime})$ by:

If $X=\tau*$, continuing in the configuration $[(C_{3}^{\prime},C_{4})]$, or 2. 2.

playing $C_{4}\xrightarrow{X}C_{4}^{\prime}$ and continuing in configuration $[(C_{3}^{\prime},C_{4}^{\prime})]$ if available, or 3. 3.

playing $C_{4}\xrightarrow{\tau*}C_{4}^{\prime}$ and continuing in configuration $[(C_{3},C_{4}^{\prime})]$ if possible.

If games starting in a configuration $[(C_{1},C_{2})]$ is won by Duplicator, we write $C_{1}\equiv_{bp}C_{2}$.

Theorem 2.9**.**

$C_{1}\approx_{bp}C_{2}$* iff $C_{1}\equiv_{bp}C_{2}$.*

3 Games for Step Bisimulations

3.1 Games for Strong Step Bisimulation

Definition 3.1** (Step transitions([18])).**

Let $\mathcal{E}$ be a PES and let $C\in\mathcal{C}(\mathcal{E})$, and $\emptyset\neq X\subseteq\mathbb{E}$, if $C\cap X=\emptyset$ and $C^{\prime}=C\cup X\in\mathcal{C}(\mathcal{E})$, then $C\xrightarrow{X}C^{\prime}$ is called a pomset transition from $C$ to $C^{\prime}$. When the events in $X$ are pairwise concurrent, we say that $C\xrightarrow{X}C^{\prime}$ is a step.

Definition 3.2** (Step bisimulation([18])).**

By replacing pomset transitions with steps, we can get the definition of step bisimulation. When PESs $\mathcal{E}_{1}$ and $\mathcal{E}_{2}$ are step bisimilar, we write $\mathcal{E}_{1}\sim_{s}\mathcal{E}_{2}$.

The Ehrenfeucht-Fraïssé game for strong step bisimulation, in which two players called Spoiler and Duplicator exist, is as follows.

Definition 3.3** (Game for step bisimulation).**

A (strong) step bisimulation game on $\mathbb{E}$ is played on an arena of Spoiler-owned configurations $[(C_{1},C_{2})]$ and Duplicator-owned configurations $\langle(C_{1},C_{2}),c\rangle$, where $(C_{1},C_{2})\in S\times S$ the set of positions, and $c\in A\times S$ the set of pending challenges, with:

• •

Spoiler moves from a configuration $[(C_{1},C_{2})]$ by:

selecting $C_{1}\xrightarrow{X_{1}}C_{1}^{\prime}$ and moving to $\langle(C_{1},C_{2}),(X_{1},C_{1}^{\prime})\rangle$ with $X_{1}\subseteq\mathbb{E}_{1}$, and all $e\in X_{1}$ are pairwise concurrent, or 2. 2.

selecting $C_{2}\xrightarrow{X_{2}}C_{2}^{\prime}$ and moving to $\langle(C_{2},C_{1}),(X_{2},C_{2}^{\prime})\rangle$ with $X_{2}\subseteq\mathbb{E}_{2}$, and all $e\in X_{2}$ are pairwise concurrent; 3. 3.

$X_{1}\sim X_{2}$;

• •

Duplicator responds from a configuration $\langle(C_{3},C_{4}),(X_{1},C_{3}^{\prime})$ by playing $C_{4}\xrightarrow{X_{2}}C_{4}^{\prime}$ and continuing in configuration $[(C_{3}^{\prime},C_{4}^{\prime})]$.

If games starting in a configuration $[(C_{1},C_{2})]$ is won by Duplicator, we write $C_{1}\equiv_{s}C_{2}$.

Theorem 3.4**.**

$C_{1}\sim_{s}C_{2}$* iff $C_{1}\equiv_{s}C_{2}$.*

3.2 Games for Branching Step Bisimulation

Definition 3.5** (Branching step bisimulation([18])).**

For $\mathcal{E}_{1}\approx_{bp}\mathcal{E}_{2}$, by replacing pomset transitions with steps, we can get the definition of branching step bisimulation. When PESs $\mathcal{E}_{1}$ and $\mathcal{E}_{2}$ are branching step bisimilar, we write $\mathcal{E}_{1}\approx_{bs}\mathcal{E}_{2}$.

The Ehrenfeucht-Fraïssé game for branching step bisimulation, in which two players called Spoiler and Duplicator exist, is as follows. Note that the game is limited to no occurrence of infinite $\tau$-loops.

Definition 3.6** (Game for branching step bisimulation).**

A limited branching step bisimulation game on $\mathbb{E}$ is played on an arena of Spoiler-owned configurations $[(C_{1},C_{2})]$ and Duplicator-owned configurations $\langle(C_{1},C_{2}),c\rangle$, where $(C_{1},C_{2})\in S\times S$ the set of positions, and $c\in A\times S$ the set of pending challenges, with:

• •

Spoiler moves from a configuration $[(C_{1},C_{2})]$ by:

selecting $C_{1}\xrightarrow{X}C_{1}^{\prime}$ and moving to $\langle(C_{1},C_{2}),(X,C_{1}^{\prime})\rangle$ with $X\subseteq\mathbb{E}$, and all $e\in X$ are pairwise concurrent, or 2. 2.

selecting $C_{2}\xrightarrow{X}C_{2}^{\prime}$ and moving to $\langle(C_{2},C_{1}),(X,C_{2}^{\prime})\rangle$ with $X\subseteq\mathbb{E}$, and all $e\in X$ are pairwise concurrent;

• •

Duplicator responds from a configuration $\langle(C_{3},C_{4}),(X,C_{3}^{\prime})$ by:

If $X=\tau*$, continuing in the configuration $[(C_{3}^{\prime},C_{4})]$, or 2. 2.

playing $C_{4}\xrightarrow{X}C_{4}^{\prime}$ and continuing in configuration $[(C_{3}^{\prime},C_{4}^{\prime})]$ if available, or 3. 3.

playing $C_{4}\xrightarrow{\tau*}C_{4}^{\prime}$ and continuing in configuration $[(C_{3},C_{4}^{\prime})]$ if possible.

If games starting in a configuration $[(C_{1},C_{2})]$ is won by Duplicator, we write $C_{1}\equiv_{bs}C_{2}$.

Theorem 3.7**.**

$C_{1}\approx_{bs}C_{2}$* iff $C_{1}\equiv_{bs}C_{2}$.*

4 Games for History-preserving Bisimulations

4.1 Games for Strong History-preserving Bisimulation

Definition 4.1** (Posetal product([18])).**

Given two PESs $\mathcal{E}_{1}$, $\mathcal{E}_{2}$, the posetal product of their configurations, denoted $\mathcal{C}(\mathcal{E}_{1})\overline{\times}\mathcal{C}(\mathcal{E}_{2})$, is defined as

[TABLE]

A subset $R\subseteq\mathcal{C}(\mathcal{E}_{1})\overline{\times}\mathcal{C}(\mathcal{E}_{2})$ is called a posetal relation. We say that $R$ is downward closed when for any $(C_{1},f,C_{2}),(C_{1}^{\prime},f^{\prime},C_{2}^{\prime})\in\mathcal{C}(\mathcal{E}_{1})\overline{\times}\mathcal{C}(\mathcal{E}_{2})$, if $(C_{1},f,C_{2})\subseteq(C_{1}^{\prime},f^{\prime},C_{2}^{\prime})$ pointwise and $(C_{1}^{\prime},f^{\prime},C_{2}^{\prime})\in R$, then $(C_{1},f,C_{2})\in R$.

For $f:X_{1}\rightarrow X_{2}$, we define $f[x_{1}\mapsto x_{2}]:X_{1}\cup\{x_{1}\}\rightarrow X_{2}\cup\{x_{2}\}$, $z\in X_{1}\cup\{x_{1}\}$,(1)$f[x_{1}\mapsto x_{2}](z)=x_{2}$,if $z=x_{1}$;(2)$f[x_{1}\mapsto x_{2}](z)=f(z)$, otherwise. Where $X_{1}\subseteq\mathbb{E}_{1}$, $X_{2}\subseteq\mathbb{E}_{2}$, $x_{1}\in\mathbb{E}_{1}$, $x_{2}\in\mathbb{E}_{2}$.

Definition 4.2** (History-preserving bisimulation([18])).**

A history-preserving (hp-) bisimulation is a posetal relation $R\subseteq\mathcal{C}(\mathcal{E}_{1})\overline{\times}\mathcal{C}(\mathcal{E}_{2})$ such that if $(C_{1},f,C_{2})\in R$, and $C_{1}\xrightarrow{e_{1}}C_{1}^{\prime}$, then $C_{2}\xrightarrow{e_{2}}C_{2}^{\prime}$, with $(C_{1}^{\prime},f[e_{1}\mapsto e_{2}],C_{2}^{\prime})\in R$, and vice-versa. $\mathcal{E}_{1},\mathcal{E}_{2}$ are history-preserving (hp-)bisimilar and are written $\mathcal{E}_{1}\sim_{hp}\mathcal{E}_{2}$ if there exists a hp-bisimulation $R$ such that $(\emptyset,\emptyset,\emptyset)\in R$.

The Ehrenfeucht-Fraïssé game for strong hp-bisimulation, in which two players called Spoiler and Duplicator exist, is as follows.

Definition 4.3** (Game for hp-bisimulation).**

A (strong) hp-bisimulation game on $\mathbb{E}$ is played on an arena of Spoiler-owned configurations $[(C_{1},f,C_{2})]$ and Duplicator-owned configurations $\langle(C_{1},f,C_{2}),c\rangle$, where $(C_{1},C_{2})\in S\times S$ the set of positions, and $c\in A\times S$ the set of pending challenges, with:

• •

Spoiler moves from a configuration $[(C_{1},f,C_{2})]$ by:

selecting $C_{1}\xrightarrow{e_{1}}C_{1}^{\prime}$ and moving to $\langle(C_{1},f,C_{2}),(e_{1},f,C_{1}^{\prime})\rangle$ with $e_{1}\in\mathbb{E}_{1}$, or 2. 2.

selecting $C_{2}\xrightarrow{e_{2}}C_{2}^{\prime}$ and moving to $\langle(C_{2},f,C_{1}),(e_{2},f,C_{2}^{\prime})\rangle$ with $e_{2}\in\mathbb{E}_{2}$; 3. 3.

$f[e_{1}\mapsto e_{2}]$;

• •

Duplicator responds from a configuration $\langle(C_{3},f,C_{4}),(e_{1},f,C_{3}^{\prime})$ by playing $C_{4}\xrightarrow{e_{2}}C_{4}^{\prime}$ and continuing in configuration $[(C_{3}^{\prime},f,C_{4}^{\prime})]$.

If games starting in a configuration $[(C_{1},f,C_{2})]$ is won by Duplicator, we write $C_{1}\equiv_{hp}C_{2}$.

Theorem 4.4**.**

$C_{1}\sim_{hp}C_{2}$* iff $C_{1}\equiv_{hp}C_{2}$.*

4.2 Games for Braching History-preserving Bisimulation

Definition 4.5** (Branching history-preserving bisimulation([18])).**

Assume a special termination predicate $\downarrow$, and let $\surd$ represent a state with $\surd\downarrow$. A branching history-preserving (hp-) bisimulation is a weakly posetal relation $R\subseteq\mathcal{C}(\mathcal{E}_{1})\overline{\times}\mathcal{C}(\mathcal{E}_{2})$ such that:

if $(C_{1},f,C_{2})\in R$, and $C_{1}\xrightarrow{e_{1}}C_{1}^{\prime}$ then

• •

either $e_{1}\equiv\tau$, and $(C_{1}^{\prime},f[e_{1}\mapsto\tau],C_{2})\in R$;

• •

or there is a sequence of (zero or more) $\tau$-transitions $C_{2}\xrightarrow{\tau^{*}}C_{2}^{0}$, such that $(C_{1},f,C_{2}^{0})\in R$ and $C_{2}^{0}\xrightarrow{e_{2}}C_{2}^{\prime}$ with $(C_{1}^{\prime},f[e_{1}\mapsto e_{2}],C_{2}^{\prime})\in R$; 2. 2.

if $(C_{1},f,C_{2})\in R$, and $C_{2}\xrightarrow{e_{2}}C_{2}^{\prime}$ then

• •

either $e_{2}\equiv\tau$, and $(C_{1},f[e_{2}\mapsto\tau],C_{2}^{\prime})\in R$;

• •

or there is a sequence of (zero or more) $\tau$-transitions $C_{1}\xrightarrow{\tau^{*}}C_{1}^{0}$, such that $(C_{1}^{0},f,C_{2})\in R$ and $C_{1}^{0}\xrightarrow{e_{1}}C_{1}^{\prime}$ with $(C_{1}^{\prime},f[e_{2}\mapsto e_{1}],C_{2}^{\prime})\in R$; 3. 3.

if $(C_{1},f,C_{2})\in R$ and $C_{1}\downarrow$, then there is a sequence of (zero or more) $\tau$-transitions $C_{2}\xrightarrow{\tau^{*}}C_{2}^{0}$ such that $(C_{1},f,C_{2}^{0})\in R$ and $C_{2}^{0}\downarrow$; 4. 4.

if $(C_{1},f,C_{2})\in R$ and $C_{2}\downarrow$, then there is a sequence of (zero or more) $\tau$-transitions $C_{1}\xrightarrow{\tau^{*}}C_{1}^{0}$ such that $(C_{1}^{0},f,C_{2})\in R$ and $C_{1}^{0}\downarrow$.

$\mathcal{E}_{1},\mathcal{E}_{2}$* are branching history-preserving (hp-)bisimilar and are written $\mathcal{E}_{1}\approx_{bhp}\mathcal{E}_{2}$ if there exists a branching hp-bisimulation $R$ such that $(\emptyset,\emptyset,\emptyset)\in R$.*

The Ehrenfeucht-Fraïssé game for branching hp-bisimulation, in which two players called Spoiler and Duplicator exist, is as follows. Note that the game is limited to no occurrence of infinite $\tau$-loops.

Definition 4.6** (Game for branching hp-bisimulation).**

A limited branching hp-bisimulation game on $\mathbb{E}$ is played on an arena of Spoiler-owned configurations $[(C_{1},f,C_{2})]$ and Duplicator-owned configurations $\langle(C_{1},f,C_{2}),c\rangle$, where $(C_{1},C_{2})\in S\times S$ the set of positions, and $c\in A\times S$ the set of pending challenges, with:

• •

Spoiler moves from a configuration $[(C_{1},f,C_{2})]$ by:

selecting $C_{1}\xrightarrow{e_{1}}C_{1}^{\prime}$ and moving to $\langle(C_{1},f,C_{2}),(e_{1},f,C_{1}^{\prime})\rangle$ with $e_{1}\in\mathbb{E}_{1}$, or 2. 2.

selecting $C_{2}\xrightarrow{e_{2}}C_{2}^{\prime}$ and moving to $\langle(C_{2},f,C_{1}),(e_{2},f,C_{2}^{\prime})\rangle$ with $e_{2}\in\mathbb{E}_{2}$; 3. 3.

$f[e_{1}\mapsto e_{2}]$;

• •

Duplicator responds from a configuration $\langle(C_{3},f,C_{4}),(e_{1},f,C_{3}^{\prime})$ by:

If $e_{1}=\tau$, continuing in the configuration $[(C_{3}^{\prime},f[e_{1}\mapsto\tau],C_{4})]$, or 2. 2.

playing $C_{4}\xrightarrow{e_{2}}C_{4}^{\prime}$ and continuing in configuration $[(C_{3}^{\prime},f[e_{1}\mapsto e_{2}],C_{4}^{\prime})]$ if available, or 3. 3.

playing $C_{4}\xrightarrow{\tau}C_{4}^{\prime}$ and continuing in configuration $[(C_{3},f[e_{2}\mapsto\tau],C_{4}^{\prime})]$ if possible.

If games starting in a configuration $[(C_{1},f,C_{2})]$ is won by Duplicator, we write $C_{1}\equiv_{bhp}C_{2}$.

Theorem 4.7**.**

$C_{1}\approx_{bhp}C_{2}$* iff $C_{1}\equiv_{bhp}C_{2}$.*

5 Games for Hereditary History-preserving Bisimulations

5.1 Games for Strong Hereditary History-preserving Bisimulation

Definition 5.1** (Hereditary history-preserving bisimulation([18])).**

A hereditary history-preserving (hhp-)bisimulation is a downward closed hp-bisimulation. $\mathcal{E}_{1},\mathcal{E}_{2}$ are hereditary history-preserving (hhp-)bisimilar and are written $\mathcal{E}_{1}\sim_{hhp}\mathcal{E}_{2}$.

Definition 5.2** (Game for hhp-bisimulation).**

A (strong) hhp-bisimulation game on $\mathbb{E}$ is a downward closed (strong) hp-bisimulation game. If games starting in a configuration $[(C_{1},f,C_{2})]$ is won by Duplicator, then for any $[(C_{1}^{\prime},f^{\prime},C_{2}^{\prime})]$, $(C_{1}^{\prime},f^{\prime}C_{2}^{\prime})\subseteq(C_{1},f,C_{2})$ pointwise, then $(C_{1}^{\prime},f^{\prime},C_{2}^{\prime})$ is won by Duplicator, we write $C_{1}\equiv_{hhp}C_{2}$.

Theorem 5.3**.**

$C_{1}\sim_{hhp}C_{2}$* iff $C_{1}\equiv_{hhp}C_{2}$.*

5.2 Games for Branching Hereditary History-preserving Bisimulation

Definition 5.4** (Branching hereditary history-preserving bisimulation([18])).**

A branching hereditary history-preserving (hhp-)bisimulation is a downward closed branching hp-bisimulation. $\mathcal{E}_{1},\mathcal{E}_{2}$ are branching hereditary history-preserving (hhp-)bisimilar and are written $\mathcal{E}_{1}\approx_{bhhp}\mathcal{E}_{2}$.

Definition 5.5** (Game for branching hhp-bisimulation).**

A branching hhp-bisimulation game on $\mathbb{E}$ is a downward closed branching hp-bisimulation game. If games starting in a configuration $[(C_{1},f,C_{2})]$ is won by Duplicator, then for any $[(C_{1}^{\prime},f^{\prime},C_{2}^{\prime})]$, $(C_{1}^{\prime},f^{\prime}C_{2}^{\prime})\subseteq(C_{1},f,C_{2})$ pointwise, then $(C_{1}^{\prime},f^{\prime},C_{2}^{\prime})$ is won by Duplicator, we write $C_{1}\equiv_{bhhp}C_{2}$.

Theorem 5.6**.**

$C_{1}\approx_{bhhp}C_{2}$* iff $C_{1}\equiv_{bhhp}C_{2}$.*

6 Conclusions

We design games for truly concurrent bisimilarities, including strongly truly concurrent bisimilarities and branching truly concurrent bisimilarities, such as pomset bisimilarities, step bisimilarities, history-preserving bisimilarities and hereditary history-preserving bisimilarities.

By this work, we can deeply understand truly concurrent bisimilarities by use of game theory, and we can do some future work on developing tools for verification and validation based on this work.