2010501-512Nancy, France 501

Alexander Kartzow

# Collapsible Pushdown Graphs of Level $\mathbf{2}$ are Tree-Automatic

A. Kartzow  TU Darmstadt, Fachbereich Mathematik, Schlossgartenstr. 7, 64289
Darmstadt, Germany

###### Abstract.

We show that graphs generated by collapsible pushdown systems of level $2$ are
tree-automatic. Even when we allow $\varepsilon$-contractions and add a
reachability predicate (with regular constraints) for pairs of configurations,
the structures remain tree-automatic. Hence, their $\mathrm{FO}$ theories are
decidable, even when expanded by a reachability predicate. As a corollary, we
obtain the tree-automaticity of the second level of the Caucal-hierarchy.

###### Key words and phrases:

tree-automatic structures, collapsible pushdown graphs, collapsible pushdown
systems, first-order decidability, reachability

###### 1991 Mathematics Subject Classification:

F.4.1[Theory of Computation]:Mathematical Logic

##  1\. Introduction

Higher-order pushdown systems were first introduced by Maslov [10, 11] as
accepting devices for word languages. Later, Knapik et al. [8] studied them as
generators for trees. They obtained an equi-expressivity result for higher-
order pushdown systems and for higher-order recursion schemes that satisfy the
constraint of _safety_ , which is a rather unnatural syntactic condition.
Recently, Hague et al. [6] introduced collapsible pushdown systems as
extensions of higher-order pushdown systems and proved that these have exactly
the same power as higher-order recursion schemes as methods for generating
trees.

Both – higher-order and collapsible pushdown systems – also form interesting
devices for generating graphs. Carayol and Wöhrle [3] showed that the graphs
generated by higher-order pushdown systems111The graph generated by a higher-
order pushdown system is the $\varepsilon$-closure of its reachable
configurations. of level $l$ coincide with the graphs in the $l$-th level of
the Caucal-hierarchy, a class of graphs introduced by Caucal [4]. Every level
of this hierarchy is obtained from the preceding level by applying graph
unfoldings and $\mathrm{MSO}$ interpretations. Both operations preserve the
decidability of the $\mathrm{MSO}$ theory whence the Caucal-hierarchy forms a
rather large class of graphs with decidable $\mathrm{MSO}$ theories. If we use
collapsible pushdown systems as generators for graphs we obtain a different
situation. Hague et al. showed that even the second level of the hierarchy
contains a graph with undecidable $\mathrm{MSO}$ theory. But they showed the
decidability of the modal $\mu$-calculus theories of all graphs in the
hierarchy. This turns graphs generated by collapsible pushdown systems into an
interesting class from a model theoretic point of view. There are few natural
classes that share these properties. In fact, the author only knows one
further example, viz. nested pushdown trees. Alur et al.[1] introduced these
graphs for $\mu$-calculus model checking purposes. We proved in [7] that
nested pushdown trees also have decidable first-order theories. We gave an
effective model checking algorithm using pumping techniques, but we also
proved that nested pushdown trees are tree-automatic structures. Tree-
automatic structures were introduced by Blumensath [2]. These structures enjoy
decidable first-order theories due to the good closure properties of finite
automata on trees.

In this paper, we are going to extend our previous result to the second level
of the collapsible pushdown hierarchy. All graphs of the second level are
tree-automatic. This subsumes our previous result as nested pushdown trees are
first-order interpretable in collapsible pushdown graphs of level two.
Furthermore, we show that collapsible pushdown graphs of level $2$ are still
tree-automatic when expanded by a reachability predicate, i.e., by the binary
relation which contains all pairs of configurations such that there is a path
from the first to the second configuration. Thus, first-order logic extended
by reachability predicates is decidable on level $2$ collapsible pushdown
graphs.

In the next section, we introduce the necessary notions concerning tree-
automaticity and in Section 3 we define collapsible pushdown graphs. We
explain the translation of configurations into trees in Section 4. Section 5
is a sketch of the proof that this translation yields tree-automatic
representations of collapsible pushdown graphs, even when enriched with
certain regular reachability predicates. The last section contains some
concluding remarks about questions arising from our result.

##  2\. Preliminaries

We write $\mathrm{MSO}$ for monadic second order logic and $\mathrm{FO}$ for
first-order logic. For words $w_{1},w_{2}\in\Sigma^{*}$, we write $w_{1}\sqcap
w_{2}$ for the greatest common prefix of $w_{1}$ and $w_{2}$. A _$\Sigma$
-labelled tree_ is a function $T:D\rightarrow\Sigma$ for a finite
$D\subseteq\\{0,1\\}^{*}$ which is closed under prefixes.

For $d\in D$ we denote by ${T}_{d}$ the _subtree rooted at $d$_.

Sometimes it is useful to define trees inductively by describing their left
and right subtrees. For this purpose we fix the following notation. Let
$\hat{T}_{0}$ and $\hat{T}_{1}$ be $\Sigma$-labelled trees and
$\sigma\in\Sigma$. Then we write
$T\mathrel{\mathop{:}}=\sigma({\hat{T}_{0}},{\hat{T}_{1}})$ for the
$\Sigma$-labelled tree $T$ with the following three properties

$\displaystyle 1.\ T(\varepsilon)=\sigma,$ $\displaystyle 2.\
{T}_{0}=\hat{T}_{0}\text{, and }$ $\displaystyle 3.\
{T}_{1}=\hat{T}_{1}\enspace.$

In the rest of this section, we briefly present the notion of a tree-automatic
structure as introduced by Blumensath [2].

The _convolution_ of two $\Sigma$-labelled trees $T$ and $T^{\prime}$ is given
by a function

$\displaystyle T\otimes
T^{\prime}:\text{dom}(T)\cup\text{dom}(T^{\prime})\rightarrow(\Sigma\cup\\{\Box\\})^{2}$

where $\Box$ is a new symbol for padding and

$\displaystyle(T\otimes
T^{\prime})(d)\mathrel{\mathop{:}}=\begin{cases}(T(d),T^{\prime}(d))&\text{ if
}d\in\text{dom}(T)\cap\text{dom}(T^{\prime})\\\ (T(d),\Box)&\text{ if
}d\in\text{dom}(T)\setminus\text{dom}(T^{\prime})\\\
(\Box,T^{\prime}(d))&\text{ if
}d\in\text{dom}(T^{\prime})\setminus\text{dom}(T)\end{cases}$

By “tree-automata” we mean a nondeterministic finite automaton that labels a
finite tree top-down.

######  Definition 2.1.

A structure $\mathfrak{B}=(B,E_{1},E_{2},\ldots,E_{n})$ with domain $B$ and
binary relations $E_{i}$ is _tree-automatic_ if there are tree-automata
$A_{B},A_{E_{1}},A_{E_{2}},\ldots,A_{E_{n}}$ and a bijection $f:L\rightarrow
B$ for $L$ the language accepted by $A_{B}$ such that the following hold. For
$T,T^{\prime}\in L$, the automaton $A_{E_{i}}$ accepts $T\otimes T^{\prime}$
if and only if $\big{(}f(T),f(T^{\prime})\big{)}\in E_{i}$.

Tree-automatic structures form a nice class because automata theoretic
techniques may be used to decide first-order formulas on these structures:

######  Lemma 2.2 ([2]).

If $B$ is tree-automatic, then its first-order theory is decidable.

We will use the classical result that regular sets of trees are $\mathrm{MSO}$
definable.

######  Theorem 2.3 ([12], [5]).

For a set $\mathbb{T}$ of finite $\Sigma$-labelled trees, there is a tree
automaton recognising $\mathbb{T}$ if and only if $\mathbb{T}$ is
$\mathrm{MSO}$ definable.

##  3\. Definition of Collapsible Pushdown Graphs (CPG)

In this section we define our notation of collapsible pushdown systems. For a
more comprehensive introduction, we refer the reader to [6].

###  3.1. Collapsible Pushdown Stacks

First, we provide some terminology concerning stacks of (collapsible) higher-
order pushdown systems. We write $\Sigma^{*2}$ for $(\Sigma^{*})^{*}$ and
$\Sigma^{+2}$ for $(\Sigma^{+})^{+}$. We call an $s\in\Sigma^{*2}$ a $2$-word.

Let us fix a $2$-word $s\in\Sigma^{*2}$ which consists of an ordered list
$w_{1},w_{2},\ldots,w_{m}\in\Sigma^{*}$. We separate the words of this list by
colons writing $s=w_{1}:w_{2}:\ldots:w_{m}$. By $\lvert s\rvert$ we denote the
number of words $s$ consists of, i.e., $\lvert s\rvert=m$.

For another word
$s^{\prime}=w_{1}^{\prime}:w_{2}^{\prime}:\ldots:w^{\prime}_{n}\in\Sigma^{*2}$,
we write $s:s^{\prime}$ for the concatenation
$w_{1}:w_{2}:\ldots:w_{m}:w_{1}^{\prime}:w_{2}^{\prime}:\ldots:w_{n}^{\prime}$.

If $w\in\Sigma^{*}$, we write $[w]$ for the $2$-word that consists of a list
of one word which is $w$.

A level $2$ collapsible pushdown stack is a special element of
$(\Sigma\times\\{1,2\\}\times\mathbb{N})^{+2}$ that is generated by certain
stack operations from an initial stack which we introduce in the following
definitions. The natural numbers following the stack symbol represent the so-
called _collapse pointer_ : every element in a collapsible pushdown stack has
a pointer to some substack and applying the collapse operation returns the
substack to which the topmost symbol of the stack points. Here, the first
number denotes the _collapse level_. If it is $1$ the collapse pointer always
points to the symbol below the topmost symbol and the collapse operations just
removes the topmost symbol. The more interesting case is when the collapse
level of the topmost symbol of the stack $s$ is $2$. Then the stack obtained
by the collapse contains the first $n$ words of $s$ where $n$ is the second
number in the topmost element of $s$.

The initial level $1$ stack is $\bot_{1}\mathrel{\mathop{:}}=(\bot,1,0)$ and
the initial level $2$ stack is $\bot_{2}\mathrel{\mathop{:}}=[\bot_{1}]$.

For $k\in\\{1,2\\}$ and for a $2$-word
$s=w_{1}:w_{2}:\ldots:w_{n}\in(\Sigma\times\\{1,2\\}\times\mathbb{N})^{+2}$
such that $w_{n}=a_{1}a_{2}\ldots a_{m}$ with
$a_{i}\in\Sigma\times\\{1,2\\}\times\mathbb{N}$ for all $1\leq i\leq m$:

  * •

we define the _topmost $(k-1)$-word of $s$_ as
$\mathrm{top}_{k}(s)\mathrel{\mathop{:}}=\begin{cases}w_{n}&\text{if }k=2\\\
a_{m}&\text{if }k=1\end{cases}$

  * •

for
$\mathrm{top}_{1}(s)=(\sigma,i,j)\in\Sigma\times\\{1,2\\}\times\mathbb{N}$, we
define the _topmost symbol_ $\mathrm{Sym}(s)\mathrel{\mathop{:}}=\sigma$, the
_collapse-level of the topmost element_
$\mathrm{CLvl}(s)\mathrel{\mathop{:}}=i$, and the _collapse-link of the
topmost element_ $\mathrm{CLnk}(s)\mathrel{\mathop{:}}=j$.

For $s$, $w_{n}$ and $k$ as before, $\sigma\in\Sigma\setminus\\{\bot\\}$, and
$w_{n}^{\prime}:=a_{1}\ldots a_{m-1}$, we define the stack operations

$\displaystyle{\mathrm{pop}_{k}}(s)\mathrel{\mathop{:}}=$
$\displaystyle\begin{cases}w_{1}:w_{2}:\ldots:w_{n-1}&\text{if }k=2,n\geq 2\\\
w_{1}:w_{2}:\ldots:w_{n-1}:w_{n}^{\prime}&\text{if }k=1,m\geq 2\\\
\text{undefined}&\text{otherwise}\end{cases}$
$\displaystyle{\mathrm{clone}_{2}}(s)\mathrel{\mathop{:}}=$ $\displaystyle\
w_{1}:w_{2}:\ldots:w_{n-1}:w_{n}:w_{n}$
$\displaystyle\mathrm{push}_{\sigma,k}(s)\mathrel{\mathop{:}}=$
$\displaystyle\begin{cases}w_{1}:w_{2}:\ldots:w_{n}(\sigma,2,n-1)&\text{ if
k=2}\\\ w_{1}:w_{2}:\ldots:w_{n}(\sigma,1,m)&\text{ if k=1}\end{cases}$
$\displaystyle\mathrm{collapse}{}(s)\mathrel{\mathop{:}}=$
$\displaystyle\begin{cases}w_{1}:w_{2}:\ldots:w_{r}&\text{if
}\mathrm{CLvl}(s)=2,\mathrm{CLnk}(s)=r>0\\\ {\mathrm{pop}_{1}}(s)&\text{if
}\mathrm{CLvl}(s)=1\\\ \text{undefined}&\text{otherwise}\end{cases}$

The _set of level $2$-operations_ is
$\mathrm{OP}\mathrel{\mathop{:}}=\left\\{\mathrm{push}_{\sigma,1},\mathrm{push}_{\sigma,2},{\mathrm{clone}_{2}},{\mathrm{pop}_{1}},{\mathrm{pop}_{2}},\mathrm{collapse}{}\right\\}$.
The _set of level $2$ stacks_, $\mathrm{Stck}(\Sigma)$, is the smallest set
that contains $\bot_{2}$ and is closed under all operations from
$\mathrm{OP}$.

Note that $\mathrm{collapse}$\- and ${\mathrm{pop}_{k}}$-operations are only
allowed if the resulting stack is in $(\Sigma^{+})^{+}$. This avoids the
special treatment of empty words or stacks. Furthermore, a $\mathrm{collapse}$
on level $2$ summarises a non-empty sequence of
${\mathrm{pop}_{2}}$-operations. For example, starting from $\bot_{2}$, we can
apply a ${\mathrm{clone}_{2}}$, a $\mathrm{push}_{\sigma,2}$, a
${\mathrm{clone}_{2}}$, and finally a $\mathrm{collapse}$. This sequence first
creates a level $2$ stack that contains $3$ words and then performs the
collapse and ends in the initial stack again. This example shows that
${\mathrm{clone}_{2}}$-operations are responsible for the fact that collapse-
operations on level $2$ may remove more than one word from the stack.

For $s,s^{\prime}\in\mathrm{Stck}(\Sigma)$, we call $s^{\prime}$ a substack of
$s$ if there are $n_{1},n_{2}\in\mathbb{N}$ such that
$s^{\prime}={\mathrm{pop}_{1}}^{n_{1}}({\mathrm{pop}_{2}}^{n_{2}}(s))$. We
write $s^{\prime}\leq s$ if $s^{\prime}$ is a substack of $s$.

###  3.2. Collapsible Pushdown Systems and Collapsible Pushdown Graphs

Now we introduce collapsible pushdown systems and graphs (of level $2$) which
are analogues of pushdown systems and pushdown graphs using collapsible
pushdown stacks instead of ordinary stacks.

######  Definition 3.1.

A _collapsible pushdown system_ of level $2$ ($\mathrm{CPS}$) is a tuple
$S=(\Sigma,Q,\Delta,q_{0})$ where $\Sigma$ is a finite stack alphabet with
$\bot\in\Sigma$, $Q$ a finite set of states, $q_{0}\in Q$ the initial state,
and $\Delta\subseteq Q\times\Sigma\times Q\times\mathrm{OP}$ the transition
relation.

For $q\in Q$ and $s\in\mathrm{Stck}(\Sigma)$ the pair $(q,s)$ is called a
_configuration_. We define labelled transitions on pairs of configurations by
setting $(q_{1},s)\mathrel{{\vdash^{(q_{2},op)}}}(q_{2},t)$ if there is a
$(q_{1},\sigma,q_{2},op)\in\Delta$ such that $\mathrm{Sym}(s)=\sigma$ and
$op(s)=t$. The union of the labelled transition relations is denoted as
$\mathrel{{\vdash}}\mathrel{\mathop{:}}=\bigcup_{l\in
Q\times\mathrm{OP}}\mathrel{{\vdash^{l}}}$. We set $C(S)$ to be the set of all
configurations that are reachable from $(q_{0},\bot_{2})$ via
$\mathrel{{\vdash}}$-paths. We call $C(S)$ the set of _reachable_ or _valid_
configurations. The _collapsible pushdown graph ( $\mathrm{CPG}$) generated by
$S$_ is

$\displaystyle\mathrm{CPG}(S)\mathrel{\mathop{:}}=\left(C(S),(C(S)^{2}\cap\mathrel{{\vdash^{\ell}}})_{\ell\in
Q\times\mathrm{OP}}\right)$

######  Example 3.2.

The following example of a collapsible pushdown graph of level $2$ is taken
from [6]. Let
$Q\mathrel{\mathop{:}}=\\{0,1,2\\},\Sigma\mathrel{\mathop{:}}=\\{\bot,a\\}$,
and $\Delta$ given by $(0,*,1,{\mathrm{clone}_{2}})$,
$(1,*,0,\mathrm{push}_{a,2})$, $(1,*,2,\mathrm{push}_{a,2})$,
$(2,a,2,{\mathrm{pop}_{1}})$, and $(2,a,0,\mathrm{collapse})$, where $*$
denotes any letter in $\Sigma$. In our picture (see Figure 1), the labels are
abbreviated as follows:
$\mathrm{cl}\mathrel{\mathop{:}}=(1,{\mathrm{clone}_{2}})$,
$a\mathrel{\mathop{:}}=(0,\mathrm{push}_{a,2})$,
$a^{\prime}\mathrel{\mathop{:}}=(2,\mathrm{push}_{a,2})$,
$p\mathrel{\mathop{:}}=(2,{\mathrm{pop}_{1}})$, and
$\mathrm{co}\mathrel{\mathop{:}}=(0,\mathrm{collapse})$.

$\textstyle{0,\bot\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathrm{cl}}$$\textstyle{1,\bot:\bot\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{a}$$\scriptstyle{a^{\prime}}$$\textstyle{0,\bot:\bot
a\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathrm{cl}}$$\textstyle{1,\bot:\bot
a:\bot
a\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{a}$$\scriptstyle{a^{\prime}}$$\textstyle{0,\bot:\bot
a:\bot
aa\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathrm{cl}}$$\textstyle{1,\bot:\bot
a:\bot aa:\bot
aa\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{a^{\prime}}$$\scriptstyle{a}$$\textstyle{\ldots}$$\textstyle{2,\bot:\bot
a\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{p}$$\scriptstyle{\mathrm{co}}$$\textstyle{2,\bot:\bot
a:\bot
aa\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{p}$$\scriptstyle{\mathrm{co}}$$\textstyle{2,\bot:\bot
a:\bot aa:\bot
aaa\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{p}$$\scriptstyle{\mathrm{co}}$$\textstyle{\ldots}$$\textstyle{2,\bot:\bot}$$\textstyle{2,\bot:\bot
a:\bot
a\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{p}$$\scriptstyle{\mathrm{co}}$$\textstyle{2,\bot:\bot
a:\bot aa:\bot
aa\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{p}$$\scriptstyle{\mathrm{co}}$$\textstyle{\ldots}$$\textstyle{2,\bot:\bot
a:\bot}$$\textstyle{2,\bot:\bot a:\bot aa:\bot
a\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{p}$$\scriptstyle{\mathrm{co}}$$\textstyle{\ldots}$$\textstyle{2,\bot:\bot
a:\bot aa:\bot}$$\textstyle{\ldots}$

Figure 1. Example of a collapsible pushdown graph

######  Remark 3.3.

Hague et al. [6] showed that modal $\mu$-calculus model checking on level $n$
$\mathrm{CPG}$ is $n$-EXPTIME complete. Note that there is an $\mathrm{MSO}$
interpretation which turns the graph of the previous example into a grid-like
structure. Hence its $\mathrm{MSO}$ theory is undecidable.

The next definition introduces runs of collapsible pushdown systems.

######  Definition 3.4.

Let $S$ be a $\mathrm{CPS}$. A run $r$ of $S$ of length $n$ is a function

$r:\\{0,1,2,\ldots,n\\}\rightarrow
Q\times(\Sigma\times\\{1,2\\}\times\mathbb{N})^{*2}\text{ such that
}r(0)\mathrel{{\vdash}}r(1)\mathrel{{\vdash}}\cdots\mathrel{{\vdash}}r(n).$

We write $\mathrm{ln}(r)\mathrel{\mathop{:}}=n$ and call $r$ a run from $r(0)$
to $r(n)$. We say $r$ visits a stack $s$ at $i$ if $r(i)=(q,s)$.

For runs $r,r^{\prime}$ of length $n$ and $m$, respectively, with
$r(n)=r^{\prime}(0)$, we define the composition $r\circ r^{\prime}$ of $r$ and
$r^{\prime}$ in the obvious manner.

######  Remark 3.5.

Note that we do not require runs to start in the initial configuration.

##  4\. Encoding of Collapsible Pushdown Graphs in Trees

In this section we prove that $\mathrm{CPG}$ are tree-automatic. For this
purpose we have to encode stacks in trees. The idea is to divide a stack into
_blocks_ and to encode different blocks in different subtrees. The crucial
observation is that every stack is a list of words that share the same first
letter. A block is a maximal list of words in the stack that share the same
two first letters222see Figure 2 for an example of blocks and Definition 4.1
for their formal definition. If we remove the first letter of every word of
such a block, the resulting $2$-word decomposes again as a list of blocks.
Thus, we can inductively carry on to decompose parts of a stack into blocks
and code every block in a different subtree. The roots of these subtrees are
labelled with the first letter of the corresponding block. This results in a
tree in which every initial left-closed path represents one word of the stack.
By left-closed, we mean that the last element of the path has no left
successor.

It turns out that – via this encoding – each stack operation corresponds to a
simple $\mathrm{MSO}$-definable tree-operation. The main difficulty is to
provide a tree-automaton that checks whether there is a run to the
configuration represented by some tree. This problem is addressed in Section
5.

As already mentioned, the encoding works by dividing stacks into blocks. The
following definition makes our notion of blocks precise. For $w\in\Sigma^{*}$
and $s=w_{1}:w_{2}:\ldots:w_{n}\in\Sigma^{*2}$, we write
$s^{\prime}\mathrel{\mathop{:}}=w\mathrel{\backslash}s$ for
$s^{\prime}=[ww_{1}]:[ww_{2}]:\ldots:[ww_{n}]$.

$\textstyle{f}$$\textstyle{e}$$\textstyle{g}$$\textstyle{i}$$\textstyle{b}$$\textstyle{d}$$\textstyle{d}$$\textstyle{d}$$\textstyle{h}$$\textstyle{j}$$\textstyle{l}$$\textstyle{a}$$\textstyle{c}$$\textstyle{c}$$\textstyle{c}$$\textstyle{c}$$\textstyle{c}$$\textstyle{c}$$\textstyle{k}$$\textstyle{\bot}$$\textstyle{\bot}$$\textstyle{\bot}$$\textstyle{\bot}$$\textstyle{\bot}$$\textstyle{\bot}$$\textstyle{\bot}$$\textstyle{\bot}$

Figure 2. Example of blocks in a stack. These form a $c$-blockline.

######  Definition 4.1 ($\sigma$-block(line)).

For $\sigma\in\Sigma$, we call $b\in\Sigma^{*2}$ a _$\sigma$ -block_ if
$b=[\sigma]$ or $b=\sigma\tau\mathrel{\backslash}s^{\prime}$ for some
$\tau\in\Sigma$ and $s^{\prime}\in\Sigma^{*2}$. See Figure 2 for examples of
blocks. If $b_{1},b_{2},\ldots,b_{n}$ are $\sigma$-blocks, then we call
$b_{1}:b_{2}:\ldots:b_{n}$ a _$\sigma$ -blockline_.

Note that every stack in $\mathrm{Stck}(\Sigma)$ forms a
$(\bot,1,0)$-blockline. Furthermore, every blockline $l$ decomposes uniquely
as $l=b_{1}:b_{2}:\ldots:b_{n}$ of maximal blocks $b_{i}$ in $l$. Another
crucial observation is that a $\sigma$-block $b\in\Sigma^{*2}\setminus\Sigma$
decomposes as $b=\sigma\mathrel{\backslash}l$ for some blockline $l$ and we
say $l$ is the induced blockline of $b$. For $b\in\Sigma$ the induced
blockline of $[b]$ is just the empty $2$-word.

Now we encode a $(\sigma,n,m)$-blockline $l$ in a tree by labelling the root
with $(\sigma,n)$, by encoding the blockline induced by the first block of $l$
in the left subtree, and by encoding the rest of the blockline in the right
subtree. In order to avoid repetitions, we do not repeat the symbol
$(\sigma,n)$ in the right subtree, but replace it by the default letter
$\varepsilon$.

######  Definition 4.2.

Let
$s=w_{1}:w_{2}:\ldots:w_{n}\in(\Sigma\times\\{1,2\\}\times\mathbb{N})^{+2}$ be
a $(\sigma,l,k)$-blockline. Let $w_{i}^{\prime}$ be words such that
$s=(\sigma,l,k)\mathrel{\backslash}[w_{1}^{\prime}:w_{2}^{\prime}:\ldots:w_{n}^{\prime}]$
and set
$s^{\prime}\mathrel{\mathop{:}}=w_{1}^{\prime}:w_{2}^{\prime}:\ldots:w_{n}^{\prime}$.
As an abbreviation we write
${}_{h}s_{i}\mathrel{\mathop{:}}=w_{h}:w_{h+1}:\ldots:w_{i}$. Furthermore, let
$w_{1}:w_{2}:\ldots:w_{j}$ be a maximal block of $s$. Note that $j>1$ implies
$w_{j^{\prime}}=(\sigma,l,k)(\sigma^{\prime},l^{\prime},k^{\prime})w_{j^{\prime}}^{\prime\prime}$
for all $j^{\prime}\leq j$, some fixed
$(\sigma^{\prime},l^{\prime},k^{\prime})\in\Sigma\times\\{1,2\\}\times\mathbb{N}$,
and appropriate $w_{j^{\prime}}^{\prime\prime}\in\Sigma^{*}$. For
$\rho\in\big{(}\Sigma\times\\{1,2\\}\big{)}\cup\\{\varepsilon\\}$, we define
recursively the
$\big{(}\Sigma\times\\{1,2\\}\big{)}\cup\\{\varepsilon\\}$-labelled tree
$\mathrm{Enc}(s,\rho)$ via

$\displaystyle\mathrm{Enc}(s,\rho)\mathrel{\mathop{:}}=\begin{cases}\rho&\text{if
}\lvert w_{1}\rvert=1,n=1\\\
\rho(\emptyset,{\mathrm{Enc}(_{2}s_{n},\varepsilon)})&\text{if }\lvert
w_{1}\rvert=1,n>1\\\
\rho({\mathrm{Enc}(_{1}s_{n}^{\prime},(\sigma^{\prime},l^{\prime}))},\emptyset)&\text{if
}j=n,\lvert w_{1}\rvert>1\\\
\rho({\mathrm{Enc}(_{1}s_{j}^{\prime},(\sigma^{\prime},l^{\prime}))},{\mathrm{Enc}(_{j+1}s_{n},\varepsilon)})&\text{otherwise.}\end{cases}$

$\mathrm{Enc}(s)\mathrel{\mathop{:}}=\mathrm{Enc}(s,(\bot,1))$ is called the
(tree-)encoding of the stack $s\in\mathrm{Stck}(\Sigma)$.

Figure 3 shows a configuration and its encoding.

$\textstyle{(c,2,1)}$$\textstyle{(e,1,3)}$$\textstyle{(b,2,0)}$$\textstyle{(b,2,0)}$$\textstyle{(c,1,2)}$$\textstyle{(d,2,3)}$$\textstyle{(a,2,0)}$$\textstyle{(a,2,0)}$$\textstyle{(a,2,2)}$$\textstyle{(a,2,2)}$$\textstyle{(a,2,2)}$$\textstyle{(\bot,1,0)}$$\textstyle{(\bot,1,0)}$$\textstyle{(\bot,1,0)}$$\textstyle{(\bot,1,0)}$$\textstyle{(\bot,1,0)}$
$\textstyle{c,2}$$\textstyle{e,1}$$\textstyle{b,2\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\varepsilon\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{c,1}$$\textstyle{d,2\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{a,2\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{a,2\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\varepsilon\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\varepsilon}$$\textstyle{\bot,1\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\varepsilon\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$

Figure 3. A stack $s$ and its encoding $\mathrm{Enc}(s)$: right arrows lead to
$1$-successors (right successors), upward arrows lead to $0$-successors (left
successors).

######  Remark 4.3.

In this encoding, the first block of a $(\sigma,l,k)$-blockline is encoded in
a subtree whose root $d$ is labelled $(\sigma,l)$. We can restore $k$ from the
position of $d$ in the tree $\mathrm{Enc}(s)$ as follows. If $l=1$ then
$k=\lvert d\rvert_{0}$, i.e., the number of occurrences of $0$ in $d$. This is
due to the fact that level $1$ links always point to the preceding letter and
that we always introduce a left-successor tree in order to encode letters that
are higher in the stack.

The case $l=2$ needs some closer inspection. Assume that some $d\in
T:=\mathrm{Enc}(s)$ is labelled $(\sigma,2)$. Then it encodes a letter
$(\sigma,2,k)$ and this is not a cloned element. Thus, $k$ equals the numbers
of words to the left of this letter $(\sigma,2,k)$. We claim that
$k=\left\lvert\big{\\{}e\in
T\cap\\{0,1\\}^{*}1:e\leq_{lex}d\big{\\}}\right\rvert$. The existence of a
pair $e,e1\in T$ corresponds to the fact that there is some blockline
consisting of blocks $b_{1}:b_{2}:\ldots:b_{n}$ with $n\geq 2$ such that
$b_{1}$ is encoded in ${T}_{e}\setminus{T}_{e1}$ and $b_{2}:\ldots:b_{n}$ is
encoded in ${T}_{e1}$. By induction, one easily sees that for each such pair
$e,e1\in T$ all the letters that are in words left of the letter encoded by
$e1$ are encoded in lexicographically smaller elements. Furthermore, the size
of $((0^{*})1)^{*}\cap T$ corresponds to the number of words in $s$ since the
introduction of a $1$-successor corresponds to the separation of the first
block of some blockline from the other blocks. Each of these separation can
also be seen as the separation of the last word of the first block from the
first word of the second block of this blockline. Note that we separate two
words that are next to each other in exactly one blockline. Putting these
facts together our claim is proved.

Another view on this correspondence is the bijection $f:\\{1,2,\ldots,\lvert
s\rvert\\}\rightarrow R$ where $R:=((0^{*})1)^{*}\cap\text{dom}(T)$ and $i$ is
mapped to the $i$-th element of $R$ in lexicographic order. $f(i)$ is exactly
the position where the $(i-1)$-st word is separated from the $i$-th one for
all $i\geq 2$. In order to state the properties of $f$, we need some more
notation. We write $\pi$ for the canonical projection
$\pi:(\Sigma\times\\{1,2\\}\times\mathbb{N})^{*}\rightarrow(\Sigma\times\\{1,2\\})^{*}$
and $w_{i}$ for the $i$-th word of $s$. Furthermore, let $w_{i}^{\prime}$ be a
word such that, $w_{i}=(w_{i}\sqcap w_{i-1})\circ w_{i}^{\prime}$ (here we set
$w_{0}:=\varepsilon$). Then the word along the path333By the word along a path
from one node to another we mean the word consisting of the non
$\varepsilon$-labels along this path. from the root to $f(i)$ is exactly
$\pi(w_{i}\sqcap w_{i-1})$ for all $2\leq i\leq\lvert s\rvert$ and the path
from $f(j)$ to $f(j)\circ 0^{m}$ for maximal $m\in\mathbb{N}$ is
$\pi(w_{j}^{\prime})$ for all $1\leq j\leq\lvert s\rvert$.

In order to encode a configuration $c:=(q,s)$, we add $q$ as a new root of the
tree and attach the encoding of $s$ as the left subtree, i.e.,
$\mathrm{Enc}(c)\mathrel{\mathop{:}}=q({\mathrm{Enc}(s)},\emptyset)$.

The image of this encoding function contains only trees of a very specific
type. We call this class $\mathbb{T}_{\mathrm{Enc}}$. In the next definition
we state the characterising properties of $\mathbb{T}_{\mathrm{Enc}}$. This
class is $\mathrm{MSO}$ definable, whence automata-recognisable.

######  Definition 4.4.

Let $\mathbb{T}_{\mathrm{Enc}}$ be the class of all trees $T$ that satisfy the
following conditions.

  1. (1)

The root of $T$ is labelled by some element of $Q$ ($T(\varepsilon)\in Q$).

  2. (2)

Every element of the form $\\{0,1\\}^{*}0$ is labelled by some
$(\sigma,l)\in\Sigma\times\\{1,2\\}$; especially, $T(0)=(\bot,1)$ and there
are no other occurrences of $(\bot,1)$ or $(\bot,2)$.

  3. (3)

Every element of the form $\\{0,1\\}^{*}1$ is labelled by $\varepsilon$.

  4. (4)

$1\notin\text{dom}(T)$, $0\in\text{dom}(T)$.

  5. (5)

For all $t\in T$, if $T(t0)=(\sigma,1)$ then $T(t10)\neq(\sigma,1)$.

######  Remark 4.5.

Note that (5) holds as $T(t0)=T(t10)=(\sigma,1)$ would imply that the subtree
rooted at $t$ encodes a blockline $l$ such that the first block of $l$ induces
a $(\sigma,1,n)$-blockline and the second one induces a
$(\sigma,1,m)$-blockline. But as level $1$ links always point to the preceding
letter, $n$ and $m$ are equal to the length of the prefix of $l$ in the stack
plus $1$, i.e., if $T$ encodes a stack $s$ then
$s=s_{1}:[w\mathrel{\backslash}l]:s_{2}$ and $n=m=\lvert w\rvert+1$. This
would contradict the maximality of the blocks in the encoding.

######  Remark 4.6.

$\mathrm{Enc}:Q\times\mathrm{Stck}(\Sigma)\rightarrow\mathbb{T}_{\mathrm{Enc}}$
is a bijection and we denote its inverse by $\mathrm{Dec}$.

Our encoding turns the transitions of a $\mathrm{CPG}$ into regular tree-
operations. The tree-operations corresponding to ${\mathrm{pop}_{2}}$ and
$\mathrm{collapse}$ can be seen in Figures 4 and 5. For the
${\mathrm{pop}_{2}}$, note that if $v_{1}$ is the $0$-successor of $v_{0}$
then $v_{0}$ and $v_{1}$ encode symbols in the same word of the encoded stack.
As a ${\mathrm{pop}_{2}}$ removes the rightmost word, we have to remove all
the nodes encoding information about this word. As the rightmost leaf
corresponds to the topmost symbol of the stack, we have to remove this leaf
and all its $0$-ancestors.

For the $\mathrm{collapse}$ (on level $2$), we note that each $\varepsilon$
represents a cloned element. The $\mathrm{collapse}$ induced by such an
element produces the same stack as a ${\mathrm{pop}_{2}}$ of its original
version. The original symbol of the rightmost leaf is its first ancestor not
labelled by $\varepsilon$.

Note that the operations corresponding to ${\mathrm{pop}_{2}}$ and
$\mathrm{collapse}$ are clearly $\mathrm{MSO}$ definable. All other
transitions in $\mathrm{CPG}$ correspond to $\mathrm{MSO}$ definable tree-
operations, too. Due to space restrictions we skip the details.

$(\sigma,l)$$\varepsilon$$\ldots$$\varepsilon$$\varepsilon$$(\tau,k)$$\vdots$$(\sigma^{\prime},l^{\prime})$$(\sigma,l)$$\varepsilon$$\ldots$$\varepsilon$
Figure 4. ${\mathrm{pop}_{2}}$-operation
$\vdots$$(\sigma,2)$$\varepsilon$$\ldots$$\varepsilon$$\varepsilon$ Figure 5.
$\mathrm{collapse}$-operation of level $2$.

######  Lemma 4.7.

Let $C$ be the set of encodings of configurations of a $\mathrm{CPS}$ $S$.
Then there are automata $A_{(q,\mathrm{op})}$ for all $q\in Q$ and all
$\mathrm{op}\in\mathrm{OP}$ such that for all $c_{1},c_{2}\in C$

$A_{(q,\mathrm{op})}\text{ accepts
}\mathrm{Enc}(c_{1})\otimes\mathrm{Enc}(c_{2})\text{\quad
iff\quad}c_{1}\mathrel{{\vdash^{(q,\mathrm{op})}}}c_{2}\enspace.$

##  5\. Recognising Reachable Configurations

We show that $\mathrm{Enc}$ maps the reachable configurations of a given
$\mathrm{CPS}$ to a regular set. For this purpose we introduce milestones of a
stack $s$. It turns out that these are exactly those substacks of $s$ that
every run to $s$ has to visit. Furthermore, the milestones of $s$ are
represented by the nodes of $\mathrm{Enc}(s)$: with every
$d\in\mathrm{Enc}(s)$, we can associate a subtree of $s$ which encodes a
milestone. Furthermore, the substack relation on the milestones corresponds
exactly to the lexicographical order $\leq_{lex}$ of the elements of
$\mathrm{Enc}(s)$. For every $d\in\mathrm{Enc}(s)$ we can guess the state in
which the corresponding milestone is visited for the last time by some run to
$s$ and we can check the correctness of this guess using $\mathrm{MSO}$ or,
equivalently, tree-automata.

We prove that we can check the correctness of such a guess by introducing a
special type of run, called _loop_ , which is basically a run that starts and
ends with the same stack. A run from one milestone to the next will mainly
consist of loops combined with a finite number of stack operations.

###  5.1. Milestones

######  Definition 5.1 (Milestone).

A substack $s^{\prime}$ of $s=w_{1}:w_{2}:\ldots:w_{n}$ is a _milestone_ if
$s^{\prime}=w_{1}:w_{2}:\ldots:w_{i}:w^{\prime}$ such that $0\leq i<n$ and
$w_{i}\sqcap w_{i+1}\leq w^{\prime}\leq w_{i+1}$. We denote by
$\mathrm{MS}(s)$ the set of milestones of $s$.

Note that the substack relation $\leq$ linearly orders $\mathrm{MS}(s)$.

######  Lemma 5.2.

If $s,t,m$ are stacks with $m\in\mathrm{MS}(t)$ but $m\not\leq s$, then every
run from $s$ to $t$ visits $m$. Thus, for every run $r$ from the initial
configuration to $s$, the function

$\displaystyle f:\mathrm{MS}(s)\rightarrow\text{dom}(r),$ $\displaystyle
s^{\prime}\mapsto\max\\{i\in\text{dom}(r):r(i)=(q,s^{\prime})\text{ for some
}q\in Q\\}$

is an order embedding with respect to substack relation on the milestones and
the natural order of $\text{dom}(r)$.

In order to state the close correspondence between milestones of a stack $s$
and the elements of $\mathrm{Enc}(s)$, we need the following definition.

######  Definition 5.3.

Let $T\in\mathbb{T}_{\mathrm{Enc}}$ be a tree and $d\in
T\setminus\\{\varepsilon\\}$. Then the _left and downward closed tree induced
by $d$_ is $LT({d,T})\mathrel{\mathop{:}}=T{\restriction}_{D}$ where
$D\mathrel{\mathop{:}}=\\{d^{\prime}\in
T:d^{\prime}\leq_{lex}d\\}\setminus\\{\varepsilon\\}$. Then we denote by
$\mathrm{LStck}(d,T)\mathrel{\mathop{:}}=\mathrm{Dec}(LT({d,T}))$ the _left
stack induced by $d$_.

######  Remark 5.4.

$\mathrm{LStck}(d,s)$ is a substack of $s$ for all
$d\in\text{dom}(\mathrm{Enc}(s))$. This observation follows from Remark 4.3
combined with the fact that the left stack is induced by a lexicographically
downward closed subset. In fact, $\mathrm{LStck}(d,s)$ is a milestone of $s$.

######  Lemma 5.5.

The map given by $g:d\mapsto\mathrm{LStck}(d,\mathrm{Enc}(s))$ is an order
isomorphism between
$\left(\text{dom}(\mathrm{Enc}(q,s))\setminus\\{\varepsilon\\},\leq_{lex}\right)$
and $\left(\mathrm{MS}(s),\leq\right)$.

Lemmas 5.5 and 5.2 imply that every run $r$ decomposes as $r=r_{1}\circ
r_{2}\circ\ldots\circ r_{n}$ where $r_{i}$ is a run from the $i$-th milestone
of $r(\mathrm{ln}(r))$ to the $(i+1)$-st milestone.

In order to describe the structure of the $r_{i}$, we have to introduce the
notion of a loop. Informally speaking, a loop is a run $r$ that starts and
ends with the same stack $s$ and which does not look too much into $s$.

######  Definition 5.6.

Let $r$ be a run of length $n$ with $r(i)=(q_{i},s_{i})$ for all $0\leq i\leq
n$.

  * •

$r$ is called a _simple high loop_ if $s_{0}=s_{n}$ and if $s_{0}<s_{i}$ for
all $0<i<n$.

  * •

$r$ is called a _simple low loop_ of $s$ if $s_{0}=s_{n}=s$, between $0$ and
$n$ the stack $s$ is never visited, $s_{1}={\mathrm{pop}_{1}}(s)$,
$\mathrm{CLvl}(s)=1$, $\lvert s_{i}\rvert\geq\lvert s\rvert$ for all $0\leq
i\leq n$, and $r{\restriction_{[2,n-1]}}$ is the composition of simple low
loops and simple high loops of ${\mathrm{pop}_{1}}(s)$.

  * •

$r$ is called _loop_ if it is a finite composition of low loops and high
loops.

######  Lemma 5.7.

Let $s$ be some stack, $m_{1},m_{2}$ milestones of $s$, and $r$ a run from
$m_{1}$ to $m_{2}$ that never visits any other milestone of $s$. Then either
$r=l_{1}\circ p\circ l_{2}$ or $r=l_{0}\circ c\circ l_{1}\circ p_{1}\circ
l_{2}\circ p_{2}\circ l_{3}\circ\ldots\circ p_{n}\circ l_{n+1}$ where each
$l_{i}$ is a loop, and all $p_{i},p$, and $c$ are runs of length $1$, $p$
performs one $\mathrm{push}_{\sigma,k}$, $c$ performs one
${\mathrm{clone}_{2}}$, and the $p_{i}$ perform one ${\mathrm{pop}_{1}}$ each.

This lemma motivates why we only define low loops for stacks $s$ with
$\mathrm{CLvl}(s)=1$. Whenever the topmost symbol of a milestone $m$ is not a
cloned element, then ${\mathrm{pop}_{1}}(m)$ is another milestone. Hence, the
$l_{i}$ can only contain low loops if they start at a stack with cloned
topmost symbol. But any stack $s$ with cloned topmost symbol and
$\mathrm{CLvl}(s)=2$ cannot be restored from ${\mathrm{pop}_{1}}(s)$ without
passing ${\mathrm{pop}_{2}}(s)$ since a $\mathrm{push}_{\sigma,2}$-operation
would create the wrong link-level.

From Lemma 5.7 we can derive that deciding whether there is a run from one
milestone to the next is possible if we know the pairs of initial and final
states of loops of certain stacks $s$. Hence we are interested in the sets
$\mathrm{Loops}(s)\subseteq Q\times Q$ with
$(q_{1},q_{2})\in\mathrm{Loops}(s)$ if and only if there is a loop from
$(q_{1},s)$ to $(q_{2},s)$. The crucial observation is that
$\mathrm{Loops}(s)$ may be calculated by a finite automaton reading
$\mathrm{top}_{2}(s)$.

######  Lemma 5.8.

For every $\mathrm{CPS}$ there exists a finite automaton $A$ that
calculates444 We consider the final state reached by $A$ on input $w$ as the
value it calculates for $w$. on input $w\in(\Sigma\times\\{1,2\\})^{*}$ the
set $\mathrm{Loops}(s)$ for all stacks $s$ such that
$w=\pi(\mathrm{top}_{2}(s))$. Here,
$\pi:(\Sigma\times\\{1,2\\}\times\mathbb{N})^{*}\rightarrow(\Sigma\times\\{1,2\\})^{*}$
is the projection onto the symbols and collapse-levels.

###  5.2. Detection of Reachable Configurations

We have already seen that every run to a valid configuration $(q,s)$ passes
all the milestones of $s$. Now, we use the last state in which a run $r$ to
$(q,s)$ visits each milestone as a certificate for the reachability of
$(q,s)$. To be precise, _a certificate for the reachability of $(q,s)$_ is a
map
$f:\text{dom}\big{(}\mathrm{Enc}(q,s)\big{)}\setminus\\{\varepsilon\\}\rightarrow
Q$ such that there is some run $r$ from $\bot_{2}$ to $(q,s)$ and $f(d)=q$ if
and only if $r(i)=\big{(}q,\mathrm{LStck}(d)\big{)}$ for $i$ the maximal
position in $r$ where $\mathrm{LStck}(d)$ is visited.

######  Lemma 5.9.

For every $\mathrm{CPG}$ $G$, there is a tree-automaton that checks for each
map

$\displaystyle f:\text{dom}(\mathrm{Enc}(q,s))\setminus\\{\varepsilon\\}$
$\displaystyle\rightarrow Q$

whether $f$ is a certificate of the reachability of $(q,s)$, i.e., whether $f$
is induced by some run $r$ from the initial configuration to $(q,s)$.

The proof of the lemma uses Lemma 5.8 and the fact that the path from the root
to some $d\in\mathrm{Enc}(s)$ encodes the topmost word of
$\mathrm{LStck}(d,\mathrm{Enc}(s))$. Hence, a tree automaton reading
$\mathrm{Enc}(s)$ is able to calculate for each position $d\in\mathrm{Enc}(s)$
the pairs of initial and final states of loops of $\mathrm{LStck}(d)$. As
every run decomposes as a sequence of loops separated by a single operation,
knowing $\mathrm{Loops}(s^{\prime})$ for each $s^{\prime}\leq s$ enables the
automaton to check the correctness of a candidate for a certificate of
reachability.

As a tree-automaton may non-deterministically guess a certificate of the
reachability of a configuration, the encodings of reachable configurations
form a regular set.

###  5.3. Extension to Regular Reachability

By now, we have already established the tree-automaticity of each
$\mathrm{CPG}$ $G$ since we have seen that our encoding yields a regular image
of the vertices of $G$ and the transition relations are turned into regular
relations of the tree encoding. Using similar techniques, we can improve this
result:

######  Theorem 5.10.

If $G$ is the $\varepsilon$-closure of some $\mathrm{CPG}$ $G^{\prime}$ then
$(G,\mathrm{Reach})$ is tree-automatic where $\mathrm{Reach}$ is the binary
predicate that is true on a pair $(c_{1},c_{2})$ of configurations if there is
a path from $c_{1}$ to $c_{2}$ in $G$.

######  Remark 5.11.

Each graph in the second level of the Caucal-hierarchy can be obtained as the
$\varepsilon$-contraction of some level $2$ $\mathrm{CPG}$ (see [3]) whence
all these graphs are tree-automatic.

For a $\mathrm{CPS}$ $S$ let $R\subseteq\Delta^{*}$ be a regular language over
the transitions of $S$. As collapsible pushdown graphs are closed under
products with finite automata even the reachability predicate
$\mathrm{Reach}_{R}$ with restriction to $R$ is tree-automatic. Here,
$\mathrm{Reach}_{R}xy$ holds if there is a path from $x$ to $y$ in
$\mathrm{CPG}(S)$ that uses a sequence of transitions in $R$. If $A$ is the
automaton recognising $R$, we obtain that
$\mathrm{Reach}_{R}(q,s)(q^{\prime},s^{\prime})$ holds in $\mathrm{CPG}(S)$
iff
$\mathrm{Reach}\big{(}(q,q_{i}),s\big{)}\big{(}(q^{\prime},q_{f}),s^{\prime}\big{)}$
holds in $\mathrm{CPG}(S\times A)$ where $q_{i}$ is the initial and $q_{f}$
the unique final state of $A$. Using this idea one can define a $\mathrm{CPG}$
$G^{\prime}$ which is basically $\mathrm{CPG}(S\cup(S\times A))$ extended by
transitions from $(q,s)$ to $((q,q_{i}),s)$ and to $((q,q_{f}),s)$.
$\mathrm{CPG}(S)$ as well as $\mathrm{Reach}_{R}$ w.r.t. $\mathrm{CPG}(S)$ are
$\mathrm{FO}[\mathrm{Reach}]$-interpretable in $G^{\prime}$. Hence we obtain:

######  Theorem 5.12.

Given a collapsible pushdown graph of level $2$, its
$\mathrm{FO}[\mathrm{Reach}_{R}]$ theory is decidable for each regular
$R\subseteq\Delta^{*}$.

###  5.4. Computation of concrete tree-automatic representations of CPG

Up to now, we have only seen that there is a tree-automatic representation for
each $\mathrm{CPG}$. For computing a concrete representation, we rely on the
following lemma.

######  Lemma 5.13.

Given some $\mathrm{CPS}$ $S=(\Gamma,Q,\Delta,q_{0})$, some $q\in Q$, and some
stack $s$, it is decidable whether $(q,s)$ is a vertex of $\mathrm{CPG}(S)$.

The proof is based on the idea that a stack is uniquely determined by its top
element and the information which substacks can be reached via
$\mathrm{collapse}$\- and ${\mathrm{pop}_{i}}$-operations. Hence we can
construct an extension $S^{\prime}$ of $S$ and a modal formula $\varphi_{q,s}$
such that there is some element $v\in\mathrm{CPG}(S^{\prime})$ satisfying
$\mathrm{CPG}(S^{\prime}),v\models\varphi_{q,s}$ iff
$(q,s)\in\mathrm{CPG}(S)$. $S^{\prime}$ basically contains new states for
every substack of $s$ and connects the different states via the appropriate
${\mathrm{pop}_{i}}$-operations which are only applied if the topmost symbol
of the stack agrees with the symbol we would expect when starting the
${\mathrm{pop}_{i}}$-sequence in configuration $(q,s)$.

From this lemma we can derive the computability of the automata in Lemma 5.8.
Having obtained these automata, the construction of a tree-automatic
representation of some $\mathrm{CPG}$ is directly derived from the proofs
yielding the following theorem.

######  Theorem 5.14.

There is an algorithm that, given a level $2$ $\mathrm{CPG}$ $G$ and regular
sets $R_{1},\ldots,R_{n}\subseteq\Delta^{*}$, computes a tree-automatic
representation of $(G,\mathrm{Reach}_{R_{1}},\ldots,\mathrm{Reach}_{R_{n}})$.

##  6\. Conclusion

We have seen that level $2$ collapsible pushdown graphs are tree-automatic.
This result holds also if we apply $\varepsilon$-contractions and if we add
regular reachability predicates. This implies that the second level of the
Caucal-hierarchy is tree-automatic. But our result can only be seen as a
starting point for further investigations of the $\mathrm{CPG}$ hierarchy: are
level $3$ collapsible pushdown graphs tree-automatic? We know an example of a
level $5$ $\mathrm{CPG}$ which is not tree-automatic. But even when tree-
automaticity of all $\mathrm{CPG}$ cannot be expected, the question remains
whether all $\mathrm{CPG}$ have decidable $\mathrm{FO}$ theories. In order to
solve this problem one has to come up with new techniques.

A rather general question concerning our result aims at our knowledge about
tree-automatic structures. Recent developments in the string case [9] show the
decidability of rather large extensions of first-order logic for automatic
structures. It would be interesting to clarify the status of the analogous
claims for tree-automatic structures. Positive answers concerning the
decidability of extensions of first-order logic on tree-automatic structures
would give us the corresponding decidability results for collapsible pushdown
graphs of level $2$.

## References

  * [1] R. Alur, S. Chaudhuri, and P. Madhusudan.  Languages of nested trees.  In Proc. 18th International Conference on Computer-Aided Verification, volume 4144 of LNCS, pages 329–342. Springer, 2006.
  * [2] A. Blumensath.  Automatic structures. Diploma thesis, RWTH Aachen, 1999.
  * [3] A. Carayol and S. Wöhrle.  The Caucal hierarchy of infinite graphs in terms of logic and higher-order pushdown automata.  In Proceedings of the 23rd Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2003, volume 2914 of LNCS, pages 112–123. Springer, 2003.
  * [4] D. Caucal.  On infinite terms having a decidable monadic theory.  In MFCS’02, pages 165–176, 2002.
  * [5] J. Doner.  Tree acceptors and some of their applications.  J. Comput. Syst. Sci., 4(5):406–451, 1970.
  * [6] M. Hague, A. S. Murawski, C-H. L. Ong, and O. Serre.  Collapsible pushdown automata and recursion schemes.  In LICS ’08: Proceedings of the 2008 23rd Annual IEEE Symposium on Logic in Computer Science, pages 452–461, 2008.
  * [7] A. Kartzow.  FO model checking on nested pushdown trees.  In MFCS’09, volume 5734 of LNCS, pages 451–463. Springer, 2009.
  * [8] T. Knapik, D. Niwinski, and P. Urzyczyn.  Higher-order pushdown trees are easy.  In FOSSACS’02, volume 2303 of LNCS, pages 205–222. Springer, 2002.
  * [9] D. Kuske.  Theories of automatic structures and their complexity.  In CAI’09, Third International Conference on Algebraic Informatics, volume 5725 of LNCS, pages 81–98. Springer, 2009.
  * [10] A. N. Maslov.  The hierarchy of indexed languages of an arbitrary level.  Sov. Math., Dokl., 15:1170–1174, 1974.
  * [11] A. N. Maslov.  Multilevel stack automata.  Problems of Information Transmission, 12:38–43, 1976.
  * [12] J. W. Thatcher and J. B. Wright.  Generalized finite automata theory with an application to a decision problem of second-order logic.  Mathematical Systems Theory, 2(1):57–81, 1968.