1–LABEL:LastPageMay 29, 2017Oct. 26, 2018

# The Complexity of Bisimulation and Simulation on Finite Systems

Moses Ganardi  University of Siegen, Germany<EMAIL_ADDRESS>,
Stefan Göller  Laboratoire Specification et Verification (LSV), ENS de Cachan
& CNRS, France<EMAIL_ADDRESS>and  Markus Lohrey  University of
Siegen, Germany<EMAIL_ADDRESS>
###### Abstract.

In this paper the computational complexity of the (bi)simulation problem over
restricted graph classes is studied. For trees given as pointer structures or
terms the (bi)simulation problem is complete for logarithmic space or ${\sf
NC}^{1}$, respectively. This solves an open problem from Balcázar, Gabarró,
and Sántha. Furthermore, if only one of the input graphs is required to be a
tree, the bisimulation (simulation) problem is contained in ${\sf AC}^{1}$
(${\sf LogCFL}$). In contrast, it is also shown that the simulation problem is
P-complete already for graphs of bounded path-width.

###### Key words and phrases:

bisimulation, computational complexity, tree-width

##  1\. Introduction

Courcelle’s theorem states that every problem definable in monadic second-
order logic (MSO) is solvable in linear time on graphs of bounded tree-width.
In recent works by Elberfeld, Jakoby, and Tantau, techniques have been
developed to transfer this famous result to low space and circuit complexity
classes [EJT10, EJT12]. In particular, the following logspace (resp., ${\sf
NC}^{1}$) version of Courcelle’s theorem was shown (see Section 2 for the
necessary definitions): [[EJT10, EJT12]] For a fixed MSO-sentence $\psi$ and a
fixed constant $k$ one can check in logspace whether a given structure
$\mathcal{A}$ of tree-width at most $k$ satisfies $\psi$. If a tree
decomposition of $\mathcal{A}$ of width $k$ is given in term representation,
then one can check in ${\sf DLOGTIME}$-uniform ${\sf NC}^{1}$ whether
$\mathcal{A}$ satisfies $\psi$. This result is a very powerful metatheorem,
which can be applied to many computational problems. On the other hand, there
are important problems solvable in logspace on graphs of bounded tree-width
that are not covered by Theorem 1. One example is the graph isomorphism
problem. Graph isomorphism is not MSO-definable even over finite paths since
two finite paths are isomorphic if they have the same length, but one cannot
express in MSO that two finite sets have the same size. Lindell [Lin92] has
shown that isomorphism of trees is in logspace, and only very recently
Elberfeld and Schweitzer [ES16] extended this result to graphs of bounded
tree-width.

In this paper, we are concerned with the complexity of simulation and
bisimulation, which are of fundamental importance in the theory of reactive
systems, see e.g. [AI07] for more background. It is known that on finite state
systems simulation and bisimulation are both P-complete [BGS92], and hence
have no efficient parallel algorithm unless ${\sf P}={\sf NC}$. Surprisingly,
no results on the complexity of (bi)simulation on natural subclasses of finite
state systems are known (whereas there exists an extensive literature on
(bi)simulation problems for various classes of infinite state systems, like
pushdown systems or Petri nets; see e.g. [Srb04]). The authors of [BGS92] pose
this open question and suggest to consider the bisimulation problem on trees.
The above remark that tree isomorphism cannot be expressed in MSO applies to
bisimulation on trees as well (two finite paths are bisimilar if and only if
they are isomorphic). Moreover, it is not clear whether there is a natural
reduction of the bisimulation problem on trees to the logspace-solvable
isomorphism problem for trees (or even bounded tree-width graphs).

In this paper, we determine the complexity of the bisimulation problem and
simulation problem on several subclasses of finite state systems. More
precisely, we show the following results; see also Table 1.

  1. (1)

On trees the (bi)simulation problem is complete for logarithmic space (resp.,
${\sf NC}^{1}$) if the trees are given as pointer structures (resp., in term
representation).

  2. (2)

The bisimulation problem between a tree and a dag (or arbitrary graph) belongs
to ${\sf AC}^{1}$ and is ${\sf NL}$-hard.

  3. (3)

The simulation problem is P-hard (and hence P-complete) already for graphs of
bounded path-width.

  4. (4)

Simulation of a tree by a dag as well as simulation of a dag by a tree is
LogCFL-complete.

Whether the bisimulation problem on graphs of bounded tree-width is in ${\sf
NC}$ remains open.

We prove our results for the bisimulation problem for trees (statement (1)
above) by a reduction to the evaluation problem for a new class of Boolean
circuits that we call tree-shaped circuits. These are circuits that are
composed in a tree-like fashion of smaller subcircuits. The important
parameter of such a circuit is its width which is defined to be the maximal
number of different paths from the root to an input gate in one of the above
mentioned subcircuits. We emphasize that the size of the subcircuits (number
of gates) may be unbounded. The main technical contributions of this paper are
logspace- and ${\sf NC}^{1}$-evaluation algorithms (depending on the input
representation) for tree-shaped circuits of bounded width. These circuits
should not be confused with circuits of bounded tree-width, which are known to
have logspace- and ${\sf NC}^{1}$-evaluation algorithms (depending on the
representation) by the above Theorem 1. We show how to partially unfold tree-
shaped circuits of bounded width into circuits of bounded tree-width. This
unfolding is possible in ${\sf TC}^{0}$ (assuming the right representation of
the circuit). Finally, the resulting bounded tree-width circuit can be
evaluated using Theorem 1. For the above logspace result we actually prove a
stronger statement: A given tree-shaped circuit of size $N$ and width $m$ can
be evaluated in space $O(\log N\cdot\log m)$.

One should also mention the paper [GGHL12], where a logic $\mathsf{LREG}$
(which extends classical first-order logic) is introduced. It is shown that
$\mathsf{LREG}$ captures logspace on directed trees. Hence, bisimulation for
trees is expressible in $\mathsf{LREG}$. Due to the very technical definition
of $\mathsf{LREG}$ we think that it is not easier to express the bisimulation
problem in $\mathsf{LREG}$ than giving a direct logspace algorithm. Moreover
expressibility in $\mathsf{LREG}$ does not imply that bisimulation for trees
in term representation is in ${\sf NC}^{1}$.

A conference version of this paper appeared in [GGL16].

|  trees (term rep.) |  trees (pointer rep.) |  tree, graph |  bounded path-width |  general graphs
---|---|---|---|---|---
bisimulation | ${\sf NC}^{1}$-compl. | ${\sf L}$-compl. | in ${\sf AC}^{1}$, ${\sf NL}$-hard | in ${\sf P}$, ${\sf L}$-hard |
simulation |  ${\sf LogCFL}$-compl. |  ${\sf P}$-compl.
Table 1. Parallel complexity of the (bi)simulation problem on restricted
classes of finite graphs.

##  2\. Preliminaries

###  2.1. Graphs and trees

A (directed) graph $G=(V,E)$ consists of a set of nodes $V$ and a set of edges
$E(G)=E\subseteq V\times V$. If $(u,v)\in E$, we call $v$ a successor of $u$.
A path (of length $n\geq 0$ from $v_{0}$ to $v_{n}$) in $G$ is a node sequence
$v_{0},v_{1},\dots,v_{n}$ such that $(v_{i},v_{i+1})\in E$ for all $0\leq
i<n$. A graph is acyclic if there is no path of length $\geq 1$ from a node to
itself. We say that two nodes $u,v\in V$ are connected if there exists a path
from $u$ to $v$ in the underlying undirected graph
$(V,E\cup\\{(v,u)\mid(u,v)\in E\\})$. A set of nodes $U\subseteq V$ is
connected if any two nodes in $U$ are connected.

A graph $T$ is a (rooted) tree if there exists a node $r\in V(T)$, called the
root of $T$, such that for all $v\in V(T)$ there exists exactly one path from
$r$ to $v$. The size $|u|$ of a node $u$ in a tree is the size of the subtree
rooted in $u$. The depth of a node $u$, denoted by $\operatorname{depth}(u)$,
is the length of the unique path from the root to $u$. A node $u$ is an
ancestor (resp., proper ancestor) of $v$, briefly $u\preceq v$ (resp., $u\prec
v$), if there exists a path (resp., a path of length $\geq 1$) in $T$ from $u$
to $v$. Given a tree $T$ we say that a node $v$ is between nodes $u$ and $w$
if either $v\in\\{u,w\\}$, or $u$ and $w$ are connected in $T\setminus v$
(which is the subgraph of $T$ obtained by removing $v$).

A node-labelled graph $(V,E,\beta)$ is a graph $(V,E)$ together with a
labelling function $\beta\colon V\to A$ into a finite set $A$. An edge-
labelled graph $(V,E)$ consists of a set of nodes $V$ and a labelled edge
relation $E\subseteq V\times A\times V$. We also write
$u\stackrel{{\scriptstyle a}}{{\longrightarrow}}v$ instead of $(u,a,v)\in E$.
Unlabelled graphs are also regarded as labelled graphs over a singleton label
set. An edge-labelled tree is an edge-labelled graph $(V,E)$ where the sets
$E_{a}=\\{(u,v)\mid(u,a,v)\in E\\}$ are pairwise disjoint for $a\in A$ and
$(V,\bigcup_{a\in A}E_{a})$ is a rooted tree.

We denote by Graphs, Unlabelled-Graphs, Trees and Unlabelled-Trees the classes
of (unlabelled) graphs and (unlabelled) trees, respectively.

###  2.2. Circuits

A (Boolean) circuit $C=(G,\beta)$ is a node-labelled graph, where $G$ is
acyclic and $\beta\colon V(G)\to\\{x_{1},\dots,x_{n},0,1,\neg,\wedge,\vee\\}$
for some $n$. Nodes of $C$ are usually called gates. Gates labelled by $0$,
$1$ (constant gates) or by a variable $x_{i}$ (input gates) have no
successors. Gates labelled by $\wedge$ or $\vee$ have at least one successor,
and gates labelled by $\neg$ have exactly one successor. A variable-free
circuit is a circuit without input gates. In a variable-free circuit every
gate can be evaluated to either $0$ or $1$. The question of deciding whether a
given gate of a given variable-free circuit evaluates to $1$ is known as the
circuit value problem. It is one of the classical ${\sf P}$-complete problems,
see [GHR95] for more details.

###  2.3. Computational complexity

In this paper we will work with the following complexity classes:

${\sf AC}^{0}\subseteq{\sf TC}^{0}\subseteq{\sf NC}^{1}\subseteq{\sf
L}\subseteq{\sf NL}\subseteq{\sf LogCFL}\subseteq{\sf AC}^{1}\subseteq{\sf
NC}\subseteq{\sf P}.$

In the following we briefly define these classes. Of course, ${\sf P}$ denotes
deterministic polynomial time. A function $f\colon\Sigma^{*}\to\Gamma^{*}$ is
logspace-computable if it can be computed on a deterministic Turing-machine
with a read-only input tape, a write-only output tape and a working tape whose
length is bounded logarithmically in the input length; such a machine is also
called a logspace transducer. We denote by ${\sf L}$ the class of languages
which can be decided in logspace, i.e., for which the characteristic function
is logspace-computable. Throughout the paper we will use implicitly that
compositions of logspace-computable functions are logspace-computable again.
The class ${\sf NL}$ is the set of languages that can be decided by
nondeterministic Turing machine in logarithmic space. It is closed under
complement by the famous theorem of Immerman-Szelepcsényi [Imm88, Sze88].

The complexity class ${\sf NC}^{i}$ ($i\geq 0$) contains all languages
$L\subseteq\\{0,1\\}^{*}$ such that there exists a circuit family
$(C_{n})_{n\in\mathbb{N}}$ where

  1. (1)

$C_{n}$ has the input gates $\\{x_{1},\ldots,x_{n},\neg x_{1},\ldots,\neg
x_{n}\\}$, $\wedge$-gates and $\vee$-gates of fan-in two, and a distinguished
output gate,

  2. (2)

$C_{n}$ has size $n^{O(1)}$ and depth $O((\log n)^{i})$,

  3. (3)

and $C_{n}$ accepts $x\in\\{0,1\\}^{n}$ if and only if $x\in L$.

If we allow in (1) $\wedge$-gates and $\vee$-gates of unbounded fan-in, we
obtain the class ${\sf AC}^{i}$. If we allow in (1) $\wedge$-gates,
$\vee$-gates and majority-gates – all of unbounded fan-in – then we obtain the
class ${\sf TC}^{i}$. Finally, the class ${\sf SAC}^{i}$ is obtained by taking
$\wedge$-gates of fan-in two and unbounded fan-in $\vee$-gates in (1). One can
easily show that ${\sf NC}^{i}\subseteq{\sf SAC}^{i}\subseteq{\sf
AC}^{i}\subseteq{\sf TC}^{i}\subseteq{\sf NC}^{i+1}$ for all $i\geq 0$. For
the classes above (and inclusively) ${\sf SAC}^{1}$, we assume logspace
uniformity, which means that there is a logspace transducer that computes from
the unary encoding of the number $n$ the $n$-th circuit $C_{n}$. For the
classes ${\sf AC}^{0}$, ${\sf TC}^{0}$ and ${\sf NC}^{1}$ logspace uniformity
is too weak (the class ${\sf NC}^{0}$ will not be used). For these classes one
usually imposes the stronger DLOGTIME-uniformity condition on the circuit
families. For the constant depth classes ${\sf AC}^{0}$ and ${\sf TC}^{0}$,
${\sf DLOGTIME}$-uniformity means that for given binary coded gate numbers
$u,v$ of the $n$-th ciruit $C_{n}$, one can (i) compute the type of gate $u$
in time $O(\log n)$ and (ii) check in time $O(\log n)$ whether $u$ is an input
gate for $v$. Since $C_{n}$ has polynomially many gates, the gates of $C_{n}$
can be encoded by bit strings of length $O(\log n)$. Thus the time bound
$O(\log n)$ is linear in the input length $|u|+|v|$. To define ${\sf
DLOGTIME}$-uniformity for ${\sf NC}^{1}$-circuits one needs the so-called
extended connection language. We do not have to go into details (which can be
found in [BIS90, Ruz81, Vol99]), since we will not work with uniformity
explicitly. The union of all classes ${\sf NC}^{i}$ is denoted by ${\sf NC}$.

The definitions of the above circuit complexity classes can be easily extended
to functions $I\colon\\{0,1\\}^{*}\to\\{0,1\\}^{*}$. This can be done by
encoding $I$ by the language $L_{I}=\\{1^{i}0w\mid w\in\\{0,1\\}^{*},\text{
the $i$-th bit of $f(w)$ is 1}\\}$. The main complexity class used in this
paper is DLOGTIME-uniform ${\sf TC}^{0}$. It can be seen as the extension of
${\sf AC}^{0}$ by the ability of counting. Typical problems in ${\sf TC}^{0}$
are the computation of the sum, product and integer quotient of two binary
encoded integers, and the sum and product of an arbitrary number of binary
encoded integers [HAB02].

The class ${\sf LogCFL}$ contains all languages $L\subseteq\\{0,1\\}^{*}$
which are logspace-reducible to a fixed context-free language. It coincides
with logspace-uniform ${\sf SAC}^{1}$ [Ven91]. Another characterizations uses
alternating logspace Turing machines with polynomial proof trees. Recall that
an alternating Turing machine is a Turing machine where the set of states is
partitioned into existential states and universal states. A configuration
where the current state is existential (resp., universal) is called a
existential (resp., universal) configuration. A existential (resp., universal)
configuration is accepting if and only if there exists an accepting successor
configuration (resp., if all successor configurations are accepting). In our
definition of alternating machines there is no explicit accepting state and to
accept the machine has to branch to a universal configuration without
successor configurations. It is well-known that ${\sf P}$ is the class of
languages that are accepted by alternating Turing machines in logarithmic
space. To get the subclass ${\sf LogCFL}$ one has to require that there exists
a polynomial $p(n)$ such that for every accepted input word $w$ of length $n$
there exists a proof tree of size at most $p(n)$. A proof tree of an
alternating Turing machine for input $w$ is a finite tree where the nodes are
labelled with configurations such that the following conditions hold:

  * •

The root is labelled with the initial configuration for input $w$.

  * •

If a node $v$ is labelled with an existential configuration $c$, then $v$ has
exactly one child that is labelled with a successor configuration of $c$.

  * •

If a node $v$ is labelled with a universal configuration $c$, then $v$ has
exactly one child $v^{\prime}$ for each successor configuration $c^{\prime}$
of $c$, and $v^{\prime}$ is labelled with $c^{\prime}$.

Ruzzo [Ruz80] proved that ${\sf LogCFL}$ coincides with the class of languages
that can be accepted by an alternating Turing machine in logarithmic space and
such that for every accepted input there exists a polynomial size proof tree.
It was shown by Borodin et al. that ${\sf LogCFL}$ is closed under complement
[BCD+89].

For more details on space and circuit complexity we refer to [Vol99].

###  2.4. Tree representations

The complexity of tree problems often depends on how the trees are
represented. Firstly, trees can be given as pointer structures where the edge
relation is given explicitly as a list of pairs consisting of two node names,
which is the standard encoding of graphs in general. Secondly, trees can be
given in term representation (or bracket representation): The string ()
represents a tree of size 1. If a tree $T$ has a root and direct subtrees
$T_{1},\dots,T_{n}$ which have term representations $r_{1},\dots,r_{n}$, then
the string $\texttt{(}r_{1}\cdots r_{n}\texttt{)}$ is a term representation of
$T$. Notice that a tree can have multiple term representations because trees
are unordered. Thirdly, trees can be represented in ancestor representation
where we specify a list of all pairs $(u,v)$ where $u$ is an ancestor of $v$.
Elberfeld et al. showed that term and ancestor representations can be
converted into each other in ${\sf TC}^{0}$ [EJT12]. We will utilize this
result since operating on ancestor representations of trees is technically
easier than on term representations.

To represent node-labelled trees (e.g., tree decompositions), in the pointer
and ancestor representation we append a list of pairs consisting of a node
name and a node label. In the term representation node labelled trees can be
encoded by introducing for each label $a$ an opening bracket symbol
$\texttt{(}_{a}$. For instance,
$\texttt{(}_{a}\texttt{(}_{b}\texttt{)}\texttt{(}_{a}\texttt{)}\texttt{)}$
encodes a tree with an $a$-labelled root and two children which are labelled
by $b$ and $a$. If the set of node labels is not fixed (this is the case for
tree decompositions) we choose an arbitrary binary block code for the opening
brackets $\texttt{(}_{a}$. To represent an edge-labelled tree we transform it
into a node-labelled tree, e.g. by assigning the label of an edge $(u,v)$ to
its end point $v$ and labelling the root by a special symbol. Let us finally
mention that these coding details for labelled trees are only relevant for our
${\sf NC}^{1}$ lower bound in Section 3.1.5, which refers to ${\sf
AC}^{0}$-reductions. The reason is that different codings of labelled trees in
term representation can be transformed in ${\sf TC}^{0}$, but not necessarily
in ${\sf AC}^{0}$, into each other.

###  2.5. Tree-width and path-width

A tree decomposition $(T,\beta)$ of a directed graph $G$ consists of a tree
$T$ and a function $\beta\colon V(T)\to 2^{V(G)}$ which assigns to each node
of $T$ a so called bag such that

  * •

for all $v\in V(G)$ the set $\\{t\in V(T)\mid v\in\beta(t)\\}$ is non-empty
and connected, and

  * •

for all $(u,v)\in E(G)$ there exists $t\in V(T)$ such that $u,v\in\beta(t)$.

The width of $(T,\beta)$ is $\max_{t\in V(T)}|\beta(t)|-1$ and the tree-width
of a graph $G$ is the minimum width over all tree decompositions of $G$. A
tree decomposition $(T,\beta)$ is a path decomposition if $T$ is a path. The
path-width of a graph $G$ is the minimum width of all path decompositions of
$G$. Tree-width and path-width are also defined for node- and edge-labelled
graphs via their underlying unlabelled graph. More background on the notions
of tree- and path-width can be found for instance in [DF13].

###  2.6. Bisimulation and simulation

A bisimulation on an edge-labelled graph $(V,E)$ is a binary relation
$R\subseteq V\times V$ such that for all $(u,v)\in R$ the following conditions
hold:

  1. (1)

For all $u\stackrel{{\scriptstyle a}}{{\longrightarrow}}u^{\prime}$ there
exists $v\stackrel{{\scriptstyle a}}{{\longrightarrow}}v^{\prime}$ such that
$(u^{\prime},v^{\prime})\in R$.

  2. (2)

For all $v\stackrel{{\scriptstyle a}}{{\longrightarrow}}v^{\prime}$ there
exists $u\stackrel{{\scriptstyle a}}{{\longrightarrow}}u^{\prime}$ such that
$(u^{\prime},v^{\prime})\in R$.

A relation $R$ that only satisfies condition 1 for all $(u,v)\in R$ is called
a simulation. A (bi)simulation on two edge-labelled graphs is a (bi)simulation
on their disjoint union. Two nodes $u,v$ are called bisimilar if there exists
a bisimulation $R$ such that $(u,v)\in R$. We say that $u$ is simulated by $v$
if there exists a simulation $R$ such that $(u,v)\in R$.

It is easy to see that the union of all bisimulations on a graph $G$ is a
bisimulation again and an equivalence relation, called the bisimulation
equivalence $\sim_{G}$, or simply $\sim$ if $G$ is clear from the context.
Similarly, the union of all simulations on a graph is a simulation again and a
preorder, called the simulation preorder $\sqsubseteq_{G}$, or simply
$\sqsubseteq$ if $G$ is clear from the context. If $u$ belongs to a graph $G$
and $v$ belongs to a graph $H\neq G$, we write $u\sqsubseteq v$ (resp., $u\sim
v$) if $u\sqsubseteq_{G\uplus H}v$ (resp., $u\sim_{G\uplus H}v$), where
$G\uplus H$ is the disjoint union of $G$ and $H$. Note that in general $u\sim
v$ is not equivalent to $u\sqsubseteq v\sqsubseteq u$. For two graph classes
$\mathcal{C}_{1},\mathcal{C}_{2}$ we define the bisimulation problem and the
simulation problem:

$\textsc{Bisim}(\mathcal{C}_{1},\mathcal{C}_{2})$
---
Given: | Two graphs $G_{1}\in\mathcal{C}_{1}$, $G_{2}\in\mathcal{C}_{2}$ and two nodes $v_{1}\in V(G_{1})$, $v_{2}\in V(G_{2})$
Question: | Are $v_{1}$ and $v_{2}$ bisimilar?

$\textsc{Sim}(\mathcal{C}_{1},\mathcal{C}_{2})$
---
Given: | Two graphs $G_{1}\in\mathcal{C}_{1}$, $G_{2}\in\mathcal{C}_{2}$ and two nodes $v_{1}\in V(G_{1})$, $v_{2}\in V(G_{2})$
Question: | Is $v_{1}$ simulated by $v_{2}$?

Note that $\textsc{Bisim}(\mathcal{C}_{1},\mathcal{C}_{2})$ and
$\textsc{Bisim}(\mathcal{C}_{2},\mathcal{C}_{1})$ are equivalent, since
bisimulation is symmetric, but this is not the case for simulation. If
$\mathcal{C}_{1}=\mathcal{C}_{2}$ then we just write
$\textsc{Bisim}(\mathcal{C}_{1})$ or $\textsc{Sim}(\mathcal{C}_{1})$. It is
known that on a finite edge-labelled graph $G=(V,E)$ bisimulation equivalence
and simulation preorder can be computed as a fixed point as follows. First we
set $u\sim_{0}v$ for all $u,v\in V$. Inductively, we define $u\sim_{k+1}v$ if

  * •

for all $u\stackrel{{\scriptstyle a}}{{\longrightarrow}}u^{\prime}$ there
exists $v\stackrel{{\scriptstyle a}}{{\longrightarrow}}v^{\prime}$ such that
$u^{\prime}\sim_{k}v^{\prime}$, and

  * •

for all $v\stackrel{{\scriptstyle a}}{{\longrightarrow}}v^{\prime}$ there
exists $u\stackrel{{\scriptstyle a}}{{\longrightarrow}}u^{\prime}$ such that
$u^{\prime}\sim_{k}v^{\prime}$.

One easily sees that $\sim_{i}\,\supseteq\,\sim_{i+1}$ for all
$i\in\mathbb{N}$. Hence there exists $n\in\mathbb{N}$ such that
$\sim_{n}\,=\,\sim_{n+i}$ for all $i\in\mathbb{N}$ and $\sim_{n}$ coincides
with bisimulation equivalence $\sim$. Using the approximants above the
bisimulation equivalence can be decided on finite graphs in polynomial time by
a partition refinement algorithm [KS90]. The fastest known algorithm is due to
Paige and Tarjan, which runs in time $O(m\log n)$ where $m$ is the number of
edges and $n$ is the number of nodes [PT87]. The simulation problem on finite
graphs is also decidable in polynomial time by a refinement algorithm [CS01].
Similar as above, one defines preorders $\sqsubseteq_{i}$ such that
$\sqsubseteq_{n}\,=\,\sqsubseteq$ for some $n\in\mathbb{N}$. It is known that
both problems are ${\sf P}$-hard [BGS92, SJ05, Srb01], and therefore:

[[BGS92, SJ05]] Bisim(Graphs) and Sim(Graphs) are ${\sf P}$-complete. For both
problems ${\sf P}$-hardness already holds for dags.

##  3\. Complexity of bisimulation

###  3.1. Bisimulation on trees

In this section we consider the bisimulation problem on edge-labelled trees.
Here we have two versions, depending on whether the trees are given as pointer
structures or in term representation. If the trees are given in term
representation then the nodes can be specified by numbers which refer to an
opening bracket in the term. Clearly, we can restrict ourselves to the problem
of deciding whether the roots of the two input trees are bisimilar, since one
can compute subtrees rooted in a given node in the pointer (term)
representation in logspace (${\sf TC}^{0}$).

######  Theorem 1.

Bisim(Trees) is in ${\sf L}$ if the trees are given as pointer structures.

######  Theorem 2.

Bisim(Trees) is in ${\sf NC}^{1}$ if the trees are given in term
representation.

We remark that the same complexity bounds hold for the tree isomorphism
problem [Bus97, JKMT03, Lin92]. In fact, converting a tree given as a pointer
structure into term representation is $\mathsf{FL}$-complete [BM95], where
$\mathsf{FL}$ is the class of functions computable in deterministic logspace.
In that sense, with the proper abstraction of the input representation the
actual complexity of Bisim(Trees) is ${\sf NC}^{1}$.

####  3.1.1. Tree-shaped Boolean circuits

Bisimilarity between two edge-labelled trees $T_{1}$ and $T_{2}$ can be
expressed as a Boolean circuit $C_{\sim}(T_{1},T_{2})$: For all $u\in
V(T_{1}),v\in V(T_{2})$ such that
$\operatorname{depth}(u)=\operatorname{depth}(v)$ the circuit contains a gate
$x_{u,v}$, which evaluates to true if and only if $u$ is bisimilar to $v$.
Since we want to test whether the roots of $T_{1}$ and $T_{2}$ are bisimilar,
it suffices to consider the reachable gates $x_{u,v}$ where
$\operatorname{depth}(u)=\operatorname{depth}(v)$. We define

$x_{u,v}=\bigwedge_{u\stackrel{{\scriptstyle
a}}{{\longrightarrow}}u^{\prime}}\bigvee_{v\stackrel{{\scriptstyle
a}}{{\longrightarrow}}v^{\prime}}x_{u^{\prime},v^{\prime}}\wedge\bigwedge_{v\stackrel{{\scriptstyle
a}}{{\longrightarrow}}v^{\prime}}\bigvee_{u\stackrel{{\scriptstyle
a}}{{\longrightarrow}}u^{\prime}}x_{u^{\prime},v^{\prime}}.$ (1)

As usual we regard an empty conjunction (resp., disjunction) as $1$ (resp.,
0). In particular, if both $u$ and $v$ are leaves, then $x_{u,v}=1$, and if
exactly one of $u$ and $v$ is a leaf, then $x_{u,v}=0$. An example circuit is
shown in Figure 1, where $T_{1}$ and $T_{2}$ are unlabelled. Note that the
circuit is composed in a tree-shaped form from smaller circuits. These smaller
circuits correspond to the definition in (1) and have the crucial property
that there exist exactly two paths from the root (of the smaller circuit) to
an arbitrary leaf, which are highlighted in one subcircuit in Figure 1. This
is the case because each gate variable $x_{u^{\prime},v^{\prime}}$ occurs once
in the first conjunction and once in the second conjunction in (1). In fact,
we will show that circuits with such a path property can be evaluated in
logspace, and even in ${\sf NC}^{1}$ under a suitable representation.

$\wedge$$\vee$$\vee$$\vee$$\vee$$\wedge$$0$$\wedge$$0$$\vee$$\vee$$\vee$$1$$1$$\vee$$\vee$$\vee$$1$$1$

Figure 1. Two trees $T_{1},T_{2}$ and the tree-shaped circuit
$C_{\sim}(T_{1},T_{2})$ for bisimulation equivalence.

We use a more syntactic definition of such circuits: A tree-shaped circuit is
a sequence of Boolean equations $\mathcal{S}=(x_{i}=\varphi_{i})_{1\leq i\leq
n}$ where $\varphi_{1},\dots,\varphi_{n}$ are Boolean formulas over the
variables $x_{1},\dots,x_{n}$ such that the graph

$T_{\mathcal{S}}=(\\{x_{1},\dots,x_{n}\\},\\{(x_{i},x_{j})\mid x_{j}\text{
occurs in }\varphi_{i}\\})$ (2)

is a tree with root $x_{1}$. This implies that there are no cyclic definitions
in $\mathcal{S}$ and that no variable $x_{k}$ appears in two distinct formulas
$\varphi_{i}$ and $\varphi_{j}$ ($i\neq j$). The size of $\mathcal{S}$ is
defined as the sum of the sizes of all formulas $\varphi_{i}$. The width of
$\mathcal{S}$ is defined as the maximal number of occurrences of a variable
$x_{j}$ in a formula $\varphi_{i}$. An example of a tree-shaped circuit of
width two is given by the formulas (1) for bisimulation. We can view
$\mathcal{S}$ as an ordinary Boolean circuit by taking the disjoint union of
the formula trees of the $\varphi_{i}$ and then merging all $x_{i}$-labelled
leaves with the root of the formula tree of $\varphi_{i}$. For example, the
tree-shaped circuit $C_{\sim}(T_{1},T_{2})$ for bisimulation equivalence can
be regarded as a tree-shaped circuit of width 2, which can be computed in
logspace from $T_{1}$ and $T_{2}$. The main goal of this section is to show
that the circuit value problem restricted to tree-shaped circuits of bounded
width belongs to logspace.

$x_{1}$$x_{3}$$x_{2}$$x_{4}$$x_{5}$$x_{6}$$x_{7}$$x_{8}$$x_{9}$

$x_{10}$

Figure 2. A tree-shaped circuit $\mathcal{S}$ where the underlying tree
$T_{\mathcal{S}}$ is drawn in green.

Note that a variable-free Boolean circuit can be represented by a relational
structure with a binary edge relation and unary relations for the labels $0$,
$1$, $\neg$, $\wedge$, $\vee$. Moreover, there is a formula of monadic-second
order logic (MSO) expressing that a variable-free Boolean circuit evaluates to
$1$. As a consequence, by Theorem 1, we can evaluate variable-free Boolean
circuits of tree-width at most $k$ in logspace for every fixed $k$. Moreover,
the complexity can be improved to ${\sf NC}^{1}$ if we also provide for the
input circuit a bounded width tree decomposition in term representation. For
this, one stores a tree decomposition $(T,\beta)$ by an expression for the
node-labelled tree $T$, where every node $t\in V(T)$ is labelled by the bag
$\beta(t)$. Note that $\beta(t)$ is a set of gates of the circuit, and these
gates are stored by their addresses. To sum up, we have:

[[EJT10, EJT12]] For every fixed $k\in\mathbb{N}$, the circuit value problem
restricted to circuits of tree-width at most $k$ can be solved in logspace. If
in addition to the input circuit $C$ a width-$k$ tree decomposition of $C$ in
term representation is given, then the circuit value problem can be solved in
${\sf NC}^{1}$.

####  3.1.2. (Un)related restricted circuit classes

We cannot directly apply Theorem 2 to tree-shaped circuits since neither their
tree-width nor clique-width is bounded by the following lemma. Clique-width is
another graph measure defined by so called $k$-expressions, see e.g. [KLM09]
for a survey. It is easy to see that Theorem 2 can be generalized to circuits
of clique-width $k$, provided a $k$-expression for the circuit is part of the
input.

######  Lemma 3.

For $n\geq 1$, let $T_{n}$ be the tree of size $n+1$ whose root has exactly
$n$ children. The set of circuits $\\{C_{\sim}(T_{n},T_{n})\mid n\geq 1\\}$
has unbounded tree-width and unbounded clique-width.

######  Proof 3.1.

The underlying undirected graph of $C_{\sim}(T_{n},T_{n})$ contains the
complete bipartite graph $K_{n,n}$ as a (topological) minor. This can be seen
by removing the output gate and dissolving all constant gates (dissolving a
node of degree 2 means deleting it and connecting its two neighbors). Figure 3
shows an example for $n=3$. Since the tree-width of $K_{n,n}$ is $n$ and the
tree-width of every minor of a graph $G$ is bounded by the tree-width of $G$,
it follows that the tree-width of $C_{\sim}(T_{n},T_{n})$ is at least $n$.

It is known that a set of graphs which has bounded clique-width and for which
there exist only finitely many $n$ such that the bipartite graph $K_{n,n}$ is
contained as a subgraph (not only minor) also has bounded tree-width [GW00].
We claim that for each $n\geq 1$ the undirected graph of
$C_{\sim}(T_{n},T_{n})$ does not contain $K_{3,3}$ as a subgraph, which
implies that $\\{C_{\sim}(T_{n},T_{n})\mid n\geq 1\\}$ also has unbounded
clique-width (note that $C_{\sim}(T_{n},T_{n})$ contains a $K_{2,2}$, i.e., a
cycle on four nodes). Note that in $C_{\sim}(T_{n},T_{n})$ for every simple
path of four nodes, one of the four nodes has degree $2$ (these are the gates
in the middle layer of Figure 3). But this is not possible in a $K_{3,3}$.

Figure 3. The circuit $C_{\sim}(T_{3},T_{3})$ for bisimulation equivalence.
Removing the output gate on the left and dissolving the constant gates in the
middle layer shows that $K_{3,3}$ is a minor of $C_{\sim}(T_{3},T_{3})$.

Let us also compare tree-shaped circuits of constant width with a class of
circuits that is presented in [GGHL12, page 5]. For the latter, the authors
require that for every path in the circuit the product of the fan-outs (i.e.,
indegrees, since we direct circuits towards the input gates) of the gates on
the path is bounded polynomially by the circuit size. It is shown that
circuits with this property can be evaluated in logspace. Note that tree-
shaped circuits of constant width do not have this path property from
[GGHL12]. On the other hand, the circuits from [GGHL12] can have nodes with
large fan-out, which is not possible for tree-shaped circuits of constant
width. Hence, the two circuit classes are incomparable.

####  3.1.3. Evaluating tree-shaped circuits given in pointer representation

Before we show how to evaluate tree-shaped circuits of bounded width in
logspace, let us briefly recall the standard logspace algorithm which performs
a depth-first traversal of a tree $T$. It stores (i) a pointer to the current
node of $T$ using $O(\log|T|)$ bits and (ii) a single bit, indicating the
current direction of the traversal (up or down). We will call this procedure
logspace depth-first traversal. If $T$ is a formula then one can evaluate the
formula using the logspace algorithm above by additionally storing the value
of the current subformula.

Next we introduce some notions. Recall that the size of the subtree rooted in
a node $u$ is denoted by $|u|$. We say that a node $u$ is heavy if for all
siblings $v$ of $u$ we either have (i) $|u|>|v|$ or (ii) $|u|=|v|$ and $u<v$
(where $<$ denotes some fixed order on the nodes of the tree). Otherwise a
node is called light. Notice that the root is heavy and that every inner node
has exactly one heavy child. Using the logspace depth-first traversal
algorithm we can compute in logspace for each node its size and determine
whether it is heavy. Note that every path in a tree contains at most $O(\log
n)$ light nodes.

By the following result, tree-shaped circuits of bounded width can be
evaluated in logspace (take $m=O(1)$). Also note that a tree-shaped circuit of
width $m=1$ is a tree and therefore can be evaluated in logspace.

######  Theorem 4.

A given tree-shaped circuit $\mathcal{S}=(x_{i}=\varphi_{i})_{1\leq i\leq n}$
of width $m\geq 2$ can be evaluated in space $O(\log s+\log n\cdot\log m)$,
where $s=\max\\{|\varphi_{i}|\mid 1\leq i\leq n\\}$ is the maximal size of one
of the formulas $\varphi_{i}$. In particular, for every fixed
$m\in\mathbb{N}$, there is a logspace algorithm which evaluates a given tree-
shaped circuit of width at most $m$.

######  Proof 3.2.

Let $\mathcal{S}=(x_{i}=\varphi_{i})_{1\leq i\leq n}$ be a tree-shaped circuit
of width $m$ and let $s=\max\\{|\varphi_{i}|\mid 1\leq i\leq n\\}$. Recall the
definition of the tree $T_{\mathcal{S}}$ with node set
$\\{x_{1},\ldots,x_{n}\\}$ from (2).

First of all, we label every node $x_{i}$ of $T_{\mathcal{S}}$ by (i) the size
$|x_{i}|$ of the subtree rooted in $x_{i}$ and (ii) a single bit indicating
whether $x_{i}$ is a heavy node of $T_{\mathcal{S}}$. This information can be
computed in space $O(\log n)$ using a logspace depth-first traversal.

The circuit $\mathcal{S}$ is evaluated in a recursive way using a pointer to
one of the nodes $x_{1},\ldots,x_{n}$ (which needs space $O(\log n)$) and a
stack of height $O(\log n\cdot\log m)$ as follows. Initially the pointer is
set to the root $x_{1}$. Assume that $x_{k}$ is the heavy child of $x_{1}$ in
$T_{\mathcal{S}}$. Then, the pointer is moved to $x_{k}$ without writing
anything on the stack. Next, the subcircuit rooted at $x_{k}$ is evaluated
recursively. By induction, space $O(\log s+\log n\cdot\log m)$ is used for
this. Once the algorithm returns from the recursion the pointer is back on
$x_{k}$ and one can release the space. The value of $x_{k}$ is stored on the
stack, which now contains a single bit. Note that the algorithm knows (using
the labeling computed before) that $x_{k}$ is the heavy child of its parent
node $x_{1}$. This information now triggers the evaluation of the Boolean
formula $\varphi_{1}$. This is done by a logspace depth-first traversal of the
Boolean formula tree of $\varphi_{1}$. Each time, this depth-first traversal
of $\varphi_{1}$ arrives at a leaf node, the following is done:

  * •

If the leaf is labelled with the variable $x_{k}$ (the heavy child of $x_{1}$
in $T_{\mathcal{S}}$), then the value of $x_{k}$ is retrieved from the stack
and the algorithm continues the evaluation of $\varphi_{1}$.

  * •

If the leaf is a light child labelled with the variable $x_{i}\neq x_{k}$,
then let $1\leq c\leq m$ such that the leaf corresponds to the $c$-th
occurrence of $x_{i}$ in $\varphi_{1}$. The algorithm stores $c$ on the stack
(which needs space $O(\log m)$) and continues recursively with the evaluation
of the subcircuit rooted at $x_{i}$. Once it comes back from the recursion,
the pointer is back on $x_{i}$. The algorithm sees that $x_{i}$ is a light
child of $x_{1}$. Using this information and the number $c$ stored on the
stack, it continues the evaluation of $\varphi_{1}$ at the right position in
$\varphi_{1}$.

Note that in the second case, we have $|x_{i}|\leq|x_{1}|/2$. This implies
that the number of bits stored on the stack is bounded by $O(\log n\cdot\log
m)$. The total space consumption is therefore $O(\log n+\log s+\log n\cdot\log
m)=O(\log s+\log n\cdot\log m)$ (since we assume $m\geq 2$).

Note that we do not assume $m$ to be a constant in Theorem 4. In particular,
since $k$, $n$, and $m$ are all bounded by the size of the tree-shaped circuit
(which is the sum of the sizes of the formulas $\varphi_{i}$), it follows that
a tree-shaped circuit of size $N$ can be evaluated in space $O(\log^{2}N)$.
For the special case $m=O(1)$ (which is used for the bisimulation problem) we
give an alternative proof below. This proof prepares our handling of trees in
term representation in the next section (proof of Theorem 5).

######  Proof 3.3 (Alternative proof of Theorem 4 for constant width.).

Let $N$ be the size of $\mathcal{S}$ and $m\in O(1)$ its width. We will
construct from $\mathcal{S}$ in logspace an equivalent polynomially sized
circuit with constant tree-width, which can be seen as a partial tree
unfolding of the circuit corresponding to $\mathcal{S}$. By Theorem 2 the
resulting circuit can be evaluated in logspace.

As before, we view the Boolean formulas $\varphi_{i}$ as node-labelled trees.
For simplicity we assume that all $\varphi_{i}$ have at least size two, which
can be ensured by replacing $\varphi_{i}$ by $\varphi_{i}\wedge 1$, so that
$\mathcal{S}$ contains no “chain rules”. Moreover, we assume that the trees
$\varphi_{i}$ have disjoint node sets. Let $x_{i}$ be an inner node of
$T_{\mathcal{S}}$ whose heavy child is $x_{k}$. Inductively we define a
circuit $C_{i}$ as follows: We take the formula $\varphi_{i}$, viewed as a
tree, and merge all $x_{k}$-labelled leaves into a single node. Note that
$x_{j}$-labelled leaves for $j\neq k$ are not merged. Then we insert into each
leaf labelled by some variable $x_{j}$ a copy of the circuit $C_{j}$. Finally
let $C$ be $C_{1}$, which clearly evaluates to the same truth value as
$\mathcal{S}$. Figure 4 shows the circuit resulting from the circuit
$C_{\sim}(T_{1},T_{2})$ on the right in Figure 1.

Note that the number of copies of $C_{i}$ in $C$ is bounded by $m^{\ell_{i}}$
where $\ell_{i}$ is the number of light nodes on the path from $x_{1}$ to
$x_{i}$ in $T_{\mathcal{S}}$. Since $\ell_{i}\leq\log n$, $C$ has size at most
$m^{\log n}\cdot N$, which is bounded by $n^{O(1)}\cdot N$ since $m$ is a
constant.

Furthermore $C$ can be computed in logspace from $\mathcal{S}$. To make this
explicit, we introduce a naming scheme for the gates in $C$. The set
$\mathrm{Addr}(x_{i})$ (addresses for the copies of $x_{i}$) contains finite
words over the alphabet $\\{1,\dots,m\\}$ defined inductively: We set
$\mathrm{Addr}(x_{1})=\\{\varepsilon\\}$ for the root $x_{1}$. If $x_{j}$ is
the heavy child of $x_{i}$ in $T_{\mathcal{S}}$, we set
$\mathrm{Addr}(x_{j})=\mathrm{Addr}(x_{i})$. If $x_{j}$ is a light child of
$x_{i}$ in $T_{\mathcal{S}}$, we set
$\mathrm{Addr}(x_{j})=\mathrm{Addr}(x_{i})\cdot\\{1,\dots,k\\}$ where $k\leq
m$ is the number of occurrences of $x_{j}$ in $\varphi_{i}$. The sets
$\mathrm{Addr}(x_{i})$ contain words of length $O(\log n)$ over the constant
sized alphabet $\\{1,\dots,m\\}$. Moreover, given a word of length $O(\log n)$
over $\\{1,\dots,m\\}$ we can easily check in logspace whether it belongs to
$\mathrm{Addr}(x_{i})$ by traversing the path from $x_{i}$ to the root of
$T_{\mathcal{S}}$. Now we can define the circuit $C$ over the gate set

$V(C)=\bigcup_{i=1}^{n}\\{(u,a)\mid a\in\mathrm{Addr}(x_{i}),~{}u\text{ is a
non-input node of the tree $\varphi_{i}$}\\}.$

For every edge $(u,u^{\prime})$ of $\varphi_{i}$ ($1\leq i\leq n$) and
$a\in\mathrm{Addr}(x_{i})$, we add the following edges to $E(C)$:

  1. (1)

If $u^{\prime}$ is a non-input gate, add the edge $((u,a),(u^{\prime},a))$.

  2. (2)

If $u^{\prime}$ is labelled by $x_{j}$, let $v$ be the root of $\varphi_{j}$
and add the edge

    1. (a)

$((u,a),(v,a\cdot d))$ if $x_{j}$ is a light child of $x_{i}$ and $u^{\prime}$
is its $d$-th occurrence of $x_{j}$ in $\varphi_{i}$,

    2. (b)

$((u,a),(v,a))$ if $x_{j}$ is the heavy child of $x_{i}$.

The labels of the gates in $C$ are inherited from the formula trees
$\varphi_{i}$. Note that a pair $(u,a)$ from $V(C)$ can be stored in logspace.
Moreover, whether a pair belongs to $V(C)$ and whether a pair of nodes from
$V(C)$ belongs to $E(C)$ can be checked in logspace. Hence, the circuit $C$
can be constructed in logspace.

Finally we show that the tree-width of $C$ is at most $2$. Let us call an edge
in $C$ crossing if it is of type 2b in the above definition of $C$ and
$u^{\prime}$ is the $d$-th occurrence of $x_{j}$ in $\varphi_{i}$ for some
$d>1$. In Figure 4 the crossing edges are drawn as dotted lines. Notice that
for each address $a$ there is at most one crossing edge $((u,a),(v,a))\in
E(C)$. Consider the subgraph $T$ of $C$ obtained by removing all crossing
edges. The resulting subgraph $T$ is indeed a tree, on which we define a tree
decomposition $(T,\beta)$ of $C$. First let $(T,\beta^{\prime})$ be the
“canonical” tree decomposition of $T$ of width 1, i.e. $\beta^{\prime}(u,a)$
contains $(u,a)$ and its parent node in $T$ (if existent). To obtain $\beta$
from $\beta^{\prime}$ we add for each address $a$ the crossing edge
$((u,a),(v,a))$ (if existent) to all bags $\beta(x,a)$. One can verify that
$(T,\beta)$ is indeed a valid tree decomposition, which has width at most 2.

Theorem 4 applied to the tree-shaped circuit defined by (1) immediately yields
Theorem 1 for the problem $\textsc{Bisim}(\mathrm{Trees})$ when trees are
given in pointer representation.

$\wedge$$\vee$$\wedge$$\vee$$1$$1$$\vee$$\vee$$1$0$\vee$$\wedge$$\vee$$1$$1$$\vee$$\vee$$1$0$\vee$$\wedge$$\vee$$1$$1$$\vee$$\vee$$1$$\vee$00
Figure 4. The partial unfolding of the tree-shaped circuit
$C_{\sim}(T_{1},T_{2})$ from Figure 1.

####  3.1.4. Evaluating tree-shaped circuits given in term representation

In this section we will prove Theorem 2 for the problem
$\textsc{Bisim}(\mathrm{Trees})$ when trees are given in term representation.
For that we prove an ${\sf NC}^{1}$-version of Theorem 4 for the case that $m$
is constant, which uses the ${\sf NC}^{1}$-part of Theorem 2, where a tree
decomposition in term representation is part of the input. Here we require
that the tree-shaped circuit $\mathcal{S}=(x_{i}=\varphi_{i})_{1\leq i\leq n}$
must be given together with the underlying tree $T_{\mathcal{S}}$ in term
representation. We also assume that the Boolean formulas $\varphi_{i}$ are
given in term representation. Recall the ancestor representation of a tree
from Section 2 and that it can be transformed into the term representation of
a tree in ${\sf TC}^{0}$ and vice versa.

######  Theorem 5.

For every fixed $m\in\mathbb{N}$, one can evaluate in ${\sf NC}^{1}$ a given
tree-shaped circuit $\mathcal{S}=(x_{i}=\varphi_{i})_{1\leq i\leq n}$ (with
all $\varphi_{i}$ given in term representation) of width at most $m$ that is
given together with the term representation of the tree $T_{\mathcal{S}}$.

######  Proof 3.4.

Let $\mathcal{S}=(x_{i}=\varphi_{i})_{1\leq i\leq n}$ be a tree-shaped circuit
of width at most $m$, where every $\varphi_{i}$ is given in term
representation. Moreover, we assume to have the term (or ancestor)
representation of the tree $T_{\mathcal{S}}$. We will show how to compute in
${\sf TC}^{0}$ the partial unfolding $C$ of $\mathcal{S}$ and the tree
decomposition of $C$ in ancestor representation from the alternative proof of
Theorem 4 on page 3.1.3.

Let $N$ be the size of $\mathcal{S}$. For each node $x_{i}$ of
$T_{\mathcal{S}}$ we can compute in ${\sf TC}^{0}$ its depth (by counting
ancestors) and the size of the subtree below $x_{i}$ (by counting
descendants). Hence, we can also compute the heavy child of every inner node
$x_{i}$ in $T_{\mathcal{S}}$. Additionally, if $x_{i}$ has a parent node
$x_{j}$, we can compute the number $d(x_{i})\in\\{1,\dots,m\\}$ of occurrences
of $x_{i}$ in $\varphi_{j}$. We transform all formulas $\varphi_{i}$ of
$\mathcal{S}$ into ancestor representation in ${\sf TC}^{0}$ where we can
assume that the encodings of all nodes have length $O(\log N)$. Also we can
ensure that all formulas have at least size two.

Recall that every node $u$ of a formula $\varphi_{i}$ has multiple copies
$(u,a)$ in $C$ where $a\in\mathrm{Addr}(x_{i})$ is an address of length
$O(\log n)$ defined on page 3.3. Given a string $a\in\\{1,\dots,m\\}^{*}$ of
length $O(\log n)$ and a node $x_{i}$ we can verify in ${\sf TC}^{0}$ whether
$a\in\mathrm{Addr}(x_{i})$: From the ancestor representation of
$T_{\mathcal{S}}$ we can compute the sequence of all light nodes
$x_{i_{1}}\prec x_{i_{2}}\prec\dots\prec x_{i_{k}}$ in $T_{\mathcal{S}}$ on
the path from the root to $x_{i}$. This can be done by sorting all light
ancestors of $x_{i}$ by their depth in ascending order. It is known that
sorting $n$ numbers with $n$ bits each is in ${\sf TC}^{0}$ [Vol99]. Then we
have $a_{1}\cdots a_{k}\in\mathrm{Addr}(x_{i})$ if and only if $a_{j}\leq
d(x_{i_{j}})$ for all $j\in\\{1,\dots,k\\}$. Hence, we can also encode all
gates of the partial unfolding $C$ by strings of length $O(\log N)$ and can
compute $V(C)$ in ${\sf TC}^{0}$. With the previous preparation the edge
relation $E(C)$ can be computed in ${\sf AC}^{0}$ using the definition on page
3.3.

It remains to show that we can compute in ${\sf TC}^{0}$ the ancestor
representation of the width-2 tree decomposition $(T,\beta)$ of $C$ from page
3.3. We set $V(T)=V(C)$. Let $(u,a),(u^{\prime},a^{\prime})\in V(T)$ be nodes
where $u$ (resp., $u^{\prime}$) belongs to $\varphi_{i}$ (resp.,
$\varphi_{j}$). Then $(u,a)$ is an ancestor of $(u^{\prime},a^{\prime})$ in
$T$ if and only if $x_{i}\preceq x_{j}$ in $T_{\mathcal{S}}$, $a$ is a prefix
of $a^{\prime}$ and the following holds:

  1. (1)

If $x_{i}=x_{j}$, then $a=a^{\prime}$ and $u\preceq u^{\prime}$ in
$\varphi_{i}$.

  2. (2)

If $x_{i}\prec x_{j}$ in $T_{\mathcal{S}}$, let $x_{k}$ be the unique child of
$x_{i}$ which is an ancestor of $x_{j}$.

    1. (a)

If $x_{k}$ is a light node, let $d\in\\{1,\dots,m\\}$ be the number in
$a^{\prime}$ at position $|a|+1$. Then the $d$-th occurrence of $x_{k}$ in
$\varphi_{i}$ is a descendant of $u$.

    2. (b)

If $x_{k}$ is a heavy node, then the first occurrence of $x_{k}$ in
$\varphi_{i}$ is a descendant of $u$.

The last condition forbids those edges that were deleted when constructing the
tree $T$ from the partial unfolding $C$ (the dotted edges in Figure 4). The
bag-function $\beta$ can be computed straightforwardly in ${\sf TC}^{0}$ using
its definition on page 3.3. By Theorem 2 we can evaluate $C$ in ${\sf
NC}^{1}$, which concludes the proof.

Finally we can apply Theorem 5 to prove Theorem 2:

######  Proof 3.5 (Proof of Theorem 2).

First we convert the term representations of $T_{1}$ and $T_{2}$ into ancestor
representations in ${\sf TC}^{0}$. We can compute the tree-shaped circuit
$\mathcal{S}$ corresponding to the circuit $C_{\sim}(T_{1},T_{2})$ and an
ancestor representation of $T_{\mathcal{S}}$ in ${\sf TC}^{0}$. The set of
variables

$\\{x_{u,v}\mid u\in V(T_{1}),\,v\in
V(T_{2}),\,\operatorname{depth}(u)=\operatorname{depth}(v)\\}$

can be clearly computed in ${\sf TC}^{0}$ since for a given node of a tree in
ancestor representation one can compute its depth by counting ancestors. The
term representations of the formulas $\varphi_{u,v}$ in (1) can then be
computed in ${\sf AC}^{0}$. The ancestor representation of $T_{\mathcal{S}}$
is also ${\sf AC}^{0}$-computable, since $x_{u,v}$ is an ancestor of
$x_{u^{\prime},v^{\prime}}$ if and only if $u$ is an ancestor of $u^{\prime}$
and $v$ is an ancestor of $v^{\prime}$. By Theorem 5 we can evaluate
$\mathcal{S}$ in ${\sf NC}^{1}$.

####  3.1.5. Lower Bounds

In this section we prove matching lower bounds for the upper bounds from
Theorem 1 and 2.

######  Theorem 6.

Bisim(Unlabelled-Trees) is L-hard if the trees are given as pointer structures
and ${\sf NC}^{1}$-hard if they are given in term representation (both with
respect to many-one ${\sf AC}^{0}$-reductions).

Before we prove Theorem 6 let us first show the following lemma:

######  Lemma 7.

Bisim(Trees) is many-one ${\sf AC}^{0}$-reducible to Bisim(Unlabelled-Trees)
in both term and pointer representation.

######  Proof 3.6.

We only show the lemma for the term representation; the same construction also
works for the pointer representation. In [Srb01] Srba presents a reduction
from the bisimulation problem for edge-labelled graphs to the bisimulation
problem for unlabelled graphs. In fact, this construction transforms trees
into trees. We slightly modify the reduction to ensure ${\sf
AC}^{0}$-computability and assume that there are only two labels, say $a$ and
$b$ (which is the case for the trees constructed in the proof of Theorem 6).

Consider a tree $T$ with edge labels $a$ and $b$. First every labelled edge of
$T$ is subdivided into two edges. In Figure 5 (middle tree), the new node
added for an $x$-labelled edge ($x\in\\{a,b\\}$) is labelled with $x$. To
distinguish the original nodes from the new nodes, we attach to each original
node two paths of length $3$. To each new node we attach one of two small
trees depending on the label of the original edge that is represented by the
new node, see the right tree in Figure 5. Let us denote the resulting
unlabelled tree with $\mathsf{ul}(T)$. It is not hard to prove that two
labelled trees $T_{1}$ and $T_{2}$ are bisimilar if and only if
$\mathsf{ul}(T_{1})$ and $\mathsf{ul}(T_{2})$ are bisimilar. The proof is
basically given in [Srb01].

$a$$b$

$a$$b$

Figure 5. From labelled to unlabelled trees

It remains to prove that the term representation of $\mathsf{ul}(T)$ can be
computed in ${\sf AC}^{0}$ from the term representation of $T$. Consider the
term representation $t$ of $T$. Recall that we identify the opening brackets
in $t$ with the nodes of $T$. We assume that the term representation $t$
contains the following three opening bracket types: $\texttt{(}_{a}$ and
$\texttt{(}_{b}$, which represent nodes with an incoming $a$-labelled (resp.,
$b$-labelled) edge, and ( for the root. For example,
$t=\texttt{(}\texttt{(}_{a}\texttt{)}\texttt{(}_{b}\texttt{)}\texttt{)}$ is a
term representation for the left tree in Figure 5. The transformation
$T\mapsto\mathsf{ul}(T)$ can be described by two isometric homomorphisms. A
homomorphism $h\colon\Sigma^{*}\to\Gamma^{*}$ is isometric if there is an
$\ell\geq 1$ such that $|h(c)|=\ell$ for all $c\in\Sigma$. In [LM98] it is
shown that for a given isometric homomorphism $h\colon\Sigma^{*}\to\Gamma^{*}$
and a word $w\in\Sigma^{*}$ one can compute $h(w)$ in ${\sf AC}^{0}$.111If the
homomorphism is fixed, this is even possible in ${\sf NC}^{0}$. Moreover, if
the homomorphism is not isometric then the problem is ${\sf TC}^{0}$-complete
[LM98].

We will proceed in two steps. Define the isometric homomorphism
$h_{1}\colon\\{\texttt{(}_{a},\texttt{(}_{b},\texttt{)}\\}^{*}\to\\{\texttt{(}_{a},\texttt{(}_{b},\texttt{(},\texttt{)},\texttt{]}\\}^{*}$
by:

$\texttt{(}_{a}\mapsto\texttt{(}_{a}\texttt{(}\qquad\qquad\texttt{(}_{b}\mapsto\texttt{(}_{b}\texttt{(}\qquad\qquad\texttt{)}\mapsto~{}\texttt{)}\texttt{]}$

Let $u\in\\{\texttt{(}_{a},\texttt{(}_{b},\texttt{)}\\}^{*}$ be the word such
that $t=\texttt{(}u\texttt{)}$ and consider the string
$\texttt{(}h_{1}(u)\texttt{)}$. Formally, it is not a term representation
(since we have two types of closing brackets). Nevertheless, it describes the
tree obtained from $T$ by subdividing every edge and labelling each new node
with the former edge label. For example
$t=\texttt{(}\texttt{(}_{a}\texttt{)}\texttt{(}_{b}\texttt{)}\texttt{)}$ is
transformed into
$\texttt{(}h_{1}(u)\texttt{)}=\texttt{(}\texttt{(}_{a}\texttt{(}\texttt{)}\texttt{]}\texttt{(}_{b}\texttt{(}\texttt{)}\texttt{]}\texttt{)}$,
which describes the node-labelled tree in Figure 5. The second isometric
homomorphism
$h_{2}\colon\\{\texttt{(}_{a},\texttt{(}_{b},\texttt{(},\texttt{)},\texttt{]}\\}^{*}\to\\{\texttt{(},\texttt{)}\\}^{*}$
is defined by:

  * •

$\texttt{(}\mapsto\texttt{(}\texttt{(}\texttt{(}\texttt{(}\texttt{)}\texttt{)}\texttt{)}$
(an opening bracket followed by a path of length $3$)

  * •

$\texttt{)}\mapsto\texttt{(}\texttt{(}\texttt{(}\texttt{)}\texttt{)}\texttt{)}\texttt{)}$
(a path of length $3$ followed by a closing bracket)

  * •

$\texttt{]}\mapsto\texttt{(}\texttt{)}\texttt{(}\texttt{)}\texttt{(}\texttt{)}\texttt{)}$
(3 leaves followed by a closing bracket)

  * •

$\texttt{(}_{a}\mapsto\texttt{(}\texttt{(}\texttt{)}\texttt{(}\texttt{)}\texttt{(}\texttt{)}$
(an opening bracket followed by 3 leaves)

  * •

$\texttt{(}_{b}\mapsto\texttt{(}\texttt{(}\texttt{(}\texttt{)}\texttt{(}\texttt{)}\texttt{)}$
(an opening bracket followed by the tree   )

Then, the string $h_{2}(\texttt{(}h_{1}(u)\texttt{)})$ is indeed a term
representation for the desired unlabelled tree $\mathsf{ul}(T)$.

######  Proof 3.7 (Proof of Theorem 6).

By Lemma 7 it suffices to show the lower bounds for edge-labelled trees. We
reuse the proofs from [JKMT03], where it is shown that the tree isomorphism
problem is L-hard (${\sf NC}^{1}$-hard, respectively) with respect to ${\sf
AC}^{0}$-reductions if the the trees are given as pointer structures (in term
representation, respectively). Let us start with the bisimulation problem for
trees given in pointer representation. Here, Jenner et al. reduce from the
L-complete reachability problem on paths, i.e., the question whether for a
given directed path graph $G$ and two nodes $v_{i},v_{j}\in V(G)$, there is a
path from $v_{i}$ to $v_{j}$ [Ete97]. Without loss of generality, $v_{i}$ and
$v_{j}$ are distinct and have successors $v_{i+1}$ and $v_{j+1}$,
respectively.

Consider the tree with a root node which has two copies of $G$ as direct
subtrees. We refer to nodes of the two copies by $v_{1},\dots,v_{n}$ and
$v_{1}^{\prime},\dots,v_{n}^{\prime}$, respectively. Additionally we replace
the edge $(v_{i},v_{i+1})$ by the new edge $(v_{i}^{\prime},v_{i+1})$. Now let
$T_{1}$ (resp., $T_{2}$) be the tree where the edge $(v_{j},v_{j+1})$ (resp.,
$(v_{j}^{\prime},v_{j+1}^{\prime})$) is labelled by a symbol $a$ (all
unlabelled edges are assumed to be labelled with a symbol $b\neq a$). Clearly,
$T_{1}$ and $T_{2}$ can be computed in ${\sf AC}^{0}$ from $G$. There is a
path from $v_{i}$ to $v_{j}$ in $G$ if and only if $T_{1}$ and $T_{2}$ are
bisimilar. See Figure 6 for an illustration of the reduction.

$v_{i}$$v_{i}^{\prime}$$v_{j}$$v_{j}^{\prime}$$a$$v_{i}$$v_{i}^{\prime}$$v_{j}$$v_{j}^{\prime}$$a$
(a) $T_{1}$ and $T_{2}$ are bisimilar.

$v_{j}$$v_{j}^{\prime}$$v_{i}$$v_{i}^{\prime}$$a$$v_{j}$$v_{j}^{\prime}$$v_{i}$$v_{i}^{\prime}$$a$
(b) $T_{1}$ and $T_{2}$ are not bisimilar.

Figure 6. The two possible forms of $T_{1}$, $T_{2}$ depending on whether
$v_{j}$ is reachable from $v_{i}$ or not

Secondly, Jenner et al. present in [JKMT03] an ${\sf AC}^{0}$-reduction from
the ${\sf NC}^{1}$-complete evaluation problem of balanced Boolean expressions
to the isomorphism problem for trees in term representation. They use the AND-
gadget $T_{\wedge}(G_{1},G_{2},H_{1},H_{2})$ and the OR-gadget
$T_{\vee}(G_{1},G_{2},H_{1},H_{2})$ which are depicted in Figure 7. Notice
that for all trees $G_{1},G_{2},H_{1},H_{2}$ the following holds, where $\sim$
can both mean bisimilarity and isomorphism:

$a$$a$$G_{1}$$G_{2}$$a$$H_{1}$$H_{2}$

$a$$a$$H_{1}$$H_{2}$$a$$G_{1}$$G_{2}$

(a) AND-gadget $T_{\wedge}$

$a$$G_{1}$$G_{2}$$a$$H_{1}$$H_{2}$

$a$$G_{1}$$H_{2}$$a$$H_{1}$$G_{2}$

(b) OR-gadget $T_{\vee}$

Figure 7. The trees for the ${\sf NC}^{1}$ lower bound

  * •

$G_{1}\sim H_{1}$ and $G_{2}\sim H_{2}\iff
T_{\wedge}(G_{1},G_{2},H_{1},H_{2})\sim T_{\wedge}(H_{1},H_{2},G_{1},G_{2})$,
and

  * •

$G_{1}\sim H_{1}$ or $G_{2}\sim H_{2}\iff
T_{\vee}(G_{1},G_{2},H_{1},H_{2})\sim T_{\vee}(G_{1},H_{2},H_{1},G_{2})$.

Using the fact that the AND-gadget and the OR-gadget have the same tree
structure (if we ignore labels), one can show that the term representations
for the resulting trees can be computed in ${\sf AC}^{0}$ from the balanced
Boolean expression; see the arguments in [JKMT03]. This yields an ${\sf
AC}^{0}$-reduction from the evaluation problem of balanced Boolean expressions
to the bisimulation problem for trees in term representation.

###  3.2. Bisimulation between trees and general graphs

As remarked in Section 2.6, the bisimulation problem is P-complete for the
class of all finite graphs. For trees we have shown that the complexity
reduces to logspace, respectively ${\sf NC}^{1}$, depending on the
representation of the input trees. This leaves the question for the complexity
of the bisimulation problem, when one of the input graphs is a tree, and the
other graph is not restricted. In this section we show that this problem
belongs to ${\sf AC}^{1}$ and that it is ${\sf NL}$-hard, but we are not able
to prove matching bounds. Let us start with the lower bound.

######  Theorem 8.

Bisim(Unlabelled-Trees, Unlabelled-Graphs) is ${\sf NL}$-hard.

######  Proof 3.8.

We reduce from the following ${\sf NL}$-complete problem: Given a graph
$G=(V,E)$, two vertices $s,t\in V$ and a number $k\in\mathbb{N}$, does there
exist a path of length exactly $k$ from $s$ to $t$?

Let $H$ be the dag defined on $V(H)=V\times\\{1,\ldots,k+1\\}\cup\\{*\\}$ with
the edge set

$E(H)=\\{((u,i),(v,i+1))\mid(u,v)\in E,\,1\leq i\leq
k\\}\cup\\{((t,k+1),*)\\}.$

Notice that $t$ is reachable from $s$ in exactly $k$ steps if and only if the
node $(s,1)$ is not bisimilar to a path of length $k$. Clearly, $H$ and the
path graph can be constructed in logspace from $G$. The result follows, since
${\sf NL}$ is closed under complement.

In the rest of the section, we show that Bisim(Trees, Graphs) belongs to ${\sf
AC}^{1}$. Using the reduction in [Srb01] (see also the proof of Lemma 7) we
can assume that the input tree and graph are unlabelled. For a number
$d\in\mathbb{N}$ we write $u\stackrel{{\scriptstyle
d}}{{\longrightarrow}}u^{\prime}$ if there exists a path of length $d$ from
$u$ to $u^{\prime}$. Let $G=(V,E)$ be a finite unlabelled directed graph, on
which we define approximants $\approx_{k}$ of the bisimulation equivalence
$\sim_{G}$. First we set $u\approx_{0}v$ for all $u,v\in V$. Inductively, we
define $u\approx_{k+1}v$ if for all $d\in\mathbb{N}$ we have

  * •

for all $u\stackrel{{\scriptstyle d}}{{\longrightarrow}}u^{\prime}$ there
exists $v\stackrel{{\scriptstyle d}}{{\longrightarrow}}v^{\prime}$ such that
$u^{\prime}\approx_{k}v^{\prime}$, and

  * •

for all $v\stackrel{{\scriptstyle d}}{{\longrightarrow}}v^{\prime}$ there
exists $u\stackrel{{\scriptstyle d}}{{\longrightarrow}}u^{\prime}$ such that
$u^{\prime}\approx_{k}v^{\prime}$.

Notice that $\approx_{i}\,\supseteq\,\approx_{i+1}$ for all $i\in\mathbb{N}$.
Hence there exists $n\in\mathbb{N}$ such that $\approx_{n}\,=\,\approx_{n+i}$
for all $i\in\mathbb{N}$ and $\approx_{n}$ coincides with the bisimulation
equivalence $\sim$. Before considering the bisimulation problem between trees
and graphs, we show that the approximants $\approx_{k}$ converge after $O(\log
n)$ rounds on trees of size $n$. For nodes $u,v\in V$ we define

$r(u,v)=\sup\\{k\in\mathbb{N}\mid
u\approx_{k}v\\}\in\mathbb{N}\cup\\{\infty\\},$

and define $r(G)=\sup\\{r(u,v)\mid u\not\sim v\text{ for }u,v\in
V\\}\in\mathbb{N}\cup\\{-\infty\\}$. Notice that $r(G)=-\infty$ if and only if
all nodes in $G$ are bisimilar. The following proposition shows that $r(T)\leq
2\log_{2}(n)+2$ for every unlabelled tree $T$ of size $n$.

######  Proposition 9.

Let $T=(V,E)$ be an unlabelled tree of size $n$. If $u_{0},v_{0}\in V$ are not
bisimilar, then $r(u_{0},v_{0})\leq 2\log_{2}(|u_{0}|+|v_{0}|)$.

######  Proof 3.9.

We prove the lemma by induction on $k=r(u_{0},v_{0})$. The cases $k=0$ and
$k=1$ are clear since $2\log_{2}(|u_{0}|+|v_{0}|)\geq 2$. Now assume that
$k\geq 2$. Since $u_{0}\approx_{k}v_{0}$, there exist nodes
$u_{1},u_{2},v_{1},v_{2}\in V$ and numbers $d_{1},d_{2}\in\mathbb{N}$ such
that

  * •

$u_{0}\stackrel{{\scriptstyle
d_{1}}}{{\longrightarrow}}u_{1}\stackrel{{\scriptstyle
d_{2}}}{{\longrightarrow}}u_{2}$ and $v_{0}\stackrel{{\scriptstyle
d_{1}}}{{\longrightarrow}}v_{1}\stackrel{{\scriptstyle
d_{2}}}{{\longrightarrow}}v_{2}$,

  * •

$r(u_{1},v_{1})=k-1$ and $r(u_{2},v_{2})=k-2$.

Let $d=d_{1}+d_{2}$. Since $u_{0}\stackrel{{\scriptstyle
d}}{{\longrightarrow}}u_{2}$ there exists $v_{0}\stackrel{{\scriptstyle
d}}{{\longrightarrow}}v_{3}$ such that $u_{2}\approx_{k-1}v_{3}$, and since
$v_{0}\stackrel{{\scriptstyle d}}{{\longrightarrow}}v_{2}$ there exists
$u_{0}\stackrel{{\scriptstyle d}}{{\longrightarrow}}u_{3}$ such that
$u_{3}\approx_{k-1}v_{2}$. Since $u_{2}\not\approx_{k-1}v_{2}$, we get
$u_{2}\neq u_{3}$ and $v_{2}\neq v_{3}$. From $r(u_{2},v_{2})=k-2$ we get
$u_{3}\approx_{k-1}v_{2}\approx_{k-2}u_{2}\approx_{k-1}v_{3}$, which implies
$u_{3}\approx_{k-2}v_{3}$. On the other hand, $u_{3}\approx_{k-1}v_{3}$ would
imply $u_{2}\approx_{k-1}v_{2}$, which contradicts $r(u_{2},v_{2})=k-2$. We
therefore have $r(u_{3},v_{3})=k-2$. Since $u_{0}\stackrel{{\scriptstyle
d}}{{\longrightarrow}}u_{2}$, $u_{0}\stackrel{{\scriptstyle
d}}{{\longrightarrow}}u_{3}$, and $u_{2}\neq u_{3}$, the nodes $u_{2}$ and
$u_{3}$ are roots of disjoint subtrees, which implies
$|u_{0}|\geq|u_{2}|+|u_{3}|$. Analogously, we get
$|v_{0}|\geq|v_{2}|+|v_{3}|$, and hence

$|u_{0}|+|v_{0}|\geq|u_{2}|+|v_{2}|+|u_{3}|+|v_{3}|.$

Observe that either

$\frac{1}{2}(|u_{0}|+|v_{0}|)\geq|u_{2}|+|v_{2}|,$

or

$\frac{1}{2}(|u_{0}|+|v_{0}|)\geq|u_{3}|+|v_{3}|$

holds. Since the two cases are symmetric we will assume the former. The
induction hypothesis implies

$k-2\leq 2\log_{2}(|u_{2}|+|v_{2}|)\leq 2\log_{2}(|u_{0}|+|v_{0}|)-2,$

and hence $k\leq 2\log_{2}(|u_{0}|+|v_{0}|)$.

######  Lemma 10.

Let $G$ be an unlabelled dag with root $u_{0}$ and $T$ be an unlabelled tree
with root $v_{0}$ of size $n$. If $u_{0}\sim v_{0}$, then $r(G\uplus T)\leq
2\log_{2}(n)+2$.

######  Proof 3.10.

Assume that $u_{0}\sim v_{0}$. Since $u_{0}$ and $v_{0}$ are the roots of the
dag $G$ and the tree $T$, respectively, every node in $G$ is bisimilar to some
node in $T$. Furthermore $r$ is invariant under bisimulation, i.e., if $u\sim
v$ and $u^{\prime}\sim v^{\prime}$, then $r(u,u^{\prime})=r(v,v^{\prime})$.
Therefore $r(G\uplus T)=r(T)\leq 2\log_{2}(n)+2$.

Now we can show the ${\sf AC}^{1}$ upper bound for Bisim(Trees, Graphs):

######  Theorem 11.

Bisim(Trees, Graphs) is in ${\sf AC}^{1}$.

######  Proof 3.11.

Let $T$ be the input tree and $G$ be the input graph. As explained before, we
can assume that $T$ and $G$ are unlabelled. Assume we want to test whether
node $u_{0}\in V(T)$ is bisimilar to node $v_{0}\in V(G)$. First we restrict
$G$ to the subgraph reachable from $v_{0}$ using a reachability oracle in
${\sf NL}\subseteq{\sf AC}^{1}$. If $G$ is not acyclic, which can be also
tested in ${\sf NL}$, then $u_{0}$ and $v_{0}$ are not bisimilar. If $G$ is a
dag, we construct a logspace-uniform ${\sf AC}^{1}$-circuit family which
computes the approximants $\approx_{k}$ on the disjoint union $G\uplus T$ for
all $0\leq k\leq 2\log_{2}|T|+2$. A similar construction can be found in
[GV06]. To do so, we first compute for all nodes $u,u^{\prime}$ the set of
path lengths from $u$ to $u^{\prime}$. Note that one can test in ${\sf
NL}\subseteq{\sf AC}^{1}$ whether there is (no) path of a given length between
two given nodes. Using this information we can compute $\approx_{k+1}$ by an
${\sf AC}^{0}$-circuit from $\approx_{k}$.

Finally, we test whether $\approx_{k}\;=\;\approx_{k+1}$ for $k=\lceil
2\log_{2}|T|+2\rceil$. If this is not the case, then Lemma 10 implies
$u_{0}\not\sim v_{0}$ and the circuit outputs false. Otherwise,
$\approx_{k}\;=\;\sim$. Hence the circuit outputs true if
$u_{0}\approx_{k}v_{0}$, and false otherwise.

##  4\. Further applications

Before we consider simulation problems, let us present two further application
of the techniques from Section 3.

###  4.1. Equality of hereditarily finite sets

The bisimulation problem on trees in term representation arises in a very
natural way. A hereditarily finite set is either the empty set $\\{\\}$ or a
set $\\{a_{1},\dots,a_{n}\\}$ containing finitely many hereditarily finite
sets $a_{1},\dots,a_{n}$. Hereditarily finite sets have a natural string
representation over the bracket symbols $\\{$ and $\\}$. By counting brackets,
one can check in ${\sf TC}^{0}$ whether a string over $\\{$ and $\\}$ is well-
bracketed [BC89]. As before, such a well-bracketed string corresponds to a
tree. By induction over the height of trees, one can easily show that two
well-bracketed strings over $\\{$ and $\\}$ represent the same set if and only
if the corresponding trees are bisimilar. Hence, the tree bisimulation problem
for (unlabelled) trees in term representation is equivalent to the set
equality problem, which asks whether two such string representations represent
the same set. For example $\\{\\{\\}\\{\\}\\}$ and $\\{\\{\\}\\}$ represent
the same set. From Theorem 2 we obtain the ${\sf NC}^{1}$ upper bound in the
following result. The ${\sf NC}^{1}$ lower bound follows from the ${\sf
NC}^{1}$-hardness of the bisimulation problem for unlabelled trees in term
representation (Theorem 6).

######  Corollary 12.

The set equality problem is ${\sf NC}^{1}$-complete with respect to ${\sf
AC}^{0}$-reductions.

###  4.2. Model checking on tree-shaped graphs

Recall that the starting point of our paper was the algorithmic meta theorem
of Elberfeld et al. (Theorem 1) which states that a fixed MSO-property can be
model-checked in logarithmic space on a graph class $\mathcal{C}$ of bounded
tree-width. On the other hand, if $\mathcal{C}$ has unbounded tree-width, then
Theorem 1 cannot be applied directly. In this section, we argue that we can
extend Theorem 1 to some graph classes of unbounded tree-width if we restrict
to bisimulation-invariant MSO (which coincides with the modal $\mu$-calculus).

Consider an MSO-formula $\psi=\psi(x)$ with a single free element variable
$x$. We would like to know, whether for a given graph $G\in\mathcal{C}$ and a
node $v\in V(G)$, $\psi$ is satisfied in $v$; $(G,v)\models\psi$ for short. We
say that $\psi$ is bisimulation-invariant if for all graphs $G$ and all nodes
$u,v\in V(G)$ we have: if $u$ and $v$ are bisimilar and $(G,u)\models\psi$
holds, then $(G,v)\models\psi$. It is known that an MSO-formula $\psi$ is
bisimulation-invariant if and only if $\psi$ is equivalent to a formula in the
modal $\mu$-calculus [JW96]. Assume now that there exist a constant $k$ and a
logspace transducer, that maps a graph $G\in\mathcal{C}$ to a pair $(H,R)$,
where $H$ is a graph of tree-width at most $k$ and $R\subseteq V(G)\times
V(H)$ is a bisimulation $R$ such that for all $v\in V(G)$ there exists
$(v,w)\in R$. Then we can check in logspace whether $(G,v)\models\psi$ holds,
by computing a bisimilar node $w\in V(H)$ with $(v,w)\in R$ and checking
$(H,w)\models\psi$ in logspace using Theorem 1.

Our second proof of Theorem 4 uses the above strategy. Whether a certain gate
of a Boolean circuit (viewed as a node-labelled graph) evaluates to true is a
bisimulation invariant property. The partial tree unfolding constructed in the
second proof of Theorem 4 has the properties of the graph $H$ from the
previous paragraph.

The following definition presents a generalization of tree decompositions that
allows to compute a pair $(H,R)$ with $H$ of bounded tree-width and
$R\subseteq V(G)\times V(H)$ a bisimulation.

Let $G=(V,E)$ be an edge-labelled graph. A tree-shaped decomposition for $G$
is a node-labelled tree $(T,\beta)$ where $\beta\colon V(T)\to 2^{V}$
satisfies the following conditions:

  * •

For all $v\in V$ there exists $t\in V(T)$ such that $v\in\beta(t)$.

  * •

For all $u\stackrel{{\scriptstyle a}}{{\longrightarrow}}v$ there exists $t\in
V(T)$ such that $u,v\in\beta(t)$.

  * •

Let $u\stackrel{{\scriptstyle a}}{{\longrightarrow}}v$ and $t_{1}\in V(T)$
such that $u\in\beta(t_{1})$. Then there exists $t_{3}\in V(T)$ such that
$u,v\in\beta(t_{3})$ and for all nodes $t_{2}\in V(T)$ between $t_{1}$ and
$t_{3}$, we have $u\in\beta(t_{2})$.

The width of $(T,\beta)$ is $\max_{t\in V(T)}|\beta(t)|$. Note that every tree
decomposition is also a tree-shaped decomposition but not vice versa since we
do not demand that $\\{t\in V(T)\mid v\in\beta(t)\\}$ is connected. The third
property of tree-shaped decompositions ensures that directed edges in $G$ can
be “traced” by paths in $T$.

######  Proposition 13.

For every constant $k\in\mathbb{N}$, there exists a logspace transducer which,
given a graph $G$ and a tree-shaped decomposition $(T,\beta)$ for $G$ of width
at most $k$, outputs a graph $H$ of tree-width at most $k-1$ and a
bisimulation $R\subseteq V(G)\times V(H)$ such that for all $v\in V(G)$ there
exists $(v,w)\in R$.

######  Proof 4.1.

Consider the set of pairs

$P=\\{(v,t)\in V(G)\times V(T)\mid v\in\beta(t)\\}.$

We say that two pairs $(v,t_{1}),(w,t_{3})\in P$ are related if $v=w$ and for
all nodes $t_{2}\in V(T)$ on the path between $t_{1}$ and $t_{3}$ we have
$v\in\beta(t_{2})$, which can be tested in logspace. This relation is an
equivalence relation on $P$ and we denote with $[v,t]$ the equivalence class
that contains $(v,t)$. We take the set of equivalence classes
$\\{[v,t]\mid(v,t)\in P\\}$ as the node set of the graph $H$. For all $t\in
V(T)$ and $v,w\in\beta(t)$ with $v\stackrel{{\scriptstyle
a}}{{\longrightarrow}}w$ we add the edge $[v,t]\stackrel{{\scriptstyle
a}}{{\longrightarrow}}[w,t]$ to $H$. Clearly, $H$ is computable in logspace
from $G$ and $(T,\beta)$.

First, we claim that $(T,\gamma)$ is a tree decomposition for $H$ of width at
most $k-1$ where $\gamma(t)=\\{[v,t]\mid v\in\beta(t)\\}$ for all $t\in V(T)$.
Clearly, every node and every edge of $H$ is contained in some bag
$\gamma(t)$. Moreover, every bag $\gamma(t)$ has size at most $k$. We need to
show that for each node $[v,t]\in V(H)$ the set

$\\{t^{\prime}\in V(T)\mid[v,t]\in\gamma(t^{\prime})\\}$

is connected. Let $t_{1},t_{3}\in V(T)$ such that
$[v,t]\in\gamma(t_{1})\cap\gamma(t_{3})$. By definition of $\gamma$ the pairs
$(v,t)$, $(v,t_{1})$ and $(v,t_{3})$ must be related. Hence for all $t_{2}\in
V(T)$ on the unique path between $t_{1}$ and $t_{3}$ we have
$v\in\beta(t_{2})$, which implies $[v,t_{2}]\in\gamma(t_{2})$. Since
$(v,t_{2})$ and $(v,t)$ are also related, we conclude $[v,t]\in\gamma(t_{2})$.

Now we show that $R=\\{(v,[v,t])\mid(v,t)\in P\\}$ is a bisimulation between
$G$ and $H$. Let $(v,t)\in P$, i.e., $v\in\beta(t)$. If
$v\stackrel{{\scriptstyle a}}{{\longrightarrow}}w$ in $G$, then there exists
$t^{\prime}\in V(T)$ such that $v,w\in\beta(t^{\prime})$ and the pairs $(v,t)$
and $(v,t^{\prime})$ are related. Hence we find the matching edge
$[v,t]=[v,t^{\prime}]\stackrel{{\scriptstyle
a}}{{\longrightarrow}}[w,t^{\prime}]$ in $H$. Conversely, if
$[v,t]\stackrel{{\scriptstyle a}}{{\longrightarrow}}[w,t]$ is an edge in $H$,
then we know by definition that $v\stackrel{{\scriptstyle
a}}{{\longrightarrow}}w$ is an edge in $G$.

Proposition 13 and Theorem 1 together yield:

######  Theorem 14.

Let $k\in\mathbb{N}$ be a constant and $\varphi$ be a $\mu$-calculus formula.
There exists a logspace algorithm which, given a graph $G$, a node $v\in V(G)$
and a tree-shaped decomposition $(T,\beta)$ for $G$ of width at most $k$,
tests whether $(G,v)\models\varphi$.

Note that in Theorem 14 we need the tree-shaped decomposition $(T,\beta)$ as
part of the input. We do not know whether for every constant $k\in\mathbb{N}$
there exists a logspace transducer that computes from a given graph $G$ a
tree-shaped decomposition $(T,\beta)$ for $G$ of width at most $k$ and
polynomial size, or outputs $0$ if such a decomposition does not exist. For
tree decompositions, such a logspace transducer indeed exists [EJT10].

##  5\. Complexity of simulation

In this section, we consider simulation problems on restricted classes of
finite graphs. As for bisimulation, it is known that simulation on finite
graphs is ${\sf P}$-complete.

The upper bounds from Theorem 1 and 2 for Bisim(Trees) carry over to
Sim(Trees). The proofs are in fact much easier, since the simulation problem
for trees reduces to the evaluation of the Boolean circuit obtained from (1)
by removing the second conjunction over all edges $v\stackrel{{\scriptstyle
a}}{{\longrightarrow}}v^{\prime}$; in fact, this circuit is a tree. Also the
lower bound proofs for Theorem 6 hold for the simulation problem: Note that in
Figure 6(A) the trees $T_{1}$ and $T_{2}$ are isomorphic and hence $T_{1}$ is
simulated by $T_{2}$. On the other hand, in Figure 6(B), $T_{1}$ is not
simulated by $T_{2}$. Similarly, for the AND-gadget
$T_{\wedge}(G_{1},G_{2},H_{1},H_{2})$ and OR-gadget
$T_{\vee}(G_{1},G_{2},H_{1},H_{2})$ (see Figure 7) from the proof of Theorem 6
we have

  * •

$G_{1}\sqsubseteq H_{1}$ and $G_{2}\sqsubseteq H_{2}\iff
T_{\wedge}(G_{1},G_{2},H_{1},H_{2})\sqsubseteq
T_{\wedge}(H_{1},H_{2},G_{1},G_{2})$, and

  * •

$G_{1}\sqsubseteq H_{1}$ or $G_{2}\sqsubseteq H_{2}\iff
T_{\vee}(G_{1},G_{2},H_{1},H_{2})\sqsubseteq
T_{\vee}(G_{1},H_{2},H_{1},G_{2})$.

Hence we get:

######  Theorem 15.

The problem Sim(Trees) is ${\sf L}$-complete (resp., ${\sf NC}^{1}$-complete)
if trees are given in pointer representation (resp., term representation).

On the other hand, the construction from the proof of Lemma 7 (elimination of
edge labels) does not carry over to the simulation problem. Indeed, there is a
difference in the complexities of the simulation problems for edge-labelled
trees and unlabelled trees, if trees are given in term representation. The
easy observation is that in unlabelled graphs, $u$ is simulated by $v$ if and
only if the longest path starting in $u$ is at most as long as the longest
path starting in $v$ (the path lengths can be infinite).

######  Theorem 16.

The following holds:

  * •

The problem Sim(Unlabelled-Graphs) is ${\sf NL}$-complete.

  * •

The problem Sim(Unlabelled-Trees) is ${\sf L}$-complete if the trees are given
in pointer representation.

  * •

The problem Sim(Unlabelled-Trees) is ${\sf TC}^{0}$-complete if the trees are
given in term representation.

######  Proof 5.1.

The upper bounds are easy to show. In general graphs we can test in ${\sf NL}$
whether from a given node there exists a path of a given length
$d\in\mathbb{N}\cup\\{\infty\\}$. Since ${\sf NL}$ is closed under complement,
we can also check whether from a given node there does not exist a path of a
given length $d\in\mathbb{N}\cup\\{\infty\\}$. To decide simulation for
unlabelled trees we only need to compare the heights, which can be done in
logspace if the trees are given in pointer representation, and in ${\sf
TC}^{0}$ if the trees are given in term representation.

For the ${\sf NL}$-hardness on general graphs we reduce from the ${\sf
NL}$-complete problem whether a cycle is reachable from a given node $u$ in a
given graph $G$. The latter holds if and only if $u$ is simulated by the root
of a path of length $|V(G)|$.

For the ${\sf L}$-hardness on trees we again reduce from the reachability
problem on directed paths [Ete97]. Assume that $G$ is a path (which we view as
a tree) with $n$ nodes and we want to test whether there exists a path from
$u\in V(G)$ to $v\in V(G)$. Note that such a path exists if and only if the
longest path starting in $v$ is at most as long as the longest path starting
in $u$. By the observation before Theorem 16 this is equivalent to the fact
that $v$ is simulated by $u$.

For the ${\sf TC}^{0}$-hardness we reduce from the ${\sf TC}^{0}$-complete
majority problem: Given a string $x=a_{1}\cdots
a_{n}\in\\{\texttt{(},\texttt{)}\\}^{*}$, is the number of opening brackets in
$x$ at least the number of closing brackets in $x$? Consider the path
$T_{1}=\texttt{(}^{2n+2}\texttt{)}^{2n+2}$ of length $2n+1$ and the tree

$T_{2}=\texttt{(}^{n+1}x\;\texttt{(}^{n+1}\texttt{)}^{n+1}\;\overline{x}\texttt{)}^{n+1}$

where $\overline{x}=\overline{a_{n}}\cdots\overline{a_{1}}$ and
$\overline{\phantom{a}}$ swaps ( and ). One can verify that $T_{2}$ is indeed
a valid term representation and that both terms can be computed in ${\sf
AC}^{0}$ from the string $x$. Notice that the node in $T_{2}$ that is
represented by the innermost bracket pair () has maximal depth. Now one can
show that the root of $T_{1}$ is simulated by the root of $T_{2}$ if and only
if the height of $T_{2}$ is at least $2n+1$ if and only if the number of (’s
in $x$ is at least the number of )’s.

In the rest of Section 5 we complete the complexity picture for the simulation
problem on finite graphs with edge labels. In Section 5.1 we show that ${\sf
P}$-completeness for the simulation problem already holds for graphs of
bounded path-width. In Section 5.2 we show that simulation between a tree and
an arbitrary graph, as well as simulation between an arbitrary graph and a
tree is ${\sf LogCFL}$-complete.

###  5.1. Simulation on graphs of bounded path-width

In this section we show that the simulation problem is ${\sf P}$-complete on
graphs of bounded path-width, and hence also on graphs of bounded tree-width.
It remains open whether the bisimulation problem for graphs of bounded tree-
width belongs to ${\sf NC}$ or remains ${\sf P}$-complete. For integers $i,j$
we use the abbreviation $[i,j]=\\{k\in\mathbb{N}\mid i\leq k\leq j\\}$. Let
PW≤k denote the class of all graphs with path-width at most $k$.

######  Theorem 17.

There is a number $k$ such that Sim(PW≤k) P-complete.

######  Proof 5.2.

Fix a P-complete language $L\subseteq\\{0,1\\}^{*}$ and a deterministic
polynomial time bounded Turing machine
$M=(Q,\Gamma,\\{0,1\\},q_{0},q_{f},\delta)$ that accepts $L$. Here $Q$ is the
set of states, $\Gamma\supseteq\\{0,1,\Box\\}$ is the tape alphabet ($\Box$ is
the blank symbol), $q_{0}$ is the initial state, $q_{f}$ is the final state,
and $\delta\colon Q\times\Gamma\to Q\times\Gamma\times\\{\to,\leftarrow\\}$ is
the transition function, where $\to$ and $\leftarrow$ indicate the head
direction. The machine has a single two-way infinite tape, whose cells are
indexed with integers. Initially, the input $x$ is written in cells
$0,\ldots,|x|-1$ and the tape head scans cell $0$. We can assume that there is
a polynomial $p(n)$ such that for every input $x\in\\{0,1\\}^{*}$ we have:
$x\in L$ if and only if after $p(|x|)$ many transitions the machine is in
state $q_{f}$, cell $0$ contains $\Box$, and the tape head scans cell $0$.

We can view configurations of $M$ as words from
$\Gamma^{*}(Q\times\Gamma)\Gamma^{*}$. Let $\Omega=\Gamma\cup(Q\times\Gamma)$.
We define a partial mapping $\Delta\colon\Omega^{3}\to\Omega$ which computes
from the three symbols at positions $i-1$, $i$, $i+1$ in a configuration the
symbol at position $i$ in the successor configuration. Formally, for all
$a,a^{\prime},b,c\in\Gamma$, $p,q\in Q$ we define

  * •

$\Delta(a,b,c)=b$

  * •

$\Delta(b,c,(q,a))=(p,c)$ if $\delta(q,a)=(p,a^{\prime},\leftarrow)$

  * •

$\Delta(b,c,(q,a))=c$ if $\delta(q,a)=(p,a^{\prime},\to)$

  * •

$\Delta(b,(q,a),c)=a^{\prime}$ if $\delta(q,a)=(p,a^{\prime},d)$ for some
$d\in\\{\to,\leftarrow\\}$

  * •

$\Delta((q,a),b,c)=b$ if $\delta(q,a)=(p,a^{\prime},\leftarrow)$

  * •

$\Delta((q,a),b,c)=(p,b)$ if $\delta(q,a)=(p,a^{\prime},\to)$

In all other cases, $\Delta$ is undefined.

Let us fix an input $x=a_{0}a_{1}\cdots a_{n-1}$ of length $n>0$ for the
machine $M$ and let $N=p(n)+1$. Then there exists a unique computation of $M$
on input $x$. We denote with $C$ the corresponding computation table.
Formally, it is a mapping $C\colon[-N,N]\times[0,N-1]\to\Omega$, where
$C(i,t)$ is the symbol at cell $i$ in the $t$-th configuration. It can be
defined by the following properties:

  * •

$C(0,0)=(a_{0},q_{0})$, $C(i,0)=a_{i}$ for $i\in[1,n-1]$, $C(i,0)=\Box$ for
$i\in[-N,N]\setminus[0,n-1]$,

  * •

$C(-N,t)=C(N,t)=\Box$ for all $t\in[0,N-1]$

  * •

$C(i,t)=\Delta(C(i-1,t-1),C(i,t-1),C(i+1,t-1))$ for all $t\in[1,N-1]$,
$i\in[-N+1,N-1]$.

Let us fix the set of edge labels $A=\\{-1,0,1,\alpha\\}\uplus\Omega$. We
define two edge-labelled graphs $P$ (for position) and $T$ (for time) with
edge labels from $A$ and the node sets

$V(P)=[-N,N]\times\\{0,1\\},\quad
V(T)=[0,N-1]\;\cup\;[0,N-1]\times\Omega\;\cup\;[0,N-1]\times\Omega^{3}.$

For better readability, we write edges of $P$ (resp., $T$) as
$x\stackrel{{\scriptstyle a}}{{\longrightarrow}}_{P}y$ (resp.,
$x\stackrel{{\scriptstyle a}}{{\longrightarrow}}_{T}y$). Then, $P$ and $T$
contain the following edges:

$\displaystyle(i,0)\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}_{P}(i,1)\text{
for all }i\in[-N,N]$
$\displaystyle(i,1)\stackrel{{\scriptstyle\delta}}{{\longrightarrow}}_{P}(i+\delta,0)\text{
for all }i\in[-N,N],\delta\in\\{-1,0,1\\}\text{ with }i+\delta\in[-N,N]$
$\displaystyle(i,0)\xrightarrow{C(i,0)}_{P}(i,0)\text{ for all }i\in[-N,N]$
$\displaystyle(t,a)\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}_{T}(t-1,b,c,d)\text{
for all }a\in\Omega,t\in[1,N-1],(b,c,d)\in\Delta^{-1}(a)$
$\displaystyle(t,a_{-1},a_{0},a_{1})\stackrel{{\scriptstyle\delta}}{{\longrightarrow}}_{T}(t,a_{\delta})\text{
for all }t\in[0,N-2],a_{-1},a_{0},a_{1}\in\Omega,\delta\in\\{-1,0,1\\}$
$\displaystyle(t,a)\stackrel{{\scriptstyle b}}{{\longrightarrow}}_{T}t\text{
for all }a,b\in\Omega,t\in[1,N-1]$ $\displaystyle(0,a)\stackrel{{\scriptstyle
b}}{{\longrightarrow}}_{T}0\text{ for all }a\in\Omega,b\in\\{a,\alpha\\}$
$\displaystyle t\stackrel{{\scriptstyle a}}{{\longrightarrow}}_{T}t\text{ for
all }t\in[0,N-1],a\in A$

An example of the construction is shown in Figure 8, where we assume $N=3$ for
simplicity. It is easy to see that both $P$ and $T$ (and hence also the
disjoint union of $P$ and $T$) have bounded path-width. More precisely, $P$
has path-width 3 (the bags are the sets $\\{(i,0),(i,1),(i+1,0),(i+1,1)\\}$
for $-N\leq i\leq N-1$), whereas the path-width of $T$ is bounded by
$|\Omega|^{3}+|\Omega|$ (the bags are the set $\\{t,(t,a),(t-1,b,c,d)\mid
a,b,c,d\in\Omega\\}$ for $1\leq t\leq N-1$ and $\\{(t,a),(t,b,c,d)\mid
a,b,c,d\in\Omega\\}$ for $0\leq t\leq N-2$). Recall that $|\Omega|$ is a fixed
constant since the machine $M$ is fixed.

$(-3,0)$$(-2,0)$$(-1,0)$$(0,0)$$(1,0)$$(2,0)$$(3,0)$$(-3,1)$$(-2,1)$$(-1,1)$$(0,1)$$(1,1)$$(2,1)$$(3,1)$$\alpha$$\alpha$$\alpha$$\alpha$$\alpha$$\alpha$$\alpha$$0$$0$$0$$0$$0$$0$$0$$1$$1$$1$$1$$1$$1$$-1$$-1$$-1$$-1$$-1$$-1$$C(-3,0)$$C(-2,0)$$C(-1,0)$$C(0,0)$$C(1,0)$$C(2,0)$$C(3,0)$$(2,a)$$(t,a)$$(t-1,b,c,d)$$(t-1,c)$$(t-1,b)$$(t-1,d)$for
$(b,c,d)\in\Delta^{-1}(a)$$\dots$$\dots$$\alpha$$\alpha$$\alpha$$0$$-1$$1$$t$$\Omega$$A$$(0,a)$$0$$a,\alpha$$A$

Figure 8. The edge-labelled graphs $P$ and $T$, where we assume $N=3$ for
simplicity.

The following claim proves the theorem, since $M$ accepts $x$ if and only if
$C(0,N-1)=(q_{f},\Box)$ by our assumptions on $M$.

##### Claim.

For all $t\in[0,N-1]$, $i\in[-N,N]$ and $a\in\Omega$ such that $i+t\leq N$ and
$i-t\geq-N$ we have: $C(i,t)=a$ if and only if $(i,0)\sqsubseteq(t,a)$.

We prove the claim by induction on $t$. First, note that for every $v\in V(P)$
and every $t\in[0,N-1]\subseteq V(T)$ we have $v\sqsubseteq t$, since at $t$
we can loop with every $a\in A$. For $t=0$ note that indeed
$(i,0)\sqsubseteq(0,C(i,0))$: The only outgoing edges for $(i,0)$ are labelled
with $C(i,0)$ and $\alpha$. From $(0,C(i,0))$ these labels lead to node $0$,
which simulates every node of $P$. On the other hand, if $a\neq C(i,0)$, then
$(i,0)$ has a $C(i,0)$-labelled outgoing edge, whereas $(0,a)$ has no such
outgoing edge. This implies $(i,0)\not\sqsubseteq(0,a)$.

Now assume that $t\in[1,N-1]$, $i\in[-N,N]$, $i+t\leq N$, and $i-t\geq-N$ and
that the claim holds for $t-1$. First assume that $C(i,t)=a$. Since $t\geq 1$,
we have $i+1\leq N$ and $i-1\geq-N$, i.e., $i\in[-N+1,N-1]$. We have to show
that $(i,0)\sqsubseteq(t,a)$. The edge $(i,0)\xrightarrow{C(i,0)}_{P}(i,0)$
can be simulated by the edge $(t,a)\xrightarrow{C(i,0)}_{T}t$ (recall that
$(i,0)\sqsubseteq t$). Now consider the other possible edge
$(i,0)\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}_{P}(i,1)$. Since
$C(i,t)=a$, there must exist $(b,c,d)\in\Delta^{-1}(a)$ such that
$b=C(i-1,t-1)$, $c=C(i,t-1)$, and $d=C(i+1,t-1)$. Also note that
$i+\delta+(t-1)\leq N$ and $i+\delta-(t-1)\geq-N$ for all
$\delta\in\\{-1,0,1\\}$. Hence, by induction $(i-1,0)\sqsubseteq(t-1,b)$,
$(i,0)\sqsubseteq(t-1,c)$, and $(i+1,0)\sqsubseteq(t-1,d)$. But this implies
that $(i,1)\sqsubseteq(t-1,b,c,d)$. Hence, we can choose the edge
$(t,a)\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}_{T}(t-1,b,c,d)$ in
order to simulate the edge
$(i,0)\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}_{P}(i,1)$.

Finally, assume that $C(i,t)\neq a$. We have to show that
$(i,0)\not\sqsubseteq(t,a)$. Let us choose the edge
$(i,0)\stackrel{{\scriptstyle\alpha}}{{\longrightarrow}}_{P}(i,1)$. We have to
show that for every $(b,c,d)\in\Delta^{-1}(a)$,
$(i,1)\not\sqsubseteq(t,b,c,d)$. Let us fix a triple
$(b,c,d)\in\Delta^{-1}(a)$. Since $C(i,t)\neq a$, one of the following three
statements holds: $C(i-1,t-1)\neq b$, $C(i,t-1)\neq c$, $C(i+1,t-1)\neq d$.
Hence, by induction, $(i-1,0)\not\sqsubseteq(t-1,b)$ or
$(i,0)\not\sqsubseteq(t-1,c)$ or $(i+1,0)\not\sqsubseteq(t-1,d)$. This implies
that, indeed, $(i,1)\not\sqsubseteq(t,b,c,d)$.  It seems to be difficult to
modify the above proof so that it shows ${\sf P}$-hardness for bisimulation on
graphs of bounded path-width or bounded tree-width. One might try to restrict
the choices of the players in the bisimulation game (see e.g. [AI07]) so that
they are forced to play as in the simulation game. There is a technique to
achieve this (defenders forcing) but the problem is that it yields grid-like
graph structures and hence graphs of unbounded tree-width.

###  5.2. Simulation between trees and general graphs

In this section we show that the problems Sim(Trees, Graphs) and Sim(Graphs,
Trees) are both LogCFL-complete. Since simulation is not symmetric, it is not
obvious that these two problems are equivalent.

######  Theorem 18.

Sim(Trees, Graphs) is LogCFL-complete.

######  Proof 5.3.

Again we can restrict ourselves to the case that the input vertices are the
roots of the graph and the tree, respectively. We start with showing that the
simulation problem in the theorem belongs to ${\sf LogCFL}$. For this we
outline a straightforward alternating logspace algorithm with polynomial proof
tree size. Given a tree $T$ and a graph $G$, the algorithm stores a pair
$(u,w)\in V(T)\times V(G)$ and continues as follows:

  * •

Branch universally to all edges $u\stackrel{{\scriptstyle
a}}{{\longrightarrow}}u^{\prime}$ in $T$.

  * •

Branch existentially to all edges $w\stackrel{{\scriptstyle
a}}{{\longrightarrow}}w^{\prime}$ in $G$.

  * •

Continue with the pair $(u^{\prime},w^{\prime})$.

The algorithm starts with the pair $(r,v)$. It is obvious that there exists a
proof tree if and only if $r\sqsubseteq v$. Moreover, a proof tree results
from $T$ by inserting on each edge a node of $G$ with a unique child.

Let us now prove the lower bound. Fix a ${\sf LogCFL}$-complete problem $L$
and let $w$ be an input word of length $n$. Let $(C_{n})_{n\geq 0}$ be a
logspace-uniform ${\sf SAC}^{1}$ circuit family for $L$. We first construct in
logspace the ${\sf SAC}^{1}$-circuit $C_{n}$ for input length $n$. We set the
input gates to the bits in $w$; let $C=(G_{0},\beta)$ be the resulting Boolean
circuit. Recall from Section 2.2 that $G_{0}$ is a directed graph
$G_{0}=(V_{0},E_{0})$ and that edges from $E_{0}$ are directed towards the
input gates.

Our goal is to reduce the question whether $C$ evaluates to $1$ to a
simulation problem. By [GLS01, Lemma 4.6] we can assume that $C$ is layered
and alternating, i.e., the set of gates is partitioned into $m\in O(\log n)$
many layers $L_{1},L_{2},\ldots,L_{m}$, where $m>1$ is odd, $L_{1}$ contains
the input gates, all wires go from layer $L_{i}$ to layer $L_{i-1}$ for some
$2\leq i\leq m$, and $L_{m}=\\{g_{0}\\}$ contains the output gate of the
circuit. Moreover, layers $2i$ ($2i+1$, resp.) contain only $\wedge$-gates
($\vee$-gates, resp.) for $1\leq i\leq\lfloor m/2\rfloor$. Since $m$ is odd,
the output gate $g_{0}$ is a $\vee$-gate. Recall that every $\wedge$-gate $u$
has exactly two input nodes that we denote with $u_{1}$ and $u_{2}$ (we allow
$u_{1}=u_{2}$).

$\vee$$\wedge$$\wedge$$\wedge$$\wedge$$a$$a$$a$$a$$\vee$$\vee$$\vee$$\vee$$\vee$$a$$b$$a$$b$$a$$b$$a$$b$$\wedge$$\wedge$$\wedge$$0$$1$$0$$1$$1$$0$$a$$a$$a$$b$$b$$b$$\omega$$a$$a$$a$$L_{m}$$L_{m-1}$$L_{m-2}$$L_{2}$$L_{1}$$a$$a$$b$$a$$a$$a$$b$$a$$b$$a$$b$$a$$b$$a$$a$$a$$a$$a$$a$$a$$a$
Figure 9. Reduction from ${\sf SAC}^{1}$-circuits to Sim(Trees, Graphs)

Define the edge-labelled graph $G=(V_{0}\uplus\\{\omega\\},E)$, where $E$
consists of the following set of $\\{a,b\\}$-labelled edges.

  * •

$v\stackrel{{\scriptstyle a}}{{\longrightarrow}}\omega$ for all $v\in L_{1}$
with $\beta(v)=1$.

  * •

$v\stackrel{{\scriptstyle a}}{{\longrightarrow}}v^{\prime}$ for all $v\in
L_{i}$ with $i>1$ odd and $(v,v^{\prime})\in E_{0}$.

  * •

$v\stackrel{{\scriptstyle a}}{{\longrightarrow}}v_{1}$,
$v\stackrel{{\scriptstyle b}}{{\longrightarrow}}v_{2}$ for all $v\in L_{i}$
with $i>1$ even, where $v_{1},v_{2}$ are the left and right child of $v$ in
$G_{0}$.

The tree $T$ is a full binary tree of height $\lfloor m/2\rfloor$ with
intermediate layers of unary nodes inserted. More precisely, we define trees
$T_{i}$ ($1\leq i\leq m$) recursively as follows:

  * •

If $i=1$ then $T_{i}$ consists of a root node $r$ with a unique outgoing edge
$r\stackrel{{\scriptstyle a}}{{\longrightarrow}}r^{\prime}$, where
$r^{\prime}$ is a leaf.

  * •

If $i>1$ is odd, then $T_{i}$ consists of a root node $r$ with a unique
outgoing edge $r\stackrel{{\scriptstyle a}}{{\longrightarrow}}r^{\prime}$,
where $r^{\prime}$ is the root of a copy of $T_{i-1}$.

  * •

If $i>1$ is even, then $T_{i}$ consists of a root node $r$ with two outgoing
edges $r\stackrel{{\scriptstyle a}}{{\longrightarrow}}r_{1}$ and
$r\stackrel{{\scriptstyle b}}{{\longrightarrow}}r_{2}$. Each of the nodes
$r_{1}$ and $r_{2}$ is the root of a copy of $T_{i-1}$.

The tree $T$ is defined as $T_{m}$. Both $T$ and $G$ are displayed in Figure
9.

##### Claim.

If $r$ denotes the root of $T_{i}$ and $v\in V(G)$ belongs to layer $L_{i}$
then $r\sqsubseteq v$ if and only if gate $v$ evaluates to $1$ in the circuit
$C$.

We prove the claim by induction on $i$. The case $i=1$ is clear: In the tree
$T_{1}$ the root node $r$ has a unique outgoing edge $r\stackrel{{\scriptstyle
a}}{{\longrightarrow}}r^{\prime}$, where $r^{\prime}$ has no outgoing edges.
Moreover, layer $L_{1}$ contains the input gates of the circuit $C$. If $v$ is
labelled with $0$, then $v$ has no outgoing edges in $G$, and hence
$r\not\sqsubseteq v$. On the other hand, if $v$ is labelled with $1$, then $v$
has a single outgoing $a$-labelled edge to a node without outgoing edges,
which implies $r\sqsubseteq v$.

Now assume that $i>1$. Let us first assume that $i$ is odd. Then, the root $r$
of $T_{i}$ has a single outgoing edge $r\stackrel{{\scriptstyle
a}}{{\longrightarrow}}r^{\prime}$, where $r^{\prime}$ is a root of $T_{i-1}$.
Moreover, $v$ is a $\vee$-gate. If $v$ evaluates to $1$, then $v$ has an
outgoing edge $v\stackrel{{\scriptstyle a}}{{\longrightarrow}}v^{\prime}$,
where $v^{\prime}\in L_{i-1}$ evaluates to $1$. By induction, we get
$r^{\prime}\sqsubseteq v^{\prime}$, which implies $r\sqsubseteq v$. On the
other hand, if $r\sqsubseteq v$, then $v$ must have an outgoing edge
$(v,a,v^{\prime})$ such that $r^{\prime}\sqsubseteq v^{\prime}$. By induction,
it follows that $v^{\prime}$ evaluates to $1$. Hence, the $\vee$-gate $v$
evaluates to $1$ too.

Now assume that $i$ is even. Then, the root $r$ of $T_{i}$ has two outgoing
edges $r\stackrel{{\scriptstyle a}}{{\longrightarrow}}r_{1}$ and
$r\stackrel{{\scriptstyle b}}{{\longrightarrow}}r_{2}$ where $r_{i}$ is a root
of a copy of $T_{i-1}$. Moreover, $v$ is a $\wedge$-gate, which has two input
gates $v_{1}$ and $v_{2}$ (we might have $v_{1}=v_{2}$). In $G$, $v$ has the
two outgoing edges $v\stackrel{{\scriptstyle a}}{{\longrightarrow}}v_{1}$ and
$v\stackrel{{\scriptstyle b}}{{\longrightarrow}}v_{2}$. If $v$ evaluates to
$1$, then $v_{1}$ and $v_{2}$ evaluate to $1$. By induction, we get
$r_{1}\sqsubseteq v_{1}$ and $r_{2}\sqsubseteq v_{2}$, which implies
$r\sqsubseteq v$. On the other hand, if $r\sqsubseteq v$, then we must have
$r_{1}\sqsubseteq v_{1}$ and $r_{2}\sqsubseteq v_{2}$. Hence, by induction, it
follows that $v_{1}$ and $v_{2}$ both evaluate to $1$. Thus, $v$ evaluates to
$1$.

######  Theorem 19.

Sim(Graphs, Trees) is LogCFL-complete.

######  Proof 5.4.

The proof of the upper bound is very similar to the previous proof, using an
alternating logspace machine with a polynomial proof tree size. Since ${\sf
LogCFL}$ is closed under complement [BCD+89], we can consider the problem of
deciding whether a graph node $u\in V(G)$ is not simulated by a tree node
$w\in V(T)$. The algorithm stores the pair $(u,w)\in V(G)\times V(T)$ and
continues as follows:

  * •

Branch existentially to all edges $u\stackrel{{\scriptstyle
a}}{{\longrightarrow}}u^{\prime}$ in $G$.

  * •

Branch universally to all edges $w\stackrel{{\scriptstyle
a}}{{\longrightarrow}}w^{\prime}$ in $T$.

  * •

Continue with the pair $(u^{\prime},w^{\prime})$.

The correctness and the polynomial proof tree size of the algorithm can be
argued as above.

For the ${\sf LogCFL}$-hardness we can use the same graph $G$ as in the proof
of Theorem 18 but define a different tree $T$. First we reconsider the tree
used in the proof of Theorem 18, which we call $T_{*}$. Notice that every node
in $G$ which is contained in an odd level $L_{i}$ is simulated by the root of
$T_{*}$. Then we define trees $T_{i}$ for all odd $1\leq i\leq m$ and trees
$T_{i,a},T_{i,b}$ for all even $1\leq i\leq m$ recursively as follows:

  * •

If $i=1$ then $T_{i}$ consists of a single node.

  * •

If $i>1$ is odd, then $T_{i}$ consists of a root node $r$ with two outgoing
edges $r\stackrel{{\scriptstyle a}}{{\longrightarrow}}r_{a}$ and
$r\stackrel{{\scriptstyle a}}{{\longrightarrow}}r_{b}$. The nodes $r_{a}$ and
$r_{b}$ are the roots of copies of the trees $T_{i-1,a}$ and $T_{i-1,b}$,
respectively.

  * •

If $i>1$ is even, then $T_{i,a}$ consists of a root node $r$ with two outgoing
edges $r\stackrel{{\scriptstyle a}}{{\longrightarrow}}r_{a}$ and
$r\stackrel{{\scriptstyle b}}{{\longrightarrow}}r_{b}$. The node $r_{a}$ is
the root of a copy of $T_{*}$, and $r_{b}$ is the root of a copy of $T_{i-1}$.

Finally the tree $T$ is defined as $T_{m}$, which is displayed together with
$G$ in Figure 10.

$\vee$$\wedge$$\wedge$$\wedge$$\wedge$$a$$a$$a$$a$$\vee$$\vee$$\vee$$\vee$$\vee$$a$$b$$a$$b$$a$$b$$a$$b$$0$$1$$0$$1$$1$$0$$\omega$$a$$a$$a$$L_{m}$$L_{m-1}$$L_{m-2}$$L_{1}$$a$$a$$T_{*}$$T_{*}$$a$$b$$a$$b$
Figure 10. Reduction from ${\sf SAC}^{1}$-circuits to Sim(Graphs, Trees)

##### Claim.

Assume $v\in V(G)$ belongs to layer $L_{i}$.

  * •

If $i$ is odd, let $r$ be the root of $T_{i}$. Then $v\not\sqsubseteq r$ if
and only if gate $v$ evaluates to $1$ in the circuit $C$.

  * •

If $i$ is even, let $r_{a},r_{b}$ be the roots of $T_{i,a}$ and $T_{i,b}$,
respectively. Then ($v\not\sqsubseteq r_{a}$ and $v\not\sqsubseteq r_{b}$) if
and only if gate $v$ evaluates to $1$ in the circuit $C$.

For $i=1$ this is clear because $v$ has a successor if and only if it
evaluates to $1$. Now let $i>1$. First assume that $i$ is odd, i.e., $v$ is a
$\vee$-gate. Let $r$ be the root of $T_{i}$. Thus, $r$ has two outgoing edges
$r\stackrel{{\scriptstyle a}}{{\longrightarrow}}r_{a}$ and
$r\stackrel{{\scriptstyle a}}{{\longrightarrow}}r_{b}$, where $r_{a}$ and
$r_{b}$ are the roots of copies of the trees $T_{i-1,a}$ and $T_{i-1,b}$,
respectively. The node $v$ evaluates to 1 in $C$ if and only if $v$ has some
$a$-successor $w$ in $G$ which evaluates to 1. By induction, this is
equivalent to saying $w\not\sqsubseteq r_{a}$ and $w\not\sqsubseteq r_{b}$ for
some successor $w$ of $v$, which in turn is equivalent to $v\not\sqsubseteq
r$.

Now let $i$ be even, i.e., $v$ is a $\wedge$-gate, which has an $a$-successor
$v_{1}$ and a $b$-successor $v_{2}$. Let $r_{a}$ and $r_{b}$ be the roots of
$T_{i,a}$ and $T_{i,b}$, respectively. The node $v$ evaluates to 1 in $C$ if
and only if both successors $v_{1}$ and $v_{2}$ of $v$ in $G$ evaluate to 1.
By induction, this is equivalent to saying $v_{1}\not\sqsubseteq r^{\prime}$
and $v_{2}\not\sqsubseteq r^{\prime}$ where $r^{\prime}$ is the root of
$T_{i-1}$. Since the root of $T_{*}$ simulates every node in an odd level of
$G$, this is equivalent to $v\not\sqsubseteq r_{a}$ and $v\not\sqsubseteq
r_{b}$.

##  6\. Conclusion

We proved the following results:

  1. (1)

The bisimulation problem for trees that are given by pointer structures
(resp., in term representation) is complete for deterministic logspace (resp.,
${\sf NC}^{1}$). These results also hold for the simulation problem for trees.

  2. (2)

Already for graphs of bounded path-width (a subclass of the graphs of bounded
tree-width), the simulation problem becomes ${\sf P}$-complete.

  3. (3)

The bisimulation problem between a tree and a dag (or arbitrary graph) belongs
to ${\sf AC}^{1}$ and is ${\sf NL}$-hard.

  4. (4)

Simulation of a tree by a dag as well as simulation of a dag by a tree is
LogCFL-complete.

As an application of (1), we showed that equality of hereditarily finite sets
is ${\sf NC}^{1}$-complete. For the proof of (1) we introduced the new class
of tree-shaped circuits and proved that the circuit evaluation problem for
tree-shaped circuits of bounded width is in logspace or ${\sf NC}^{1}$,
depending on the representation of the circuit. It would be nice to find
further applications of tree-shaped circuits.

The main open problem that remains is whether the bisimulation problem for
graphs of bounded tree-width is in ${\sf NC}$ or ${\sf P}$-complete. Another
open problem is the exact complexity of the bisimulation problem for a tree
and a dag. Our bounds (in ${\sf AC}^{1}$ and ${\sf NL}$-hard) are not
matching. In many situations (e.g. for various classes of infinite state
systems), simulation is harder than bisimulation. We proved that simulation of
a tree by a dag (or vice versa) is ${\sf LogCFL}$-complete. Hence, one might
conjecture that also the bisimulation problem for a tree and a dag belongs to
${\sf LogCFL}$.

## References

  * [AI07] L. Aceto and A. Ingólfsdóttir.  Reactive Systems: Modelling, Specification and Verification.  Cambridge University Press, 2007.
  * [BC89] D. A. M. Barrington and J. Corbet.  On the relative complexity of some languages in $\text{NC}^{1}$.  Information Processing Letters, 32:251–256, 1989.
  * [BCD+89] A. Borodin, S. A. Cook, P. W. Dymond, W. L. Ruzzo, and M. Tompa.  Two applications of inductive counting for complementation problems.  SIAM Journal on Computing, 18(3):559–578, 1989.
  * [BGS92] J. L. Balcázar, J. Gabarró, and M. Sántha.  Deciding bisimilarity is P-complete.  Formal Aspects of Computing, 4(6A):638–648, 1992.
  * [BIS90] D. A. M. Barrington, N. Immerman, and H. Straubing.  On uniformity within $\text{NC}^{1}$.  Journal of Computer and System Sciences, 41:274–306, 1990.
  * [BM95] M. Beaudry and P. Mckenzie.  Circuits, matrices, and nonassociative computation.  Journal of Computer and System Sciences, 50(3):441 – 455, 1995\.
  * [Bus97] S. R. Buss.  Alogtime algorithms for tree isomorphism, comparison, and canonization.  In Kurt Gödel Colloquium 97, pages 18–33, 1997.
  * [CS01] R. Cleaveland and O. Sokolsky.  Chapter 6 - equivalence and preorder checking for finite-state systems.  In J.A. Bergstra, A. Ponse, and S.A. Smolka, editors, Handbook of Process Algebra, pages 391 – 424. Elsevier Science, Amsterdam, 2001.
  * [DF13] R. G. Downey and M. R. Fellows.  Fundamentals of Parameterized Complexity.  Texts in Computer Science. Springer, 2013.
  * [EJT10] M. Elberfeld, A. Jakoby, and T. Tantau.  Logspace versions of the theorems of Bodlaender and Courcelle.  In Proceedings of FOCS 2010, pages 143–152. IEEE, 2010.
  * [EJT12] M. Elberfeld, A. Jakoby, and T. Tantau.  Algorithmic meta theorems for circuit classes of constant and logarithmic depth.  In Proceedings of STACS 2012, volume 14 of LIPIcs, pages 66–77. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2012.
  * [ES16] M. Elberfeld and P. Schweitzer.  Canonizing graphs of bounded tree width in logspace.  In Proceedings of STACS 2016, volume 47 of LIPIcs, pages 32:1–32:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.
  * [Ete97] K. Etessami.  Counting quantifiers, successor relations, and logarithmic space.  Journal of Computer and System Sciences, 54(3):400–411, 1997.
  * [GGHL12] M. Grohe, B. Grußien, A. Hernich, and B. Laubner.  L-recursion and a new logic for logarithmic space.  Logical Methods in Computer Science, 9(1), 2012.
  * [GGL16] M. Ganardi, S. Göller, and M. Lohrey.  On the parallel complexity of bisimulation on finite systems.  In Proceedings of CSL 2016, volume 62 of LIPIcs, pages 12:1–12:17. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016.
  * [GHR95] R. Greenlaw, H. J. Hoover, and W. L. Ruzzo.  Limits to Parallel Computation: ${P}$-Completeness Theory.  Oxford University Press, 1995.
  * [GLS01] G. Gottlob, N. Leone, and F. Scarcello.  The complexity of acyclic conjunctive queries.  Journal of the ACM, 48(3):431–498, 2001.
  * [GV06] M. Grohe and O. Verbitsky.  Testing graph isomorphism in parallel by playing a game.  In Proceedings of ICALP 2006, Part I, volume 4051 of Lecture Notes in Computer Science, pages 3–14. Springer, 2006.
  * [GW00] F. Gurski and E. Wanke.  The tree-width of clique-width bounded graphs without $K_{n,n}$.  In Proceedings of WG 2000, volume 1928 of Lecture Notes in Computer Science, pages 196–205. Springer, 2000.
  * [HAB02] W. Hesse, E. Allender, and D. A. M. Barrington.  Uniform constant-depth threshold circuits for division and iterated multiplication.  Journal of Computer and System Sciences, 65:695–716, 2002.
  * [Imm88] N. Immerman.  Nondeterministic space is closed under complementation.  SIAM Journal on Computing, 17(5):935–938, 1988.
  * [JKMT03] B. Jenner, J. Köbler, P. McKenzie, and J. Torán.  Completeness results for graph isomorphism.  Journal of Computer and System Sciences, 66(3):549–566, 2003.
  * [JW96] D. Janin and I. Walukiewicz.  On the expressive completeness of the propositional mu-calculus with respect to monadic second order logic.  In Proceedings of CONCUR ’96, volume 1119 of Lecture Notes in Computer Science, pages 263–277. Springer, 1996.
  * [KLM09] M. Kaminski, V. V. Lozin, and M. Milanic.  Recent developments on graphs of bounded clique-width.  Discrete Applied Mathematics, 157(12):2747–2761, 2009.
  * [KS90] P. C. Kanellakis and S. A. Smolka.  CCS expressions, finite state processes, and three problems of equivalence.  Information and Computation, 86(1):43–68, 1990.
  * [Lin92] S. Lindell.  A logspace algorithm for tree canonization (extended abstract).  In Proceedings of STOC 1992, pages 400–404. ACM, 1992.
  * [LM98] K.-J. Lange and P. McKenzie.  On the Complexity of Free Monoid Morphisms.  In Proceedings of ISAAC ’98, volume 1533 of Lecture Notes in Computer Science, pages 247–256. Springer, 1998.
  * [PT87] R. Paige and R. E. Tarjan.  Three partition refinement algorithms.  SIAM Journal on Computing, 16(6):973–989, 1987.
  * [Ruz80] W. L. Ruzzo.  Tree–size bounded alternation.  Journal of Computer and System Sciences, 21:218–235, 1980.
  * [Ruz81] W. L. Ruzzo.  On uniform circuit complexity.  Journal of Computer and System Sciences, 22:365–383, 1981.
  * [SJ05] Z. Sawa and P. Jancar.  Behavioural equivalences on finite-state systems are PTIME-hard.  Computers and Artificial Intelligence, 24(5):513–528, 2005.
  * [Srb01] J. Srba.  On the power of labels in transition systems.  In Proceedings of CONCUR 2001, volume 2154 of Lecture Notes in Computer Science, pages 277–291. Springer, 2001.
  * [Srb04] J. Srba.  Roadmap of infinite results.  In Current Trends In Theoretical Computer Science, The Challenge of the New Century, volume Vol 2: Formal Models and Semantics, pages 337–350. World Scientific Publishing Co., 2004.
  * [Sze88] R. Szelepcsényi.  The method of forced enumeration for nondeterministic automata.  Acta Informatica, 26(3):279–284, 1988.
  * [Ven91] H. Venkateswaran.  Properties that characterize LOGCFL.  Journal of Computer and System Sciences, 43(2):380–404, 1991.
  * [Vol99] H. Vollmer.  Introduction to Circuit Complexity.  Springer, 1999.