This is a revised and extended version of a paper that appeared in LICS’15
[MRT15]

# Bisimilarity in Fresh-Register Automata

Andrzej S. Murawski  University of Oxford  ,  Steven J. Ramsay  University of
Bristol  and  Nikos Tzevelekos  Queen Mary University of London

###### Abstract.

Register automata are a basic model of computation over infinite alphabets.
Fresh-register automata extend register automata with the capability to
generate fresh symbols in order to model computational scenarios involving
name creation. This paper investigates the complexity of the bisimilarity
problem for classes of register and fresh-register automata. We examine all
main disciplines that have appeared in the literature: general register
assignments; assignments where duplicate register values are disallowed; and
assignments without duplicates in which registers cannot be empty. In the
general case, we show that the problem is EXPTIME-complete.

However, the absence of duplicate values in registers enables us to identify
inherent symmetries inside the associated bisimulation relations, which can be
used to establish a polynomial bound on the depth of Attacker-winning
strategies. Furthermore, they enable a highly succinct representation of the
corresponding bisimulations. By exploiting results from group theory and
computational group theory, we can then show solvability in PSPACE and NP
respectively for the latter two register disciplines. In each case, we find
that freshness does not affect the complexity class of the problem.

The results allow us to close a complexity gap for language equivalence of
deterministic register automata. We show that deterministic language
inequivalence for the no-duplicates fragment is NP-complete, which disproves
an old conjecture of Sakamoto.

Finally, we discover that, unlike in the finite-alphabet case, the addition of
pushdown store makes bisimilarity undecidable, even in the case of visibly
pushdown storage.

###### Key words and phrases:

Register automata, bisimilarity, computational group theory, automata over
infinite alphabets

##  1\. Introduction

Register automata are one of the simplest models of computation over infinite
alphabets. They consist of finite-state control and finitely many registers
for storing elements from the infinite alphabet. Since their introduction by
Kaminski and Francez [KF94] as a candidate formalism for capturing regularity
in the infinite-alphabet setting, they have been actively researched
especially in the database and verification communities: selected applications
include the study of markup languages [NSV04] and run-time verification
[GDPT13]. While register automata can detect symbols that are currently not
stored in registers (local freshness), the bounded number of registers means
that they are not in general capable of recognising inputs that are genuinely
fresh in the sense that they occur in the computation for the first time
(global freshness). Because such a feature is desirable in many contexts,
notably dynamic resource allocation, the formalism has been extended in
[Tze11] to fresh-register automata, which do account for global freshness.
This paper is concerned with the problem of _bisimilarity testing_ for
register and fresh-register automata.

Bisimulation is a fundamental notion of equivalence in computer science. Its
central role is, in part, derived from the fact that it is intensional and yet
very robust. Consequently, the algorithmics of bisimilarity have attracted a
lot of attention from researchers interested in the theory and practice of
equivalence checking. When the set of observable actions available to a system
is finite, a lot is already known about the complexity of the problem for
specific classes of systems, although tight bounds are often difficult to
obtain in the infinite-state cases [Srb08]. In this paper we prove a number of
bounds on the complexity of bisimulation equivalence checking. We note that in
this setting language equivalence is known to be undecidable [NSV04].

Our results are expressed using a unified framework that comprises all
variations that have appeared in the literature. They differ in the allowed
register assignment discipline, which turns out to affect complexity.
Assignments are allowed to be

($S$):

_single_ , if the contents of all registers are required to be distinct; or

($M$):

_multiple_ , if we allow for duplicate values.

Furthermore, registers are required to

($F$):

always be filled; or

($\\#_{0}$):

initially allowed to be empty; or

($\\#$):

allowed to be erased and filled during a run111Empty content is “$\\#$”. A
full definition of each of the automaton variants is given in Section 2..

The complexity of bisimilarity checking for each combination is summarised in
the table below, where we use the suffix “-c” to denote completeness for this
class and “-s” to denote solvability only. The results hold regardless of
whether one considers register or fresh-register automata.

($M\\#$) | ($M\\#_{0}$) | ($MF$) | ($S\\#$) | ($S\\#_{0}$) | ($SF$)
---|---|---|---|---|---
EXP-c | EXP-c | EXP-c | EXP-c | PSPACE-c | NP-s

Our work thus provides a practical motivation for modelling systems with
single assignment whenever possible — if the system does not need to erase the
contents of registers mid-run, the corresponding equivalence problems are
lower in the complexity hierarchy.

We start by giving coarse, exponential-time upper bounds for all the classes
of system considered by showing how any such bisimilarity problem can be
reduced to one for finite-state automata at exponential cost. For all the
multiple assignment machines this bound is tight and, for single assignment,
tightness depends upon whether or not erasing is allowed. The implied
significance of being able to erase the contents of registers is explained by
our proof that the bisimulation games associated with such systems can
simulate the computations of alternating Turing machines running in PSPACE.
Here we set up an encoding of the tape, determined by the presence or absence
of content in certain registers, and erasing of registers corresponds to
writing of tape cells.

Once erasure is forbidden under single assignments, we obtain better bounds by
investigating the structure of the associated bisimulation relations. Such
relations are generally infinite, but only the relationship between the
register assignments in two configurations is relevant to bisimilarity, and so
we work with a finite, though exponentially large, class of symbolic relations
built over partial permutations (to link register indices). Due to the
inherent symmetry and transitivity of bisimilarity, each such relation forms
an inverse semigroup under function composition. Also, crucially, the
relations are upward closed in the information order. Although, taken
separately, neither of the preceding facts leads to an exponential leap in
succinctness of representation, taken together they reveal an interconnected
system of (total) permutation groups underlying each relation. What is more,
in any play of the associated bisimulation game, the number of registers that
are empty must monotonically decrease. This, together with an application of
Babai’s result on the length of subgroup chains in symmetric groups [Bab86],
allows us to show that any violation of bisimilarity can be detected after
polynomially many rounds of the bisimulation game. Consequently, in this case,
we are able to decide bisimilarity in polynomial space.

The polynomial bound mentioned above enables us to close a complexity gap
(between NP and PSPACE) in the study of deterministic language equivalence.
Namely, we show that the language inequivalence problem for _deterministic_
RA($S\\#_{0}$) is solvable in NP, and thus NP-complete, refuting a conjecture
by Sakamoto [Sak98].

Further, if registers are additionally required to be filled $(SF)$, we can
exhibit very compact representations of the relevant bisimulation relations.
The fact that permutation groups have small generating sets [MN87] allows us
then to design a representation for symbolic bisimulations that is at most
polynomial in size. Furthermore, by exploiting polynomial-time membership
testing for permutation groups given in terms of their generators [FHL80], we
show that such a representation can be guessed and verified by a
nondeterministic Turing machine in polynomial time.

Finally, we consider bisimilarity for visibly pushdown register automata
(VPDRA) under the $SF$ register discipline, and we show that the problem here
is already undecidable. Since VPDRA($SF$) are a particularly weak variant,
this result implies undecidability for all PDRA considered in [MRT14]. In
contrast, for finite alphabets, bisimilarity of pushdown automata is known to
be decidable [Sén05] but non-elementary [BGKM13] and, in the visibly pushdown
case, EXPTIME-complete [Srb06].

##### Related Work

The complexity of bisimilarity problems has been studied extensively in the
finite-alphabet setting and the current state of the art for infinite-state
systems is summarised nicely in [Srb08]. Recent papers concerning the
complexity of decision problems for register automata have, until now, not
considered bisimulation equivalence. However, there are several related
complexity results in the concurrency literature.

In his PhD thesis, Pistore [Pis99], gives an exponential-time algorithm for
bisimilarity of HD-automata [MP97]. Since Pistore shows that bisimulation
relations for HD-automata have many of the algebraic properties222E.g. the
_active names_ of [Pis99] are comparable to our _characteristic sets_. as the
relations we study here, it seems likely that our algorithm could be adapted
to show NP-solvability of the bisimilarity problem for HD-automata. Indeed, a
compact representation of symmetries using generators for such a purpose was
envisaged by [CM10].

Jonsson and Parrow [JP93] and Boreale and Trevisan [BT00] consider
bisimilarity over a class of data-independent processes. These processes are
terms built over an infinite alphabet, but the behaviour of such a process
does not depend upon the data from which it is built. In the latter work, the
authors also consider a class of value-passing processes, whose behaviour may
depend upon the result of comparing data for equality. They show that if such
processes can be defined recursively then the problem is EXPTIME-complete.
Since value passing can be seen as a purely functional proxy for multiple
register assignments, this result neatly reflects our findings for RA($M\\#$).
Finally, decidability of bisimilarity for FRA($S\\#_{0}$) was proven in
[Tze11], albeit without a proper study of its complexity (the procedure given
in _loc. cit._ can be shown to run in NEXPTIME).

Finally, in a recent follow-up paper [MRT18], we showed that the language
equivalence problem for deterministic RA($SF$) is in P, in contrast to NP-
completeness for RA($S\\#_{0}$), established in the present paper. For
RA($SF$), this still leaves a complexity gap between NL and P.

It would be interesting to see to what extent our decidability and complexity
results can be generalised, e.g. in settings with ordered infinite alphabets
or nominal automata [BKL14].

##### Structure

In Section 2 we introduce the preliminaries and prove all of the EXPTIME
bounds in Section 3. Then we start the presentation of other results with
register automata, as the addition of global freshness requires non-trivial
modifications. In Section 4 we show bounds for the ($S\\#_{0}$) problems and
apply the techniques to deterministic language equivalence in Section 5.
Section 6 covers further improvements for the ($SF$) case. In Section 7 we
generalise our techniques to fresh-register automata and, finally, consider
the pushdown case in Section 8.

##  2\. Preliminaries

We introduce some basic notation. Given a relation $R\subseteq X\times Y$, we
define $\mathsf{dom}(R)=\\{x\in X\,|\,\exists y.(x,y)\in R\\}$ and
$\mathsf{rng}(R)=\\{y\in Y\,|\,\exists x.(x,y)\in R\\}$. For natural numbers
$i\leq j$, we write $[i,j]$ for the set $\\{i,i+1,\ldots,j\\}$.

###  2.1. Bisimilarity

We define bisimulations generally with respect to a labelled transition
system. As we shall see, the particular systems that we will be concerned with
in this paper are the configuration graphs of various classes of (fresh-)
register automata.

A labelled transition system (LTS) is a tuple
$\mathcal{S}=(\mathbb{C},\mathcal{A}\mathit{ct},\\{\mathord{\xrightarrow{\ell}}\mid\ell\in\mathcal{A}\mathit{ct}\\})$,
where $\mathbb{C}$ is a set of configurations, $\mathcal{A}\mathit{ct}$ is a
set of action labels, and
$\mathord{\xrightarrow{\ell}}\subseteq\mathbb{C}\times\mathbb{C}$ is a
transition relation for each $\ell\in\mathcal{A}\mathit{ct}$.

A binary relation $R\subseteq\mathbb{C}\times\mathbb{C}$ is a bisimulation if
for each $(\kappa_{1},\kappa_{2})\in R$ and each
$\ell\in\mathcal{A}\mathit{ct}$, we have:

  1. (1)

if $\kappa_{1}\xrightarrow{\ell}\kappa_{1}^{\prime}$, then there is some
$\kappa_{2}\xrightarrow{\ell}\kappa_{2}^{\prime}$ with
$(\kappa_{1}^{\prime},\kappa_{2}^{\prime})\in R$;

  2. (2)

if $\kappa_{2}\xrightarrow{\ell}\kappa_{2}^{\prime}$, then there is some
$\kappa_{1}\xrightarrow{\ell}\kappa_{1}^{\prime}$ with
$(\kappa_{1}^{\prime},\kappa_{2}^{\prime})\in R$.

We say that $\kappa_{1}$ and $\kappa_{2}$ are bisimilar, written
$\kappa_{1}\sim\kappa_{2}$, just if there is some bisimulation $R$ with
$(\kappa_{1},\kappa_{2})\in R$.

Let us recall that bisimilarity has a very natural game-theoretic account.
Given two configurations, one can consider a _bisimulation game_ involving two
players, traditionally called Attacker and Defender respectively. They play
rounds in which Attacker fires a transition from one of the configurations and
Defender has to follow with an identically labelled transition from the other
configuration. In the first round, the chosen transitions must lead from the
configurations to be tested for bisimilarity, while, in each subsequent round,
they must start at the configurations reached after the preceding round.
Defender loses if he cannot find a matching transition. In this framework,
bisimilarity corresponds to the existence of a winning strategy for Defender.
The process of playing a bisimulation game naturally favours Attacker as the
decision maker but, thanks to the forcing technique of [JS08], it is possible
to construct transition systems in which Defender effectively ends up making
choices.

###  2.2. Fresh-register automata

We will be interested in testing bisimilarity of configurations generated by
machines with registers and pushdown stack in the infinite-alphabet setting,
i.e. as $\mathcal{A}\mathit{ct}$ we shall use the set
$\Sigma\times{\mathcal{D}}$ for a finite alphabet $\Sigma$ and an infinite
alphabet ${\mathcal{D}}$ (with its elements sometimes called _names_), cf.
data words [NSV04].

Given a natural number $r$, a class of $r$-register assigments $A$ is a set of
functions from $[1,r]$ to ${\mathcal{D}}\uplus\\{\\#\\}$. Fix such a class. An
$r$-fresh-register automaton ($r$-FRA) is a tuple $\mathcal{A}=\langle
Q,q_{0},\rho_{0},\delta,F\rangle$, where:

  * •

$Q$ is a finite set of states, $q_{0}\in Q$ initial and $F\subseteq Q$ final;

  * •

$\rho_{0}\in A$ is the initial $r$-register assignment;

  * •

$\delta\subseteq
Q\times\Sigma\times(\mathcal{P}([1,r])\cup\\{\circledast\\})\times[0,r]\times\mathcal{P}([1,r])\times
Q$ is the transition relation, with elements written as
$q\xrightarrow{t,X,i,Z}q^{\prime}$. We assume that in any such transition
$i\notin Z$.

Finally an $r$-register automaton ($r$-RA) is a special case of an $r$-FRA
such that all its transitions $q\xrightarrow{t,X,i,Z}q^{\prime}$ satisfy
$X\not=\circledast$.

A register assignment then is just a mapping of register indices to letters
from the infinite alphabet $\mathcal{D}$ and the special symbol $\\#$. This
symbol is used to represent the fact that a register is empty, i.e. contains
no letter from $\mathcal{D}$. Consequently, by slight abuse of notation, for
any $r$-register assignment $\rho$ we will be writing $\mathsf{rng}(\rho)$ for
the set $\rho([1,r])\cap\mathcal{D}$, and $\mathsf{dom}(\rho)$ for
$\rho^{-1}(\mathsf{rng}(\rho))$. Moreover, $\rho^{-1}=\\{(d,i)\ |\
d\in{\mathcal{D}}\land(i,d)\in\rho\\}$.

The meaning of a transition $q\mathrel{\xrightarrow{t,X,i,Z}}q^{\prime}$ is
described as follows. The components $t$ and $X$ are a precondition: for the
transition to be applicable, it must be that the next letter of the input has
shape $(t,a)$ for some $a\in\mathcal{D}$ and, moreover:

  * •

if $X\subseteq[1,r]$ then $a$ is already stored in exactly those registers
named by $X$;

  * •

if $X=\circledast$ then $a$ is (globally) _fresh_ : it has so far not appeared
in the computation of $\mathcal{A}$.

If the transition applies then taking it results in changes being made to the
current register assignment, namely: $a$ is written into register $i$ (unless
$i=0$, in which case it is not written at all) and all registers named by $Z$
have their contents erased.

A configuration $\kappa$ of an $r$-FRA $\mathcal{A}$ is a triple $(q,\rho,H)$
consisting of a state $q\in Q$, an $r$-register assignment $\rho\in A$ and a
finite set $H\subseteq\mathcal{D}$, called the _history_ , such that
$\mathsf{rng}(\rho)\subseteq H$. If $q_{1}\xrightarrow{t,X,i,Z}q_{2}$ is a
transition of $\mathcal{A}$, then a configuration $(q_{1},\rho_{1},H_{1})$ can
make a transition to a configuration $(q_{2},\rho_{2},H_{2})$ accepting input
$(t,d)$, written
$(q_{1},\rho_{1},H_{1})\mathrel{\xrightarrow{(t,d)}}(q_{2},\rho_{2},H_{2})$,
just if:

  * •

$X=\\{j\,|\,\rho_{1}(j)=d\\}$, or $X=\circledast$ and $d\notin H$;

  * •

for all $j\in[1,r]$, $\rho_{2}(j)=d\ \text{ if }j=i$; and $\rho_{2}(j)=\\#$ if
$j\in Z$; and $\rho_{2}(j)=\rho_{1}(j)$ otherwise;

  * •

$H_{2}=H_{1}\cup\\{d\\}$.

We will sometimes write the set of configurations of $\mathcal{A}$ by
$\mathbb{C}_{\mathcal{A}}$ and the induced transition relation by
$\rightarrow_{\mathcal{A}}$. We let $\mathcal{S}(\mathcal{A})$ be the LTS
$\langle\mathbb{C}_{\mathcal{A}},\,\Sigma\times\mathcal{D},\,\rightarrow_{\mathcal{A}}\rangle$.

On the other hand, a configuration $\kappa$ of an $r$-RA $\mathcal{A}$ is a
pair $(q,\rho)$ of a state $q\in Q$ and an $r$-register assignment $\rho\in
A$. The LTS
$\langle\mathbb{C}_{\mathcal{A}},\,\Sigma\times\mathcal{D},\,\rightarrow_{\mathcal{A}}\rangle$
is defined precisely as above, albeit excluding the underlined conditions.

We define the specific classes of fresh-register automata that we will study
in this work by considering specialisations of Definition 2.2 by the register
assignment discipline followed.

Duplication in assignment. We consider two register storage policies, namely
single assignment ($S$) or multiple assignment ($M$). In single assignment, we
restrict the class of register assignments to be injective on non-empty
registers, i.e. each $\rho\in A$ has, for all $i,j\in[1,r]$, $\rho(i)=\rho(j)$
just if $i=j$ or $\rho(i)=\\#=\rho(j)$. In multiple assignment there is no
such restriction. To ensure that all configurations respect the register
assignment discipline, in an ($S$) automaton every transition
$q_{1}\xrightarrow{t,X,i,Z}q_{2}$ is required to have $X=\circledast$ or
$X\subseteq\\{i\\}$.

Emptiness of registers. We consider the automaton’s ability to process empty
registers. We say that either all registers must always be filled ($F$), that
registers may be initially empty ($\\#_{0}$) or that the contents of registers
may be erased ($\\#$) during a run. Under condition ($F$), the class of
$r$-register assignments $A$ is restricted so that $\\#\notin\rho([1,r])$ for
each $\rho\in A$. Under conditions ($F$) and ($\\#_{0}$), every transition
$q_{1}\xrightarrow{t,X,i,Z}q_{2}$ has $Z=\emptyset$ and $i\not=0$. Condition
($\\#$) imposes no specific restrictions.

We describe particular classes by the acronym FRA($XY$) in which

$X\,{\in}\,\\{M,\,S\\}\textrm{ and }Y\,{\in}\,\\{F,\,\\#_{0},\,\\#\\}.$

The class FRA($XY$) is the specialisation of Definition 2.2 to the largest
class of register assignments $A$ satisfying the constraints imposed by $X$
and $Y$. E.g. FRA($S\\#_{0}$) are those automata whose register assignments
are all functions from $[1,r]$ to ${\mathcal{D}}\,{\cup}\,\\{\\#\\}$ that are
injective on non-empty registers, and every transition of such a machine is of
the form $q_{1}\xrightarrow{t,X,i,Z}q_{2}$ with $Z=\emptyset$, $i\not=0$ and
$X\in\\{\circledast,\emptyset,\\{i\\}\\}$. In a similar manner we define the
classes RA($XY$).

######  Remark 1.

The class RA($MF$) follow the register assignment discipline of the register
automata defined by Segoufin [Seg06]. The class RA($M\\#_{0}$) follow the
register assignment discipline of the $M$-Automata defined by Kaminski and
Francez [KF94] and the class of RA($S\\#_{0}$) follows the assignment
discipline of the finite memory automata considered in the same paper. The
class RA($SF$) contain automata that follow the register assignment discipline
of the machines considered by Nevin, Schwentick and Vianu [NSV04]. The
condition $i\not=0$, which stipulates that every name encountered by the
automaton be stored in some register, also originates from [KF94, NSV04]. The
class FRA($S\\#_{0}$) follow the register assignment discipline of the
automata defined in [Tze11].

In this paper we are concerned with the following family of decision problems.

Let $X\,{\in}\,\\{M,\,S\\}$ and $Y\,{\in}\,\\{F,\,\\#_{0},\,\\#\\}$.

  * •

The problem $\bm{\sim}$-FRA($XY$) is: given an FRA($XY$) $\mathcal{A}$ and
configurations $\kappa_{1}=(q_{1},\rho_{1},H)$ and
$\kappa_{2}=(q_{2},\rho_{2},H)$, does $\kappa_{1}\sim\kappa_{2}$ hold in
$\mathcal{S}(\mathcal{A})$?

  * •

The problem $\bm{\sim}$-RA($XY$) is: given an RA($XY$) $\mathcal{A}$ and
configurations $\kappa_{1}$ and $\kappa_{2}$ , does $\kappa_{1}\sim\kappa_{2}$
hold in $\mathcal{S}(\mathcal{A})$?

We shall relate the various classes of bisimilarity problems that we study by
their complexity. We write $P_{1}\leq P_{2}$ to denote that there is a
polynomial-time many-one reduction from problem $P_{1}$ to problem $P_{2}$.

######  Lemma 2.

The considered bisimilarity problems can be related as in Figure 1.

######  Proof 2.1.

First note that, for all $XY$, any RA($XY$) $\mathcal{A}$ can be trivially
seen as an FRA($XY$) $\mathcal{A}^{\prime}$ (i.e. $\mathcal{A}^{\prime}$ has
the same components as $\mathcal{A}$). We claim that, for any pair
$(q_{1},\rho_{1}),(q_{2},\rho_{2})$ of RA-configurations of $\mathcal{A}$,

$(q_{1},\rho_{1})\sim(q_{2},\rho_{2})\iff(q_{1},\rho_{1},H)\sim(q_{2},\rho_{2},H)$

where $H=\mathsf{rng}(\rho_{1})\cup\mathsf{rng}(\rho_{2})$ and
$(q_{1},\rho_{1},H),(q_{2},\rho_{2},H)$ are configurations of
$\mathcal{A}^{\prime}$. Indeed, we can show that the relation between
$\mathcal{A}$\- and $\mathcal{A}^{\prime}$-configurations given by:

$R=\\{\ ((q,\rho),(q,\rho,H))\ |\ \mathsf{rng}(\rho)\subseteq H\ \\}$

is a bisimulation, from which we obtain ($*$).

We next show the FRA-bisimilarity inclusions; the RA-bisimilarity inclusions
are shown in a similar (simpler) way.

Observe that, for any $X\in\\{S,M\\}$, $\bm{\sim}$-FRA($XF$) $\leq$
$\bm{\sim}$-FRA($X\\#_{0}$) $\leq$ $\bm{\sim}$-FRA($X\\#$). This is because
any FRA($XF$) can be viewed trivially as an FRA($X\\#_{0}$) in which all
registers begin filled and, similarly, any FRA($X\\#_{0}$) can be viewed
trivially as an FRA($X\\#$) in which no registers are ever erased.

Now, given an $r$-FRA($S\\#$) $\mathcal{A}$ and two configurations
$\kappa_{1}$ and $\kappa_{2}$ we construct a $2r$-FRA($MF$)
$\mathcal{A}^{\prime}$ and configurations $\widehat{\kappa_{1}}$ and
$\widehat{\kappa_{2}}$ in which every register $k$ of $\mathcal{A}$ is
simulated by two registers $2k-1$ and $2k$ of $\mathcal{A}^{\prime}$. The
states of $\mathcal{A}^{\prime}$ are the states of $\mathcal{A}$ augmented by
an additional state $q^{i}_{\tau}$ for every $q\in Q$, $i\in[1,r]$ and every
$\tau\in\delta$. The representation scheme is as follows: if registers $2k-1$
and $2k$ of $\mathcal{A}^{\prime}$ contain the same letter then register $k$
of $\mathcal{A}$ is empty, otherwise the register $k$ in $\mathcal{A}$
contains exactly the contents of register $2k$ in $\mathcal{A}^{\prime}$.

Each transition $\tau=q\mathrel{\xrightarrow{t,X,i,Z}}q^{\prime}$ of
$\mathcal{A}$, in which $X\subseteq[1,r]$, is simulated by a sequence of
transitions of $\mathcal{A}^{\prime}$ with the following shape:

$q\vphantom{{}^{0}}$$q_{\tau}^{1}$$q_{\tau}^{2}$$\cdots$$q_{\tau}^{r}$$q^{\prime}$$\scriptstyle
t,2X,2i,\emptyset$$\scriptstyle t,\\{1\\},2,\emptyset$$\scriptstyle
t,\\{1\\},0,\emptyset$$\scriptstyle t,\\{1,2\\},0,\emptyset$$\scriptstyle
t,\\{2r-1\\},2r,\emptyset$$\scriptstyle t,\\{2r-1\\},0,\emptyset$$\scriptstyle
t,\\{2r-1,2r\\},0,\emptyset$

where $2X$ is a shorthand for $\\{2x\,|\,x\in X\\}$ and, for each $j\in[1,r]$
the solid arrows labelled $(t,\\{2j-1\\},2i,\emptyset)$ and
$(t,\\{2j-1,2j\\},0,\emptyset)$ respectively exist just if $j\in Z$ and the
dashed arrow labelled $(t,\\{2j-1\\},0,\emptyset)$ exists just if $j\notin Z$.
On the other hand, each transition
$\tau=q\mathrel{\xrightarrow{t,\circledast,i,Z}}q^{\prime}$ of $\mathcal{A}$
is simulated by a sequence of transitions of $\mathcal{A}^{\prime}$:

$q\vphantom{{}^{0}}$$q_{\tau}^{1}$$q_{\tau}^{2}$$\cdots$$q_{\tau}^{r}$$q^{\prime}$$\scriptstyle
t,\circledast,2i,\emptyset$$\scriptstyle t,\\{1\\},2,\emptyset$$\scriptstyle
t,\\{1\\},0,\emptyset$$\scriptstyle t,\\{1,2\\},0,\emptyset$$\scriptstyle
t,\\{2r-1\\},2r,\emptyset$$\scriptstyle t,\\{2r-1\\},0,\emptyset$$\scriptstyle
t,\\{2r-1,2r\\},0,\emptyset$

where solid and dashed arrows are as above.

We say that a pair of configurations $(q_{1},\widehat{\rho_{1}})$,
$(q_{2},\widehat{\rho_{2}})$ of $\mathcal{A}^{\prime}$ _represents_ a pair of
configurations $(q_{1},\rho_{1})$, $(q_{2},\rho_{2})$ of $\mathcal{A}$ just if
$\widehat{\rho_{1}}$ is a representation of $\rho_{1}$ and
$\widehat{\rho_{2}}$ is a representation of $\widehat{\rho_{2}}$ as discussed
above and, furthermore:

  * •

for all $k\in[1,r]$, $i\in[1,2r]$, $j\in\\{1,2\\}$: if
$\widehat{\rho_{j}}(2k-1)=\widehat{\rho_{j}}(i)$ then $i\in\\{2k-1,2k\\}$

  * •

for all $k\in[1,r]$: $\widehat{\rho_{1}}(2k-1)=\widehat{\rho_{2}}(2k-1)$

These latter two properties can easily be seen to be an invariant of
configurations reachable from any pair that initially satisfy it, since
transitions of $\mathcal{A}^{\prime}$ only write to even numbered registers
$2k$ and then only then with a fresh letter or the contents of the adjacent
register $2k-1$.

By construction, the automaton $\mathcal{A}^{\prime}$ faithfully simulates the
original in the following sense, given configurations $(q_{1},\rho_{1})$,
$(q_{2},\rho_{2})$ of $\mathcal{A}$ and $\mathcal{A}^{\prime}$ representations
$\widehat{\rho_{1}}$ of $\rho_{1}$ and $\widehat{\rho_{2}}$ of $\rho_{2}$:
$(q_{1},\rho_{1})\sim(q_{2},\rho_{2})$ in $\mathcal{S}(\mathcal{A})$ iff
$(q_{1},\widehat{\rho_{1}})\sim(q_{2},\widehat{\rho_{2}})$ in
$\mathcal{S}(\mathcal{A}^{\prime})$.

$\begin{array}[]{ccccccccccc}\text{$\bm{\sim}$-FRA($SF$)}&\leq&\text{$\bm{\sim}$-FRA($S\\#_{0}$)}&\leq&\textrm{$\bm{\sim}$-FRA($S\\#$)}&\leq&\text{$\bm{\sim}$-FRA($MF$)}&\leq&\text{$\bm{\sim}$-FRA($M\\#_{0}$)}&\leq&\text{$\bm{\sim}$-FRA($M\\#$)}\\\
\rotatebox[origin={c}]{90.0}{$\leq$}&&\rotatebox[origin={c}]{90.0}{$\leq$}&&\rotatebox[origin={c}]{90.0}{$\leq$}&&\rotatebox[origin={c}]{90.0}{$\leq$}&&\rotatebox[origin={c}]{90.0}{$\leq$}&&\rotatebox[origin={c}]{90.0}{$\leq$}\\\
\text{$\bm{\sim}$-RA($SF$)}&\leq&\text{$\bm{\sim}$-RA($S\\#_{0}$)}&\leq&\text{$\bm{\sim}$-RA($S\\#$)}&\leq&\text{$\bm{\sim}$-RA($MF$)}&\leq&\text{$\bm{\sim}$-RA($M\\#_{0}$)}&\leq&\text{$\bm{\sim}$-RA($M\\#$)}\end{array}$
Figure 1. Relationship between the main bisimilarity problems considered in
this work.

###  2.3. Groups and permutations

For any $S\subseteq[1,n]$, we shall write $\mathcal{S}_{S}$ for the group of
permutations on $S$, and $\mathcal{IS}_{S}$ for the inverse semigroup of
partial permutations on $S$. For economy, we write $\mathcal{S}_{n}$ for
$\mathcal{S}_{[1,n]}$; and $\mathcal{IS}_{n}$ for $\mathcal{IS}_{[1,n]}$.

For partial permutations $\sigma$ and $\tau$, we write $\sigma;\tau$ for their
relational composition: $\sigma;\tau=\\{\,(i,j)\ |\ \exists
k.\sigma(i)=k\land\tau(k)=j\,\\}$. Moreover, for any $\sigma$ and
$i,j\in[1,n]$, we let $\sigma[i\mapsto j]$ be the result of updating $\sigma$
with $(i,j)$:

$\sigma[i\mapsto j]\ =\ \\{(i,j)\\}\cup\\{(k,\sigma(k))\ |\ k\neq
i\land\sigma(k)\neq j\\}.\vspace{-1.25mm}$

For all $j\in[1,n]$, $\sigma\in\mathcal{S}_{S}$ and $S\subseteq[1,n]$ we also
write $S[j]$ for $S\cup\\{j\\}$, and $\sigma\cdot S$ for $\\{\sigma(i)\ |\
i\in S\\}$.

##  3\. Bisimilarity problems complete for EXPTIME

In this section we show that the upper four classes in our two hierachies of
automata all have bisimilarity problems that are complete for exponential
time.

######  Theorem 3.

All of the problems $\bm{\sim}$-RA($S\\#$), $\bm{\sim}$-RA($MF$),
$\bm{\sim}$-RA($M\\#_{0}$), $\bm{\sim}$-RA($M\\#$), $\bm{\sim}$-FRA($S\\#$),
$\bm{\sim}$-FRA($MF$), $\bm{\sim}$-FRA($M\\#_{0}$) and $\bm{\sim}$-FRA($M\\#$)
are EXPTIME-complete.

######  Proof 3.1.

The result follows immediately from Propositions 4 and 12 and Lemma 2.

Our argument proceeds by showing that $\bm{\sim}$-FRA($M\\#$) can be solved in
EXPTIME (Proposition 4) and $\bm{\sim}$-RA($S\\#$) is already EXPTIME-hard
(Proposition 12). For the former, we reduce the problem to a bisimilarity
problem for finite state automata of exponential size.

Given an instance of the $r$-register, FRA($M\\#$) bisimilarity problem, the
idea is to construct a bisimilarity problem for a finite automaton over an
alphabet derived from a finite subset $N\subseteq\mathcal{D}$ of size $2r+2$.
Given a configuration $\kappa=(q,\rho,H)$ of the FRA, we represent it by an
abstract configuration $\phi\cdot\kappa=(q,{\phi\cdot\rho},\phi\cdot H)$ which
is built entirely from letters in $N$. Here $\phi:{\mathcal{D}}\to N$ is
surjective, $\phi\cdot\rho=(\phi[\\#\,{\mapsto}\,\\#])\circ\rho$ and
$\phi\cdot H=\\{\phi(d)\ |\ d\in H\\}$. We choose the abstraction $\phi$ in
such a way that it partitions $\mathcal{D}$ and $N$ with respect to
$\mathsf{rng}(\rho)$ and $H$: that is,
$\phi=\phi_{1}\uplus\phi_{2}\uplus\phi_{3}$ where $\mathsf{rng}(\phi_{i})$ are
all distinct and $\mathsf{dom}(\phi_{1})=\mathsf{rng}(\rho)$,
$\mathsf{dom}(\phi_{2})=H\setminus\mathsf{rng}(\rho)$ and
$\mathsf{dom}(\phi_{3})={\mathcal{D}}\setminus H$. In addition, $\phi_{1}$ is
injective.

The partitioning conditions ensure that our representation by abstract
configurations is faithful. But, due to global freshness, the abstraction
$\phi$ cannot be chosen uniformly for the entire simulation. This is because,
with the alphabet limited to $N$, there would be no letters available to be
played as part of globally fresh transitions as soon as the simulated history
$\phi\cdot H$ became equal to $N$. Hence, the simulation needs to recycle
letters in the history as soon as they become otherwise irrelevant to the
current configuration and, consequently, a new (typically smaller) history and
a new abstraction $\phi^{\prime}$ must be chosen at each step. However, at
position $(q_{1},\phi\cdot\rho_{1},\phi\cdot
H),(q_{2},\phi\cdot\rho_{2},\phi\cdot H)$ of the simulation, the only letters
that can be recycled are those that are not in $\phi\cdot\rho_{1}$ or
$\phi\cdot\rho_{2}$. Recycling such a letter $d$ by removing it from
$\phi\cdot H$ is unfaithful to the simulation, since it would potentially
allow a globally fresh transition playing $d$ to be matched by a local one.
This demonstrates that it is necessary to know _both_ register assignments of
the position in order to choose which letters are available to recycle and
hence the shape of a new history.

To this end, the bisimulation game induced by the simulating finite automaton
is constructed so that both of the two component systems contain both of
$\phi\cdot\rho_{1}$ and $\phi\cdot\rho_{2}$.

######  Proposition 4.

$\bm{\sim}$-FRA($M\\#$) is solvable in EXPTIME.

Given an instance $\langle\mathcal{A},\kappa_{1},\kappa_{2}\rangle$ of the
bisimilarity problem for FRA(M#), where $\mathcal{A}=\langle
Q,q_{0},\rho_{0},\delta,F\rangle$ has $r$-registers, and we construct an
instance $\langle\mathcal{B},\gamma_{1},\gamma_{2}\rangle$ of the bisimilarity
problem for finite state automata (FSA).

The idea of the construction is to induce a bisimulation game over a _finite
alphabet_ which simulates the original, turn by turn. To simulate a turn
(Attacker move then Defender move) of the original game, the game induced by
$\mathcal{B}$ will use several of its own turns. The key insight of the
construction is that $2r+2$ letters of $\mathcal{D}$ are all that are required
to simulate the behaviour of $\mathcal{A}$ over the whole $\mathcal{D}$, even
in the presence of global freshness.

Hence, first we choose any subset $N\subseteq\mathcal{D}$ of letters of size
$2r+2$. Let the $r$-register assignments whose range is a subset of $N$ be
called _$N$ -assignments_. An _$N$ -configuration_ is a pair $(q,\,\rho)$
consisting of a state $q$ and $N$-assignment $\rho$. We shall use the
metavariable $\gamma$ to refer to $N$-configurations. A _potted history_ is a
finite subset of $N$ of size at most $2r+1$.

To help describe the construction we will use the following two definitions.
The first will allow us to relate configurations of an
$\mathcal{S}(\mathcal{A})$-bisimulation game to configurations of the more
abstract $\mathcal{B}$-game.

Given two sets of letters $X_{1},X_{2}\subseteq\mathcal{D}$, an _$N$
-representation_ for $(X_{1},X_{2})$ is a surjective function
$\phi:{\mathcal{D}}\to N$ satisfying the following constraints:

  1. (1)

$\phi\,{\restriction}\,X_{1}:X_{1}\to\phi(X_{1})$ is a bijection;

  2. (2)

for all $i\in\\{1,2\\}$, $a\in\mathcal{D}$: $\phi(a)\in\phi(X_{i})$ implies
$a\in X_{i}$.

Thus, in each case, $X_{i}$ partitions $\phi$ as
$\phi=\phi_{i}^{1}\uplus\phi_{i}^{2}$ with $\mathsf{dom}(\phi_{i}^{1})=X_{i}$
and
$\mathsf{dom}(\phi_{i}^{1})\cap\mathsf{dom}(\phi_{i}^{2})=\mathsf{rng}(\phi_{i}^{1})\cap\mathsf{rng}(\phi_{i}^{2})=\emptyset$.
In addition, $\phi_{1}^{1}$ is a bijection.

We extend the action of a representation to register assignments, histories
and configurations by writing:

$\begin{array}[]{rcl}(\phi\cdot\rho)(i)&=&\begin{cases}\\#&\text{if
$\rho(i)=\\#$}\\\ \phi(\rho(i))&\text{otherwise}\end{cases}\\\
&&\vphantom{yay}\\\ \phi\cdot H&=&\\{\phi(d)\mid d\in H\\}\\\
&&\vphantom{yay}\\\ \phi\cdot(q,\rho,H)&=&(q,\phi\cdot\rho,\phi\cdot
H)\end{array}$

If the concrete $\mathcal{A}$-game configuration is related to the abstract
$\mathcal{B}$ one by an $N$-representation then this ensures that all the
choices available to the player of the $\mathcal{A}$-game are essentially
available to the player of the $\mathcal{B}$-game.

######  Lemma 5.

Let $\rho$ be a register assignment, $H$ a history containing
$\mathsf{rng}(\rho)$, and $a\in\mathcal{D}$. If $\phi$ is an
$N$-representation of $(\mathsf{rng}(\rho),H)$ then consider the following
transitions induced by $q\xrightarrow{t,X,i,Z}q^{\prime}$:

$\begin{array}[]{c}(q_{1},\rho,H)\xrightarrow{t,a}(q_{1}^{\prime},\rho^{\prime}[i\mapsto
a],H\cup\\{a\\})\\\\[2.84526pt] \text{implies}\\\\[2.84526pt]
(q_{1},\phi\\!\cdot\\!\rho,\phi\\!\cdot\\!H)\xrightarrow{t,\phi(a)}(q_{1}^{\prime},(\phi\\!\cdot\\!\rho^{\prime})[i\mapsto\phi(a)],(\phi\\!\cdot\\!H)\\!\cup\\!\\{\phi(a)\\})\end{array}$

and, for $a\in N$:

$\begin{array}[]{c}(q_{1},\phi\cdot\rho,\phi\cdot
H)\xrightarrow{t,a}(q_{1}^{\prime},(\phi\cdot\rho^{\prime})[i\mapsto
a],(\phi\cdot H)\cup\\{a\\})\\\\[2.84526pt] \text{implies, for all
$b\in\phi^{-1}(a)$,}\\\\[2.84526pt]
(q_{1},\rho,H)\xrightarrow{t,b}(q_{1}^{\prime},\rho^{\prime}[i\mapsto
b],H\cup\\{b\\})\end{array}$

where, for all $j\in[1,r]$, $\rho^{\prime}(j)=\\#$ if $j\in Z$ and
$\rho^{\prime}(j)=\rho(j)$ otherwise.

######  Proof 3.2.

We deal with the two facts separately. For the first, we verify the validity
of the concluded transition by cases. If $X=\\{j\mid\rho(j)=a\\}$ then by
(R1,R2) also $X=\\{j\mid\phi\cdot\rho(j)=\phi(a)\\}$. Otherwise
$X=\circledast$ and $a\notin H$, by (R2) also $\phi(a)\notin\phi\cdot H$.

For the second, let $b\in\phi^{-1}(a)$, we verify the validity of the
concluded transition by cases. If $X=\\{j\mid(\phi\cdot\rho)(j)=a\\}$ then it
follows from (R1,R2) that $X=\\{j\mid\rho(j)=b\\}$. If $X=\circledast$ then
$a\notin\phi\cdot H$ and hence, by (R2), $b\notin H$.

We note the following two facts:

######  Proposition 6.

Let $\rho_{1}$, $\rho_{2}$ be register assignments and
$H\supseteq\mathsf{rng}(\rho_{1})\cup\mathsf{rng}(\rho_{2})$ a history.

  1. (1)

There exists some $N$-representation $\phi$ for
$(\mathsf{rng}(\rho_{1})\cup\mathsf{rng}(\rho_{2}),H)$.

  2. (2)

If $\phi$ is an $N$-representation for
$(\mathsf{rng}(\rho_{1})\cup\mathsf{rng}(\rho_{2}),H)$ then $\phi$ is an
$N$-representation for $(\mathsf{rng}(\rho_{1}),H)$ and
$(\mathsf{rng}(\rho_{2}),H)$.

######  Proof 3.3.

  1. (1)

Since $\mathsf{rng}(\rho_{1})\cup\mathsf{rng}(\rho_{2})\leq 2r\leq|N|$, start
by choosing any injection $f_{1}$ from
$\mathsf{rng}(\rho_{1})\cup\mathsf{rng}(\rho_{2})$ into $N$. Next, we split by
cases on whether $H\subseteq\mathsf{rng}(\rho_{1})\cup\mathsf{rng}(\rho_{2})$
holds to define

$f_{2}:(H\setminus\mathsf{rng}(\rho_{1})\cup\mathsf{rng}(\rho_{2}))\to N.$

If the condition is true then set $f_{2}$ to be $\emptyset$. Otherwise choose
any $d\in N\setminus f_{1}(\mathsf{rng}(\rho_{1})\cup\mathsf{rng}(\rho_{2}))$
and define the constant function $f_{2}$ by $f_{2}(\ell)=d$ for all $\ell\in
H\setminus\mathsf{rng}(\rho_{1})\cup\mathsf{rng}(\rho_{2})$. Finally, because
$N$ has size $2r+2$, $N\setminus(f_{1}\cup f_{2})(H)\neq\emptyset$ and hence
one may obtain some surjection

$f_{3}:({\mathcal{D}}\setminus H)\to(N\setminus(f_{1}\cup f_{2})(H))$

The required representation is then $f_{1}\cup f_{2}\cup f_{3}$.

  2. (2)

Immediate from the definition.

What makes the reduction difficult is that, having chosen a representation
$\phi$, the $\mathcal{B}$-configuration arrived at after simulating an
$\mathcal{A}$-transition may no longer be correctly represented by $\phi$.
This is because, due to the restriction on the size of $N$, it is necessary to
“recycle” names from the new history $\phi\cdot(H\cup\\{a\\})$, since the new
history may become identified with $N$ and hence there are no spare letters
with which to faithfully simulate globally fresh transitions.

So, if we say that $a$ and $b$ are two letters from $N$, it can be that in one
transition $a$ is a letter local to the current configuration and $b$ is
played as a globally fresh one and stored in place of $a$ in the registers. We
expect that afterwards both of $a$ and $b$ are in the history, preventing them
from being played as globally fresh letters, but if $a$ no longer appears in
the registers it may need to be recycled by removing it from the subsequent
history.

Hence, after simulating a transition, $\mathcal{B}$ must discard the history
it has reached in favour of a new (but still related one) in which it has
recycled some names. We say that the new history is a potting of the old one
and the next definition allows to describe the valid class of potted histories
for a given (concrete) history and a distinguished subset.

Given histories $H$ and $\hat{H}$ and set of letters $X\subseteq H$ such that
$|X|\leq 2r$, $\hat{H}$ is a _potting of $H$ wrt $X$_ whenever:

  1. (1)

$X\subseteq\hat{H}$

  2. (2)

$|\hat{H}|=\lceil|H|\rceil^{2r+1}$.

As we shall see, the set $X$ will always be taken to be the range of the two
register assignments of the current position in the game. This will ensure
that the abstract, potted history always contains all the letters in the
registers of the current game position and hence it will be impossible for a
player of the $\mathcal{B}$-game to make a globally fresh transition using a
letter which is actually already contained in a register of the opposite
system. However, for the potted history to be chosen in this way requires that
the player who chooses it know the contents of both of the register
assignments of the current position of the game. For this reason, we design
$\mathcal{B}$ so that a state contains _both_ the (representations of the)
register assignments of the two configurations involved in the current
position of the $\mathcal{A}$-game which is being simulated.

Let us start to unpack this by making an artificial distinction between the
two “systems” involved in the bisimulation game. Recall that a configuration
of the bisimulation game is a pair $(\kappa,\kappa^{\prime})$ of
configurations of $\mathcal{A}$ where $\kappa$ has been reached from
$\kappa_{1}$ and $\kappa^{\prime}$ has been reached from $\kappa_{2}$
according to the rules of the game. We shall refer to the left component of
this pair as the _left system_ and the right component as the _right system_.
We aim to design $\mathcal{B}$ so as to simulate the bisimulation game induced
by $\mathcal{A}$ and, to this end, the left systems in the $\mathcal{B}$ will
represent the left system in the $\mathcal{A}$ game and conversely. However,
for the reasons given above a configuration of $\mathcal{B}$ (which is just a
state of $\mathcal{B}$) contains a snapshot of a configuration of the
$\mathcal{A}$ bisimulation game (i.e. components from both the left and right
system configurations), plus some additional bookeeping information. Then, to
tell apart the two $\mathcal{B}$ systems, we tag configurations with either
(L)eft or (R)ight.

We make the construction of $\mathcal{B}$ precise as follows. We build the
alphabet as (note that $\delta$ is the finite transition relation of
$\mathcal{A}$):

$\Sigma=(\delta\times N)\cup(\delta\times
N\times\mathcal{P}(N))\cup\\{\heartsuit,L,R\\}$

The states of $\mathcal{B}$ are all the tuples
$(\sigma,\gamma_{1},H,\gamma_{2},p)$ in which
$\sigma\in\\{\mathsf{L},\mathsf{R}\\}$ is the system, $\gamma_{1}$ is an
$N$-configuration of the left system, $H$ is a potted history and $\gamma_{2}$
is an $N$-configuration of the right system. The final component $p$ tracks
the state of the simulation using the following tokens and their meanings:

$\begin{array}[]{ll}\hphantom{\cup\;}\\{\mathsf{A}\\}&\text{(Attacker to
play)}\\\ \cup\;\\{\mathsf{AL}\\}&\text{(Attacker plays in $\mathsf{L}$)}\\\
\cup\;\\{\mathsf{AR}\\}&\text{(Attacker plays in $\mathsf{R}$)}\\\
\cup\;\\{\mathsf{DL}[a]\mid a\in N\\}&\text{(Defender plays $a$ in
$\mathsf{L}$)}\\\ \cup\;\\{\mathsf{DR}[a]\mid a\in N\\}&\text{(Defender plays
$a$ in $\mathsf{R}$)}\\\ \cup\;\\{\mathsf{FL}[a]\mid a\in N\\}&\text{($a$
forced in $\mathsf{L}$)}\\\ \cup\;\\{\mathsf{FR}[a]\mid a\in N\\}&\text{($a$
forced in $\mathsf{R}$)}\\\ \cup\;\\{\mathsf{DL}[\tau]\mid\tau\in\delta\times
N\times\mathcal{P}(N)\\}&\text{(Defender plays $\tau$ in $\mathsf{L}$)}\\\
\cup\;\\{\mathsf{DR}[\tau]\mid\tau\in\delta\times
N\times\mathcal{P}(N)\\}&\text{(Defender plays $\tau$ in
$\mathsf{R}$)}\end{array}$

The following invariant is maintained throughout.

  * •

At the start of simulating an $\mathcal{A}$-turn from position
$((q_{1},\rho_{1},H),(q_{2},\rho_{2},H))$, the $\mathcal{B}$-game is in a
configuration of shape:

$(\,(\mathsf{L},\gamma_{1},\phi\cdot
H,\gamma_{2},\mathsf{A}),\;(\mathsf{R},\gamma_{1},\phi\cdot
H,\gamma_{2},\mathsf{A})\,)$

where $\gamma_{i}=(q_{i},\phi\cdot\rho_{i})$ for some $N$-representation
$\phi$ of $(\mathsf{rng}(\rho_{1})\cup\mathsf{rng}(\rho_{2}),H)$.

In this way, the ($N$-representation of the) internal snapshot of the
$\mathcal{A}$-game is synchronised between the two $\mathcal{B}$ systems and,
according to the bookeeping, Attacker is to play. What makes the simulation
complicated is that one cannot choose $\phi$ uniformly for the whole game.
Instead, because of global freshness, a different representation must be
sought for each new turn.

From the position described by the invariant, the $\mathcal{B}$-game simulates
an Attacker move from the original game using two turns. The first turn allows
Attacker to choose which of the two systems to play in. This is enabled by
adding to $\mathcal{B}$, for all $\sigma$, $\gamma_{1}$, $H$, $\gamma_{2}$ all
transitions of shapes:

$\begin{array}[]{c}(\sigma,\gamma_{1},H,\gamma_{2},\mathsf{A})\xrightarrow{\mathsf{L}}(\sigma,\gamma_{1},H,\gamma_{2},\mathsf{AL})\\\
(\sigma,\gamma_{1},H,\gamma_{2},\mathsf{A})\xrightarrow{\mathsf{R}}(\sigma,\gamma_{1},H,\gamma_{2},\mathsf{AR})\end{array}$

The second turn simulates Attacker’s choice of transition and is implemented
by adding, for all $\sigma$, $\gamma_{1}$, $H$, $\gamma_{2}$, and all
$T\in\delta$ and $a\in N$ the following transitions to $\mathcal{B}$:

$\begin{array}[]{c}(\sigma,\gamma_{1},H,\gamma_{2},\mathsf{AL})\xrightarrow{(T,a)}(\sigma,\gamma_{1}^{\prime},H,\gamma_{2},\mathsf{DR}[a])\\\
(\sigma,\gamma_{1},H,\gamma_{2},\mathsf{AR})\xrightarrow{(T,a)}(\sigma,\gamma_{1},H,\gamma_{2}^{\prime},\mathsf{DL}[a])\end{array}$

subject to the constraint that, for the left case,
$(\gamma_{1},H)\xrightarrow{t,a}(\gamma_{1}^{\prime},H\cup\\{a\\})$ is a
transition of $\mathcal{A}$ induced by $T$ and, for the right case,
$(\gamma_{2},H)\xrightarrow{t,a}(\gamma_{2}^{\prime},H\cup\\{a\\})$ is a
transition of $\mathcal{A}$ induced by $T$.

Next, the $\mathcal{B}$-game simulates a Defender move in the
$\mathcal{A}$-game. This is accomplished over two turns, using Defender
forcing. For the particular case in which Defender is to play on the right and
has exactly two choices $\tau_{1}=(T_{1},a,H^{1})$ and
$\tau_{2}=(T_{2},a,H^{2})$ to choose from, the Defender forcing circuit is
shown in Figure 2. Each choice consists of a transition from $\delta$, a
letter from $N$ and a potted history, subject to certain constraints. In this
case, the game is forced into either the pair of configurations:

$(\mathsf{L},\gamma_{1}^{\prime},H^{1},\gamma_{2}^{1},\mathsf{A})\;(\mathsf{R},\gamma_{1}^{\prime},H^{1},\gamma_{2}^{1},\mathsf{A})$

where $\gamma_{2}^{1}$ is such that
$(\gamma_{2},H)\xrightarrow{t,a}(\gamma_{2}^{1},H\cup\\{a\\})$ is a transition
of $\mathcal{A}$ induced by $T_{1}$ and $H^{1}$ is a potting of $H\cup\\{a\\}$
wrt $\mathsf{rng}(\gamma_{1}^{\prime})\cup\mathsf{rng}(\gamma_{2}^{1})$. Or,
analogously, the game is forced into:

$(\mathsf{L},\gamma_{1}^{\prime},H^{2},\gamma_{2}^{2},\mathsf{A})\;(\mathsf{R},\gamma_{1}^{\prime},H^{2},\gamma_{2}^{2},\mathsf{A})$

where $\gamma_{2}^{2}$ is such that
$(\gamma_{2},H)\xrightarrow{t,a}(\gamma_{2}^{2},H\cup\\{a\\})$ is a transition
of $\mathcal{A}$ induced by $T_{2}$ and $H^{2}$ is a potting of $H\cup\\{a\\}$
wrt $\mathsf{rng}(\gamma_{1}^{\prime})\cup\mathsf{rng}(\gamma_{2}^{2})$.

In general, there are not exactly two choices $\tau_{1}$ and $\tau_{2}$ from
which Defender can choose from, so we generalise the gadget in the obvious way
to support one choice

$(\mathsf{R},\gamma_{1}^{\prime},H,\gamma_{2},\mathsf{DR}[\tau_{i}])\xrightarrow{\tau_{i}}(\mathsf{R},\gamma_{1}^{\prime},H^{i},\gamma_{2}^{i},\mathsf{A})$

for each $\tau_{i}=(T_{i},a,H^{i})$ such that
$(\gamma_{2},H)\xrightarrow{t,a}(\gamma_{2}^{i},H\cup\\{a\\})$ is a transition
of $\mathcal{A}$ induced by $T_{i}$ ($a$ is fixed) and $H^{i}$ is a potting of
$H\cup\\{a\\}$ wrt
$\mathsf{rng}(\gamma_{1}^{\prime})\cup\mathsf{rng}(\gamma_{2}^{i})$. Note that
this generalisation includes the possibility that there are no choices for
Defender, in which case the only transition in the gadget is
$(\mathsf{L},\gamma_{1}^{\prime},H,\gamma_{2},\mathsf{DR}[a])\xrightarrow{\heartsuit}(\mathsf{L},\gamma_{1}^{\prime},H,\gamma_{2},\mathsf{DR}[a])$.
When Attacker has played on the right, so that Defender is to play on the
left, we use a symmetric version of the gadget.

$(\mathsf{L},\gamma_{1}^{\prime},H,\gamma_{2},\mathsf{DR}[a])$$(\mathsf{R},\gamma_{1}^{\prime},H,\gamma_{2},\mathsf{DR}[a])$$(\mathsf{L},\gamma_{1}^{\prime},H,\gamma_{2},\mathsf{FR}[a])$$(\mathsf{R},\gamma_{1}^{\prime},H,\gamma_{2},\mathsf{DR}[\tau_{1}])$$(\mathsf{R},\gamma_{1}^{\prime},H,\gamma_{2},\mathsf{DR}[\tau_{2}])$$(\mathsf{R},\gamma_{1}^{\prime},H^{1},\gamma_{2}^{1},\mathsf{A})$$(\mathsf{R},\gamma_{1}^{\prime},H^{2},\gamma_{2}^{2},\mathsf{A})$$(\mathsf{L},\gamma_{1}^{\prime},H^{2},\gamma_{2}^{2},\mathsf{A})$$(\mathsf{L},\gamma_{1}^{\prime},H^{1},\gamma_{2}^{1},\mathsf{A})$$\heartsuit$$\heartsuit$$\heartsuit$$\heartsuit$$\heartsuit$
$\tau_{1}$$\tau_{2}$$\tau_{1}$$\tau_{2}$$\tau_{1}$$\tau_{2}$ Figure 2.
Simulating Defender’s move by forcing.

Given a binary relation $\approx$ over $\mathcal{B}$-configurations, let us
write $\gamma_{1}\approx_{H}\gamma_{2}$ whenever

$((\mathsf{L},\gamma_{1},H,\gamma_{2},\mathsf{A}),(\mathsf{R},\gamma_{1},H,\gamma_{2},\mathsf{A}))\in{\approx}.$

The central property of automaton construction is the following.

######  Lemma 7.

Let $\approx$ be a binary relation on $\mathcal{B}$-configurations whose
elements are all of the form
$(\mathsf{L},\gamma_{1},H,\gamma_{2},\mathsf{A}),(\mathsf{R},\gamma_{1},H,\gamma_{2},\mathsf{A})$.
Then there exists a $\mathcal{S}(\mathcal{B})$-bisimulation
$R\supseteq\>\approx$ iff for all such elements of $R$:

  * •

if $(\gamma_{1},H)\xrightarrow{t,a}(\gamma_{1}^{\prime},H\cup\\{a\\})$ then
there is some $\gamma_{2}^{\prime}$ and some potting $\hat{H}$ of
$H\cup\\{a\\}$ wrt
$\mathsf{rng}(\gamma_{1}^{\prime})\cup\mathsf{rng}(\gamma_{2}^{\prime})$ such
that: $(\gamma_{2},H)\xrightarrow{t,a}(\gamma_{2}^{\prime},H\cup\\{a\\})$ and
$\gamma_{1}^{\prime}\approx_{\hat{H}}\gamma_{2}^{\prime}$.

  * •

if $(\gamma_{2},H)\xrightarrow{t,a}(\gamma_{2}^{\prime},H\cup\\{a\\})$ then
there is some $\gamma_{1}^{\prime}$ and some potting $\hat{H}$ of
$H\cup\\{a\\}$ wrt
$\mathsf{rng}(\gamma_{1}^{\prime})\cup\mathsf{rng}(\gamma_{2}^{\prime})$ such
that: $(\gamma_{1},H)\xrightarrow{t,a}(\gamma_{1}^{\prime},H\cup\\{a\\})$ and
$\gamma_{1}^{\prime}\approx_{\hat{H}}\gamma_{2}^{\prime}$.

######  Proof 3.4.

In the forward direction, assume that there exists a
$\mathcal{S}(\mathcal{B})$-bisimulation $R$ including $\approx$ and consider
some $\gamma_{1}\approx_{H}\gamma_{2}$. Let
$(\gamma_{1},H)\xrightarrow{t,a}(\gamma_{1}^{\prime},H\cup\\{a\\})$ (*). By
construction, if Defender is to win the Bisimulation game from this position,
a necessary condition is that for every transition (i):

$(\mathsf{L},\gamma_{1},H,\gamma_{2},\mathsf{AL})\xrightarrow{(T_{1},a)}(\mathsf{L},\gamma_{1}^{\prime},H,\gamma_{2},\mathsf{DR}[a])$

there is a corresponding transition (ii):

$(\mathsf{R},\gamma_{1}^{\prime},H,\gamma_{2},\mathsf{DR}[(T_{2},a,H^{2})])\xrightarrow{(T_{2},a,H^{2})}(\mathsf{R},\gamma_{1}^{\prime},H^{2},\gamma_{2}^{\prime},\mathsf{A})$

It follows from $(*)$ that there is a transition (i) and therefore also a
transition (ii). Necessarily then
$(\gamma_{2},H)\xrightarrow{t,a}(\gamma_{2}^{\prime},H\cup\\{a\\})$ and it
follows from the construction that there will be such a transition for each
potted history satisfying the constraints (of which there is always at least
one). The other case is symmetric.

In the backward direction, assume the conditions are satisfied and we show
that such an $R$ exists by arguing that every pair of configurations in
$\approx$ is a winning position for Defender in the induced bisimulation game.
To see this simply observe that, by construction, the only way that Attacker
can win in the bisimulation game is for the game to reach a position of shape
$((\mathsf{L},\gamma_{1}^{\prime},H,\gamma_{2},\mathsf{DR}[a]),(\mathsf{R},\gamma_{1}^{\prime},H,\gamma_{2},\mathsf{DR}[a]))$
(or symmetrically with final component $\mathsf{DL}[a]$) and for Defender to
have zero choices in the Defender forcing gadget. However, this can only
happen if Attacker was able to choose some transition

$(\mathsf{L},\gamma_{1},H,\gamma_{2},\mathsf{AL})\xrightarrow{(T_{1},a)}(\mathsf{L},\gamma_{1}^{\prime},H,\gamma_{2},\mathsf{DR}[a])$

and there is no corresponding transition for Defender to force. However, it
follows from the assumption that there is always some choice of corresponding
transition. Note that if a transition
$(\gamma_{2},H)\xrightarrow{t,a}(\gamma_{2}^{\prime},H\cup\\{a\\})$ is valid
then there is always some choice of $\hat{H}$ satisfying the constraints. The
other case is symmetrical.

From a $\mathcal{S}(\mathcal{B})$-bisimulation and an appropriate
$N$-representation one may construct a
$\mathcal{S}(\mathcal{A})$-bisimulation.

######  Lemma 8.

Suppose $\approx$ is a $\mathcal{S}(\mathcal{B})$-bisimulation. Then let
$R^{\prime}$ contain $((q_{1},\rho_{1},H),(q_{2},\rho_{2},H))$ just if:

  1. (1)

$(q_{1},\phi\cdot\rho_{1})\approx_{\phi\cdot H}(q_{2},\phi\cdot\rho_{2})$

  2. (2)

and $\phi$ is any $N$-representation of
$(\mathsf{rng}(\rho_{1})\cup\mathsf{rng}(\rho_{2}),H)$.

Then $R^{\prime}$ is a $\mathcal{S}(\mathcal{A})$-bisimulation.

######  Proof 3.5.

Suppose $((q_{1},\rho_{1},H),(q_{2},\rho_{2},H))\in R^{\prime}$ and
$(q_{1},\rho_{1},H)\xrightarrow{t,a}(q_{1}^{\prime},\rho_{1}^{\prime}[i\mapsto
a],H\cup\\{a\\})$ by some transition $T_{1}\in\delta$. It follows from Lemma 5
that therefore $(q_{1},\phi\cdot\rho_{1},\phi\cdot
H)\xrightarrow{t,\phi(a)}(q_{1}^{\prime},(\phi\cdot\rho_{1}^{\prime})[i\mapsto\phi(a)],(\phi\cdot
H)\cup\\{\phi(a)\\})$. Since $\approx$ is a bisimulation, it follows from
Lemma 7 that there is some $(q_{2},\phi\cdot\rho_{2},\phi\cdot
H)\xrightarrow{t,\phi(a)}(q_{2}^{\prime},(\phi\cdot\rho_{2}^{\prime})[j\mapsto\phi(a)],(\phi\cdot
H)\cup\\{\phi(a)\\})$, and some $\hat{H}$ a potting of $(\phi\cdot
H)\cup\\{\phi(a)\\}$ wrt
$\mathsf{rng}(\phi\cdot\rho_{1}^{\prime})\cup\mathsf{rng}(\phi\cdot\rho_{2}^{\prime})\cup\\{a\\}$
such that
$(q_{1}^{\prime},(\phi\cdot\rho_{1}^{\prime})[i\mapsto\phi(a)])\approx_{\hat{H}}(q_{2}^{\prime},(\phi\cdot\rho_{2}^{\prime})[j\mapsto\phi(a)])$.
It follows again from Lemma 5 that therefore there is some
$(q_{2},\rho_{2},H)\xrightarrow{t,a}(q_{2}^{\prime},\rho_{2}^{\prime}[j\mapsto
a],H\cup\\{a\\})$. Next observe that, by construction,
$N\setminus\hat{H}\neq\emptyset$ and, if
$H\setminus\mathsf{rng}(\rho_{1}^{\prime})\cup\mathsf{rng}(\rho_{2}^{\prime})\neq\emptyset$,
then
$\hat{H}\setminus(\mathsf{rng}(\phi\cdot\rho_{1}^{\prime})\cup\mathsf{rng}(\phi\cdot\rho_{2}^{\prime})\cup\\{\phi(a)\\})\neq\emptyset$.
Consequently, it is possible to find surjections:

$\begin{array}[]{lcl}f_{1}&:&(\mathcal{D}\setminus(H\cup\\{a\\}))\to(N\setminus\hat{H})\\\
f_{2}&:&(H\cup\\{a\\}\setminus\mathsf{rng}(\rho_{1}^{\prime})\cup\mathsf{rng}(\rho_{2}^{\prime})\cup\\{a\\})\\\
&&\qquad\to(\hat{H}\setminus\mathsf{rng}(\phi\cdot\rho_{1}^{\prime})\cup\mathsf{rng}(\phi\cdot\rho_{2}^{\prime})\cup\\{\phi(a)\\}\\\
\end{array}$

and construct the particular bijection:

$f_{3}:\mathsf{rng}(\rho_{1}^{\prime})\cup\mathsf{rng}(\rho_{2}^{\prime})\cup\\{a\\}\to\mathsf{rng}(\phi\cdot\rho_{1}^{\prime})\cup\mathsf{rng}(\phi\cdot\rho_{2}^{\prime})\cup\\{\phi(a)\\}$

given by
$f_{3}=\phi\restriction\mathsf{rng}(\rho_{1}^{\prime})\cup\mathsf{rng}(\rho_{2}^{\prime})\cup\\{a\\}$.
It follows that $\phi=f_{1}\cup f_{2}\cup f_{3}$ is an $N$-representation of
$(\mathsf{rng}(\rho_{1}^{\prime})\cup\mathsf{rng}(\rho_{2}^{\prime})\cup\\{a\\},H)$
such that $\phi^{\prime}\cdot(\rho_{1}^{\prime}[i\mapsto
a])=(\phi\cdot\rho_{1}^{\prime})[i\mapsto\phi(a)]$,
$\phi^{\prime}\cdot(\rho_{2}^{\prime}[i\mapsto
a])=(\phi\cdot\rho_{2}^{\prime})[j\mapsto\phi(a)]$ and $\phi^{\prime}\cdot
H=\hat{H}$ as required. The case in which the second component makes a
transition is symmetrical.

Similarly, from a $\mathcal{S}(\mathcal{A})$-bisimulation and an appropriate
$N$-representation, one may construct a
$\mathcal{S}(\mathcal{B})$-bisimulation.

######  Lemma 9.

Suppose $R$ is a $\mathcal{S}(\mathcal{A})$-bisimulation. Let $\approx$ relate
$(\mathsf{L},q_{1},\phi\cdot\rho_{1},\phi\cdot
H,q_{2},\phi\cdot\rho_{2},\mathsf{A})$ to
$(\mathsf{R},q_{1},\phi\cdot\rho_{1},\phi\cdot{H},q_{2},\phi\cdot\rho_{2},\mathsf{A})$
just if:

  1. (1)

$((q_{1},\rho_{1},H),(q_{2},\rho_{2},H))\in R$

  2. (2)

and $\phi$ is an $N$-representation of
$(\mathsf{rng}(\rho_{1})\cup\mathsf{rng}(\rho_{2}),H)$.

Then there exists a $\mathcal{B}$-simulation containing $\approx$.

######  Proof 3.6.

By Lemma 7 suppose $(q_{1},\phi\cdot\rho_{1},\phi\cdot
H)\xrightarrow{t,a}(q_{1}^{\prime},(\phi\cdot\rho_{1}^{\prime})[i\mapsto
a],(\phi\cdot H)\cup\\{a\\})$. It follows from Lemma 7 and surjectivity of
representations that there is a corresponding
$(q_{1},\rho_{1},H)\xrightarrow{t,b}(q_{1}^{\prime},\rho_{1}^{\prime}[i\to
b],H\cup\\{b\\})$. Since $R$ is a bisimulation, it follows that there is some
$(q_{2},\rho_{2},H)\xrightarrow{t,b}(q_{2}^{\prime},\rho_{2}^{\prime}[j\to
b],H\cup\\{b\\})$ and $(q_{1}^{\prime},\rho_{1}^{\prime}[i\to b],H)$ is
related to $(q_{2}^{\prime},\rho_{2}^{\prime}[j\to b],H\cup\\{b\\})$ by $R$.
It follows from Lemma 5 that there is a corresponding
$(q_{2},\phi\cdot\rho_{2},\phi\cdot
H)\xrightarrow{t,a}(q_{2}^{\prime},(\phi\cdot\rho_{2}^{\prime})[j\to
a],(\phi\cdot H)\cup\\{a\\})$. Let $\hat{H}$ be any potting of $(\phi\cdot
H)\cup\\{a\\}$ wrt
$\mathsf{rng}(\phi\cdot\rho_{1}^{\prime})\cup\mathsf{rng}(\phi\cdot\rho_{2}^{\prime})\cup\\{a\\}$.
Then it follows that $N\setminus\hat{H}\neq\emptyset$ and
$(H\cup\\{b\\})\setminus(\mathsf{rng}(\rho_{1}^{\prime})\cup\mathsf{rng}(\rho_{2}^{\prime})\cup\\{b\\})\neq\emptyset$
implies
$\hat{H}\setminus(\mathsf{rng}(\phi\cdot\rho_{1}^{\prime})\cup\mathsf{rng}(\phi\cdot\rho_{2}^{\prime})\cup\\{a\\})\neq\emptyset$.
Consequently it is possible to find surjections:

$\begin{array}[]{lcl}f_{1}&:&(\mathcal{D}\setminus(H\cup\\{b\\}))\to(N\setminus\hat{H})\\\
f_{2}&:&(H\cup\\{b\\}\setminus\mathsf{rng}(\rho_{1}^{\prime})\cup\mathsf{rng}(\rho_{2}^{\prime})\cup\\{b\\})\\\
&&\qquad\to(\hat{H}\setminus\mathsf{rng}(\phi\cdot\rho_{1}^{\prime})\cup\mathsf{rng}(\phi\cdot\rho_{2}^{\prime})\cup\\{a\\}\\\
\end{array}$

and construct the particular bijection:

$f_{3}:\mathsf{rng}(\rho_{1}^{\prime})\cup\mathsf{rng}(\rho_{2}^{\prime})\cup\\{b\\}\to\mathsf{rng}(\phi\cdot\rho_{1}^{\prime})\cup\mathsf{rng}(\phi\cdot\rho_{2}^{\prime})\cup\\{a\\}$

given by
$f_{3}=\phi\restriction\mathsf{rng}(\rho_{1}^{\prime})\cup\mathsf{rng}(\rho_{2}^{\prime})\cup\\{b\\}$.
It follows that $\phi=f_{1}\cup f_{2}\cup f_{3}$ is an $N$-representation of
$(\mathsf{rng}(\rho_{1}^{\prime})\cup\mathsf{rng}(\rho_{2}^{\prime})\cup\\{b\\},H)$
such that $\phi^{\prime}\cdot(\rho_{1}^{\prime}[i\mapsto
b])=(\phi\cdot\rho_{1}^{\prime})[i\mapsto a]$,
$\phi^{\prime}\cdot(\rho_{2}^{\prime}[i\mapsto
b])=(\phi\cdot\rho_{2}^{\prime})[j\mapsto a]$ and $\phi^{\prime}\cdot
H=\hat{H}$ as required. The case in which the second component makes a
transition is symmetrical. Hence, we conclude by Lemma 7.

Consequently, we can prove the main result:

######  Theorem 10.

Suppose $\phi$ is an $N$-representation of
$(\mathsf{rng}(\rho_{1})\cup\mathsf{rng}(\rho_{2}),H)$. Then
$(q_{1},\rho_{1},H)\sim(q_{2},\rho_{2},H)$ iff
$(q_{1},\phi\cdot\rho_{1})\sim_{\phi\cdot H}(q_{2},\phi\cdot\rho_{2})$.

######  Proof 3.7.

Suppose $(q_{1},\rho_{1},H)\sim(q_{2},\rho_{2},H)$ in
$\mathcal{S}(\mathcal{A})$. Then it follows from Lemma 9 that there is some
$\mathcal{S}(\mathcal{B})$-bisimulation $\approx$ such that
$(q_{1},\phi\cdot\rho_{1})\approx_{\phi\cdot H}(q_{2},\phi\cdot\rho_{2})$.
Conversely, suppose that $(q_{1},\phi\cdot\rho_{1})\sim_{\phi\cdot
H}(q_{2},\phi\cdot\rho_{2})$ in $\mathcal{S}(\mathcal{B})$. It follows from
Lemma 8 that there is some $\mathcal{S}(\mathcal{B})$-bisimulation $R$ such
that $((q_{1},\rho_{1},H),(q_{2},\rho_{2},H))\in R$.

######  Remark 11.

The preceding proof shows that one turn of the FRA($M\\#)$ bisimulation game
can be simulated by using four turns of the bisimulation game for the
simulating finite automaton. Consequently, any winning strategy for the FRA-
induced game can be transformed into a winning strategy for the finite
automaton-induced game with at most a constant-factor increase in depth.

Further down the hierachy, to show $\bm{\sim}$-RA($S\\#$) is EXPTIME-hard, we
use the registers of this class of automata to represent the tape content of
bounded Turing machines. An alternating linear bounded automaton (ALBA) is a
tuple
$\mathcal{A}=\langle\Gamma,Q_{\forall},Q_{\exists},q_{0},q_{\text{acc}},q_{\text{rej}},\delta\rangle$.
We write $Q=Q_{\forall}\uplus Q_{\exists}$. The components are:

  * •

A finite tape alphabet $\Gamma$ containing end-of-tape markers $\triangleleft$
and $\triangleright$.

  * •

A finite set of universal states $Q_{\forall}$.

  * •

A disjoint, finite set of existential states $Q_{\exists}$.

  * •

Distinguished initial state $q_{0}\in Q$.

  * •

Disjoint accepting and rejecting states $q_{\text{acc}},\,q_{\text{rej}}\notin
Q$.

  * •

A transition function
$\delta:Q\times\Gamma\to(Q\times\Gamma\times\\{-1,\,+1\\})^{*}$, satisfying
the following properties: (i) if
$(q^{\prime},a,d)\in\mathsf{rng}(\delta(q,\triangleright))$ then
$a=\triangleright$ and $d=+1$; (ii) if
$(q^{\prime},a,d)\in\mathsf{rng}(\delta(q,\triangleleft))$ then
$a=\triangleleft$ and $d=-1$; (iii) if $(q^{\prime},a,d)\in\delta(q,b)$ then
$b\in\Gamma\setminus\\{\triangleleft,\triangleright\\}$ implies
$a\in\Gamma\setminus\\{\triangleleft,\triangleright\\}$.

A configuration of such a machine is a triple $c=(q,\,k,\,t)$ with $q$ a
state, $t$ the current tape contents and $k$ the index of the cell currently
under the head of the machine. We assume that the tape contents is of the form
$\triangleright a_{1}\cdots a_{n}\triangleleft$ for some letters
$a_{i}\in\Gamma\setminus\\{\triangleleft,\triangleright\\}$. We write $t(k)$
for the contents of cell $k$ of tape $t$. We say that a configuration
$(q,k,t)$ is accepting (respectively rejecting, universal, existential) just
if $q=q_{\text{acc}}$ (respectively $q=q_{\text{rej}}$, $q\in Q_{\forall}$,
$q\in Q_{\exists}$).

A configuration $(q_{1},k_{1},t_{1})$ can make a transition to a successor
$(q_{2},k_{2},t_{2})$ just if there is
$a\in\Gamma\setminus\\{\triangleleft,\triangleright\\}$ and $d\in\\{-1,+1\\}$
such that $(q_{2},a,d)\in\mathsf{rng}(\delta(q_{1},t_{1}(k_{1})))$ and
$k_{2}=k_{1}+d$ and $t_{2}=t_{1}[k_{1}\mapsto a]$.

Given an input $w\in\Gamma\setminus\\{\triangleleft,\triangleright\\}$, a
computation tree on $w$ for such a machine is an unordered tree labelled by
configurations which additionally satisfies the following conditions:

  * •

The tree is rooted at $(q_{0},1,\triangleright w\triangleleft)$.

  * •

If a universal configuration $c$ labels some node of the tree then this node
has one child for each possible successor to $c$.

  * •

If an existential configuration $c$ labels some node of the tree then this
node has exactly one child which can be any successor to $c$.

We say that an input $w$ is accepted just if every leaf of the computation
tree on $w$ is accepting.

The problem of deciding whether a given input is accepted by a given ALBA is
well known to be EXPTIME-complete. The problem ALBA-Mem is, given an ALBA
$\mathcal{M}$ and an input $w$, to determine whether $w$ is accepted by
$\mathcal{M}$.

For the purposes of the argument, we will assume without loss of generality
that $\Gamma\setminus\\{\triangleleft,\triangleright\\}=\\{0,1\\}$ and, for
all $(q,a)$, $|\delta(q,a)|=2$. Thus all choices presented by the alternation
are binary — a unary choice may be represented by having
$\delta(q,a)(1)=\delta(q,a)(2)$. Starting from an instance of the ALBA-Mem
problem $\langle\mathcal{M},w\rangle$, we construct a bisimulation problem for
RA($S\\#$) in which two configurations are bisimilar iff $\mathcal{M}$ accepts
$w$. From an ALBA $\mathcal{M}$ we construct an RA($S\\#$) $\mathcal{A}$ that
simulates it, with the the binary tape content of $\mathcal{M}$ encoded by the
register assignment of $\mathcal{A}$. At every step of the bisimulation game,
we arrange for Defender to choose transitions from existential states (using
Defender forcing [JS08]) and Attacker to choose from universal states.

The ability of $\mathcal{A}$ to use empty registers and to erase full
registers is key to encoding the exponential amount of information held on the
tape in a number of registers that is polynomial in its size. To this end, to
represent a tape of size $n$, we equip $\mathcal{A}$ with $2n$ registers,
under the following encoding. Cell $k$ of the tape has $0$ written on it iff
register $2k-1$ is empty and it has $1$ written on it iff register $2k$ is
empty.

######  Proposition 12.

$\bm{\sim}$-RA($S\\#$) is EXPTIME-hard.

Given an instance $\langle\mathcal{M},\,w\rangle$ of the ALBA-Mem problem, we
construct a $2|w|+2$ register RA($S\\#$) $\mathcal{A}_{\mathcal{M}}^{w}$ whose
induced bisimulation game simulates the computations of $\mathcal{M}$ by
having Attacker choose successor configurations from universal states and
Defender choose successor configurations from existential states. A
configuration of a computation of $\mathcal{M}$ will be represented, in
duplicate, by a pair of configurations of $\mathcal{A}_{\mathcal{M}}^{w}$
which together make up a single configuration of the bisimulation game. These
configurations will track the current state of $\mathcal{M}$ and the current
position of the head of $\mathcal{M}$ in their state and the current tape
contents of $\mathcal{M}$ will be represented by their current register
assignment $\mathcal{A}_{\mathcal{M}}^{w}$.

##### Tape encoding

In particular, the last $2|w|$ registers of $\mathcal{A}_{\mathcal{M}}^{w}$
will be used to encode the non-endmarker tape contents of $\mathcal{M}$. For
this purpose we use the following encoding: tape cell $k\in[2,|w|+1]$ contains
$0$ iff register $2k-1$ is empty and register $2k$ contains a letter;
similarly tape cell $k\in[2,|w|+1]$ contains $1$ iff register $2k-1$ contains
a letter and register $2k$ is empty. The first two registers $1$ and $2$ are
used to help implement a simulation of alternation and will never be empty.

We build the states of this automaton from the transition relation of
$\mathcal{M}$, tape cell indices and special tags $L$, $R$, $0$, $1$ and $2$.
The states are as follows:

  * •

For each $q\in Q$, $k\in[1,|w|+2]$, $a\in\Gamma$, $C\in\\{L,R\\}$: states
$(q,k,C)$, $(q,k,a,C)$.

  * •

For each $q\in Q_{\forall}$, $k\in[1,|w|+2]$: states $(q,k,L)$ and $(q,k,R)$

  * •

For each $q\in Q_{\exists}$, $k\in[1,|w|+2]$: states $(q,k,L)$, $(q,k,R)$,
$(q,k,0)$, $(q,k,1)$ and $(q,k,2)$.

  * •

For each $(q,a,d)\in\bigcup\mathsf{rng}(\delta)$, $k\in[1,|w|+2]$: states
$(k,q,a,d,L)$ and $(k,q,a,d,R)$.

  * •

For each $k\in[1,|w|+2]$, $C\in\\{L,R\\}$: states $(q_{\text{acc}},k,C)$ and
$(q_{\text{rej}},k,C)$.

Let us write a typical state of $\mathcal{A}_{\mathcal{M}}^{w}$ as $p$. Given
a state $p$, we write $p[t]$ for the tuple $p$ with its final component
replaced by tag $t\in\\{L,R,0,1,2\\}$.

Let us take any $2|w|+2$-register assignment $\rho_{I}$ that encodes the
initial input $w$ as above and also assigns some letters to registers $1$ and
$2$. We define the construction of $\mathcal{A}_{\mathcal{M}}^{w}$ to ensure
that configurations $((q_{0},1,L),\rho_{I})$ and $((q_{0},1,R),\rho_{I})$ are
bisimilar iff $\mathcal{M}$ accepts $w$.

We motivate the construction via the bisimulation game that it induces, a
configuration of which is a pair of configurations
$((p_{1},\rho_{1}),\,(p_{2},\rho_{2}))$ of $\mathcal{A}_{\mathcal{M}}^{w}$. We
define $\mathcal{A}_{\mathcal{M}}^{w}$ so that the following invariant holds
for configurations in the induced bisimulation game: every configuration in
the game has shape $((p_{1},\rho),(p_{2},\rho))$ in which $p_{1}$ and $p_{2}$
are either identical or identical except for the final tag component. The idea
is that when the two configurations are of the form $((q,k,C),\rho)$, with
$C\in\\{L,R\\}$, the play is simulating a configuration of $\mathcal{M}$ which
is in state $q$, with the head over tape cell $k$ and the tape contents itself
encoded by the first $2|w|$ registers of $\rho$. When the two configurations
are of the form $(q,k,a,C)$ then furthermore the simulation as decoded symbol
$a$ as being the current contents of the tape at cell $k$. When the two
configurations are of the form $((k,q,a,d,C),\rho)$, then the play is part of
the way through simulating a transition, as given by
$(q,a,d)\in\bigcup\mathsf{rng}(\delta)$. Finally, when the configurations are
of the form $((k,q,i)\,\rho)$, for $i\in\\{0,1,2\\}$, the play is part of the
way through simulating a transition which is, in particular, a transition from
an existential state and for which defender forcing is required.

We will not require the use of any tags (cf. data words) in our construction,
so we assume that $\Sigma$ is a unary alphabet and omit this component in
transitions. In order to describe the transition relation of the automaton we
will make use of a gadget to implement defender forcing. Since the
configurations of the induced bisimulation game are guaranteed, by the
invariant, to have the same register contents, we are able to instantiate the
general construction of [JS08], in which Attacker is punished for making
choices inconsistent with Defender’s wishes by allowing Defender to move his
system into a configuration identical with that of Attacker. The gadget
$\mathsf{DF}(p)(p^{\prime},p^{\prime\prime})$ ensures that, when the game
configuration consists of two system configurations of shape $(p[L],\rho)$ and
$(p[R],\rho)$, then Defender can force the play so that the game enters a
configuration consisting of either the two system configurations
$(p^{\prime}[L],\rho)$ and $(p^{\prime}[R],\rho)$, or the two system
configurations $(p^{\prime\prime}[L],\rho)$ and $(p^{\prime\prime}[R],\rho)$.
The gadget is shown in Figure 3, in which the labels on the transitions are
given by $\ell_{1}=\\{1\\},0,\emptyset$ and $\ell_{2}=\\{2\\},0,\emptyset$. It
is by this defender forcing gadget that we will be able to ensure that the two
players correctly simulate existential choices made by $\mathcal{M}$,
essentially by allowing Defender to make the choice.

$\textstyle{p[L]\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\ell_{1}}$$\scriptstyle{\ell_{1}}$$\scriptstyle{\ell_{1}}$$\textstyle{p[R]\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\ell_{1}}$$\scriptstyle{\ell_{1}}$$\textstyle{p[0]\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\ell_{1}}$$\scriptstyle{\ell_{2}}$$\textstyle{p[1]\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\ell_{1}}$$\scriptstyle{\ell_{2}}$$\textstyle{p[2]\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\ell_{1}}$$\scriptstyle{\ell_{2}}$$\textstyle{p^{\prime}[L]}$$\textstyle{p^{\prime}[R]}$$\textstyle{p^{\prime\prime}[L]}$$\textstyle{p^{\prime\prime}[R]}$
Figure 3. $\mathsf{DF}(p)(p^{\prime},p^{\prime\prime})$

We describe the transitions of $\mathcal{A}_{\mathcal{M}}^{w}$ as part of a
general description of how the induced bisimulation game simulates
$\mathcal{M}$. Recall that a configuration of the form $((q,k,C),\rho)$ is
used to simulate $\mathcal{M}$ in operating in state $q$ with the head over
cell $k$ of tape encoded by $\rho$. Simulating a transition of $\mathcal{M}$
from this configuration is broken into three parts. In the first part the tape
encoding in $\rho$ is decoded to obtain the letter $a$ under the head. In the
second part a successor is chosen from among $\delta(q,a)$. In the third part
the game over $\mathcal{A}_{\mathcal{M}}^{w}$ moves into a configuration
representing the simulation of the successor in $\mathcal{M}$.

##### Decoding the tape

The decoding of the tape is split into two cases, depending on whether the
head of the machine being simulated is over an endmarker or not. If
$k\in\\{1,|w|+1\\}$ then the head is over an endmarker, and the contents of
cell $k$ is completely determined by $k$. Hence, in such cases we use
transitions of shape:

$(q,k,C)\mathrel{\xrightarrow{\\{1\\},0,\emptyset}}(q,k,a,C)$

where $k=1$ implies $a=\triangleright$ and $k=|w|+1$ implies
$a=\triangleleft$. Otherwise $k\in[2,|w|]$ and the head is over a cell which
is encoded in the way described above. To decode it we use pairs of
transitions of shape:

$\begin{array}[]{c}(q,k,C)\mathrel{\xrightarrow{\\{2k\\},0,\\{2k\\}}}(q,k,0,C)\\\
(q,k,C)\mathrel{\xrightarrow{\\{2k-1\\},0,\\{2k-1\\}}}(q,k,1,C)\end{array}$

since the tape encoding has cell $k$ represented by cells $2k-1$ and $2k$, of
which exactly one contains a letter. Hence, from a configuration
$((q,k,C),\rho)$ with $\rho$ an encoding of the tape, exactly one of these two
transitions will be applicable. The state $(q,k,i,C)$ records the value $i$
that was read, and the tape contents after the transition empties the register
that stored the letter, so that both cells $k-1$ and $k$ are empty. This
prepares the way for writing a new value in the third part.

##### Choosing a transition from a universal state

If $q\in Q_{\forall}$ then it is up to Attacker to choose the successor.
Hence, we use the following transitions:

$\\{(q,k,a,C)\mathrel{\xrightarrow{\\{l\\},0,\emptyset}}(k,q^{\prime},b,d,C)\,|\,\delta(q,a)(l)=(q^{\prime},b,d)\\}$

Since, in each round of the bisimulation game, Attacker gets to choose the
next transition of $\mathcal{A}_{\mathcal{M}}^{w}$ first, he will choose which
transition of $\mathcal{M}$ is simulated. Since his choice is communicated by
announcing (in the $\mathcal{A}_{\mathcal{M}}^{w}$-transition label) the index
$l\in\\{1,2\\}$ of the $\mathcal{M}$-transition, Defender will be forced to
choose the same transition in the complementary system.

##### Choosing a transition from an existential state

If $q\in Q_{\exists}$ then it is up to Defender to choose the successor. In
this case we use an instance of the defender forcing gadget:

$\mathsf{DF}(q,k,i,\\_)((k,q_{1},b_{1},d_{1},\\_),(k,q_{2},b_{2},d_{2},\\_))$

where $\delta(q,i)=(q_{1},b_{1},d_{1})\,(q_{2},b_{2},d_{2})$. Note that the
tags on the states here are irrelevant since they will be replaced by the
construction of the gadget. This ensures that Defender can steer the
simulation into her choice whilst maintaining the invariant about the shape of
configurations.

##### Computing the successor

Moving the configuration of $\mathcal{A}_{\mathcal{M}}^{w}$ into a state that
simulates the successor according to the chosen transition of $\mathcal{M}$
involves changing the contents of the current register assignment to reflect
the action of $\mathcal{M}$ writing to the tape. Hence, we split the
construction based on whether or not the cell $k$ contains an endmarker. If
$k\in\\{1,|w|+1\\}$ then the cell under the head contains an endmarker and
hence the register assignment should not change, but only the state since that
contains the information about the current position of the head. To this end
we use transitions of the following shape:

$(k,q^{\prime},b,d,C)\mathrel{\xrightarrow{\\{1\\},0,\emptyset}}(q^{\prime},k+d,C)$

Otherwise $k\in[2,|w|]$ and the registers should be updated according to the
encoding described above. We use the transitions of shape:

$(k,q^{\prime},b,d,C)\mathrel{\xrightarrow{\emptyset,2k-b,\emptyset}}(q^{\prime},k+d,C)$

##### Accepting and rejecting states

If the simulation reaches an accepting state then Defender should win. We
organise for this to happen by forbidding any transition out of any state of
shape $(q_{\text{acc}},k,C)$. In this way, any two configurations that are
both in states of this form are trivially bisimilar since neither can perform
an action. Conversely Attacker should win if the simulation reaches a
rejecting state. We organise for this to happen by transitions of the
following shape:

$(q_{\text{rej}},k,L)\mathrel{\xrightarrow{{1},0,\emptyset}}(q_{\text{rej}},k,L)$

Notice that such transitions only occur in those states that are tagged $L$.
By construction, when the simulation arrives at a rejecting state, one
configuration will in such a state tagged with $L$ and the other with $R$ and
it follows that the two configurations will not be bisimilar.

######  Lemma 13.

Given an ALBA $\mathcal{M}$ and input $w$, $\mathcal{M}$ accepts $w$ iff
Defender has a winning strategy in the bisimulation game for
$\langle\mathcal{S}_{\mathcal{A}_{\mathcal{M}}^{w}},((q_{0},1,L),\rho_{I})((q_{0},1,R),\rho_{I})\rangle$,
where $\rho_{I}$ is a register assignment encoding $w$ in the way described
above.

######  Proof 3.8.

First notice that, by construction, there are only two ways that Defender can
win a play of the bisimulation game:

  1. (1)

By Attacker choosing a move in the defender forcing gadget which results in a
punishment response from Defender so that every game configuration that
follows in the play is of shape $((p,\rho),(p,\rho))$ whose components are
trivially bisimilar.

  2. (2)

By the play reaching a game configuration in which the two component
configurations are of shape $((q,k,L),\rho)$ and $((q,k,R),\rho)$ for
$q=q_{\text{acc}}$, which are bisimilar by construction.

In the forward direction, assume that $\mathcal{M}$ accepts $w$. Then there is
a computation tree $T$ for $w$ in which every leaf is accepting. Hence
Defender can win every play of the corresponding bisimulation game by using
$T$ as a representation of a winning strategy. In particular, for any given
play there are two possibilities. If Attacker plays badly inside a defender
forcing gadget and is punished then the result is (i) above. Otherwise, as
long as Defender makes choices consistent with $T$ then every play will
eventually reach a configuration which simulates $\mathcal{M}$ in accepting
state $q_{\text{acc}}$. By construction, the corresponding game configuration
must have component configurations of shape $((q_{\text{acc}},k,L),\rho)$ and
$((q_{\text{acc}},k,R),\rho)$ and Defender wins as described in (ii).

In the backward direction, assume that Defender has a winning strategy for the
bisimulation game. Then, since this strategy must specify which transition to
choose when simulating a computation from an existential state, the strategy
can be used to build a computation tree $T$ for $\mathcal{M}$ on $w$. Since,
by construction, Attacker can always avoid being punished whilst playing in a
defender forcing gadget, it follows that $W$ must allow Defender to win any
such play by the criterion (ii). Hence, every simulation which follows $W$
ends in an accepting state and it follows that every leaf of $T$ is accepting.

##  4\. PSPACE-completeness for RAs with single assignment without erasure
(RA($S\\#_{0}$))

We next prove that the EXPTIME bound can be improved if duplicate values and
erasures are forbidden. We handle register automata first to expose the
flavour of our technique. The main result is given below, it follows from
Propositions 28 and 29.

######  Theorem 14.

$\bm{\sim}$-RA($S\\#_{0}$) is PSPACE-complete.

#### Simplified notation

Recall that, in any transition $q_{1}\xrightarrow{t,X,i,Z}q_{2}$ of an
$r$-RA($S\\#_{0}$), we have that $Z=\emptyset$, $i\not=0$ and
$X\subseteq\\{i\\}$. These restrictions allow for a simpler notation for
transitions, with $\delta\subseteq
Q\times\Sigma\times([1,r]\cup\\{i\,^{\bullet}\ |\ i\in[1,r]\,\\})\times Q$:

  1. (1)

we write each transition $q_{1}\xrightarrow{t,\\{i\\},{i},\emptyset}q_{2}$ as
$q_{1}\xrightarrow{t,i}q_{2}$;

  2. (2)

and each transition $q_{1}\xrightarrow{t,\emptyset,i,\emptyset}q_{2}$ as
$q_{1}\xrightarrow{t,i^{\bullet}}q_{2}$.

Thus, transitions of type (a) correspond to the automaton reading an input
$(t,a)$ where $a$ is the name in the $i$-th register; while in (b) transitions
the automaton reads $(t,a)$ if $a$ is _locally fresh_ , that is, it does not
appear in the registers, and in this case $a$ will be stored in register $i$.

###  4.1. Symbolic bisimulation

We attack the bisimulation problem _symbolically_ , i.e. by abstracting actual
names in the bisimulation game to the indices of the registers where these
names reside. This will lead us to consider groups of finite permutations and
inverse semigroups of partial finite permutations. We shall define symbolic
bisimulations over pairs $(q,S)$ of a state $q$ and a set of register indices
$S\subseteq[1,r]$. In this way, the locations of the empty registers
$[1,r]\setminus S$ are made explicit.

Let $\mathcal{A}=\langle Q,q_{0},\rho_{0},\delta,F\rangle$ be an
$r$-RA($S\\#_{0}$). We first set:

$\displaystyle\mathcal{U}_{0}$ $\displaystyle=\
Q\times\mathcal{P}([1,r])\times\mathcal{IS}_{r}\times
Q\times\mathcal{P}([1,r])$ $\displaystyle\mathcal{U}$ $\displaystyle=\
\\{\,(q_{1},S_{1},\sigma,q_{2},S_{2})\in\mathcal{U}_{0}\ |\ \sigma\subseteq
S_{1}\times S_{2}\,\\}$

A _symbolic simulation_ on $\mathcal{A}$ is a relation
$R\subseteq\mathcal{U}$, with elements $(q_{1},S_{1},\sigma,q_{2},S_{2})\in R$
written infix $(q_{1},S_{1})\,R_{\sigma}\,(q_{2},S_{2})$, such that all
$(q_{1},S_{1},\sigma,q_{2},S_{2})$ satisfy the following _symbolic simulation
conditions_ (SyS)333We say that _$(q_{1},S_{1},\sigma,q_{2},S_{2})$ satisfies
the (SyS) conditions in $R$_.:

  * •

for all $q_{1}\xrightarrow{t,i}q_{1}^{\prime}$,

    * –

if $i\in\mathsf{dom}(\sigma)$ then there is some
$q_{2}\xrightarrow{t,\sigma(i)}q_{2}^{\prime}$ with
$(q_{1}^{\prime},S_{1})\,R_{\sigma}\,(q_{2}^{\prime},S_{2})$,

    * –

if $i\in S_{1}\setminus\mathsf{dom}(\sigma)$ then there is some
$q_{2}\xrightarrow{t,j^{\bullet}}q_{2}^{\prime}$ with
$(q_{1}^{\prime},S_{1})\,R_{\sigma[i\mapsto j]}\,(q_{2}^{\prime},S_{2}[j])$;

  * •

for all $q_{1}\xrightarrow{t,i^{\bullet}}q_{1}^{\prime}$,

    * –

there is some $q_{2}\xrightarrow{t,j^{\bullet}}q_{2}^{\prime}$ with
$(q_{1}^{\prime},S_{1}[i])\,R_{\sigma[i\mapsto
j]}\,(q_{2}^{\prime},S_{2}[j])$,

    * –

for all $j\in S_{2}\setminus\mathsf{rng}(\sigma)$, there is some
$q_{2}\xrightarrow{t,j}q_{2}^{\prime}$ with
$(q_{1}^{\prime},S_{1}[i])\,R_{\sigma[i\mapsto j]}\,(q_{2}^{\prime},S_{2})$.

We let the inverse of $R$ be

$R^{-1}=\\{\,(q_{2},S_{2},\sigma^{-1},q_{1},S_{1})\ |\
(q_{1},S_{1},\sigma,q_{2},S_{2})\in R\,\\}$

and call $R$ a symbolic bisimulation if both $R$ and $R^{-1}$ are symbolic
simulations. We let _s-bisimilarity_ , denoted $\overset{\mathsf{s}}{\sim}$,
be the union of all symbolic bisimulations. We say that configurations
$(q_{1},\rho_{1})$ and $(q_{2},\rho_{2})$ are _s-bisimilar_ , written
$(q_{1},\rho_{1})\overset{\mathsf{s}}{\sim}(q_{2},\rho_{2})$, if
$(q_{1},\mathsf{dom}(\rho_{1}))\overset{\mathsf{s}}{\sim}_{\rho_{1};\rho_{2}^{-1}}(q_{2},\mathsf{dom}(\rho_{2}))$.

We approximate symbolic bisimilarity by a sequence of indexed bisimilarity
relations ${\overset{i}{\sim}}\subseteq\mathcal{U}$ defined inductively as
follows. First, we let $\overset{0}{\sim}$ be the whole of $\mathcal{U}$.
Then, for all $i\in\omega$,
$(q_{1},S_{1})\overset{i+1}{\sim}_{\tau}(q_{2},S_{2})$ just if
$(q_{1},S_{1},\tau,q_{2},S_{2})$ and
$(q_{2},S_{2},\tau^{-1}\\!\\!,q_{1},S_{1})$ both satisfy the (SyS)
conditions in $\overset{i}{\sim}$.

######  Lemma 15.

Let $(q_{1},\rho_{1})$, $(q_{2},\rho_{2})$ be configurations of an
$r$-RA($S\\#_{0}$), then:
$(q_{1},\rho_{1})\sim(q_{2},\rho_{2})\iff(q_{1},\rho_{1})\overset{\mathsf{s}}{\sim}(q_{2},\rho_{2})$.
Furthermore, for all $i\in\omega$,
${\overset{i+1}{\sim}}\subseteq{\overset{i}{\sim}}$ and
$(\bigcap_{i\in\omega}\overset{i}{\sim})={\overset{\mathsf{s}}{\sim}}$.

The second part of the result is the content of the following two lemmata.

######  Lemma 16.

For all $i\in\omega$, $\overset{i+1}{\sim}\subseteq\overset{i}{\sim}$

######  Proof 4.1.

The proof is by induction on $i$. When $i$ is $0$, the result is trivial as
$\overset{i}{\sim}$ is the universe. When $i=k+1$, assume
$(q_{1},S_{1})\overset{k+2}{\sim}_{\tau}(q_{2},S_{2})$. It follows by
definition that $(q_{1},S_{1},\tau,q_{2},S_{2})$ and
$(q_{2},S_{2},\tau^{-1},q_{1},S_{1})$ satisfy the (SyS) conditions in
$\overset{k+1}{\sim}$. It follows from the induction hypothesis that
$\overset{k+1}{\sim}\subseteq\overset{k}{\sim}$ since set union is monotonic.
Hence, they also satisfy the (SyS) conditions in $\overset{k}{\sim}$ whence
$(q_{1},S_{1})\overset{k+1}{\sim}_{\tau}(q_{2},S_{2})$.

######  Lemma 17.

$\bigcap_{i\in\omega}\overset{i}{\sim}\ =\ \overset{\mathsf{s}}{\sim}$

######  Proof 4.2.

We start with the $\supseteq$ direction and argue that, for all $i\in\omega$,
$\overset{\mathsf{s}}{\sim}$ is a lower bound on $\overset{i}{\sim}$. The
proof is by induction on $i$. When $i=0$ the result is trivial. When $i=k+1$,
assume $(q_{1},S_{1})\overset{\mathsf{s}}{\sim}_{\tau}(q_{2},S_{2})$. We wish
to show that it and its inverse satisfy the (SyS) conditions in
$\overset{k}{\sim}$. By definition, they satisfy the (SyS) conditions in
$\overset{\mathsf{s}}{\sim}$. Now observe that it follows from the induction
hypothesis that $\overset{\mathsf{s}}{\sim}\subseteq\overset{k}{\sim}$, so the
tuples satisfy the (SyS) conditions in $\overset{k}{\sim}$.

For the $\subseteq$ direction, we argue that the left-hand side is a symbolic
bisimulation. To see this, assume
$(q_{1},S_{1},\tau,q_{2},S_{2})\in\bigcap_{i\in\omega}\overset{i}{\sim}$ so
that $(q_{1},S_{1},\tau,q_{2},S_{2})$ and its inverse satisfy the (SyS)
conditions in $\overset{i}{\sim}$, for all $i\in\omega$. However, this is just
to say that they satisfies the (SyS) conditions in
$\bigcap_{i\in\omega}\overset{i}{\sim}$.

For the first part, we show a correspondence between bisimulations and
symbolic bisimulations from which the result follows.

######  Proof 4.3 (Proof of Lemma 15 (Part 1)).

##### bisim $\to$ s-bisim

Let $R$ be a bisimulation on $\mathcal{A}$. We claim that the relation
$R^{\prime}\subseteq\mathcal{U}$,

$\displaystyle R^{\prime}=\\{\,(q_{1},S_{1},\sigma,q_{2},S_{2})$
$\displaystyle|\ \exists\rho_{1},\rho_{2}.\ (q_{1},\rho_{1})R(q_{2},\rho_{2})$
$\displaystyle\;\;\land\sigma=\rho_{1};\rho_{2}^{-1}\land\mathsf{dom}(\rho_{i})=S_{i}\,\\}$

is a symbolic bisimulation. For the latter (by symmetry in the definition) it
suffices to show that $R^{\prime}$ is a symbolic simulation. So suppose that
$(q_{1},S_{1},\sigma,q_{2},S_{2})\in R^{\prime}$ due to some
$(q_{1},\rho_{1})R(q_{2},\rho_{2})$. Let
$q_{1}\xrightarrow{t,i}q_{1}^{\prime}$ for some $i\in S_{1}$. Then,
$(q_{1},\rho_{1})\xrightarrow{t,a}(q_{1}^{\prime},\rho_{1})$ with
$a=\rho_{1}(i)$ and, hence,
$(q_{2},\rho_{2})\xrightarrow{t,a}(q_{2}^{\prime},\rho_{2}^{\prime})$ with
$(q_{1}^{\prime},\rho_{1})R(q_{2}^{\prime},\rho_{2}^{\prime})$.

  * •

If $i\in\mathsf{dom}(\sigma)$ then $a=\rho_{2}(\sigma(i))$ and therefore the
above transition is due to some
$q_{2}\xrightarrow{t,\sigma(i)}q_{2}^{\prime}$, and
$\rho_{2}^{\prime}=\rho_{2}$. Hence,
$(q_{1}^{\prime},S_{1})R^{\prime}_{\sigma}(q_{2}^{\prime},S_{2})$.

  * •

If $i\notin\mathsf{dom}(\sigma)$ then the transition is due to some
$q_{2}\xrightarrow{t,j^{\bullet}}q_{2}^{\prime}$, and
$\rho_{2}^{\prime}=\rho_{2}[j\mapsto a]$. Hence, since $\sigma[i\mapsto
j]=\rho_{1};(\rho_{2}[j\mapsto a])^{-1}$ and
$\mathsf{dom}(\rho_{2}^{\prime})=S_{2}[j]$, we have
$(q_{1}^{\prime},S_{1})R^{\prime}_{\sigma[i\mapsto
j]}(q_{2}^{\prime},S_{2}[j])$.

Now let $q_{1}\xrightarrow{t,i^{\bullet}}q_{1}^{\prime}$. For each
$a\notin\mathsf{rng}(\rho_{1})$,
$(q_{1},\rho_{1})\xrightarrow{t,a}(q_{1}^{\prime},\rho_{1}^{\prime})$ with
$\rho_{1}^{\prime}=\rho_{1}[i\mapsto a]$ and, hence, there is some
$(q_{2},\rho_{2})\xrightarrow{t,a}(q_{2}^{\prime},\rho_{2}^{\prime})$ with
$(q_{1}^{\prime},\rho_{1}^{\prime})R(q_{2}^{\prime},\rho_{2}^{\prime})$.

  * •

Select some $a\notin\mathsf{rng}(\rho_{2})$. Then, the transition above is due
to some $q_{2}\xrightarrow{t,j^{\bullet}}q_{2}^{\prime}$, and
$\rho_{2}^{\prime}=\rho_{2}[j\mapsto a]$. Moreover, since $\sigma[i\mapsto
j]=\rho_{1}[i\mapsto a];(\rho_{2}[j\mapsto a])^{-1}$,
$\mathsf{dom}(\rho_{1}^{\prime})=S_{1}[i]$ and
$\mathsf{dom}(\rho_{2}^{\prime})=S_{2}[j]$, we have
$(q_{1}^{\prime},S_{1}[i])R^{\prime}_{\sigma[i\mapsto
j]}(q_{2}^{\prime},S_{2}[j])$.

  * •

Let $j\in S_{2}\setminus\mathsf{rng}(\sigma)$. Then, we can take $a$ to be
$\rho_{2}(j)$, so the transition is due to some
$q_{2}\xrightarrow{t,j}q_{2}^{\prime}$, and $\rho_{2}^{\prime}=\rho_{2}$. We
moreover have $(q_{1}^{\prime},S_{1}[i])R^{\prime}_{\sigma[i\mapsto
j]}(q_{2}^{\prime},S_{2})$.

##### s-bisim $\to$ bisim

Let $R$ be a symbolic bisimulation on $\mathcal{A}$. We claim that the
relation

$\displaystyle R^{\prime}=\\{\,((q_{1},\rho_{1}),(q_{2},\rho_{2}))$
$\displaystyle|\ (q_{1},S_{1})R_{\sigma}(q_{2},S_{2})$
$\displaystyle\;\,\land\sigma=\rho_{1};\rho_{2}^{-1}\land
S_{i}=\mathsf{dom}(\rho_{i})\,\\}$

is a bisimulation, for which it suffices to show that $R^{\prime}$ is a
simulation. So suppose that $((q_{1},\rho_{1}),(q_{2},\rho_{2}))\in
R^{\prime}$ due to some $(q_{1},S_{1})R_{\sigma}(q_{2},S_{2})$, and let
$(q_{1},\rho_{1})\xrightarrow{t,a}(q_{1}^{\prime},\rho_{1}^{\prime})$ for some
$(t,a)\in\Sigma\times\mathcal{D}$. If $a\in\mathsf{rng}(\rho_{1})$, say
$a=\rho_{1}(i)$, then $q_{1}\xrightarrow{t,i}q_{1}^{\prime}$ and
$\rho_{1}^{\prime}=\rho_{1}$. We distinguish two cases:

  * •

If $a\in\mathsf{rng}(\rho_{2})$ then $i\in\mathsf{dom}(\sigma)$, so
$q_{2}\xrightarrow{t,\sigma(i)}q_{2}^{\prime}$ and
$(q_{1}^{\prime},S_{1})R_{\sigma}(q_{2}^{\prime},S_{2})$. Hence,
$(q_{2},\rho_{2})\xrightarrow{t,a}(q_{2}^{\prime},\rho_{2})$ and
$(q_{1}^{\prime},\rho_{1})R^{\prime}(q_{2}^{\prime},\rho_{2})$.

  * •

If $a\notin\mathsf{rng}(\rho_{2})$ then $i\in
S_{1}\setminus\mathsf{dom}(\sigma)$, so
$q_{2}\xrightarrow{t,j^{\bullet}}q_{2}^{\prime}$ and
$(q_{1}^{\prime},S_{1})R_{\sigma[i\mapsto j]}(q_{2}^{\prime},S_{2}[j])$.
Hence, $(q_{2},\rho_{2})\xrightarrow{t,a}(q_{2}^{\prime},\rho_{2}[j\mapsto
a])$ and $(q_{1}^{\prime},\rho_{1})R^{\prime}(q_{2}^{\prime},\rho_{2}[j\mapsto
a])$.

If $a\notin\mathsf{rng}(\rho_{1})$ then there is
$q_{1}\xrightarrow{t,i^{\bullet}}q_{1}^{\prime}$ such that
$\rho_{1}^{\prime}=\rho_{1}[i\mapsto a]$.

  * •

If $a\notin\mathsf{rng}(\rho_{2})$ then, since
$q_{2}\xrightarrow{t,j^{\bullet}}q_{2}^{\prime}$ with
$(q_{1}^{\prime},S_{1}[i])R_{\sigma[i\mapsto j]}(q_{2}^{\prime},S_{2}[j])$, we
obtain $(q_{2},\rho_{2})\xrightarrow{t,a}(q_{2}^{\prime},\rho_{2}[j\mapsto
a])$ and
$(q_{1}^{\prime},\rho_{1}^{\prime})R^{\prime}(q_{2}^{\prime},\rho_{2}[j\mapsto
a])$.

  * •

If $a\in\mathsf{rng}(\rho_{2})$, say $a=\rho_{2}(j)$, then $j\in
S_{2}\setminus\mathsf{rng}(\sigma)$. Hence,
$q_{2}\xrightarrow{t,j}q_{2}^{\prime}$ with
$(q_{1}^{\prime},S_{1}[i])R_{\sigma[i\mapsto j]}(q_{2}^{\prime},S_{2})$, from
which we get $(q_{2},\rho_{2})\xrightarrow{t,a}(q_{2}^{\prime},\rho_{2})$ and
$(q_{1}^{\prime},\rho_{1}^{\prime})R^{\prime}(q_{2}^{\prime},\rho_{2})$.

Our next aim is to show that $\overset{\mathsf{s}}{\sim}$ and each
$\overset{i}{\sim}$ are closed under composition and extension of partial
permutations. The latter allows us, in Lemma 24, to bound the convergence of
the indexed bisimulations by finding within them strict chains of subgroups.
The former, in Section 6, helps us to represent $\overset{\mathsf{s}}{\sim}$
succinctly by appropriate choices of representatives.

Given $S_{1},S_{2}\subseteq[1,r]$ and
$\sigma,\sigma^{\prime}\in\mathcal{IS}_{r}$ we write
$\sigma\leq_{S_{1},S_{2}}\sigma^{\prime}$ just if
$\sigma\subseteq\sigma^{\prime}\subseteq S_{1}\times S_{2}$. Moroever, given
$X\subseteq S\subseteq[1,r]$, we write $\mathsf{id}_{X}$ for the partial map
from $S$ to $S$ that acts as identity on $X$ (and is undefined
otherwise).noteChanged the wording here as it wasn’t clear what the range of
$S$ was (it looked like it captured the (ID) rule) For any
$R\subseteq\mathcal{U}$, we define its closure $\textit{Cl}(R)$ to be the
smallest relation $R^{\prime}$ containing $R$ and closed under the following
rules.

$\displaystyle\frac{}{{(q,S,\mathsf{id}_{S},q,S)\in
R^{\prime}}}\;(\textsc{Id})\quad\frac{(q_{1},S_{1},\sigma,q_{2},S_{2})\in
R^{\prime}}{(q_{2},S_{2},\sigma^{-1},q_{1},S_{1})\in
R^{\prime}}\;(\textsc{Sym})$
$\displaystyle\frac{(q_{1},S_{1},\sigma,q_{2},S_{2})\in
R^{\prime}\qquad\sigma\leq_{S_{1},S_{2}}\sigma^{\prime}}{(q_{1},S_{1},\sigma^{\prime},q_{2},S_{2})\in
R^{\prime}}\;(\textsc{Ext})$
$\displaystyle\frac{(q_{1},S_{1},\sigma_{1},q_{2},S_{2})\in
R^{\prime}\qquad(q_{2},S_{2},\sigma_{2},q_{3},S_{3})\in
R^{\prime}}{(q_{1},S_{1},\sigma_{1};\sigma_{2},q_{3},S_{3})\in
R^{\prime}}\;(\textsc{Tr})$

We say $R$ is _closed_ in case $\textit{Cl}(R)=R$. We can show:

######  Lemma 18.

Let $P,R\subseteq\mathcal{U}$ be such that $R=R^{-1}$. If all $g\in R$ satisfy
the (SyS) conditions in $P$ then all $g\in\textit{Cl}(R)$ satisfy the (SyS)
conditions in $\textit{Cl}(P)$.

######  Proof 4.4.

We first observe that, since $R=R^{-1}$, $\textit{Cl}(R)=\textit{Cl}^{-}(R)$
where, for any relation $X$, we let $\textit{Cl}^{-}(X)$ be the smallest
relation that contains $X$ and is closed under the rules (Id), (Tr) and (Ext)
above. Let us set $R^{\prime}=\textit{Cl}^{-}(R)$ and
$P^{\prime}=\textit{Cl}(P)$. We show that all elements in $R^{\prime}$ satisfy
the (SyS) conditions in $P^{\prime}$, by rule induction on $R^{\prime}$.
For the base, either the element is in $R$ or is an identity. In both cases
the result is clear. For the inductive step, consider the rule:

$\frac{(q_{1},S_{1},\sigma_{1},q_{2},S_{2})\in
R^{\prime}\qquad(q_{2},S_{2},\sigma_{2},q_{3},S_{3})\in
R^{\prime}}{(q_{1},S_{1},\sigma_{1};\sigma_{2},q_{3},S_{3})\in
R^{\prime}}\;(\textsc{Tr})$

and assume that the premises satisfy the (SyS) conditions in $P^{\prime}$. Let
us write $\sigma$ for $\sigma_{1};\sigma_{2}$. Suppose
$q_{1}\xrightarrow{t,i}q_{1}^{\prime}$.

  * •

If $i\in\mathsf{dom}(\sigma_{1})$ and
$j=\sigma_{1}(i)\in\mathsf{dom}(\sigma_{2})$ then
$q_{2}\xrightarrow{t,j}q_{2}^{\prime}$ with
$(q_{1}^{\prime},S_{1})\,P_{\sigma_{1}}^{{}^{\prime}}\,(q_{2}^{\prime},S_{2})$,
and $q_{3}\xrightarrow{t,k}q_{3}^{\prime}$ with
$(q_{2}^{\prime},S_{2})\,P_{\sigma_{2}}^{{}^{\prime}}\,(q_{3}^{\prime},S_{3})$
and $k=\sigma^{\prime}(i)=\sigma_{2}(j)$. By (Tr) we obtain
$(q_{1}^{\prime},S_{1})\,P_{\sigma}^{{}^{\prime}}\,(q_{3}^{\prime},S_{3})$.

  * •

If $i\in\mathsf{dom}(\sigma_{1})$ and
$j=\sigma_{1}(i)\notin\mathsf{dom}(\sigma_{2})$ then
$q_{2}\xrightarrow{t,j}q_{2}^{\prime}$ with
$(q_{1}^{\prime},S_{1})\,P_{\sigma_{1}}^{{}^{\prime}}\,(q_{2}^{\prime},S_{2})$,
and $q_{3}\xrightarrow{t,k^{\bullet}}q_{3}^{\prime}$ with
$(q_{2}^{\prime},S_{2})\,P_{\sigma_{2}[j\mapsto
k]}^{{}^{\prime}}\,(q_{3}^{\prime},S_{3}[k])$ for some $k$. By (Tr) we obtain
$(q_{1}^{\prime},S_{1})\,P_{\sigma[i\mapsto
k]}^{{}^{\prime}}\,(q_{3}^{\prime},S_{3}[k])$.

  * •

If $i\notin\mathsf{dom}(\sigma_{1})$ then
$q_{2}\xrightarrow{t,j^{\bullet}}q_{2}^{\prime}$ with
$(q_{1}^{\prime},S_{1})\,P_{\sigma_{1}[i\mapsto
j]}^{{}^{\prime}}\,(q_{2}^{\prime},S_{2}[j])$, for some $j$, so
$q_{3}\xrightarrow{t,k^{\bullet}}q_{3}^{\prime}$ with
$(q_{2}^{\prime},S_{2}[j])\,P_{\sigma_{2}[j\mapsto
k]}^{{}^{\prime}}\,(q_{3}^{\prime},S_{3}[k])$ for some $k$. By (Tr,Ext), using
$\sigma_{1}[i\mapsto j];\sigma_{2}[j\mapsto
k]\leq_{S_{1},S_{3}[k]}\sigma[i\mapsto k]$, we get
$(q_{1}^{\prime},S_{1})\,P_{\sigma[i\mapsto
k]}^{{}^{\prime}}\,(q_{3}^{\prime},S_{3}[k])$.

Now suppose $q_{1}\xrightarrow{t,i^{\bullet}}q_{1}^{\prime}$.

  * •

Then, $q_{2}\xrightarrow{t,j^{\bullet}}q_{2}^{\prime}$ with
$(q_{1}^{\prime},S_{1}[i])\,P_{\sigma_{1}[i\mapsto
j]}^{{}^{\prime}}\,(q_{2}^{\prime},S_{2}[j])$, for some $j$, so
$q_{3}\xrightarrow{t,k^{\bullet}}q_{3}^{\prime}$ with

$(q_{2}^{\prime},S_{2}[j])\,P_{\sigma_{2}[j\mapsto
k]}^{{}^{\prime}}\,(q_{3}^{\prime},S_{3}[k])$

for some $k$. By (Tr,Ext), $(q_{1}^{\prime},S_{1}[i])\,P_{\sigma[i\mapsto
k]}^{{}^{\prime}}\,(q_{3}^{\prime},S_{3}[k])$.

  * •

If $k\in\mathsf{rng}(\sigma_{2})$ and
$j=\sigma_{2}^{-1}(k)\notin\mathsf{rng}(\sigma_{1})$ then
$q_{2}\xrightarrow{t,j}q_{2}^{\prime}$ with
$(q_{1}^{\prime},S_{1}[i])\,P_{\sigma_{1}[i\mapsto
j]}^{{}^{\prime}}\,(q_{2}^{\prime},S_{2})$, and
$q_{3}\xrightarrow{t,k}q_{3}^{\prime}$ with
$(q_{2}^{\prime},S_{2})\,P_{\sigma_{2}}^{{}^{\prime}}\,(q_{3}^{\prime},S_{3})$.
By (Tr) obtain $(q_{1}^{\prime},S_{1}[i])\,P_{\sigma[i\mapsto
k]}^{{}^{\prime}}\,(q_{3}^{\prime},S_{3})$.

  * •

If $k\in S_{3}\setminus\mathsf{rng}(\sigma_{2})$ then
$q_{2}\xrightarrow{t,j^{\bullet}}q_{2}^{\prime}$ with
$(q_{1}^{\prime},S_{1}[i])\,P_{\sigma_{1}[i\mapsto
j]}^{{}^{\prime}}\,(q_{2}^{\prime},S_{2}[j])$, for some $j$, and so
$q_{3}\xrightarrow{t,k}q_{3}^{\prime}$ with
$(q_{2}^{\prime},S_{2}[j])\,P_{\sigma_{2}[j\mapsto
k]}^{{}^{\prime}}\,(q_{3}^{\prime},S_{3})$. By (Tr,Ext) we obtain
$(q_{1}^{\prime},S_{1}[i])\,P_{\sigma[i\mapsto
k]}^{{}^{\prime}}\,(q_{3}^{\prime},S_{3})$.

Consider now the rule:

$\frac{(q_{1},S_{1},\sigma,q_{2},S_{2})\in
R^{\prime}\qquad\sigma\leq_{S_{1},S_{2}}\sigma^{\prime}}{(q_{1},S_{1},\sigma^{\prime},q_{2},S_{2})\in
R^{\prime}}\;(\textsc{Ext})$

and assume $(q_{1},S_{1},\sigma,q_{2},S_{2})$ satisfies the (SyS) conditions
in $P^{\prime}$. Suppose $q_{1}\xrightarrow{t,i}q_{1}^{\prime}$.

  * •

If $i\in\mathsf{dom}(\sigma)$ then
$q_{2}\xrightarrow{t,\sigma(i)}q_{2}^{\prime}$ and
$(q_{1}^{\prime},S_{1})\,P_{\sigma}^{{}^{\prime}}\,(q_{2}^{\prime},S_{2})$.
Since $\sigma\subseteq\sigma^{\prime}$, we have $\sigma(i)=\sigma^{\prime}(i)$
and
$(q_{1}^{\prime},S_{1})\,P_{\sigma^{\prime}}^{{}^{\prime}}\,(q_{2}^{\prime},S_{2})$.

  * •

If $i\notin\mathsf{dom}(\sigma^{\prime})$ then also
$i\notin\mathsf{dom}(\sigma)$ and therefore
$q_{2}\xrightarrow{t,j^{\bullet}}q_{2}^{\prime}$, for some $j$, and
$(q_{1}^{\prime},S_{1})\,P_{{\sigma[i\mapsto
j]}}^{{}^{\prime}}\,(q_{2}^{\prime},S_{2}[j])$. From
$\sigma\leq_{S_{1},S_{2}}\sigma^{\prime}$ we obtain $\sigma[i\mapsto
j]\leq_{S_{1},S_{2}[j]}\sigma^{\prime}[i\mapsto j]$, so
$(q_{1}^{\prime},S_{1})\,P_{\sigma^{\prime}[i\mapsto
j]}^{{}^{\prime}}\,(q_{2}^{\prime},S_{2}[j])$.

  * •

If $i\in\mathsf{dom}(\sigma^{\prime})\setminus\mathsf{dom}(\sigma)$ then we
reason as follows. Let $\sigma^{\prime}(i)=j\in S_{2}$.

    1. (1)

Since $i\notin\mathsf{dom}(\sigma)$, there is some
$q_{2}\xrightarrow{t,{j^{\prime}}^{\bullet}}q_{2}^{\prime\prime}$ with
$(q_{1}^{\prime},S_{1})\,P_{\sigma[i\mapsto
j^{\prime}]}^{{}^{\prime}}\,(q_{2}^{\prime\prime},S_{2}[j^{\prime}])$;

    2. (2)

hence, there is some
$q_{1}\xrightarrow{t,{i^{\prime}}^{\bullet}}q_{1}^{\prime\prime}$ with
$(q_{1}^{\prime\prime},S_{1}[i^{\prime}])\,P_{\sigma[i^{\prime}\mapsto
j^{\prime}]}^{{}^{\prime}}\,(q_{2}^{\prime\prime},S_{2}[j^{\prime}])$;

    3. (3)

then, there is some $q_{2}\xrightarrow{t,j}q_{2}^{\prime}$ with
$(q_{1}^{\prime\prime},S_{1}[i^{\prime}])\,P_{\sigma[i^{\prime}\mapsto
j]}^{{}^{\prime}}\,(q_{2}^{\prime},S_{2})$.

Taking stock (and using symmetry of $P^{\prime}$),

$\begin{split}(q_{1}^{\prime},S_{1})\,P_{\sigma[i\mapsto
j^{\prime}]}^{{}^{\prime}}\,(q_{2}^{\prime\prime},S_{2}[j^{\prime}])\,P_{\sigma^{-1}[j^{\prime}\mapsto
i^{\prime}]}^{{}^{\prime}}\,(q_{1}^{\prime\prime},S_{1}[i^{\prime}])\\\
\,P_{\sigma[i^{\prime}\mapsto
j]}^{{}^{\prime}}\,(q_{2}^{\prime},S_{2})\end{split}$

and thus, since $\sigma[i\mapsto j^{\prime}];\sigma^{-1}[j^{\prime}\mapsto
i^{\prime}];\sigma[i^{\prime}\mapsto j]\leq_{S_{1},S_{2}}\sigma[i\mapsto j]$,
we have $(q_{1}^{\prime},S_{1})\,P_{\sigma[i\mapsto
j]}^{{}^{\prime}}\,(q_{2}^{\prime},S_{2})$.

Suppose now $q_{1}\xrightarrow{t,i^{\bullet}}q_{1}^{\prime}$.

  * •

Then, $q_{2}\xrightarrow{t,j^{\bullet}}q_{2}^{\prime}$ and
$(q_{1}^{\prime},S_{1}[i])\,P_{\sigma[i\mapsto
j]}^{{}^{\prime}}\,(q_{2}^{\prime},S_{2}[j])$. Since $\sigma[i\mapsto
j]\leq_{S_{1}[i],S_{2}[j]}\sigma^{\prime}[i\mapsto j]$, we have
$(q_{1}^{\prime},S_{1}[i])\,P_{\sigma^{\prime}[i\mapsto
j]}^{{}^{\prime}}\,(q_{2}^{\prime},S_{2}[j])$.

  * •

If $j\in S_{2}\setminus\mathsf{rng}(\sigma^{\prime})$ then
$j\notin\mathsf{rng}(\sigma)$, hence $q_{2}\xrightarrow{t,j}q_{2}^{\prime}$
and $(q_{1}^{\prime},S_{1}[i])\,P_{\sigma[i\mapsto
j]}^{{}^{\prime}}\,(q_{2}^{\prime},S_{2})$. Again, we obtain
$(q_{1}^{\prime},S_{1}[i])\,P_{\sigma^{\prime}[i\mapsto
j]}^{{}^{\prime}}\,(q_{2}^{\prime},S_{2})$.

Hence, all elements of $R^{\prime}$ satisfy the (SyS) conditions in
$P^{\prime}$.

Much of the following development relies upon the fact that bisimilarity and
indexed bisimilarity have a closed structure.

######  Corollary 19.

(Closures) Bisimilarity and indexed bisimilarity for RA($S\\#_{0}$) are both
closed:

  1. (1)

$\overset{\mathsf{s}}{\sim}\;\;=\>\textit{Cl}(\overset{\mathsf{s}}{\sim})$ ;

  2. (2)

for all $i\in\omega$:
$\overset{i}{\sim}\;\;=\>\textit{Cl}(\overset{i}{\sim})$.

######  Proof 4.5.

For 1 note that
${\overset{\mathsf{s}}{\sim}}={(\overset{\mathsf{s}}{\sim})}^{-1}$ and all its
elements satisfy the (SyS) conditions in $\overset{\mathsf{s}}{\sim}$. Hence,
by Lemma 18 we have that $\textit{Cl}(\overset{\mathsf{s}}{\sim})$ is a
symbolic bisimulation, i.e.
$\textit{Cl}(\overset{\mathsf{s}}{\sim})={\overset{\mathsf{s}}{\sim}}$. The
result then follows. For 2 we proceed by induction on $i$. When $i=0$ then the
result follows from the fact that $\overset{0}{\sim}$ is the universal
relation. For the inductive case, note first that $\overset{i+1}{\sim}$ is
symmetric by construction and all $g\in{\overset{i+1}{\sim}}$ satisfy the
(SyS) conditions in $\overset{i}{\sim}$. Hence, by Lemma 18, all elements of
$\textit{Cl}(\overset{i+1}{\sim})$ satisfy the (SyS) conditions in
$\textit{Cl}(\overset{i}{\sim})$. By IH,
$\textit{Cl}(\overset{i}{\sim})={\overset{i}{\sim}}$ so
$\textit{Cl}(\overset{i+1}{\sim})\subseteq{\overset{i+1}{\sim}}$, as required.

###  4.2. Permutation groups

Next we present a series of results that uncover group-theoretic structure in
closed relations. Given $p\in Q$, $S\subseteq[1,r]$ and $R$ closed, let
$\mathcal{J}_{S}^{p}(R)=\\{X\,|\,X\subseteq
S,\,(p,S)\mathrel{{R}}_{\mathsf{id}_{X}}(p,S)\\}$.

######  Lemma 20.

$\mathcal{J}_{S}^{p}{(R)}\neq\emptyset$ and if
$X_{1},X_{2}\in\mathcal{J}_{S}^{p}{(R)}$ then $X_{1}\cap
X_{2}\in\mathcal{J}_{S}^{p}{(R)}$.

######  Proof 4.6.

$\mathcal{J}_{S}^{p}{(R)}\neq\emptyset$ follows from
$S\in\mathcal{J}_{S}^{p}{(R)}$. For the rest, we observe that
$\mathsf{id}_{X_{1}};\mathsf{id}_{X_{2}}=\mathsf{id}_{X_{1}\cap X_{2}}$ and
$R$ is closed.

It follows from the lemma above that $\mathcal{J}_{S}^{p}{(R)}$ contains the
least element with respect to inclusion, which we shall call _the
characteristic set of $(p,S)$ in $R$_ and denote by $X_{S}^{p}(R)$. By
Corollary 19, $\mathcal{J}_{S}^{p}{(R)}=\\{X\,|\,X_{S}^{p}{(R)}\subseteq
X\subseteq S\\}$.

The family $\\{X_{S}^{p}{(R)}\\}_{p\in Q}$ turns out to play an important
structural role in $R$ for the following reason.

######  Lemma 21.

Let $p\in Q$ and $\mathcal{G}_{S}^{p}{(R)}=\\{\sigma\cap(X_{S}^{p}{(R)}\times
X_{S}^{p}{(R)})\,|\,(p,S)\mathrel{{R}}_{\sigma}(p,S)\\}$. Then
$\mathcal{G}_{S}^{p}{(R)}$ is a group (under composition). In particular, it
is a subgroup of $\mathcal{S}_{X_{S}^{p}{(R)}}$.

Before tackling Lemma 21, we prove two auxiliary lemmata.

######  Lemma 22.

Suppose $(p,S)\mathrel{{R}}_{\sigma}(q,S)$. Then
$\mathsf{dom}(\sigma)\supseteq X_{S}^{p}{(R)}$ and
$\mathsf{rng}(\sigma)\supseteq X_{S}^{q}{(R)}$.

######  Proof 4.7.

Since $R$ is closed, $(p,S)\mathrel{{R}}_{\sigma;\sigma^{-1}}(p,S)$. Because
$\sigma;\sigma^{-1}=\mathsf{id}_{X}$ for some $X\subseteq S$, we have
$X\in\mathcal{J}_{Q}^{p}{(R)}$ and, thus $X\supseteq X_{S}^{p}{(R)}$. Because
$\sigma;\sigma^{-1}=\mathsf{id}_{X}$, we must have
$\mathsf{dom}(\sigma)\supseteq X$. Hence $\mathsf{dom}(\sigma)\supseteq
X_{S}^{p}{(R)}$.

A symmetric argument establishes that $\mathsf{dom}(\sigma^{-1})\supseteq
X_{S}^{q}{(R)}$. Since $\mathsf{rng}(\sigma)=\mathsf{dom}(\sigma^{-1})$, the
lemma follows.

######  Lemma 23.

Given $(p,S)\overset{\mathsf{s}}{\sim}_{\sigma}(q,S)$, consider
$\sigma^{\prime}=\sigma\cap(X_{S}^{p}{(R)}\times X_{S}^{q}{(R)})$. Then
$\mathsf{dom}(\sigma^{\prime})=X_{S}^{p}{(R)}$ and
$\mathsf{rng}(\sigma)=X_{S}^{q}{(R)}$, i.e. $\sigma^{\prime}$ is a bijection
between $X_{S}^{p}{(R)}$ and $X_{S}^{q}{(R)}$.

######  Proof 4.8.

Observe that
$\sigma^{\prime}=\mathsf{id}_{X_{S}^{p}{(R)}};\sigma;\mathsf{id}_{X_{S}^{q}{(R)}}$.
By the preceding lemma, $\mathsf{dom}(\sigma^{\prime})\supseteq
X_{S}^{p}{(R)}$ and $\mathsf{rng}(\sigma^{\prime})\supseteq X_{S}^{q}{(R)}$.
On the other hand, because of $\mathsf{id}_{X_{S}^{p}{(R)}}$ and
$\mathsf{id}_{X_{S}^{q}{(R)}}$ in the definition of $\sigma^{\prime}$, we have
$\mathsf{dom}(\sigma^{\prime})\subseteq X_{S}^{p}{(R)}$ and
$\mathsf{rng}(\sigma^{\prime})\subseteq X_{S}^{q}{(R)}$. Hence,
$\mathsf{dom}(\sigma^{\prime})=X_{S}^{p}{(R)}$ and
$\mathsf{rng}(\sigma^{\prime})=X_{S}^{q}{(R)}$. Because $\sigma^{\prime}$ is
injective (as a composite of injections), it must be a bijection between
$X_{S}^{p}{(R)}$ and $X_{S}^{q}{(R)}$.

The above Lemma shows that $({R}\restriction S)$ can be generated from
elements of the form $(p,S)\mathrel{{R}}_{\sigma}(q,S)$, where $\sigma$ is a
bijection between $X_{S}^{p}{(R)}$ and $X_{S}^{q}{(R)}$, using up-closure
under $\leq_{S,S}$. That is, $(p,S)\mathrel{{R}}_{\sigma^{\prime}}(q,S)$ iff
there exists a bijection $\sigma:X_{S}^{p}{(R)}\rightarrow X_{S}^{q}{(R)}$
such that $\sigma\leq_{S,S}\sigma^{\prime}$ and
$(p,S)\mathrel{{R}}_{\sigma}(q,S)$.

######  Proof 4.9 (Proof of Lemma 21).

First, since $(p,S)\mathrel{{R}}_{\mathsf{id}_{S}}(p,S)$, we have
$\mathsf{id}_{X_{S}^{p}}\in\mathcal{G}_{S}^{p}$. Now,
$(p,S)\mathrel{{R}}_{\sigma}(p,S)$ implies
$(p,S)\mathrel{{R}}_{\sigma^{-1}}(p,S)$. By Lemma 23,
$\sigma\cap(X_{S}^{p}{(R)}\times X_{S}^{p}{(R)})$ and
$\sigma^{-1}\cap(X_{S}^{p}{(R)}\times X_{S}^{p}{(R)})$ are bijections. Thus,
$(\sigma\cap(X_{S}^{p}{(R)}\times
X_{S}^{p}{(R)}));(\sigma^{-1}\cap(X_{S}^{p}{(R)}\times
X_{S}^{p}{(R)}))=\mathsf{id}_{X_{S}^{p}{(R)}}$.

Since indexed bisimulations are closed, they have group-theoretic structure.
We use it to help estimate their rate of convergence. Recall
$\mathcal{U}=Q\times\mathcal{P}([1,r])\times\mathcal{IS}_{r}\times
Q\times\mathcal{P}([1,r])$.

######  Lemma 24.

Let $S_{1},S_{2}\subseteq[1,r]$ and
$\mathcal{U}_{S_{1},S_{2}}=Q\times\\{S_{1},S_{2}\\}\times\mathcal{IS}_{r}\times
Q\times\\{S_{1},S_{2}\\}$. Then the sub-chain
$\\{\overset{i}{\sim}\,|\,(\overset{i+1}{\sim}\cap\
\mathcal{U}_{S_{1},S_{2}})\subsetneq(\overset{i}{\sim}\cap\
\mathcal{U}_{S_{1},S_{2}})\\}$ has size $O(|Q|^{2}+r^{2}|Q|)$.

We are going to show that changes in $\overset{j}{\sim}\cap\
{\mathcal{U}_{S_{1},S_{2}}}$ (as $j$ increases) can be traced back to either
shrinkage of a characteristic set $X^{p}_{S}({\overset{j}{\sim}})$
($S\in\\{S_{1},S_{2}\\}$), or shrinkage of
$\mathcal{G}_{S}^{p}({\overset{j}{\sim}})$ ($S\in\\{S_{1},S_{2}\\}$) or
disappearance of all tuples
$(q_{1},S_{1}^{\prime},\sigma,q_{2},S_{2}^{\prime})$ for some $q_{1},q_{2}\in
Q$ and $S_{1}^{\prime},S_{2}^{\prime}\in\\{S_{1},S_{2}\\}$. The number of
changes of each kind can be bounded by a polynomial. In the second case, we
shall need the following theorem of Babai which concerns subgroup chains in a
group $G$:

$G=G_{0}>G_{1}>\cdots{}>G_{m}=I$

in which $I$ is the trivial $1$-point identity group and, for all
$i\in[0,m-1]$, $G_{i+1}$ is a subgroup of $G_{i}$.

######  Theorem 25.

([Bab86]) For $n\geq 2$, the length of every subgroup chain in
$\mathcal{S}_{[1,n]}$ is at most $2n-3$.

Now we come to proof of Lemma 24.

######  Proof 4.10.

Fix $S_{1},S_{2}\subseteq[1,r]$. We argue that
$\\{\overset{i}{\sim}\,|\,(\overset{i+1}{\sim}\cap\
\mathcal{U}_{S_{1},S_{2}})\subsetneq(\overset{i}{\sim}\cap\
\mathcal{U}_{S_{1},S_{2}})\\}$ has length at most $4|Q|^{2}+4r^{2}|Q|-2r|Q|$.

Let us say that two configurations $(q_{1},S_{1}^{\prime})$ and
$(q_{1},S_{2}^{\prime})$ are _separated_ in $\overset{i}{\sim}$ just if there
is no $\sigma$ such that
$(q_{1},S_{1}^{\prime})\overset{i}{\sim}_{\sigma}(q_{2},S_{2}^{\prime})$, we
say they are _unseparated_ otherwise. We claim that if
$(\overset{i+1}{\sim}\cap\
\mathcal{U}_{S_{1},S_{2}})\subsetneq(\overset{i}{\sim}\cap\
\mathcal{U}_{S_{1},S_{2}})$ then there is some $q\in Q$ and
$S\in\\{S_{1},S_{2}\\}$ such that either:

  1. (1)

$X^{q}_{S}({\overset{i+1}{\sim}})>X^{q}_{S}({\overset{i}{\sim}})$

  2. (2)

or $\mathcal{G}^{q}_{S}({\overset{i+1}{\sim}})$ is a strict subgroup of
$\mathcal{G}^{q}_{S}({\overset{i}{\sim}})$

  3. (3)

or there are configurations $(q_{1},S_{1}^{\prime})$ and
$(q_{2},S_{2}^{\prime})$
($\\{S_{1}^{\prime},S_{2}^{\prime}\\}\subseteq\\{S_{1},S_{2}\\}$) that are
unseparated in $\overset{i}{\sim}$ and become separated in
$\overset{i+1}{\sim}$.

We argue as follows. If $(\overset{i+1}{\sim}\cap\
\mathcal{U}_{S_{1},S_{2}})\subsetneq(\overset{i}{\sim}\cap\
\mathcal{U}_{S_{1},S_{2}})$ then there is some $p,q\in Q$,
$S_{1}^{\prime},S_{2}^{\prime}\in\\{S_{1},S_{2}\\}$ and $\sigma$ such that
$(q_{1},S_{1}^{\prime})\overset{i}{\sim}_{\sigma}(q_{2},S_{2}^{\prime})$ but
not
$(q_{1},S_{1}^{\prime})\overset{i+1}{\sim}_{\sigma}(q_{2},S_{2}^{\prime})$.
Note that, in such a case it follows that also
$(q_{1},S_{1}^{\prime})\overset{i}{\sim}_{\sigma^{\prime}}(q_{2},S_{2}^{\prime})$
and
$(q_{1},S_{1}^{\prime})\not\overset{i+1}{\sim}_{\sigma^{\prime}}(q_{2},S_{2}^{\prime})$,
where
$\sigma^{\prime}=\sigma\cap(X^{q_{1}}_{S_{1}^{\prime}}({\overset{i}{\sim}})\times
X^{q_{2}}_{S_{2}^{\prime}}({\overset{i}{\sim}}))$, by composing with partial
identites. Hence, we assume wlog that
$\mathsf{dom}(\sigma)=X^{q_{1}}_{S_{1}^{\prime}}({\overset{i}{\sim}})$ and
$\mathsf{rng}(\sigma)=X^{q_{2}}_{S_{2}^{\prime}}({\overset{i}{\sim}})$. Now,
assume that, for all $q\in Q$, $S\in\\{S_{1},S_{2}\\}$,
$X^{q}_{S}({\overset{i+1}{\sim}})=X^{q}_{S}({\overset{i}{\sim}})$ and no
previously unseparated pair of configurations become separated in
$\overset{i+1}{\sim}\cap\ \mathcal{U}_{S_{1},S_{2}}$. It follows that there is
some $\tau$ such that
$(q_{1},S_{1}^{\prime})\overset{i+1}{\sim}_{\tau}(q_{2},S_{2}^{\prime})$ and
hence
$\sigma;\tau^{-1}\in\mathcal{G}^{q_{1}}_{S_{1}^{\prime}}({\overset{i}{\sim}})$
but
$\sigma;\tau^{-1}\notin\mathcal{G}^{q_{1}}_{S_{1}^{\prime}}({\overset{i+1}{\sim}})$
so that
$\mathcal{G}^{q_{1}}_{S_{1}^{\prime}}({\overset{i}{\sim}})>\mathcal{G}^{q_{1}}_{S_{1}^{\prime}}({\overset{i+1}{\sim}})$.

Since (i) may happen at most $2|Q|r$ times and (iii) may happen at most
$4|Q|^{2}$ times and, by Theorem 25, (ii) may happen at most $2r-2$ times (we
relax the bound given by the theorem slightly so as to include the case $r=1$)
for each group, of which there are $r$ possible groups per pair $(q,S)$ since
there is a subgroup chain associated with each set
$X^{q}_{S}({\overset{i}{\sim}})$. Hence, this gives an overall bound on the
length of the chain $(\overset{i}{\sim}\cap\ \mathcal{U}_{S_{1},S_{2}})_{i\in
I}$ of $4|Q|^{2}+4r^{2}|Q|-2r|Q|$.

Note that it does not quite follow from the above result that the sequence
$(\overset{i}{\sim})$ converges in polynomially many steps, because there are
exponentially many pairs $(S_{1},S_{2})$. Next we shall establish such a bound
by studying more closely the overlap in evolutions of different
$(S_{1},S_{2})$. Let us write $\gamma(S_{1},S_{2})$ for $|S_{1}|+|S_{2}|$,
i.e. $0\leq\gamma(S_{1},S_{2})\leq 2r$.

######  Lemma 26.

Let
$\mathcal{U}_{S_{1},S_{2}}^{-}=Q\times\\{S_{1}\\}\times\mathcal{IS}_{r}\times
Q\times\\{S_{2}\\}$ and let $c$ be the constant of $O(|Q|^{2}+r^{2}|Q|)$ in
Lemma 24 (2).

  1. (1)

Then, for any $(S_{1},S_{2})$, we have $\overset{j}{\sim}\cap\
\mathcal{U}_{S_{1},S_{2}}^{-}=\ \overset{\mathsf{s}}{\sim}\cap\
\mathcal{U}_{S_{1},S_{2}}^{-}$, where
$j=c(2r-\gamma(S_{1},S_{2})+1)(|Q|^{2}+r^{2}|Q|)$.

  2. (2)

Let $B=c(2r+1)(|Q|^{2}+r^{2}|Q|)$. For any $(S_{1},S_{2})$,
$\overset{B}{\sim}\cap\ \mathcal{U}_{S_{1},S_{2}}^{-}=\
\overset{\mathsf{s}}{\sim}\cap\ \mathcal{U}_{S_{1},S_{2}}^{-}$.

######  Proof 4.11.

For Part 1 we reason by induction on $(2r-\gamma(S_{1},S_{2}))$. We tackle the
inductive step first. Assume the result holds for all
$(S_{1}^{\prime},S_{2}^{\prime})$ with
$\gamma(S_{1}^{\prime},S_{2}^{\prime})>\gamma(S_{1},S_{2})$. Let
$j^{\prime}={c}(2r-(\gamma(S_{1},S_{2})+1)+1)(|Q|^{2}+r^{2}|Q|)={c}(2r-\gamma(S_{1},S_{2}))(|Q|^{2}+r^{2}|Q|)$.
Then, for all such $(S_{1}^{\prime},S_{2}^{\prime})$,
$(\overset{j^{\prime}}{\sim}\cap\
\mathcal{U}_{S_{1}^{\prime},S_{2}^{\prime}}^{-})=(\overset{\mathsf{s}}{\sim}\cap\
\mathcal{U}_{S_{1}^{\prime},S_{2}^{\prime}}^{-})$.

Observe that, for $k>j^{\prime}$, if $\overset{k}{\sim}\cap\
\mathcal{U}_{S_{1},S_{2}}^{-}=\ \overset{k+1}{\sim}\cap\
\mathcal{U}_{S_{1},S_{2}}^{-}$, then we must have $\overset{k}{\sim}\cap\
\mathcal{U}_{S_{1},S_{2}}^{-}=\ \overset{\mathsf{s}}{\sim}\cap\
\mathcal{U}_{S_{1},S_{2}}^{-}$, because the (SyS) conditions for
$(S_{1},S_{2})$ refer to either $(S_{1},S_{2})$ or
$(S_{1}^{\prime},S_{2}^{\prime})$ with
$\gamma(S_{1}^{\prime},S_{2}^{\prime})>\gamma(S_{1},S_{2})$.Consequently, if
$\overset{j^{\prime}}{\sim}\cap\ \mathcal{U}_{S_{1},S_{2}}^{-}\neq\
\overset{\mathsf{s}}{\sim}\cap\ \mathcal{U}_{S_{1},S_{2}}^{-}$, the sequence
$(\overset{k}{\sim}\cap\ \mathcal{U}_{S_{1},S_{2}}^{-})$
($k=j^{\prime},j^{\prime}+1,\cdots$) will have to change in every step before
stabilisation. Thus, the steps before stabilisation will induce a subchain of
the chain analysed in Lemma 24 (2). Hence, at most $c(|Q|^{2}+r^{2}|Q|)$ extra
steps from $(\overset{j^{\prime}}{\sim})$ will be required to arrive at
$\overset{\mathsf{s}}{\sim}\cap\ \mathcal{U}_{S_{1},S_{2}}^{-}$, which
delivers the required bound.

The base case ($\gamma(S_{1},S_{2})=2r$) can be established in a similar
fashion: in this case the (SyS) conditions can only refer to $(S_{1},S_{2})$,
thus the sequence $(\overset{k}{\sim}\cap\ \mathcal{U}_{S_{1},S_{2}}^{-})$
($k\geq 0$) will be strictly decreasing before stabilisation and the bound
from Lemma 24 (2) can be applied.

Part 2 follows from Part 1, because $c(2r+1)(|Q|^{2}+r^{2}|Q|)$ is the largest
of all the bounds.

######  Proposition 27.

For any RA($S\\#_{0}$) bisimulation problem, if there is a winning strategy
for Attacker then there is one of depth $O(r|Q|^{2}+r^{3}|Q|)$.

######  Proof 4.12.

We first observe that bisimulation strategies and their corresponding symbolic
bisimulation strategies have the same depth. Thus, it suffices to bound
symbolic strategies for Attacker. The $O(r|Q|^{2}+r^{3}|Q|)$ bound follows
from Part 2 of the preceding Lemma.

######  Proposition 28.

$\bm{\sim}$-RA($S\\#_{0}$) is solvable in PSPACE.

######  Proof 4.13.

In Remark 11 we established that bisimilarity for RA($M\\#$) can be reduced to
the finite-alphabet case at the cost of prolonging the bisimulation game by a
constant factor. Consequently, the polynomial bound from the preceding
Proposition (for RA($S\\#_{0}$)) is also valid after the reduction to the
finite-alphabet case.

Thanks to the bound, it suffices to play the corresponding bisimulation games
for polynomially many steps. The existence of a winning strategy can then be
established by an alternating Turing machine running in polynomial time. The
PSPACE bounds then follows from APTIME $=$ PSPACE.

For PSPACE-hardness, we reduce from the well-known PSPACE-complete problem of
checking validity of totally quantified boolean formulas in prenex conjunctive
normal form. Universal quantification and selection of conjuncts is performed
by Attacker. For existential quantification and disjunctions, we rely on
Defender Forcing. The choices of truth values by both players are recorded in
registers by using, for each variable $x_{i}$, registers $2i,2i+1$, both
initialised to $\\#$. If a player chooses _true_ for $x_{i}$, we fill register
$2i$ leaving $2i+1$ empty; we do the opposite otherwise. This makes it
possible to arrange for bisimilarity/non-bisimilarity (as appropriate) in the
final stage of the game, depending on whether the resulting literal is
negated.

######  Proposition 29.

$\bm{\sim}$-RA($S\\#_{0}$) is PSPACE-hard.

######  Proof 4.14.

We reduce from TQBF, i.e. the problem of deciding whether a formula $\Phi$ of
the shape $\square_{1}x_{1}\cdots\square_{h}x_{h}.\phi(x_{0},\cdots,x_{h})$
(with $\phi$ in conjunctive normal form) is true.

We shall construct a $(2h+1)$-register RA($S\\#_{0}$) and configurations
$(\kappa^{1},\kappa^{2})$ such that $\kappa^{1}\sim\kappa^{2}$ if and only if
$\Phi$ is true. For $j\in\\{1,2\\}$, we shall have
$\kappa^{j}=(\mathit{init}^{j},\tau^{j})$ with $\tau^{j}(i)=\\#$ for all $i$.
The initial transitions will simply initialize the first register, whose
content will never change and will be used in Attacker/Defender forcing
widgets so that they do not interfere with other registers.

$\textstyle{\mathit{init}^{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{(t,1)}$$\textstyle{\mathit{init}^{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{(t,1)}$$\textstyle{q^{1}_{1}}$$\textstyle{q^{2}_{1}}$

Registers $2,\cdots,2h+1$ will represent truth-value assignments. Registers
$2i,2i+1$ will be used to represent the value of $x_{i}$ ($i=1,\cdots,h$). The
values will be selected by Attacker (when $\square_{i}=\forall_{i}$) or
Defender (when $\square_{i}=\exists$) and we shall use the forcing circuits
$AF$ and $DF$ to that end. More precisely, for $i=1,\cdots,h$, we use
$AF(q^{1}_{i},q^{2}_{i},q^{1}_{iT},q^{2}_{iT},q^{1}_{iF},q^{2}_{iF})$ or
$DF(q^{1}_{i},q^{2}_{i},q^{1}_{iT},q^{2}_{iT},q^{1}_{iF},q^{2}_{iF})$ and
follow up the state choices with initializations of registers subject to the
following conditions:

  * •

register $2i$ is filled if and only if the value of $x_{i}$ is true,

  * •

register $2i+1$ is filled if and only if the value of $x_{i}$ is false.

Formally, we add the following transitions.

$\textstyle{q^{1}_{iT}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{{(2i)}^{\bullet}}$$\textstyle{q^{2}_{iT}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{(2i+1)^{\bullet}}$$\textstyle{q^{1}_{iF}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{(2i+2)^{\bullet}}$$\textstyle{q^{2}_{iF}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{(2i+1)^{\bullet}}$$\textstyle{q^{1}_{i+1}}$$\textstyle{q^{2}_{i+1}}$$\textstyle{q^{1}_{i+1}}$$\textstyle{q^{2}_{i+1}}$

The above handles quantification. To represent the formula
$\phi=\phi_{1}\wedge\cdots\wedge\phi_{k}$, we iterate the AF circuit $(k-1)$
times so that Attacker can force the play from $(q^{1}_{h+1},q^{2}_{h+1})$
into any of $(q^{1}_{(h+2)l},q^{2}_{(h+2)l})$ for $l=1,\cdots,k$.

Now assume $\phi_{l}=\phi_{l1}\vee\cdots\vee\phi_{ln_{l}}$ , where
$\phi_{lm}=X_{i}$ or $\phi_{lm}=\neg X_{i}$ ($m=1,\cdots,n_{l}$). To represent
$\phi_{l}$, we iterate the DF circuit $n_{l}-1$ times so that Defender can
force the play from $(q^{1}_{(h+2)l},q^{2}_{(h+2)l})$ into any of
$(q^{1}_{(h+3)lm},q^{2}_{(h+3)lm)}$ for $m=1,\cdots,n_{l}$.

Finally, we need to handle the formulas $\phi_{lm}$.

  * •

If $\phi_{lm}=X_{i}$ we add

$\textstyle{q^{1}_{(h+3)lm}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{2i+1}$$\textstyle{q^{2}_{(h+3)lm}}$$\textstyle{\mathit{end}}$

  * •

If $\phi_{lm}=\neg X_{i}$ we add

$\textstyle{q^{1}_{(h+3)lm}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{2i}$$\textstyle{q^{2}_{(h+3)lm}}$$\textstyle{\mathit{end}}$

Note that the outgoing transitions are added only for states subscripted with
$1$. They give Attacker a chance to win if $\phi_{lm}$ does _not_ hold after
Defender’s choices.

Overall the construction yields a winning strategy for Defender if and only if
the given formula is true.

##  5\. Language equivalence for $RA(S\\#_{0})$

The results of the previous section can be used to close an existing
complexity gap for deterministic language equivalence of register automata.
Recall that, in the non-deterministic case, language equivalence (even
universality) is undecidable [NSV04]. In the deterministic case, however, the
problem can be solved in PSPACE. Sakamoto [Sak98] conjectured that the
language inequivalence problem is not in NP. Below we refute the conjecture,
showing that, for RA($S\\#_{0}$), the complexity of deterministic language
inequivalence actually matches that of nonemptiness [SI00].

We call an $r$-RA($S\\#_{0}$) $\mathcal{A}$ _deterministic_ if, for all states
$q$ of $\mathcal{A}$:

  1. (1)

for all $(t,i)\in\Sigma\times[1,r]$ there is at most one transition of the
form $q\xrightarrow{t,i}q^{\prime}$, and

  2. (2)

for all $t\in\Sigma$ there is at most one transition of the form
$q\xrightarrow{t,i^{\bullet}}q^{\prime}$.

On the other hand, an LTS is deterministic if, for all $\kappa\in\mathbb{C}$
and $\ell\in\mathcal{A}\mathit{ct}$, there is at most one transition
$\kappa\xrightarrow{\ell}\kappa^{\prime}$. Note that if $\mathcal{A}$ is
deterministic then so is its transition system
$\mathcal{S}(\mathcal{A})$.444The converse may fail due to transitions of
$\mathcal{A}$ not being fireable in $\mathcal{S}(\mathcal{A})$. Then, from
Proposition 27, one obtains the following.

######  Lemma 30.

Let $\mathcal{A}_{i}=\langle Q_{i},q_{0i},\rho_{0i},\delta_{i},F_{i}\rangle$
be a deterministic $r_{i}$-RA($S\\#_{0}$) ($i=1,2$), $r=\max(r_{1},r_{2})$ and
$N=|Q_{1}|+|Q_{2}|$. If
$\mathcal{L}(\mathcal{A}_{1})\neq\mathcal{L}(\mathcal{A}_{2})$ then there is
some
$w\in(\mathcal{L}(\mathcal{A}_{1})\cup\mathcal{L}(\mathcal{A}_{2}))\setminus(\mathcal{L}(\mathcal{A}_{1})\cap\mathcal{L}(\mathcal{A}_{2}))$
with $|w|\in O(rN^{2}+r^{3}N)$.

######  Proof 5.1.

We view $\mathcal{A}_{1},\mathcal{A}_{2}$ as $r$-RA($S\\#_{0}$)s with some
unused registers and consider the $r$-RA($S\\#_{0}$) $\mathcal{A}=\langle
Q_{1}\uplus Q_{2}\uplus\\{q_{0}\\}\uplus\\{q_{s}\\},q_{0},\\{(i,\\#)\ |\
i\in[1,r]\\},\delta_{1}\cup\delta_{2}\cup\delta_{s}\cup\delta_{s}^{\prime}\cup\delta_{F},\emptyset\rangle$,
where $q_{0}$ is a “blind” initial state, $q_{s}$ is a sink state,
$\delta_{s}=\\{q\xrightarrow{t,i}q_{s}\ |\
\delta(q)\upharpoonright(t,i)=\emptyset\\}\cup\\{q\xrightarrow{t,1^{\bullet}}q_{s}\
|\ \delta(q)\upharpoonright(t,i^{\bullet})=\emptyset\\}$ adds any missing
outgoing transitions to $\delta=\delta_{1}\cup\delta_{2}$,
$\delta^{\prime}_{s}=\\{q_{s}\xrightarrow{t,i}q_{s}\ |\ t\in\Sigma\land
i\in[1,r]\\}\cup\\{q_{s}\xrightarrow{t,1^{\bullet}}q_{s}\ |\ t\in\Sigma\\}$ is
a set of sink transitions, and $\delta_{F}=\\{q\xrightarrow{t_{F},i}q_{0}\ |\
i\in[1,r]\land q\in F_{1}\cup
F_{1}\\}\cup\\{q\xrightarrow{t_{F},1^{\bullet}}q_{0}\ |\ q\in F_{1}\cup
F_{2}\\}$ is a set of “final” transitions for some newly introduced constant
$t_{F}$.

Assume WLOG that
$\mathcal{L}(\mathcal{A}_{1})\not\subseteq\mathcal{L}(\mathcal{A}_{2})$. Then,
there is some transition path for $\mathcal{A}_{1}$ from $(q_{01},\rho_{01})$
to some $q_{1}\in F_{1}$ that, when simulated by $\mathcal{A}_{2}$ from
$(q_{02},\rho_{02})$, does not lead in $F_{2}$. For $\mathcal{A}$, this means
that $(q_{01},\rho_{01})$ and $(q_{02},\rho_{02})$ are not bisimilar: Attacker
can lead the game to a configuration pair
$((q_{1},\rho_{1}),(q_{2},\rho_{2}))$, with $q_{2}\in(Q_{2}\setminus
F_{2})\cup\\{q_{s}\\}$, where he wins by playing some $(t_{F},a)$ from
$(q_{1},\rho_{1})$. By Proposition 27, Attacker has some strategy
$\mathcal{T}$ of depth $O(rN^{2}+r^{3}N)$ for winning the same game. We
observe that, because $\mathcal{A}$ is saturated with sink transitions, the
latter can only be achieved by Attacker being able to play a final transition
with label $(t_{F},a)$ in one part of the game. Suppose the happens in the
part starting from $(q_{01},\rho_{01})$ and let $w\,(t_{F},a)$ be the string
accepted by the corresponding transition path, so
$w\in\mathcal{L}(\mathcal{A}_{1})$. By determinacy of $\mathcal{A}_{2}$,
$w\notin\mathcal{L}(\mathcal{A}_{2})$.

######  Theorem 31.

Language inequivalence for deterministic RA($S\\#_{0}$) is NP-complete.

######  Proof 5.2.

Membership in NP is achieved via Lemma 30. NP-hardness follows from NP-
completeness of language non-emptiness for deterministic RA($S\\#_{0}$)
[SI00].

##  6\. NP bound for single assignment with filled registers (RA($SF$))

In Section 4 we showed, in the setting with single assignment and no erasures
(denoted by RA($S\\#_{0}$)) the bisimilarity problem was solvable in
polynomial space. Here we show that a further improvement is possible in the
RA($SF$) case, i.e. if the registers are required to be filled from the very
start. We shall show an NP upper bound.

We start off with a series of results aiming to identify succinct (polynomial-
size) sets of generators for $\overset{\mathsf{s}}{\sim}$, which we shall call
_generating systems_. In Section 4 we already found that parts of
$\overset{\mathsf{s}}{\sim}$ exhibit group-theoretic structure. Namely, Lemma
21 shows that, for any $p\in Q$ and $S\subseteq[1,r]$,
$\mathcal{G}_{S}^{p}{(\overset{\mathsf{s}}{\sim})}=\\{\sigma\cap(X_{S}^{p}\times
X_{S}^{p})\,|\,(p,S)\overset{\mathsf{s}}{\sim}_{\sigma}(p,S)\\}$ is a group,
where $X_{S}^{p}(\overset{\mathsf{s}}{\sim})\subseteq S$ is the characteristic
set of $(p,S)$.

Note that, for RA($SF$), we only have the case $S=[1,r]$. Furthermore,
$\overset{\mathsf{s}}{\sim}$ will be the only closed relation that we shall
consider. For these reasons, we write simply $X^{p}$ for characteristic set
$X^{p}_{[1,r]}(\overset{\mathsf{s}}{\sim})$ and $\mathcal{G}^{p}$ for group
$\mathcal{G}^{p}_{[1,r]}(\overset{\mathsf{s}}{\sim})$.

The group-theoretic structure implies that ${\mathcal{G}^{p}}$ can be
generated by linearly many generators with respect to $r$.

######  Lemma 32 ([MN87]).

Every subgroup of $\mathcal{S}_{n}$ has at most
$\max(2,\lfloor{\frac{n}{2}}\rfloor)$ generators.

To handle the more general case
$(p,S)\overset{\mathsf{s}}{\sim}_{\sigma}(q,S)$ of different states, consider

${\mathcal{K}^{p,q}=\\{\sigma\cap(X^{p}\times
X^{q})\,\,|\,\,(p,[1,r])\overset{\mathsf{s}}{\sim}_{\sigma}(q,[1,r])\\}.}$

Observe that, for $\sigma_{1},\sigma_{2}\in{\mathcal{K}^{p,q}}$, we have
$\sigma_{2}=(\sigma_{2};\sigma_{1}^{-1});\sigma_{1}$, because
$\sigma_{1}^{-1};\sigma_{1}=\mathsf{id}_{{X^{q}}}$. Moreover,
$\sigma_{2};\sigma_{1}^{-1}\in{\mathcal{G}^{p}}$, so $\sigma_{2}$ has been
obtained from $\sigma_{1}$ and an element of $\mathcal{G}^{p}$. Consequently,
in presence of generators of ${\mathcal{G}^{p}}$, one member of
${\mathcal{K}^{p,q}}$ suffices to generate the whole of ${\mathcal{K}^{p,q}}$
by composition. This observation motivates the following definition of a
generating system.

A generating system ${\mathcal{G}}$ consists of:

  * •

a partitioning of $Q$ into $P_{1},\cdots,P_{k}$;

  * •

for each partition $P_{i}$, a single representative $p_{i}\in P_{i}$ and:

    * –

a characteristic set ${X^{p_{i}}}\subseteq{[1,r]}$;

    * –

a set ${G^{p_{i}}}$, of up to $\max(2,\lfloor{\frac{{r}}{2}}\rfloor)$
permutations $\sigma\in\mathcal{S}_{{X^{p_{i}}}}$;

    * –

for each $q\in P_{i}\setminus\\{p_{i}\\}$, a partial permutation
$\mathsf{ray}^{p_{i}}_{q}\in\mathcal{IS}_{{[1,r]}}$ such that
$\mathsf{dom}(\mathsf{ray}^{p_{i}}_{q})={X^{p_{i}}}$; for technical
convenience, we also add
$\mathsf{ray}^{p_{i}}_{p_{i}}=\mathsf{id}_{X^{p_{i}}}$.

We write $\mathit{rep}({\mathcal{G}})$ for the set $\\{p_{1},\cdots,p_{k}\\}$
of representatives.