1: \documentclass[11pt,envcountsect,envcountsame]{llncs}

2: 

3: \usepackage{a4wide,amsmath,amssymb,enumerate,gastex}%,pdfsync}

4: 

5: \pagestyle{plain}

6: 

7: \newcommand{\mcA}{{\mathcal{A}}}

8: \newcommand{\mcB}{{\mathcal{B}}}

9: \newcommand{\mcS}{\mathcal{S}}

10: 

11: \newcommand{\dA}{\mathsf{A}}

12: \newcommand{\dB}{\mathsf{B}}

13: \newcommand{\dC}{\mathsf{C}}

14: \newcommand{\dN}{\mathbb{N}}

15: \newcommand{\dT}{\mathsf{T}}

16: 

17: \newcommand{\bin}{\mathrm{bin}}

18: \newcommand{\Decision}{\mathrm{FOMC}}

19: \newcommand{\degree}{\mathrm{deg}}

20: \newcommand{\dom}{\mathrm{dom}}

21: \newcommand{\eq}{\mathrm{eq}}

22: \newcommand{\FO}{\mathrm{FO}}

23: \newcommand{\FOTh}{\mathrm{FOTh}}

24: \newcommand{\modulo}{\mathrm{mod}}

25: \newcommand{\ol}{\overline}

26: \newcommand{\Real}{\mathrm{REAL}}

27: \newcommand{\ul}{\underline}

28: \newcommand{\val}{\mathrm{val}}

29: \newcommand{\rest}{\mathord\restriction}

30: 

31: \begin{document}

32: 

33: \title{Automatic structures of bounded degree revisited}

34: \author{Dietrich Kuske \and Markus Lohrey\thanks{The second author

35:     acknowledges support from the DFG-project GELO.}

36:   \institute{Universit\"at Leipzig, Institut f\"ur Informatik, Germany \\

37:     \email{\{kuske,lohrey\}@informatik.uni-leipzig.de}}}

38: 

39: \maketitle

40: 

41: \begin{abstract}

42:   The first-order theory of a string automatic structure is known to be

43:   decidable, but there are examples of string automatic structures with

44:   nonelementary first-order theories. We prove that the first-order

45:   theory of a string automatic structure of bounded degree is decidable in

46:   doubly exponential space (for injective automatic presentations,

47:   this holds even uniformly). This result is shown to be optimal since

48:   we also present a string automatic structure of bounded degree whose

49:   first-order theory is hard for {\sf 2EXPSPACE}. We prove similar results

50:   also for tree automatic structures. These findings close the gaps

51:   left open in~\cite{Loh03} by improving both, the lower and the

52:   upper bounds.

53: \end{abstract}

54: 

55: \section{Introduction}

56: 

57: The idea of an automatic structure goes back to B\"uchi and Elgot who

58: used finite automata to decide, e.g., Presburger

59: arithmetic~\cite{Elg61}. Automaton decidable theories~\cite{Hod82}

60: and automatic groups~\cite{EpsCHLPT92} are similar concepts. A

61: systematic study was initiated by Khoussainov and Nerode~\cite{KhoN95}

62: who also coined the name ``{\em automatic structure}'' (we prefer the term

63: ``{\em string automatic structures}'' in this paper). In essence, a

64: structure is string automatic if the elements of the universe can be

65: represented as strings from a regular language (an element can be

66: represented by several strings) and every relation of the structure

67: can be recognized by a finite state automaton with several heads that

68: proceed synchronously.  String automatic structures received

69: increasing interest over the last

70: years~\cite{BluG00,KhoR01,IshKR02,BenLSS03,KhoRS03a,%

71:   Kus03,Bar06,KusL08a,KusL08b,Rub08,BarKR08}. One of the main

72: motivations for investigating string automatic structures is that

73: their first-order theories can be decided uniformly (i.e., the input

74: is a string automatic presentation and a first-order sentence). But

75: even the non-uniform first-order theory is far from efficient since

76: there exist string automatic structures with a nonelementary

77: first-order theory. This motivates the search for subclasses of string

78: automatic structures whose first-order theories are elementary. The

79: first such class was identified by the second author in~\cite{Loh03}

80: who showed that the first-order theory of every string automatic

81: structure of \emph{bounded degree} can be decided in triply

82: exponential alternating time with linearly many alternations. A

83: structure has bounded degree, if in its Gaifman graph, the number of

84: neighbors of a node is bounded by some fixed constant. The paper

85: \cite{Loh03} also presents a specific example of a string automatic

86: structure of bounded degree, where the first-order theory is hard for

87: doubly exponential alternating time with linearly many

88: alternations. Hence, an exponential gap between the upper and lower

89: bound remained. An upper bound of 4-fold exponential alternating time

90: with linearly many alternations was shown for \emph{tree automatic

91:   structures} (which are defined analogously to automatic structures

92: using tree automata) of bounded degree. Our paper~\cite{KusL08} proves

93: a triply exponential space bound for the first-order theory of an

94: injective $\omega$-automatic structure (that is defined via

95: B\"uchi-automata) of bounded degree. Here, injectivity means that

96: every element of the structure is represented by a {\em unique}

97: $\omega$-word from the underlying regular language.

98: 

99: In this paper, we achieve three goals: 

100: \begin{itemize}

101: \item We close the complexity gaps from \cite{Loh03} for

102:   string/tree automatic structures of bounded degree.

103: \item We investigate, for the first time, the complexity of the {\em

104:     uniform} first-order theory (where the automatic presentation is

105:   part of the input) of string/tree automatic structures of bounded

106:   degree.

107: \item We refine our complexity analysis using the growth function

108: of a structure. This function measures the size of a sphere in the 

109: Gaifman graph depending on the radius of the sphere. 

110: The growth function of a structure of bounded degree can be at most

111: exponential.

112: \end{itemize}

113: Our main results are the following:

114: \begin{itemize}

115: \item 

116: The uniform first-order theory

117: for injective string automatic presentations is {\sf 2EXPSPACE}-complete.

118: The lower bound already holds in the non-uniform setting, i.e. there

119: exists a string automatic structure of bounded degree with a 

120: {\sf 2EXPSPACE}-complete first-order theory. 

121: \item 

122: For every string automatic structure of bounded degree, where the 

123: growth function is polynomially bounded, the first-order

124: theory is in {\sf EXPSPACE}, and there exists an example with an

125: {\sf EXPSPACE}-complete first-order theory.

126: \item 

127: The uniform first-order theory for injective tree automatic presentations

128: belongs to {\sf 4EXPTIME}; the non-uniform one to {\sf 3EXPTIME} for arbitrary

129: tree automatic structures, and to {\sf 2EXPTIME} if the growth function is

130: polynomial. Our bounds for the non-uniform problem are sharp,

131: i.e., there are tree automatic structures of bounded degree (and

132: polynomial growth) with a {\sf 3EXPTIME}-complete

133: ({\sf 2EXPTIME}-complete, resp.) first-order theory.

134: \end{itemize}

135: We conclude this paper with some results on the complexity of

136: first-order fragments with fixed quantifier alternation depth one or

137: two on string/tree automatic structures of bounded degree. 

138: 

139: \section{Preliminaries}

140: 

141: Let $\Gamma$ be a finite alphabet and $w \in \Gamma^*$ be 

142: a finite word over $\Gamma$. The length of $w$ is denoted by $|w|$.

143: We also write $\Gamma^n = \{ w \in \Gamma^* \mid n=|w|\}$.

144: 

145: Let us define $\exp(0, x) = x$ and $\exp(n+1,x) = 2^{\exp(n,x)}$ for

146: $x \in \mathbb{N}$. We assume that the reader has some basic knowledge

147: in complexity theory, see e.g. \cite{Pap94}.  By Savitch's theorem,

148: $\mathsf{NSPACE}(s(n)) \subseteq \mathsf{DSPACE}(s(n)^2)$ if $s(n) \geq

149: \log(n)$. Hence, we can just write $\mathsf{SPACE}(s(n)^{O(1)})$ for

150: either $\mathsf{NSPACE}(s(n)^{O(1)})$ or $\mathsf{DSPACE}(s(n)^{O(1)})$.

151: For $k \geq 1$, we denote with $k${\sf EXPSPACE} (resp. $k${\sf EXPTIME}) the

152: class of all problems that can be accepted in space (resp. time)

153: $\exp(k,n^{O(1)})$ on a deterministic Turing machine. For {\sf 1EXPSPACE} we

154: write just {\sf EXPSPACE}. A computational problem is called

155: \emph{elementary} if it belongs to $k${\sf EXPTIME} for some $k\in\dN$.

156: 

157: \subsection{Tree and string automata}  \label{S automata}

158: 

159: For our purpose it suffices to consider only tree automata on binary trees.

160: Let $\Gamma$ be a finite alphabet.  A \emph{finite

161:   binary tree} over $\Gamma$ is a mapping $t : \dom(t) \to \Gamma$,

162: where $\dom(t) \subseteq \{0,1\}^*$ is finite, nonempty, and satisfies

163: the following closure condition for all $w \in \{0,1\}^*$: if $\{w0,

164: w1\} \cap \dom(t) \neq \emptyset$, then also $w,w0 \in \dom(t)$.  With

165: $T_\Gamma$ we denote the set of all finite binary trees over~$\Gamma$.

166: A (top-down) \emph{tree automaton over $\Gamma$} is a tuple $A = (Q,

167: \Delta, q_0)$, where $Q$ is the finite set of states, $q_0 \in Q$ is

168: the initial state, and

169: \begin{equation}\label{transition relation}

170: \Delta \subseteq (Q \times \Gamma \times Q

171: \times Q) \cup (Q \times \Gamma \times Q) \cup (Q \times \Gamma)

172: \end{equation}

173: is the non-empty transition relation.  A \emph{successful run} of $A$ on a tree $t$

174: is a mapping $\rho : \dom(t) \to Q$ such that (i) $\rho(\varepsilon) =

175: q_0$ and (ii) for every $w \in \dom(t)$ with children $w0, \ldots, wi$

176: (thus $-1 \leq i \leq 1$) we have

177: $(\rho(w), t(w), \rho(w0), \ldots, \rho(wi)) \in \Delta$.  With

178: $L(A)$ we denote the set of all finite binary trees $t$ such that

179: there exists a successful run of $A$ on~$t$.  A set $L \subseteq

180: T_\Gamma$ is called \emph{regular} if there exists a finite tree

181: automaton $A$ with $L = L(A)$.

182: 

183: A tree $t$ with $\dom(t)\subseteq 0^*$ can be considered as a nonempty

184: string $t(\varepsilon)t(0)t(00)\dots t(0^{n-1})$ with

185: $n=|\dom(t)|$. In the same spirit, a finite \emph{string} automaton

186: can be defined as a tree automaton, where the transition relation

187: $\Delta$ in (\ref{transition relation}) satisfies $\Delta \subseteq (Q

188: \times \Gamma \times Q) \cup (Q \times \Gamma)$.

189: 

190: We will need the following well known facts on string/tree automata:

191: Emptiness (resp. inclusion) of the languages of string automata can be

192: decided in nondeterministic logarithmic space (resp. polynomial space), whereas

193: emptiness (resp. inclusion) of the languages of tree automata can be

194: decided in polynomial time (resp. exponential time), see

195: e.g.~\cite{tata2007}. In all four cases completeness holds.

196: 

197: 

198: \subsection{Structures and first-order logic}

199: 

200: A \emph{signature} is a finite set $\mcS$ of relational symbols, where

201: every symbol $r\in \mcS$ has some fixed arity~$m_r$. The notion of an

202: $\mcS$-structure (or model) is defined as usual in logic. Note that we

203: only consider relational structures. Sometimes, we will also use

204: constants, but in our context, a constant $c$ can be always replaced

205: by the unary relation $\{c\}$. Let us fix an $\mcS$-structure $\mcA =

206: (A, (r^\mcA)_{r\in\mcS})$, where $r^\mcA \subseteq A^{m_r}$.  To

207: simplify notation, we will write $a \in \mcA$ for $a \in A$.  For $B

208: \subseteq A$ we define the restriction ${\mcA}\rest B = (B, (r^\mcA

209: \cap B^{m_r})_{r\in\mcS})$.  Given further constants $a_1, \ldots, a_n

210: \in \mcA$, we write $(\mcA, a_1, \ldots, a_k)$ for the structure $(A,

211: (r^\mcA)_{r\in\mcS}, a_1, \ldots, a_k)$.  In the rest of the paper, we

212: will always identify a symbol $r\in\mcS$ with its interpretation

213: $r^\mcA$.

214: 

215: A {\em congruence} on the structure $\mcA = (A, (r)_{r\in\mcS})$

216: is an equivalence relation $\equiv$ on $A$ such that

217: for every $r \in \mcS$ and all $a_1,b_1, \ldots, a_{m_r}, b_{m_r} \in A$

218: we have: If $(a_1,\ldots, a_{m_r}) \in r$ and $a_1 \equiv b_1,\ldots,

219: a_{m_r} \equiv b_{m_r}$, then also $(b_1,\ldots, b_{m_r}) \in r$.

220: As usual, the equivalence class of $a \in A$ w.r.t. $\equiv$ is 

221: denoted by $[a]_\equiv$ or just $[a]$ and $A/_\equiv$ denotes the set of all 

222: equivalence classes. We define the {\em quotient structure} 

223: $\mcA/_\equiv = (A/_\equiv, (r/_\equiv)_{r\in\mcS})$,

224: where $r/_\equiv = \{ ([a_1], \ldots, [a_{m_r}]) \mid

225: (a_1,\ldots,a_{m_r}) \in r \}$.

226: 

227: 

228: The \emph{Gaifman-graph} $G(\mcA)$ of the $\mcS$-structure $\mcA$ is

229: the following symmetric graph:

230: \[ 

231:   G(\mcA) = (A, \{ (a,b) \in A \times A \mid 

232:    \bigvee_{r\in\mcS} \exists (a_1, \ldots, a_{m_r}) \in r \;

233:     \exists j,k : a_j = a, a_k=b \})\ .

234: \]

235: Thus, the set of nodes is the universe of $\mcA$ and there is an edge

236: between two elements, if and only if they are contained in some tuple

237: belonging to one of the relations of~$\mcA$.  With $d_{\mcA}(a,b)$,

238: where $a,b\in \mcA$, we denote the distance between $a$ and $b$ in

239: $G(\mcA)$, i.e., it is the length of a shortest path connecting $a$

240: and $b$ in $G(\mcA)$.  For $a \in \mcA$ and $d \geq 0$ we denote with

241: $S_{\mcA}(d, a) = \{ b \in A \mid d_{\mcA}(a,b) \leq d\}$ the

242: $d$-sphere around $a$. If $\mcA$ is clear from the context, then we

243: will omit the subscript $\mcA$. We say that the structure $\mcA$ is

244: \emph{locally finite} if its Gaifman graph~$G(\mcA)$ is locally finite

245: (i.e., every node has finitely many neighbors). Similarly, the

246: structure $\mcA$ has \emph{bounded degree}, if $G(\mcA)$ has bounded

247: degree, i.e., there exists a constant~$\delta$ such that every $a \in

248: A$ is adjacent to at most $\delta$ many other nodes in $G(\mcA)$; the

249: minimal such $\delta$ is called the \emph{degree of $\mcA$}.  For a

250: structure $\mcA$ of bounded degree we can define its {\em growth

251:   function} as the mapping $g_{\mcA} : \dN \to \dN$ with $g_{\mcA}(n)

252: = \max \{ |S_{\mcA}(n,a)| \mid a \in \mcA \}$. Note that if the

253: function $g_{\mcA}$ is not bounded then $g_{\mcA}(n) \geq n$ for all

254: $n \geq 1$. For us, it is more convenient to not have a bounded

255: function describing the growth. Therefore, we define the

256: \emph{normalized growth function $g'_\mcA$} by

257: $g'_\mcA(n)=\max\{n,g_\mcA(n)\}$. Note that $g_\mcA$ and $g'_\mcA$ are

258: different only in the pathological case that all connected components

259: of $\mcA$ contain at most $m$ elements (for some fixed $m$). Clearly,

260: $g'_{\mcA}(n)$ can grow at most exponentially.  We say that $\mcA$ has

261: {\em exponential growth} if $g'_{\mcA}(n) \in 2^{\Omega(n)}$; if

262: $g'_{\mcA}(n) \in n^{O(1)}$, then $\mcA$ has {\em polynomial growth}.

263:  

264: To define logical formulas, we fix a countable infinite set~$V$ of

265: variables, which evaluate to elements of structures.  \emph{Formulas

266:   over the signature~$\mcS$} (or \emph{formulas} if the the signature

267: is clear from the context) are constructed from the atomic formulas

268: $x=y$ and $r(x_1,\ldots,x_{m_r})$, where $r\in\mcS$ and

269: $x,y,x_1,\ldots,x_{m_r} \in V$, using the Boolean connectives $\lor$

270: and $\neg$ and existential quantification over variables

271: from~$V$. The Boolean connective $\land$ and universal quantification

272: can be derived from these operators in the usual way.  The

273: \emph{quantifier depth} of a formula~$\varphi$ is the maximal nesting

274: of quantifiers in~$\varphi$. The notion of a free variable is defined

275: as usual. A formula without free variables is called \emph{closed}.

276: If $\varphi(x_1, \ldots, x_m)$ is a formula with free

277: variables among $x_1, \ldots, x_m$ and $a_1, \ldots, a_m \in \mcA$,

278: then $\mcA \models \varphi(a_1, \ldots, a_m)$ means that $\varphi$

279: evaluates to true in $\mcA$ when the free variable $x_i$ evaluates to

280: $a_i$.  The \emph{first-order theory} of $\mcA$, denoted by

281: $\FOTh(\mcA)$, is the set of all closed formulas $\varphi$

282: such that $\mcA \models \varphi$.

283: 

284: \subsection{Structures from automata}

285: 

286: This section recalls string automatic and tree automatic structures and basic

287: results about them. Details can be found in the survey \cite{Rub08}.

288: 

289: 

290: \subsubsection{Tree and string automatic structures}

291: 

292: String automatic structures were introduced in~\cite{Hod82}, their systematic

293: study was later initiated by~\cite{KhoN95}.

294: Tree automatic structures were introduced in \cite{Blu99}, they

295: generalize string automatic structures. Here, we will first introduce 

296: tree automatic structures. String automatic structures can be 

297: considered as a special case of tree automatic structures.

298: 

299: Let $\Gamma$ be a finite alphabet and  

300: let $\$ \not \in \Gamma$ be an additional padding symbol.  Let $t_1,

301: \ldots, t_m \in T_\Gamma$. We define the {\em convolution} $t = t_1

302: \otimes \cdots \otimes t_m$, which is a finite binary tree over the

303: alphabet $(\Gamma \cup \{\$\})^m$, as follows: $\dom(t) =

304: \bigcup_{i=1}^m \dom(t_i)$ and for all $w \in \bigcup_{i=1}^m

305: \dom(t_i)$ we define $t(w) = (a_1, \ldots, a_m)$, where $a_i = t_i(w)$

306: if $w \in \dom(t_i)$ and $a_i = \$$ otherwise.  In

307: Fig.~\ref{fig:convolution}, the third tree is the convolution of the

308: first two trees.

309: \begin{figure}[t]

310:   \begin{center}

311:     \setlength{\unitlength}{1mm}

312:     \begin{picture}(94,34)(0,-12)

313:       \gasset{linewidth=.3,Nframe=n,Nadjust=wh,Nadjustdist=0.8}

314:       \node(1)(10,20){$a$} \node(2)(5,10){$b$} \node(3)(15,10){$b$}

315:       \node(4)(0,0){$a$} \node(5)(10,0){$a$} \drawedge(1,2){}

316:       \drawedge(1,3){} \drawedge(2,4){} \drawedge(2,5){}

317:       \node(6)(30,20){$a$} \node(7)(35,10){$a$} \node(8)(30,0){$b$}

318:       \node(9)(40,0){$b$} \node(10)(25,-10){$a$} \drawedge(6,7){}

319:       \drawedge(7,8){} \drawedge(7,9){} \drawedge(8,10){}

320:       \node(11)(76,20){$(a,a)$} \node(12)(68,10){$(b,\$)$}

321:       \node(13)(84,10){$(b,a)$} \node(14)(60,0){$(a,\$)$}

322:       \node(15)(70,0){$(a,\$)$} \node(16)(82,0){$(\$,b)$}

323:       \node(17)(92,0){$(\$,b)$} \node(18)(80,-10){$(\$,a)$}

324:       \drawedge(11,12){} \drawedge(11,13){} \drawedge(12,14){}

325:       \drawedge(12,15){} \drawedge(13,16){} \drawedge(13,17){}

326:       \drawedge(16,18){}

327:     \end{picture}

328:   \end{center}

329:   \caption{The convolution of two trees}

330: \label{fig:convolution}

331: \end{figure}

332: 

333: An {\em $m$-dimensional (synchronous) tree automaton} over $\Gamma$ is just

334: a tree automaton $A$ over the alphabet $(\Gamma \cup \{\$\})^m$ such

335: that $L(A) \subseteq \{ t_1 \otimes \cdots \otimes t_n \mid t_1,

336: \ldots, t_m \in T_\Gamma \}$. Such an automaton defines an $m$-ary

337: relation

338: $$R(A) = \{ (t_1,\ldots, t_m) \mid  t_1 \otimes \cdots \otimes t_m \in L(A)

339: \}\ .$$ A {\em tree automatic presentation} is a tuple $P =

340: (\Gamma,A_0, A_=, (A_r)_{r \in \mcS})$, where:

341: \begin{itemize}

342: \item $\Gamma$ is a finite alphabet.

343: \item $\mcS$ is a signature (the signature of $P$), 

344:   as before $m_r$ is the arity of the symbol $r \in \mcS$.

345: \item $A_0$ is a tree automaton over the alphabet $\Gamma$.

346: \item For every $r \in \mcS$, $A_r$ is an $m_r$-dimensional tree

347:   automaton over the alphabet $\Gamma\cup\{\$\}$ such that $R(A_r)

348:   \subseteq L(A_0)^{m_r}$.

349: \item $A_=$ is a 2-dimensional tree automaton over the alphabet

350:   $\Gamma\cup\{\$\}$ such that $R(A_=) \subseteq L(A_0) \times L(A_0)$

351:   and $R(A_=)$ is a congruence on the structure $(L(A_0), (R(A_r))_{r

352:     \in {\cal S}})$.

353: \end{itemize}

354: This presentation~$P$ is called {\em injective} if $R(A_=)$ is the

355: identity relation on $L(A_0)$. In this case, we can omit the automaton

356: $A_=$ and identify $P$ with the tuple $(\Gamma,A_0, (A_r)_{r \in

357:   \mcS})$. The structure presented by $P$ is the quotient

358: $$\mcA(P) =  (L(A_0), (R(A_r))_{r \in {\cal S}})/_{R(A_=)}\ .$$ 

359: A structure $\mcA$ is called {\em tree automatic} if there exists a

360: tree automatic presentation $P$ such that $\mcA \simeq \mcA(P)$.  We

361: will write $[u]$ for the element $[u]_{R(A_=)}$ ($u \in L(A_0)$) of

362: the structure $\mcA(P)$.  We say that the presentation $P$ has bounded

363: degree if the structure $\mcA(P)$ has bounded degree.

364: 

365: A {\em string automatic presentation} is a tree automatic

366: presentation, where all tree automata are in fact string automata (as

367: explained in Section~\ref{S automata}), and a structure $\mcA$ is

368: called {\em string automatic} if there exists a string automatic

369: presentation~$P$ such that $\mcA \simeq \mcA(P)$.  Typical examples of

370: string automatic structures are $(\dN,+)$ (Presburger's arithmetic),

371: $(\mathbb{Q}, \leq)$, and all ordinals below

372: $\omega^\omega$~\cite{KhoN95,DelGK03}. An example of a tree automatic

373: structure, which is not string automatic is $(\dN, \cdot)$ (the

374: natural numbers with multiplication)~\cite{Blu99}, or the ordinal

375: $\omega^\omega$~\cite{DelGK03}. Examples of string automatic

376: structures of bounded degree are transition graphs of Turing machines

377: and Cayley-graphs of automatic groups \cite{EpsCHLPT92} (or even

378: right-cancellative monoids \cite{SiSt04}).

379: 

380: \begin{remark}

381:   Usually a \emph{tree automatic presentation} for an $\mcS$-structure

382:   $\mcA = (A, (r)_{r\in\mcS})$ is defined as a tuple $(\Gamma, L, h)$ such that

383:   \begin{itemize}

384:   \item $\Gamma$ is a finite alphabet,

385:   \item $L \subseteq T_\Gamma$ is a regular set of trees,

386:   \item $h : L \to A$ is a surjective function,

387:   \item the relation $\{ (u,v) \in L \times L \mid h(u)=h(v) \}$ can

388:     be recognized by a 2-dimensional tree automaton, and

389:   \item for every $r\in\mcS$, the relation $\{ (u_1, \ldots, u_{m_r})

390:     \in L^{m_r} \mid (h(u_1), \ldots, h(u_{m_r})) \in r \}$ can be

391:     recognized by an $m_r$-dimensional tree automaton.

392:   \end{itemize}

393:   Since for our considerations, tree automatic presentations are part

394:   of the input for algorithms, we prefer our definition, where a tree

395:   automatic presentation is a finite object (a tuple of finite tree

396:   automata), whereas in the standard definition, the presentation also

397:   contains the presentation map $h$.

398: \end{remark}

399: 

400: We will consider the following classes of tree automatic

401: presentations:

402: \begin{eqnarray*}

403: \mathsf{SA} & = & \text{the class of all string automatic presentations} \\

404: \mathsf{SAb} & = & \text{the class of all string automatic presentations of bounded degree} \\

405: \mathsf{iSAb} & = & \text{the class of all injective string automatic

406:   presentations of bounded degree} \\

407: \mathsf{TA} & = & \text{the class of all tree automatic presentations} \\

408: \mathsf{TAb} & = & \text{the class of all tree automatic presentations of bounded degree} \\

409: \mathsf{iTAb} & = & \text{the class of all injective tree automatic

410:   presentations of bounded degree} 

411: \end{eqnarray*}

412: 

413: \subsubsection{The model checking problem}

414: 

415: For the above classes of tree automatic presentations, we will be

416: interested in the following decision problems.

417: 

418: \begin{definition}

419:   Let $\dC$ be a class of tree automatic presentations. Then the

420:   \emph{first-order model checking problem $\Decision(\dC)$ for $\dC$}

421:   denotes the set of all pairs $(P,\varphi)$ where $P \in \dC$, and

422:   $\varphi$ is a closed formula over the signature of $P$ such that

423:   $\mcA(P) \models \varphi$.

424: \end{definition}

425: 

426: If $\dC=\{P\}$ is a singleton, then the model checking problem

427: $\Decision(\dC)$ for $\dC$ can be identified with the first-order

428: theory of the structure $\mcA(P)$.  An algorithm deciding the model

429: checking problem for a nontrivial class~$\dC$ decides the first-order

430: theories of each element of $\dC$ uniformly.

431: 

432: The following two results are the main motivations for investigating

433: tree automatic structures.

434: 

435: \begin{proposition}[cf.\ \cite{KhoN95,Blu99}] \label{P closure

436:     automatic} There exists an algorithm that computes from a tree

437:   automatic presentation $P = (\Gamma,A_0, A_=, (A_r)_{r \in \mcS})$

438:   and a formula $\varphi(x_1,\dots,x_m)$ an $m$-dimensional tree

439:   automaton $A$ over $\Gamma$ with $R(A) = \{ (u_1, \ldots, u_m) \in L(A_0)^m \mid

440:   \mcA(P) \models \varphi([u_1], \ldots, [u_m]) \}$.

441: \end{proposition}

442: %

443: The automaton is constructed by induction on the structure of the

444: formula~$\varphi$: disjunction corresponds to the disjoint union of

445: automata, existential quantification to projection, and negation to

446: complementation. The following result is a direct

447: consequence.

448: 

449: \begin{theorem}[cf.\ \cite{KhoN95,Blu99}]\label{T KhoNer94}  

450:  The model checking problem $\Decision(\mathsf{TA})$ for all tree

451:   automatic presentations is decidable. In particular, the first-order

452:   theory $\FOTh(\mcA)$ of every tree automatic structure $\mcA$ is

453:   decidable.

454: \end{theorem}

455: %

456: \begin{remark}

457:   Strictly speaking, \cite{KhoN95,Blu99} device algorithms that, given

458:   a tree automatic presentation and a closed formula, decide whether

459:   the formula holds in the presented

460:   structure. But a priori, it is not clear whether it is decidable,

461:   whether a given tuple $(\Gamma,A_0, A_=, (A_r)_{r \in \mcS})$ is a 

462:   tree automatic presentation. Lemma~\ref{L-TA-decidable} below shows that 

463:   $\mathsf{TA}$ is indeed decidable, which then completes the proof of this theorem.

464: \end{remark}

465: 

466: Theorem~\ref{T KhoNer94} holds even if we add quantifiers for ``there

467: are infinitely many $x$ such that~$\varphi(x)$''

468: \cite{Blu99,BluG00} and ``the number of elements satisfying

469: $\varphi(x)$ is divisible by $k$'' (for

470: $k\in\dN$)~\cite{KhoRS04}\footnote{\cite{KhoRS04} only provides the

471:   proofs for string automatic structures. These proofs are easily

472:   extended to tree automatic structures once the presentation is

473:   injective.  But every tree automatic presentation can be transformed

474:   into an equivalent injective one \cite[Cor.~4.2]{ColL07}.}.  This

475: implies in particular that it is decidable whether a tree automatic

476: presentation describes a locally finite structure. But the

477: decidability of the first-order theory is far from efficient, since

478: there are even string automatic structures with a nonelementary

479: first-order theory~\cite{BluG00}. For instance the structure

480: $(\{0,1\}^*, s_0, s_1, \preceq)$, where $s_i = \{ (w,wi) \mid

481: w \in \{0,1\}^* \}$ for $i \in \{0,1\}$ and $\preceq$ is the prefix order on

482: finite words, has a nonelementary first-order theory, see

483: e.g.~\cite[Example 8.3]{ComH90}. A locally finite example (encoding

484: the set of all finite labeled linearly ordered sets~\cite{Mey75}) is

485: as follows: the universe is the set $L=\{u\otimes v\mid

486: u\in\{0,1\}^+,v\in 0^*,|v|<|u|\}$. In addition, we have a partial

487: order $\{(u\otimes v,u\otimes v') \in L \times L \mid |v| \leq 

488: |v'| \}$ that encodes the union of all the linear order relations,

489: and a unary relation $\{u\otimes v \in L \mid\text{ position $|v|$ in

490:   $u$ carries }1\}$ that encodes the labeling.

491: 

492: \subsubsection{First complexity results: the classes $\mathsf{TA}$ etc

493:   and boundedness}

494: 

495: This paper is concerned with the uniform and non-uniform complexity of

496: the first-order theory of (some subclass of) tree automatic structures

497: of bounded degree. Thus, we will consider algorithms that take as

498: input tree automatic presentations (together with closed formulas).

499: For complexity considerations, we have to define the size $|P|$ of a

500: tree automatic presentation $P = (\Gamma,A_0, A_=, (A_r)_{r \in

501:   \mcS})$.  First, let us define the size $|A|$ of an $m$-dimensional

502: tree automaton $A = (Q, \Delta, q_0)$ over $\Gamma$.  A transition

503: tuple from $\Delta$ (see (\ref{transition relation})) can be stored

504: with at most $3 \log(|Q|) + m\log(|\Gamma|)$ many bits.  Hence, up to

505: constant factors, $\Delta$ can be stored in space $|\Delta| \cdot

506: (\log(|Q|) + m \log(|\Gamma|))$.  We can assume that every state is

507: the first component of some transition tuple, i.e., $|Q|\leq

508: |\Delta|$. Furthermore, the size of the basic alphabet $\Gamma$ can be

509: bounded by $|\Delta|$ as well, but the dimension $m$ is independent

510: from the size of~$\Delta$. Since our complexity measures will be up to

511: polynomial time reductions, it makes sense to define the size of the

512: tree automaton $A$ to be $|A| = |\Delta|\cdot m$. We assume $\Delta$

513: to be nonempty, hence $|A| \geq 1$. The size of the presentation $P =

514: (\Gamma,A_0, A_=, (A_r)_{r \in \mcS})$ is $|P| = |A_0|+|A_=|+\sum_{r

515:   \in \mcS} |A_r|$.  Note that $|\mcS| \leq |P|$ and $m \leq |P|$,

516: when $m$ is the maximal arity in $\mcS$.  

517: %Note also that $P$

518: %implicitly defines the signature $\mcS$, hence we can speak of the

519: %signature of the presentation~$P$.

520: 

521: It will be convenient to work with injective string (resp.\ tree)

522: automatic presentations. The following lemma says that this is no

523: restriction, at least if we do not consider complexity aspects.

524: 

525: \begin{lemma}[\protect{\cite[Cor.~4.3]{KhoN95} and

526:     \cite[Cor.~4.2]{ColL07}}]\label{L-injective}

527:   {}From a given $P \in \mathsf{TA}$ we can compute effectively $P'

528:   \in \mathsf{iTA}$ with $\mcA(P) \simeq \mcA(P')$. If $P \in

529:   \mathsf{SA}$, then $P' \in \mathsf{iSA}$ with $\mcA(P) \simeq

530:   \mcA(P')$ can be computed in time $2^{O(|P|)}$.

531: \end{lemma}

532: 

533: \begin{remark}

534:   In \cite{ColL07}, only the existence of an equivalent injective tree

535:   automatic presentation is stated, but the proofs of \cite[Prop.~3.1

536:   and Theorem~4.1]{ColL07} are effective although the complexity is

537:   difficult to extract.

538: \end{remark}

539: 

540: The following lemma shows that the classes of all tree and string

541: automatic presentations are decidable and gives complexity

542: bounds. While these two results are not surprising, it is not clear

543: how to determine whether $\mcA(P)$ has bounded degree -- this will be

544: solved by Prop.~\ref{P-degree1} below.

545: 

546: \begin{lemma}\label{L-TA-decidable}

547:   The class $\mathsf{TA}$ is in~{\sf EXPTIME}, and the class

548:   $\mathsf{SA}$ belongs to~{\sf PSPACE}.

549: \end{lemma}

550: 

551: \begin{proof}

552:   We start with a proof of the first statement. Suppose we are given a

553:   finite alphabet~$\Gamma$, tree automata $A_0$ over $\Gamma$, and

554:   multi-dimensional tree automata $A_=$ and $A_r$ for $r\in\mcS$

555:   over~$\Gamma\cup\{\$\}$.  In a first step, we check that $L(A_=)$

556:   and $L(A_r)$ are languages of convolutions of elements of $L(A_0)$,

557:   in particular

558:   \begin{equation}

559:     \label{eq:test1}

560:     L(A_r)\subseteq \underbrace{L(A_0)\otimes L(A_0)\dots\otimes

561:     L(A_0)}_{m_r\ \text{times}}

562:   \end{equation}

563:   where $m_r$ is the arity of the automaton~$A_r$. An automaton for

564:   the right-hand side has size $|A_0|^{m_r}$. Thus, the inclusion

565:   can be decided in time exponential in $|A_r|+|A_0|^{m_r}$. Since

566:   $m_r$ depends on the input, this yields a doubly exponential

567:   algorithm. Alternatively, we proceed as follows:

568:   \begin{enumerate}[(a)]

569:   \item We check that no tree from $L(A_r)$ contains the label

570:     $(\$,\dots,\$)$. To this aim, replace in all transitions of $A_r$

571:     the letters from $(\Gamma\cup\{\$\})^{m_r}\setminus\{(\$,\dots,\$)\}$

572:     by $\top$ and the letter $(\$,\dots,\$)$ by $\bot$ and check

573:     whether the language of the resulting automaton $A_r'$ is

574:     contained in $T_{\{\top\}}$ (the set of all $\top$-labeled 

575:     binary trees). Since the set $T_{\{\top\}}$ can be

576:     accepted by a fixed automaton, this inclusion can be decided in

577:     polynomial time.

578:   \item Let $H\subseteq T_{\Gamma\cup\{\$\}}$ denote the set of those

579:     trees $t$ whose $\Gamma$-labeled nodes form an initial segment

580:     of~$t$ that belongs to $L(A_0)$. To accept $H$, we extend $A_0$ as

581:     follows (where $a \in \Gamma$):

582:     \begin{itemize}

583:     \item We add a new state $q_\$$ and transitions $(q_\$,\$)$,

584:       $(q_\$,\$,q_\$)$, and $(q_\$,\$,q_\$,q_\$)$.

585:     \item For each transition $(p,a,q)$, we add the transition

586:       $(p,a,q,q_\$)$.

587:     \item For each transition $(p,a)$, we add the transitions

588:       $(p,a,q_\$)$ and $(p,a,q_\$,q_\$)$.

589:     \end{itemize}

590:     Let $A_0^\$$ denote the resulting tree automaton and, for $1\le

591:     i\le m_r$, let $A_r^i$ denote the projection of $A_r$ to its

592:     $i^{th}$ component. Then we check, for all $1\le i\le m_r$ whether

593:     $L(A_r^i)\subseteq L(A_0^\$)$ which can be done in exponential

594:     time.

595:   \end{enumerate}

596:   All these tests are passed if and only if (\ref{eq:test1}) holds

597:   for~$A_r$. In particular, we can from now on speak of the relations

598:   $R(A_=)$ and $R(A_r)$ over $L(A_0)$.

599: 

600:   It remains to be checked that $R(A_=)$ is a congruence on the

601:   structure $(L(A_0),(R(A_r))_{r\in\mcS})$. For this, we proceed as

602:   follows

603:   \begin{enumerate}[(a)]

604:     \addtocounter{enumi}{2}

605:   \item First build 2-dimensional tree automata $A_\circ$, $A_{-1}$,

606:     and $A_{\text{id}}$ of polynomial size with

607:     $R(A_\circ)=R(A_=)\circ R(A_=)$, $R(A_{-1})=R(A_=)^{-1}$, and

608:     $R(A_{\text{id}})=\{(t,t)\mid t\in L(A_0)\}$. Then check

609:     $R(A_\circ)\cup R(A_{-1})\cup R(A_{\text{id}})\subseteq R(A_=)$

610:     which can be done in exponential time. This test is passed if and

611:     only if $R(A_=)$ is an equivalence relation on $L(A_0)$.

612:   \item For each $r\in\mcS$, first construct an $2m_r$-dimensional

613:     tree automaton $A_r'$ such that the tuple

614:     $(s_1,\dots,s_{m_r},t_1,\dots,t_{m_r})$ belongs to $R(A'_r)$ if

615:     and only if $(s_i,t_i)\in R(A_=)$ for all $1\le i\le m_r$ and

616:     $(t_1,\dots,t_{m_r})\in R(A_r)$. This can be achieved by running

617:     $m_r$ copies of $A_=$ as well as one copy of $A_r$ in

618:     parallel. Then project the automaton $A_r'$ onto the first $m_r$

619:     components and check whether the relation accepted by the

620:     resulting tree automaton is contained in~$R(A_r)$.  Although

621:     $A'_r$ has exponential size (since $m_r$ depends on the

622:     presentation~$P$), this can be done again in exponential time: we

623:     complement $A_r$, take the intersection with $A'_r$ and check the

624:     resulting automaton (of exponential size) for emptiness.

625:   \end{enumerate}

626:   This finishes the proof of the first statement. To prove the second,

627:   one can proceed analogously using that the inclusion problem for

628:   string automata belongs to {\sf PSPACE}.\qed

629: \end{proof}

630: %

631: {}From the lower bounds for inclusion of string/tree automata,

632: it follows easily that the upper bounds in Lemma~\ref{L-TA-decidable}

633: are sharp.

634: 

635: The following lemma says that the Gaifman graph of a string (resp.\

636: tree) automatic structure is effectively string (resp.\ tree)

637: automatic. This is an immediate consequence of Prop.~\ref{P closure

638:   automatic}, so the novelty lies in the estimation of the complexity.

639: 

640: \begin{lemma}\label{L-Gaifman-automaton}

641:   {}From a given tree (string) automatic presentation $P =

642:   (\Gamma,A_0, A_=, (A_r)_{r \in \mcS})$ one can construct a

643:   2-dimensional tree (string) automaton $A$ such that

644:   \begin{equation} \label{auto for Gaifman}

645:    R(A) = \{ (u,v)\in L(A_0)\times L(A_0) \mid ([u], [v])  

646:    \text{ is an edge of the Gaifman-graph } G(\mcA(P)) \}\ .

647:   \end{equation}

648:   If $m$ is the maximal arity in $\mcS$, then $A$ can be computed 

649:   in time $O(m^2\cdot |P|^2) \le |P|^{O(1)}$.

650: \end{lemma}

651: 

652: \begin{proof}

653:   We only give the proof for string automatic presentations, the tree

654:   automatic case can be shown verbatim.  Let $E$ be the edge relation

655:   of the Gaifman-graph $G(\mcA(P))$.  Note that for all $u,v \in

656:   L(A_0)$ we have $([u], [v])\in E$ iff for some $r\in\mcS$ of arity

657:   $m_r\le m$ and $1\le i,j\le m_r$, there exist $u_1,\dots,u_{m_r}\in

658:   L(A_0)$ with $(u_1,\dots,u_{m_r}) \in R(A_r)$, $u=u_i$, and

659:   $v=u_j$. Let $r\in\mcS$ and $1\le i,j\le m_r$.  Projecting the

660:   automaton $A_r$ onto the tracks $i$ and $j$, one obtains a

661:   2-dimensional automaton accepting all pairs $(u,v) \in\Gamma^*

662:   \times \Gamma^*$ such that there exists $(u_1,\dots,u_{m_r})\in

663:   R(A_r)$ with $u=u_i$ and $v=u_j$. Then the disjoint union of all

664:   these automata (for $r\in\mcS$ and $1\le i,j\le m_r$) satisfies

665:   (\ref{auto for Gaifman}).  Since $|\mcS|\le |P|$, the construction

666:   can be performed in time $O(m^2 \cdot |P|^2)$.  \qed

667: \end{proof}

668: 

669: Lemma~\ref{L-Gaifman-automaton} allows to show that also 

670: the bounded classes $\mathsf{TAb}$

671: etc.\ are decidable:

672: 

673: \begin{proposition}\label{P-degree1}

674:   The following hold:

675:   \begin{enumerate}[(a)] 

676:   \item The class $\mathsf{TAb}$ is decidable.

677:   \item The class $\mathsf{iTAb}$ can be decided in exponential time

678:     (in fact, it can be checked in polynomial time whether a given

679:      $P \in \mathsf{iTA}$ has bounded degree).

680:   \item The class $\mathsf{SAb}$ can be decided in exponential time.

681:   \end{enumerate}

682: \end{proposition}

683: 

684: \begin{proof}

685:   For statement (a), let $P \in \mathsf{TA}$ (which is decidable by

686:   Lemma~\ref{L-TA-decidable} in exponential time). By

687:   Lemma~\ref{L-injective}, we can assume $P$ to be injective. By

688:   Lemma~\ref{L-Gaifman-automaton} we can compute an automaton $A$ with

689:   (\ref{auto for Gaifman}), i.e., $A$ defines the edge relation of the

690:   Gaifman-graph of $\mcA(P)$.  Since $P$ was assumed to be injective

691:   (i.e. every equivalence class $[u]$ is the singleton $\{u\}$),

692:   $\mcA(P)$ is of bounded degree iff $A$ (seen as a transducer) is

693:   finite-valued. But this is decidable in polynomial

694:   time~\cite{Web90,Sei92}. This finishes the proof of~(a). 

695: 

696:   Next consider statement~(b): Provided the input is guaranteed to be

697:   an injective tree automatic presentation, the polynomial time bound

698:   follows from the arguments above since there is no need to apply

699:   Lemma~\ref{L-injective}. It remains to decide whether the input is

700:   indeed an injective tree automatic presentation: Using

701:   Lemma~\ref{L-TA-decidable}, it suffices to decide injectivity which

702:   can be done in exponential time by checking inclusion of $L(A_=)$ in

703:   the convolution of the identity on~$T_\Gamma$.

704: 

705:   For (c), where we start with a string automatic presentation (which

706:   can be decided in polynomial space and therefore exponential time by

707:   Lemma~\ref{L-TA-decidable}), the initial application of

708:   Lemma~\ref{L-injective} leads to an exponential blow-up, which gives

709:   in total an exponential running time for deciding the

710:   class~$\mathsf{SAb}$.\qed

711: \end{proof}

712: 

713: Finally, since we deal with structures of bounded degree, it will be

714: important to estimate the degree of such a structures given its

715: presentation. Such estimates are provided by the following result.

716: 

717: \begin{proposition}\label{P-degree}

718:   The following hold:

719:   \begin{enumerate}[(a)] 

720:   \item If $P \in \mathsf{iSAb}$, then the degree

721:     of the structure $\mcA(P)$ is bounded by $\exp(1,|P|^{O(1)})$.

722:   \item If $P \in \mathsf{iTAb}$, then the

723:      degree of the structure $\mcA(P)$ is bounded by $\exp(2,|P|^{O(1)})$.

724:   \item If $P \in \mathsf{SAb}$, then the degree

725:     of the structure $\mcA(P)$ is bounded by $\exp(2,|P|^{O(1)})$.

726:   \end{enumerate}

727: \end{proposition}

728: 

729: \begin{proof}

730:   For statement~(a) let $P \in \mathsf{iSAb}$.  {}From

731:   Lemma~\ref{L-Gaifman-automaton}, we can construct a string

732:   automaton~$A$ of size $|P|^{O(1)}$ that accepts the edge relation of

733:   the Gaifman graph of $\mcA(P)$. Then the degree of $\mcA(P)$ equals

734:   the maximal outdegree of the relation $R(A)$.  For string

735:   transducer, this number is exponential in the size of~$A$, i.e., it

736:   is in $\exp(1,|P|^{O(1)})$~\cite{Web90}.

737: 

738:   For (b) we can use a similar argument. But since the maximal 

739:   outdegree of the relation recognized by a tree transducer $A$

740:   is doubly exponential in the size of $A$ \cite{Sei92}, we obtain 

741:   the bound $\exp(2,|P|^{O(1)})$ for the degree of $\mcA(P)$.

742: 

743:   Finally statement (c) follows immediately from Lemma~\ref{L-injective}

744:   and (a).  \qed

745: \end{proof}

746: 

747: The bounds on injective string (resp. tree) automatic presentations in

748: Prop.~\ref{P-degree} are sharp: Let $E_n=\{(uw,vw)\mid u,v,w, \in

749: \{a,b\}^*, |u|=|v|=n\}$. Then the structure $(\{a,b\}^*,E_n)$ has an

750: injective string automatic presentation of size $O(n)$. The degree of

751: this structure is $2^n$. Similarly, let $E'_n$ the set of all pairs

752: $(t_1,t_2) \in T_{\{a,b\}} \times T_{\{a,b\}}$ of trees that differ at

753: most in the first $n$~levels. Then $(T_{\{a,b\}},E'_n)$ allows an

754: injective tree automatic presentation of size $O(n)$ and the degree of

755: this structure is doubly exponential in~$n$.  But it is not clear

756: whether the doubly exponential bound for automatic presentations in

757: Prop.~\ref{P-degree}(c) can be realized.  Moreover, we cannot give any

758: bound for general tree automatic presentations since, as already

759: remarked, \cite{ColL07} does not provide any estimate on the size of

760: an equivalent \emph{injective} tree automatic presentation.

761: 

762: 

763: \section{Upper bounds}

764: 

765: It is the aim of this section to give an algorithm that decides the

766: theory of a string/tree automatic structure of bounded degree. The algorithm from

767: Theorem~\ref{T KhoNer94} (that in particular solves this problem) is

768: based on Prop.~\ref{P closure automatic}, i.e., the inductive

769: construction of an automaton accepting all satisfying

770: assignments. Differently, we base our algorithm on Gaifman's

771: Theorem~\ref{T-Gaifman}, i.e., on the combinatorics of spheres. We

772: therefore start with some model theory.

773: 

774: \subsection{Model-theoretic background}

775: 

776: The following locality principle of Gaifman implies that super-exponential

777: distances cannot be handled in first-order logic:

778: 

779: \begin{theorem}[\cite{Gai82}]\label{T-Gaifman} 

780:   Let $\mcA$ be a structure, $(a_1,\ldots,a_k), (b_1,\ldots,b_k) \in

781:   \mcA^k$, $d \geq 0$, and $D_1, \ldots, D_k \geq 2^d$ such that

782:   \begin{equation} \label{iso}

783:     (\mcA \rest (\bigcup_{i=1}^k S(D_i,a_i) ), \ a_1, \ldots, a_k) \simeq

784:     (\mcA \rest (\bigcup_{i=1}^k S(D_i,b_i) ), \ b_1, \ldots, b_k)\ .

785:   \end{equation}

786:   Then, for every formula $\varphi(x_1,\ldots,x_k)$ of quantifier

787:   depth at most $d$, we have: $$\mcA\models\varphi(a_1,\ldots,a_k) \

788:   \Longleftrightarrow \ \mcA\models\varphi(b_1,\ldots,b_k) \ .$$

789: \end{theorem}

790: Note that (\ref{iso}) says that there is an isomorphism between the two 

791: induced substructures $\mcA \rest (\bigcup_{i=1}^k S(D_i,a_i) )$ and 

792: $\mcA \rest (\bigcup_{i=1}^k S(D_i,b_i))$ that maps $a_i$ to $b_i$ 

793: for all $1 \leq i \leq k$.

794: 

795: Let $\mcS$ be a signature and let $k,d \in \dN$ with $0 \leq k \leq d$.  A

796: \emph{potential $(d,k)$-sphere} is a tuple $(\mcB, b_1,\ldots, b_k)$

797: such that the following holds:

798: \begin{itemize}

799: \item $\mcB$ is an $\mcS$-structure with $b_1, \ldots, b_k \in

800:   \mcB$.

801: \item For all $b \in \mcB$ there exists $1 \leq i \leq k$ such that

802: $d_{\mcB}(b_i,b) \leq 2^{d-i}$.

803: \end{itemize}

804: There is only one $(d,0)$-sphere namely the empty sphere $\emptyset$.

805: For our later applications, $\mcB$ will be always a finite structure,

806: but in this subsection finiteness is not needed.  The potential

807: $(d,k)$-sphere $(\mcB, b_1,\ldots, b_k)$ is \emph{realizable in the

808:   structure $\mcA$} if there exist $a_1, \ldots, a_k \in \mcA$ such

809: that

810: \[

811:     (\mcA \rest ( \bigcup_{i=1}^k S(2^{d-i},a_i) ),a_1,\dots,a_k) 

812:     \simeq (\mcB, b_1,\dots,b_k)\ .

813: \]

814: Let $\sigma = (\mcB, b_1,\ldots, b_k)$ be a potential $(d,k)$-sphere

815: and let $\sigma' = (\mcB', b'_1,\ldots, b'_k, b'_{k+1})$ be a

816: potential $(d,k+1)$-sphere ($k+1 \leq d$).  

817: Then $\sigma'$ \emph{extends} $\sigma$

818: (abbreviated $\sigma \preceq \sigma'$) if 

819: \[

820:     (\mcB' \rest ( \bigcup_{i=1}^k S(2^{d-i}, b_i) ), b_1',\dots,b_k') 

821:     \simeq (\mcB,b_1,\dots,b_k)\ .

822: \]

823: The following definition is the basis for our decision procedure.

824: 

825: \begin{definition}\label{D-boolean}

826:   Let $\mcA$ be an $\mcS$-structure, $\psi(y_1,\ldots,y_k)$ a

827:   formula of quantifier depth at most~$d$, and let $\sigma =

828:   (\mcB, b_1,\ldots, b_k)$ be a potential $(d+k,k)$-sphere.  The

829:   Boolean value $\psi_\sigma \in \{0,1\}$ is defined inductively as

830:   follows:

831:   \begin{itemize}

832:   \item If $\psi(y_1,\ldots,y_k) $ is an atomic formula, then

833:     \begin{equation} \label{qf} \psi_\sigma =

834:       \begin{cases}

835:         0 & \text{if $\mcB \models \psi(b_1,\ldots,b_k)$}\\

836:         1 & \text{if $\mcB \not\models \psi(b_1,\ldots,b_k)$}\ .

837:       \end{cases}

838:     \end{equation}

839:   \item If $\psi=\neg\theta$, then $\psi_\sigma=1-\theta_\sigma$.

840: %  \item If $\psi=\alpha\land\beta$, then

841: %    $\psi_\sigma=\min(\alpha_\sigma,\beta_\sigma)$.

842:   \item If $\psi=\alpha\lor\beta$, then

843:     $\psi_\sigma=\max(\alpha_\sigma,\beta_\sigma)$.

844:   \item If $\psi(y_1,\ldots,y_k) = \exists y_{k+1}

845:     \theta(y_1,\ldots,y_k,y_{k+1})$ then

846:     \begin{equation} \label{existential} \psi_\sigma = \max \{

847:       \theta_{\sigma'} \mid \sigma' \text{ is a realizable potential

848:         $(d+k,k+1)$-sphere with } \sigma \preceq \sigma' \}\ .

849:     \end{equation}

850:   \end{itemize}

851: \end{definition}

852: 

853: The following result ensures for every closed formula~$\psi$ 

854: that $\psi_\emptyset=1$ if and only if

855: $\mcA\models\psi$. Hence the above

856: definition can possibly be used to decide validity of the

857: formula~$\varphi$ in the structure~$\mcA$.

858: 

859: \begin{proposition}\label{P upper bound}

860:   Let $\mcS$ be a signature, $\mcA$ an $\mcS$-structure with

861:   $a_1,\dots,a_k\in\mcA$, $\psi(y_1,\dots,y_k)$ a formula of

862:   quantifier depth at most~$d$, and $\sigma=(\mcB,b_1,\dots,b_k)$ a

863:   potential $(d+k,k)$-sphere with

864:   \begin{equation} \label{real}

865:     (\mcA \rest ( \bigcup_{i=1}^k S(2^{d+k-i},a_i) ), \ a_1,\ldots, a_k)

866:      \simeq (\mcB, b_1,\ldots,b_k)\ .

867:   \end{equation}

868:   Then $\mcA \models \psi(a_1,\ldots,a_k) \ \Longleftrightarrow \

869:   \psi_\sigma = 1$.

870: \end{proposition}

871: 

872: \begin{proof}

873:   We prove the lemma by induction on the structure of the

874:   formula~$\psi$.  First assume that $\psi$ is atomic, i.e. $d=0$. Then we have:

875:   \begin{align*}

876:   \psi_\sigma = 1 \ 

877:   & \stackrel{(\ref{qf})}{\Longleftrightarrow} \ \mcB \models \psi(b_1,\ldots,b_k) \\

878:   & \stackrel{(\ref{real})}{\Longleftrightarrow} \ 

879:       \mcA \rest ( \bigcup_{i=1}^k S(2^{k-i},a_i) ) \models

880:       \psi(a_1,\ldots,a_k) \\

881:    & \Longleftrightarrow \ \mcA \models \psi(a_1,\ldots,a_k)\ ,

882:   \end{align*} 

883:   where the last equivalence holds since $\psi$ is atomic.

884: 

885:   The cases $\psi=\neg\theta$ and $\psi=\alpha\lor\beta$ 

886:   are straightforward and therefore omitted.

887: 

888:   We finally consider the case $\psi(y_1,\ldots,y_k) = \exists y_{k+1}

889:   \theta(y_1,\ldots,y_k,y_{k+1})$.

890:   

891:   First assume that $\psi_\sigma=1$. By (\ref{existential}), there exists a realizable

892:   potential $(d+k,k+1)$-sphere $\sigma'$ with

893:   $\sigma \preceq \sigma'$ and $\theta_{\sigma'}=1$.  Since $\sigma'$ is realizable, there exist

894:   $a'_1, \ldots, a'_k, a'_{k+1} \in \mcA$ with

895:   \begin{equation} \label{real' k+1}

896:     (\mcA \rest ( \bigcup_{i=1}^{k+1} S(2^{d+k-i},a'_i) ), \ a'_1,\ldots, a'_k, a'_{k+1})

897:      \simeq (\mcB', b_1,\ldots,b_k, b_{k+1}) = \sigma'\ .

898:   \end{equation}

899:   By induction, we have $\mcA\models\theta(a_1',\ldots,a_k',a_{k+1}')$

900:   and therefore $\mcA\models\psi(a_1',\ldots,a_k')$. {}From

901:   (\ref{real}), (\ref{real' k+1}), and $\sigma\preceq\sigma'$, we also

902:   obtain

903:   $$

904:     (\mcA \rest ( \bigcup_{i=1}^k S(2^{d+k-i},a'_i) ), \  a'_1,\ldots, a'_k)

905:     \simeq

906:     (\mcA \rest ( \bigcup_{i=1}^k S(2^{d+k-i},a_i) ), \ a_1,\ldots, a_k)

907:   $$

908:   and therefore by Gaifman's Theorem~\ref{T-Gaifman} $\mcA \models

909:   \psi(a_1,\ldots, a_k)$.

910: 

911:   Conversely, let $a_{k+1}\in\mcA$ with

912:   $\mcA\models\theta(a_1,\dots,a_k,a_{k+1})$.  Let $\sigma' = (\mcB',

913:   b_1,\ldots,b_k,b_{k+1})$ be the unique (up to isomorphism) potential $(d+k,k+1)$-sphere

914:   such that

915:   \begin{equation} \label{real k+1}

916:     (\mcA \rest ( \bigcup_{i=1}^{k+1} S(2^{d+k-i},a_i) ), \ a_1,\ldots, a_k, a_{k+1})

917:      \simeq (\mcB', b_1,\ldots,b_k, b_{k+1})\ .

918:   \end{equation}

919:   Then (\ref{real}) implies $\sigma \preceq \sigma'$.  Moreover, by

920:   (\ref{real k+1}), $\sigma'$ is realizable in $\mcA$, and

921:   $\mcA\models\theta(a_1,\dots,a_k,a_{k+1})$ implies by induction

922:   $\theta_{\sigma'}=1$. Hence, by (\ref{existential}), we get $\psi_\sigma=1$ which finishes

923:   the proof of the lemma.\qed

924: \end{proof}

925: 

926: \subsection{The decision procedure}

927: 

928: Now suppose we want to decide whether the closed formula $\varphi$

929: holds in a tree automatic structure~$\mcA$ of {\em bounded degree}. By

930: Prop.~\ref{P upper bound} it suffices to compute the Boolean

931: value~$\varphi_\emptyset$. This computation will follow the inductive

932: definition of $\varphi_\sigma$ from Def.~\ref{D-boolean}. Since

933: every $(d,k)$-sphere that is realizable in $\mcA$ is finite, we only have 

934: to deal with finite spheres. The crucial part of our algorithm

935: is to determine whether a finite potential $(d,k)$-sphere is

936: realizable in~$\mcA$. In the following, for a finite potential

937: $(d,k)$-sphere $\sigma = (\mcB,b_1,\dots,b_k)$, 

938: we denote with $|\sigma|$ the number of elements of $\mcB$ and 

939: with $\delta(\sigma)$ we denote the degree of the finite structure

940: $\mcB$. We have to solve the following realizability problem:

941: 

942: \begin{definition}

943:   Let $\dC$ be a class of tree automatic presentations. Then the

944:   \emph{realizability problem $\Real(\dC)$ for $\dC$} denotes the set

945:   of all pairs $(P,\sigma)$ where

946:   $P \in\dC$ and $\sigma$ is a {\em finite} potential

947:   $(d,k)$-sphere over the signature of $P$ for some $0\le k\le d$ 

948:   such that $\sigma$ can be realized in $\mcA(P)$.

949: \end{definition}

950: 

951: \begin{lemma}\label{L-realisability} 

952:   The problems $\Real(\mathsf{iSA})$ and $\Real(\mathsf{iTA})$ are decidable.

953:   More precisely:

954:   \begin{itemize}

955:   \item Let $P \in \mathsf{iSA}$ and let $m$ be the maximal arity of a

956:     relation in $\mcA(P)$. Let $\sigma$ be a finite potential

957:     $(d,k)$-sphere over the signature of $P$. Then it can be checked

958:     in space $|\sigma|^{O(m)}\cdot |P|^2\cdot 2^{O(\delta(\sigma))}$,

959:     whether $\sigma$ is realizable in $\mcA(P)$.

960:   \item If $P \in \mathsf{iTA}$, then realizability can be checked 

961:     in time $\exp(1, |\sigma|^{O(m)}\cdot |P|^2\cdot 2^{O(\delta(\sigma))})$.

962:    \end{itemize}

963: \end{lemma}

964: 

965: \begin{proof}

966:   We first prove the statement on injective string automatic presentations.

967:   Let $P = (\Gamma,A_0, (A_r)_{r \in \mcS}) \in \mathsf{iSA}$. 

968:   Let $\sigma = (\mcB,b_1,\dots,b_k)$ and 

969:   let $c_1,\dots,c_{|\sigma|}$ be a list of all elements of $\mcB$.

970:   Note that every $b_i$ occurs in this list.

971:   Let $E_{\mcA(P)}$ be the edge

972:   relation of the Gaifman graph~$G(\mcA(P))$ and $E_\mcB$ that of the

973:   Gaifman graph~$G(\mcB)$. Then $\sigma$ is realizable

974:   in $\mcA(P)$ if and only if there are words $u_1,\dots,u_{|\sigma|} \in

975:   \Gamma^*$ such that

976:   \begin{enumerate}[(a)]

977:   \item $u_i\in L(A_0)$ for all $1\le i\le |\sigma|$,

978:   \item $u_i \neq u_j$ for all $1\le i<j\le |\sigma|$,

979:   \item $(u_{i_1},\dots, u_{i_{m_r}}) \in R(A_r)$ for all $r\in\mcS$

980:     and all $(c_{i_1},\dots,c_{i_{m_r}}) \in r^{\mcB}$,

981:   \item $(u_{i_1},\dots,u_{i_{m_r}})\notin R(A_r)$ for all $r\in\mcS$

982:     and all $(c_{i_1},\dots,c_{i_{m_r}})\in \mcB^{m_r}\setminus r^{\mcB}$, and

983:   \item there is no $v\in L(A_0)$ such that, for some $1\le j \le |\sigma|$ and

984:     $1\le i\le k$ with $d(c_j,b_i) < 2^{d-i}$, we have

985:     \begin{enumerate}[(\alph{enumi}.1)]

986:     \item $(u_j,v)\in E_{\mcA(P)}$ and

987:     \item $v \notin \{ u_p \mid (c_j,c_p)\in E_\mcB\}$.

988:     \end{enumerate}

989:   \end{enumerate}

990:   Then (a-d) express that the mapping $c_i\mapsto u_i$ is

991:   well-defined and an embedding of $\mcB$ into~$\mcA(P)$. In~(e),

992:   $(u_j,v)\in E_{\mcA(P)}$ implies that $v$ belongs to

993:   $\bigcup_{1\le i\le k}S(2^{d-i},u_i)$. Hence (e) expresses that

994:   all elements of $\bigcup_{1\le i\le k}S(2^{d-i},u_i)$ belong to

995:   the image of this embedding.

996: 

997:   We now construct a $|\sigma|$-dimensional automaton~$A$ over the

998:   alphabet $\Gamma$ that checks (a-e). At the end, we have to check

999:   the language of this automaton for non-emptiness. The automaton $A$

1000:   is the direct product of automata $A_a$, $A_b$, $A_c$, $A_d$, and

1001:   $A_e$ that check the conditions separately. Then $A_a$ is the direct

1002:   product of $|\sigma|$ many copies of the automaton $A_0$, hence

1003:   $A_a$ has at most $|P|^{|\sigma|}$ many states.

1004: 

1005:   Next, the automaton for (b) is the direct product of $O(|\sigma|^2)$

1006:   many copies of an automaton of fixed size (that checks whether two

1007:   tracks are different). Hence, this automaton has 

1008:   $2^{|\sigma|^{O(1)}}$ many states.

1009: 

1010:   The automaton $A_c$ is again a direct product, this time of one 

1011:   automaton for each $r\in\mcS$ (and therefore of at most~$|P|$

1012:   many automata). Each of these automata is the direct product of

1013:   $|r^{\mcB}|$~many copies of the automaton $A_r$. Since

1014:   the arity of $r\in\mcS$ is bounded by $m$, we have $|r^{\mcB}| \leq

1015:   |\sigma|^m$. Hence, the automaton $A_c$ has at most

1016:   $(|P|^{|\sigma|^m})^{|P|} = |P|^{|P|\cdot |\sigma|^m}$ many states. 

1017:   For~$A_d$, we can argue similarly, but this time using

1018:   copies of the complement of the automaton~$A_r$. 

1019:   This yields for $A_d$ the bound $(2^{|P|})^{|P|\cdot |\sigma|^m} = 

1020:   \exp(1, |P|^2 \cdot |\sigma|^m)$ on the number of states.

1021: 

1022:   It remains to construct the automaton~$A_e$. For this, we first

1023:   construct its complement, i.e., an automaton~$A_e'$ that checks for

1024:   the existence of $v\in L(A_0)$ with the desired

1025:   properties. This automaton $A_e'$ is the disjoint union of at most

1026:   $|\sigma|$~many automata, one for each $1\le j \le |\sigma|$ such that there exists

1027:   $1\le i\le k$ with $d(c_j,b_i)<2^{d-i}$. Any of these components

1028:   consists of the direct product of automata $A_{e.1}$ and $A_{e.2}$

1029:   checking (e.1) and (e.2), respectively. By

1030:   Lemma~\ref{L-Gaifman-automaton}, $A_{e.1}$ hast at most

1031:   $m^2\cdot |P|^2$ many states. Recall that the

1032:   degree of $\mcB$ is $\delta(\sigma)$. Hence, the set 

1033:   $\{ u_p \mid (c_j,c_p)\in E_\mcB\}$ 

1034:   contains at most $\delta(\sigma)$ many elements. Thus, (e.2) can be checked by an

1035:   automaton~$A_{e.2}$ with $2^{O(\delta(\sigma))}$ many states.  Hence, $A_e'$ is the

1036:   disjoint union of at most $|\sigma|$ copies of an automaton of size

1037:   $|P|^2\cdot m^2\cdot 2^{O(\delta(\sigma))}$ and therefore has

1038:   at most $|\sigma|\cdot |P|^2\cdot m^2\cdot 2^{O(\delta(\sigma))}$ many states. 

1039:   Now the number of states of $A_e$ can be bound

1040:   by $\exp(1,|\sigma|\cdot |P|^2\cdot m^2\cdot 2^{O(\delta(\sigma))})$.

1041: 

1042:   In summary, the automaton $A$ has at most

1043:   \[

1044:     |P|^{|\sigma|}\cdot 

1045:     2^{|\sigma|^{O(1)}}\cdot

1046:     |P|^{|P|\cdot |\sigma|^m}\cdot

1047:     2^{|P|^2\cdot |\sigma|^m}\cdot

1048:     2^{|\sigma|\cdot |P|^2\cdot m^2\cdot 2^{O(\delta(\sigma))}}

1049:     \le \exp(1,|\sigma|^{O(m)}\cdot |P|^2\cdot 2^{O(\delta(\sigma))})

1050:   \]

1051:   many states. Hence checking emptiness of its language (and therefore

1052:   realizability of $\sigma$ in $\mcA(P)$) can be done in space 

1053:   logarithmic to the number of states, i.e., in 

1054:   space $|\sigma|^{O(m)}\cdot |P|^2\cdot 2^{O(\delta(\sigma))}$ which proves the

1055:   statement for string automatic presentations.

1056: 

1057:   For injective tree automatic presentations, the construction and

1058:   size estimate for~$A$ are the same as above. But emptiness of tree

1059:   automata can only be checked in deterministic polynomial time (and

1060:   not in logspace unless $\mathsf{NL} = \mathsf{P}$). Hence, emptiness of $A$ can be

1061:   checked in time $\exp(1,|\sigma|^{O(m)}\cdot |P|^2\cdot

1062:   2^{O(\delta(\sigma))})$. \qed

1063: \end{proof}

1064: 

1065: In the following, for a tree automatic presentation $P$ of bounded

1066: degree, we denote with $g'_P = g'_{\mcA(P)}$ the normalized growth

1067: function of the structure $\mcA(P)$.

1068: 

1069: \begin{theorem}\label{T-upper}

1070:   The model checking problem $\Decision(\mathsf{TAb})$ is decidable,

1071:   i.e., on input of a tree automatic presentation~$P$ of bounded

1072:   degree and a closed formula~$\varphi$ over the signature of~$P$, one

1073:   can effectively determine whether $\mcA(P)\models\varphi$ holds.

1074:   More precisely (where $m$ is the maximal arity of a relation from

1075:   the signature of~$P$):

1076:   \begin{enumerate}[(1)]

1077:   \item $\Decision(\mathsf{iSAb)}$ can be decided in space

1078:     \[

1079:        g'_P(2^{|\varphi|})^{O(m)}\cdot \exp(2,|P|^{O(1)})

1080:             \le \exp(2,|P|^{O(1)}+|\varphi|)\ .

1081:     \]

1082:   \item $\Decision(\mathsf{SAb})$ can be decided in space

1083:     \[

1084:        \exp(3, O(|P|)+\log(|\varphi|))\ .

1085:     \]

1086:   \item $\Decision(\mathsf{iTAb})$ can be decided in time

1087:   \[

1088:      \exp\biggl(1,\ g'_P(2^{|\varphi|})^{O(m)} \cdot \exp(3,|P|^{O(1)}) \biggr)

1089:       \leq \exp(4, |P|^{O(1)}+\log(|\varphi|))\ .

1090:   \]

1091:  \end{enumerate}

1092: \end{theorem}

1093: 

1094: \begin{proof}

1095:   The decidability follows immediately from Theorem~\ref{T KhoNer94}

1096:   and Prop.~\ref{P-degree1}(a).

1097: 

1098:   We first give the proof for injective string automatic presentations.

1099:   By Prop.~\ref{P upper bound} it suffices to compute the Boolean

1100:   value $\varphi_\emptyset$. Recall the inductive definition of

1101:   $\varphi_\sigma$ from Def.~\ref{D-boolean} that we now translated

1102:   into an algorithm for computing~$\varphi_\emptyset$.

1103: 

1104:   First note that such an algorithm has to handle potential

1105:   $(d,k)$-spheres for $1 \leq k \leq d \leq|\varphi|$ ($d$ is the

1106:   quantifier rank of $\varphi$) that are realizable in~$\mcA(P)$.  The

1107:   number of nodes of a potential $(d,k)$-sphere realizable in

1108:   $\mcA(P)$ is bounded by $k \cdot g'_P(2^d) \in g'_P(2^d)^{O(1)}$

1109:   since $k\le d<2^d\le g'_P(2^d)$. The number of relations of

1110:   $\mcA(P)$ is bounded by~$|P|$. Hence, any potential $(d,k)$-sphere

1111:   can be described by $|P| \cdot g'_P(2^d)^{O(m)}$ many bits.

1112: 

1113:   Note that the set of $(d,k)$-spheres with $0\le k\le d$ (ordered by

1114:   the extension relation~$\preceq$) forms a tree of depth~$d+1$. The

1115:   algorithm visits the nodes of this tree in a depth-first manner (and

1116:   descents when unraveling an existential quantifier). Hence we have

1117:   to store $d+1$ many spheres. For this, the algorithm needs space

1118:   $(d+1)\cdot |P|\cdot g'_P(2^d)^{O(m)} = |P|\cdot g'_P(2^d)^{O(m)}$.

1119: 

1120:   Moreover, during the unraveling of a quantifier, the algorithm has

1121:   to check realizability of a potential $(d,k)$-sphere for $1\le k\le

1122:   d\le|\varphi|$. Any such sphere has at most $g'_P(2^d)^{O(1)}$ many

1123:   elements and the degree $\delta$ of $\mcA$ is bounded by $\exp(1,

1124:   |P|^{O(1)})$ by Prop.~\ref{P-degree}. Hence, by

1125:   Lemma~\ref{L-realisability}, realizability can be checked in

1126:   space $g'_P(2^d)^{O(m)}\cdot |P|^2\cdot \exp(2,|P|^{O(1)}) \le

1127:   g'_P(2^{|\varphi|})^{O(m)}\cdot \exp(2,|P|^{O(1)})$.

1128: 

1129:   At the end, we have to check whether a tuple $\overline{b}$

1130:   satisfies an atomic formula $\psi(\overline{y})$, which is trivial.

1131:   In total, the algorithm runs in space

1132:   \begin{equation*}

1133:      |P|\cdot g'_P(2^{|\varphi|})^{O(m)} +

1134:      g'_P(2^{|\varphi|})^{O(m)}\cdot\exp(2,|P|^{O(1)}) 

1135:      \le g'_P(2^{|\varphi|})^{O(m)}\cdot\exp(2,|P|^{O(1)})\ .

1136:   \end{equation*}

1137: 

1138:   Recall that $g'_\mcA(2^{|\varphi|})\le\delta^{2^{|\varphi|}}$ and

1139:   $\delta\le 2^{|P|^{O(1)}}$ by Prop.~\ref{P-degree}. Since also $m \le

1140:   |P|$, we obtain

1141:   \begin{align*}

1142:     g'_P(2^{|\varphi|})^{O(m)}\cdot\exp(2,|P|^{O(1)})

1143:      & \le \exp(1, |P|^{O(1)} \cdot 2^{|\varphi|} \cdot O(m)) \cdot\exp(2,|P|^{O(1)})\\

1144:      & \le \exp(2,|P|^{O(1)}+|\varphi|)\ .

1145:   \end{align*}

1146:   This completes the consideration for injective string automatic

1147:   presentations. 

1148: 

1149:   If $P$ is just automatic, we can transform it into an

1150:   equivalent injective automatic presentation which increases the size

1151:   exponentially by Lemma~\ref{L-injective}. Hence, replacing 

1152:   $|P|$ by $2^{O(|P|)}$ yields the space

1153:   bound.

1154: 

1155:   Next, we consider injective tree automatic presentations. The

1156:   algorithm is the same, i.e., it parses the tree of all potential

1157:   $(d,k)$-spheres and checks them for realizability. Note that the

1158:   number of potential $(d,k)$-spheres is in $\exp(1,|P|\cdot

1159:   g'_P(2^d)^{O(m)})$.  By Prop.~\ref{P-degree}, the degree $\delta$ is

1160:   bounded by $\exp(2,|P|^{O(1)})$. Hence, by

1161:   Lemma~\ref{L-realisability}, the realizability of any potential

1162:   $(d,k)$-sphere can be checked in time

1163:   $$\exp\biggl(1,\ g'_P(2^d)^{O(m)}\cdot |P|^2\cdot \exp(3,|P|^{O(1)}) \biggr)\le

1164:   \exp\biggl(1,\ g'_P(2^{|\varphi|})^{O(m)} \cdot

1165:   \exp(3,|P|^{O(1)})\biggr)\ .$$

1166:   Recall that $g'_P(2^{|\varphi|})\le\delta^{2^{|\varphi|}}$ and

1167:   $\delta\le \exp(2,|P|^{O(1)})$ by Prop.~\ref{P-degree}. Since also

1168:   $m\le |P|$, we obtain

1169:   \begin{align*}

1170:     g'_P(2^{|\varphi|})^{O(m)} \cdot \exp(3,|P|^{O(1)})

1171:       &\le \exp(2,|P|^{O(1)})^{2^{|\varphi|}\cdot O(|P|)}\cdot

1172:             \exp(3,|P|^{O(1)}) \\

1173:       &=\exp(2,{|P|^{O(1)}}+|\varphi|) \cdot \exp(3,|P|^{O(1)})\\

1174:       &=\exp(3,|P|^{O(1)}+\log(|\varphi|))\ .

1175:   \end{align*}\qed

1176: \end{proof}

1177: 

1178: \begin{remark}

1179:   Note that the above theorem does not give the complexity

1180:   for~$\Decision(\mathsf{TAb})$, i.e., for arbitrary tree automatic

1181:   presentations of bounded degree: Here, one can proceed as for string

1182:   automatic presentations, i.e., make the presentation injective and

1183:   refer to the above result on $\Decision(\mathsf{iTAb})$ -- this

1184:   gives the decidability that we already know from Theorem~\ref{T

1185:     KhoNer94} and Prop.~\ref{P-degree1}.  At present, we cannot

1186:   compare the complexity of this new algorithm with the nonelementary

1187:   one from Theorem~\ref{T KhoNer94} since the size of the injective

1188:   presentation is not known.

1189: \end{remark}

1190: 

1191: We derive a number of consequences on the uniform and non-uniform

1192: complexity of the first-order theories of string/tree

1193: automatic structures of bounded degree. The first one concerns the

1194: uniform model checking problems and is a direct consequence of the

1195: above theorem.

1196: 

1197: \begin{corollary}

1198:  The following holds:

1199: \begin{itemize}

1200: \item The model checking problem $\Decision(\mathsf{iSAb})$ belongs to

1201:   {\sf 2EXPSPACE}.

1202: \item The model checking problem $\Decision(\mathsf{SAb})$ belongs to

1203:   {\sf 3EXPSPACE}.

1204: \item The model checking problem $\Decision(\mathsf{iTAb})$ belongs to

1205:   {\sf 4EXPTIME}.

1206: \end{itemize}

1207: \end{corollary}

1208: 

1209: Next we concentrate on the non-uniform complexity, where the 

1210: structure is fixed. For string automatic

1211: structures, we do not get a better upper bound in this case

1212: (statement~(i) below) except in case of polynomial growth

1213: (statement~(ii) below).

1214: 

1215: \begin{corollary}\label{C automatic}

1216:   Let $\mcA$ be a string automatic structure of bounded degree.

1217:   \begin{enumerate}[(i)]

1218:   \item Then $\FOTh(\mcA)$ belongs to {\sf 2EXPSPACE}.

1219:   \item If $\mcA$ has polynomial growth then $\FOTh(\mcA)$ belongs to

1220:     {\sf EXPSPACE}.

1221:   \end{enumerate}

1222: \end{corollary}

1223: 

1224: \begin{proof}

1225:   Since $\mcA$ is string automatic, it has a fixed injective string

1226:   automatic presentation~$P$, i.e., $|P|$ and $m$ are fixed constants.

1227:   Hence the result follows immediately from (1) in

1228:   Theorem~\ref{T-upper}.

1229: 

1230:   Now suppose that $\mcA$ has polynomial growth, i.e.,

1231:   $g'_\mcA(x)\in x^{O(1)}$. Then, again, the claim follows

1232:   immediately from (1) in Theorem~\ref{T-upper}, since

1233:   $g'_\mcA(2^{|\varphi|})^{O(m)}\le 2^{O(|\varphi|)}$.\qed

1234: \end{proof}

1235: 

1236: The last consequence of Theorem~\ref{T-upper} concerns tree automatic

1237: structures. Here, we can improve the upper bound from

1238: Theorem~\ref{T-upper} for the non-uniform case by one exponent. In

1239: case of polynomial growth, we can save yet another exponent:

1240: 

1241: \begin{corollary}\label{C tree automatic}

1242:   Let $\mcA$ be a tree automatic structure of bounded degree.

1243:   \begin{enumerate}[(i)]

1244:   \item Then $\FOTh(\mcA)$ belongs to {\sf 3EXPTIME}.

1245:   \item If $\mcA$ has polynomial growth then $\FOTh(\mcA)$ belongs to

1246:     {\sf 2EXPTIME}.

1247:   \end{enumerate}

1248: \end{corollary}

1249: 

1250: \begin{proof}

1251:   Since $\mcA$ is tree automatic, it has a fixed injective

1252:   tree automatic presentation~$P$. Hence, again, the first

1253:   claim follows immediately from (3) in Theorem~\ref{T-upper}.

1254: 

1255:   Now suppose that $\mcA$ has polynomial growth, i.e.,

1256:   $g'_\mcA(x)\in x^{O(1)}$. Then the claim follows since

1257:   \[

1258:      \exp(1,g'_\mcA(2^{|\varphi|})^{O(m)})

1259:        \le \exp(1,2^{O(|\varphi|)}) = \exp(2,O(|\varphi|))\ ,

1260:   \]

1261:   implying that the problem belongs to {\sf 2EXPTIME}.\qed

1262: \end{proof}

1263: 

1264: \subsubsection{Two observations on the growth function}

1265: 

1266: We complement this section with a short excursion into the field of

1267: growth functions of automatic structures. The two results to be

1268: reported indicate that these growth functions do not behave as nicely

1269: as one would wish. Fortunately, these negative findings are of no

1270: importance to our main concerns.

1271: 

1272: Recall that the growth rate of a regular language is either bounded by

1273: a polynomial from above or by an exponential function from below and

1274: that it is decidable which of these cases applies. The next lemmas

1275: show that the analogous statements for growth functions of string

1276: automatic structures are false.

1277: 

1278: \begin{lemma}

1279:   There is a string automatic graph of intermediate growth (i.e., the growth

1280:   is neither exponential nor polynomial).

1281: \end{lemma}

1282: 

1283: \begin{proof}

1284:   Let $L=\{0,1\}^*\$\{0,1\}^*$ and let $E$ be %the symmetric closure of

1285:   \[

1286:     \{(u\$bv,ub\$v)\mid u,v\in \{0,1\}^*,b\in\{0,1\}\}

1287:     \cup \{(u\$,\$ub)\mid u\in\{0,1\}^*,b\in\{0,1\}\}\ .

1288:   \]

1289:   Then $T = (L,E)$ is a string automatic tree obtained from the complete

1290:   binary tree $\$\{0,1\}^*$ by adding a path of length $n$ between $u$

1291:   and $ub$ for $u\in\{0,1\}^n$ and $b\in\{0,1\}$.  Hence, a path of

1292:   length $n$ starting in the root $\$$ of $T$ branches at distance

1293:   $0,2,5,10,\ldots, i^2+1, \ldots, \lfloor\sqrt{n-1}\rfloor^2+1$ from

1294:   the root.  Hence, for the growth function $g_T$ we

1295:   obtain the following estimate:

1296:   $$

1297:   g_T(n) \in \sum_{i=0}^{\Theta(\sqrt{n})} (i+1) \cdot 2^i = \Theta(\sqrt{n})

1298:   \cdot 2^{\Theta(\sqrt{n})} = 2^{\Theta(\sqrt{n})}

1299:   $$

1300: \qed

1301: \end{proof}

1302: 

1303: \begin{lemma}

1304:   It is undecidable whether a string automatic graph of bounded degree has

1305:   polynomial growth.

1306: \end{lemma}

1307: 

1308: \begin{proof}

1309:   We show the undecidability by a reduction of the halting problem

1310:   (with empty input) for  Turing machines. So let $N$ be a Turing

1311:   machine. We can transform $N$ into a deterministic reversible Turing

1312:   machine $M$ such that:

1313:   \begin{enumerate}[(i)]

1314:   \item $N$ halts on empty input if and only if $M$ does so.

1315:   \item $M$ does not allow infinite sequences of backwards steps

1316:     (i.e., there are no configurations $c_i$ with $c_{i+1}\vdash_M

1317:     c_i$ for all $i\in\dN$), see also \cite{KusL08b} for a similar construction.

1318:   \end{enumerate}

1319:   Let $C$ be the set of configurations of $M$ (a regular set) and

1320:   $c_0$ the initial configuration with empty input. Now define

1321:   $L=(\{0,1\}C)^+$ (we assume that $0$ and $1$ do not belong to 

1322:   the alphabet of $C$) and

1323:   \begin{align*}

1324:     E \ = \ & \{(uac,uac')\mid u\in L\cup\{\varepsilon\}, a\in\{0,1\}, 

1325:                              c,c'\in C, c\vdash_M c'\} \ \cup \\

1326:             & \{(uac,uacbc_0)\mid u\in L\cup\{\varepsilon\}, a,b\in\{0,1\},

1327:                              c\in C\text{ is halting}\}\ .

1328:   \end{align*}

1329:   Then $(L,E)$ is an automatic directed graph. Since $M$ is

1330:   reversible, it is a forest of rooted trees (by (ii)). 

1331: 

1332:   First suppose there are configurations $c_1,c_2,\dots,c_n$ with

1333:   $c_{i-1}\vdash_M c_i$ for $1\leq  i \leq n$ such that $c_n$ is

1334:   halting. Then the set $0(c_n\{0,1\})^*\{c_0,c_1,\dots,c_n\}$

1335:   forms an infinite tree in $(L,E)$. Any branch in this tree branches

1336:   every $n$ steps. Hence $(L,E)$ has exponential growth.

1337: 

1338:   Now assume that $c_0$ is the starting point of an infinite

1339:   computation.  Let $T$ be any tree in the forest $(L,E)$. Then its

1340:   root is of the form $uac\in L$ with $u \in L \cup \{\varepsilon\}$, 

1341:   $a\in\{0,1\}$, and $c\in C$ such

1342:   that $c$ is no successor configuration of any other

1343:   configuration. There are two possibilities:

1344:   \begin{enumerate}

1345:   \item The configuration $c$ is the starting configuration of an

1346:     infinite computation of $M$. Then $T$ is an infinite path.

1347:   \item There is a halting configuration $c'$ and $n\in\dN$ with

1348:     $c\vdash^n_M c'$. Then $T$ starts with a path of length $n$. The

1349:     final node of this path has two children, namely $u a c' 0 c_0$

1350:     and $u a c' 1 c_0$. But,

1351:     since $M$ does not halt on the empty input,

1352:     each of these nodes is the root of an infinite path.

1353:   \end{enumerate}

1354:   Thus, in this case $(L,E)$ has polynomial (even linear) growth.\qed

1355: \end{proof}

1356: 

1357: 

1358: \section{Lower bounds}

1359: 

1360: In this section, we will prove that the upper complexity bounds for

1361: the non-uniform problems (Cor.~\ref{C automatic} and

1362: Cor.~\ref{C tree automatic}) are sharp. This will imply that the complexity of

1363: the uniform problem for injective string automatic presentations from

1364: Theorem~\ref{T-upper} is sharp as well.

1365: 

1366: For a binary relation $r$ and $m \in \dN$ we denote with $r^m$ the

1367: $m$-fold composition of $r$. Then the following lemma is folklore.

1368: 

1369: \begin{lemma} \label{L long paths}

1370:   Let the signature $\mcS$ contain a binary symbol $r$.  {}From a given

1371:   number $m$ (encoded unary), we can construct in linear time a

1372:   formula $\varphi_m(x,y)$ such that for every

1373:   $\mcS$-structure $\mcA$ and all elements $a,b \in \mcA$ we have:

1374:   $(a,b) \in r^{2^m}$ if and only if $\mcA \models \varphi_m(a,b)$.

1375: \end{lemma}

1376: %

1377: \begin{proof}

1378:   Let $\varphi_0(x,y)=r(x,y)$ and, for $m>0$ define

1379:   \[

1380:     \varphi_m(x,y)=\exists

1381:     z\forall x',y'(((x'=x\land y'=z)\lor(x'=z\land y'=y))

1382:      \rightarrow\varphi_{m-1}(x',y'))\ .

1383:   \]

1384:   \qed

1385: \end{proof}

1386: 

1387: 

1388: For a bit string $u = a_1 \cdots a_m$ ($a_i \in \{0,1\}$) let $\val(u)

1389: = \sum_{i=0}^{m-1} a_{i+1} 2^i$ be the integer value represented by

1390: $u$. Vice versa, for $0 \leq i \leq 2^m-1$ let $\bin_m(i) \in

1391: \{0,1\}^m$ be the unique string with $\val(\bin_m(i)) = i$.

1392: 

1393: \begin{theorem} \label{T 2EXPSPACE}

1394: There exists a fixed string automatic structure $\mcA$ of bounded degree

1395: such that $\FOTh(\mcA)$ is {\sf 2EXPSPACE}-hard.

1396: \end{theorem}

1397: 

1398: \begin{proof}

1399:   Let $M$ be a fixed Turing machine with a space bound of $\exp(2,n)$

1400:   such that $M$ accepts a {\sf 2EXPSPACE}-complete language; such a machine

1401:   exists by standard arguments.  Let $\Gamma$ be the tape alphabet,

1402:   $\Sigma\subseteq \Gamma$ be the input alphabet, and $Q$ be the set

1403:   of states. The initial (resp. accepting) state is $q_0 \in Q$

1404:   (resp. $q_f \in Q$), the blank symbol is $\Box \in \Gamma \setminus

1405:   \Sigma$. Let $\Omega = Q \cup \Gamma$.  A configuration of $M$ is

1406:   described by a string from $\Gamma^* Q \Gamma^+ \subseteq \Omega^+$

1407:   (later, symbols of configurations will be preceded with additional

1408:   counters). For two configurations $u$ and $v$ with $|u|=|v|$ we

1409:   write $u \vdash_M v$ if $u$ can evolve with a single $M$-transition

1410:   into $v$.  Note that there exists a relation $\alpha_M \subseteq

1411:   \Omega^3 \times \Omega^3$ such that for all configurations $u = a_1

1412:   \cdots a_m$ and $v = b_1 \cdots b_m$ ($a_i, b_i \in \Omega$) we have

1413:   \begin{equation}\label{equiv alpha}

1414:   u \vdash_M v \quad \Longleftrightarrow \quad

1415:   \forall i \in \{1, \ldots,m-2\} : (a_i a_{i+1} a_{i+2}, b_i b_{i+1}

1416:   b_{i+2}) \in \alpha_M.

1417:   \end{equation}

1418:   Let $\Delta = \{0,1,\#\} \cup \Omega$, and let $\pi : \Delta \to

1419:   \Omega \cup \{\#\}$ be the projection morphism with $\pi(a)=a$ for

1420:   $a \in \Omega \cup \{\#\}$ and $\pi(0)=\pi(1)=\varepsilon$.  For $m

1421:   \in \dN$, a string $x \in \Delta^*$ is an \emph{accepting

1422:     $2^m$-computation} if $x$ can be factorized as $x = x_1 \# x_2 \#

1423:   \cdots x_n\#$ for some $n \geq 1$ such that the following holds:

1424:   \begin{itemize}

1425:   \item For every $1 \leq i \leq n$ there exist 

1426:   $a_{i,0}, \ldots, a_{i,2^m-1} \in \Omega$ 

1427:   such that $x_i = \prod_{j=0}^{2^m-1} \bin_m(j) a_{i,j}$.

1428:   \item For every $1 \leq i \leq n$,  $\pi(x_i) \in \Gamma^* Q \Gamma^+$.

1429:   \item $\pi(x_1) \in q_0 \Sigma^* \Box^*$ and 

1430:   $\pi(x_n) \in \Gamma^* q_f \Gamma^+$

1431:   \item For every $1 \leq i < n$,  $\pi(x_i) \vdash_M \pi(x_{i+1})$.

1432:   \end{itemize} 

1433:   {}From $M$ we now construct a fixed string automatic structure $\mcA$ of

1434:   bounded degree. We start with the following regular language $U_0$:

1435:   \begin{align}

1436:   U_0 \ =\ & \pi^{-1}( (\Gamma^* Q \Gamma^+\#)^*) \ \cap \label{U0-1}\\

1437:         & (0^+ \Omega ( \{0,1\}^+ \Omega )^* 1^+ \Omega \#)^+  \ \cap \label{U0-2}\\

1438:         & 0^+ q_0 (\{0,1\}^+ \Sigma)^* (\{0,1\}^+ \Box)^* \# \Delta^* \ \cap

1439:         \label{U0-3}\\

1440:         & \Delta^* q_f (\Delta \setminus \{\#\})^* \# \label{U0-4}

1441:   \end{align}

1442:   A string $x \in U_0$ is a candidate for an accepting

1443:   $2^m$-computation of $M$.  With (\ref{U0-1}) we describe the basic

1444:   structure of such a computation, it consists of a list of

1445:   configurations separated by~$\#$.  Moreover, every symbol in a

1446:   configuration is preceded by a bit string, which represents a {\em

1447:     counter}.  By (\ref{U0-2}) every counter is non-empty, the first

1448:   symbol in a configuration is preceded by a counter from $0^+$, the

1449:   last symbol is preceded by a counter from $1^+$. Moreover, by

1450:   (\ref{U0-3}), the first configuration is an initial configuration,

1451:   whereas by (\ref{U0-4}), the last configuration is accepting

1452:   (i.e. the current state is $q_f$).

1453: 

1454:   For the further considerations, let us fix some $x \in U_0$. Hence,

1455:   we can factorize $x$ as $x = x_1 \# x_2 \# \cdots x_n\#$ such that:

1456:   \begin{itemize}

1457:   \item For every $1 \leq i \leq n$, there exist $m_i \geq 1$, 

1458:   $a_{i,0}, \ldots, a_{i,m_i} \in \Omega$ and counters

1459:   $u_{i,0}, \ldots, u_{i,m_i} \in \{0,1\}^+$ such that

1460:   $x_i = \prod_{j=0}^{m_i} u_{i,j} a_{i,j}$.

1461:   \item For every $1 \leq i \leq n$,  

1462:   $u_{i,0} \in 0^+$, $u_{i,m_i} \in 1^+$, and

1463:   $\pi(x_i) \in \Gamma^* Q \Gamma^+$.

1464:   \item $\pi(x_1) \in q_0 \Sigma^* \Box^*$ and 

1465:   $\pi(x_n) \in \Gamma^* q_f \Gamma^+$

1466:   \end{itemize}

1467:   We next want to construct, from $m\in\dN$, a small formula

1468:   expressing that $x$ is an accepting $2^m$-computation. To achieve

1469:   this, we add some structure around strings

1470:   from~$U_0$. Then the formula we are seeking has to ensure two facts:

1471:   \begin{enumerate}[(a)]

1472:   \item The counters behave correctly, i.e. for all $1 \leq i \leq n$

1473:     and $0 \leq j \leq m_i$, we have $|u_{i,j} | = m$ and if $j < m_i$,

1474:     then $\val(u_{i,j+1}) = \val(u_{i,j})+1$.  Note that this enforces

1475:     $m_i = 2^m-1$ for all $1 \leq i \leq n$.

1476:   \item For two successive configurations, the second one is the

1477:     successor configuration of the first one with respect to the machine

1478:     $M$, i.e., $\pi(x_i) \vdash_M \pi(x_{i+1})$ for all $1 \leq i < n$.

1479:   \end{enumerate}

1480:   In order to achieve (a), we introduce the following three binary

1481:   relations; it is straightforward to exhibit 2-dimensional automata for these

1482:   relations:

1483:   \begin{align*}

1484:   \delta \ =\ & \{ (w,\, w \otimes w) \mid w \in U_0 \} \\

1485:   \sigma_0 \ = \ & \{  \bigl( (0 v_1 \# 0 v_2 \# \cdots 0 v_n\#) \otimes w, \, 

1486:   (v_1 0 \# v_2 0 \# \cdots v_n 0\#) \otimes w \bigr) \mid \\

1487:   & \qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad w \in U_0, v_1,\ldots,v_n \in

1488:   (\Delta\setminus\{\#\})^* \}  \\

1489:   \sigma_\Omega \ = \ & \{  \bigl( (a_1 v_1 \# a_2 v_2 \# \cdots a_n v_n\#) \otimes w, \, 

1490:   (v_1 a_1 \# v_2 a_2 \# \cdots v_n a_n\#) \otimes w \bigr) \mid \\

1491:   & \qquad\qquad\qquad\qquad\qquad\qquad\qquad\qquad w \in U_0, 

1492:   a_1,\ldots,a_n \in \Omega, v_1,\ldots,v_n \in (\Delta\setminus\{\#\})^* \} 

1493:   \end{align*}

1494:   Hence, $\delta$ just duplicates a string from $U_0$ and $\sigma_0$

1495:   cyclically rotates every configuration to the left for one symbol, provided the

1496:   first symbol is $0$, whereas $\sigma_\Omega$ rotates symbols from

1497:   $\Omega$.  Moreover, let $U_1$ be the following regular language

1498:   over $\Delta^* \otimes \Delta^*$:

1499:   $$

1500:   U_1 \ = \ \biggr(\bigl(\{ u \otimes v \mid u, v \in \{0,1\}^+, |u|=|v|, \val(u) = \val(v)+1

1501:   \ \modulo \ 2^{|u|} \} (\Omega

1502:   \times \Omega) \bigr)^+ (\#,\#) \biggl)^+

1503:   $$

1504:   Clearly, $U_1$ is a regular language.  The crucial fact is the

1505:   following:

1506: 

1507:   \medskip

1508: 

1509:   \noindent {\bf Fact 1.} For every $m \in \dN$, the following two

1510:   properties are equivalent (recall that $x \in U_0$):

1511:   \begin{itemize}

1512:   \item There exist

1513:   $y_1, y_2, y_3 \in \Delta^* \otimes \Delta^*$ such that

1514:   $\delta(x,y_1)$, $\sigma_0^{m}(y_1,y_2)$, $\sigma_\Omega(y_2,y_3)$, $y_3 \in U_1$.

1515:   \item For all

1516:   $1 \leq i \leq n$ and $0 \leq j \leq m_i$, we have 

1517:   $|u_{i,j}| = m$ and if $j < m_i$, then 

1518:   $\val(u_{i,j+1}) = \val(u_{i,j})+1$. 

1519:   \end{itemize}

1520:   Assume now that $x \in U_0$ satisfies one (and hence both) of the

1521:   two properties from Fact 1 for some $m$. It follows that $m_i = 2^m-1$

1522:   for all $1 \leq i \leq n$ and

1523:   \begin{equation}\label{string x}

1524:   x= x_1 \# x_2 \# \cdots x_n \#, \text{ where } x_i = \prod_{j=0}^{2^m-1} \bin_m(j)

1525:   a_{i,j} \text{ for every } 1 \leq i \leq n\ .

1526:   \end{equation}

1527:   In order to establish (b) we need additional structure. The idea is,

1528:   for every counter value~$0\le j<2^m$, to have a word $y_j$ that

1529:   coincides with $x$, but has all the occurrences of $\bin_m(j)$

1530:   marked. Then an automaton can check that successive occurrences of

1531:   the counter $\bin_m(j)$ obey the transition condition of the Turing

1532:   machine. There are two problems with this approach: first, in order

1533:   to relate $x$ and $y_j$, we would need a binary relation of

1534:   degree~$2^m$ (for arbitrary $m$) and, secondly, an automaton cannot

1535:   mark all the occurrences of $\bin_m(j)$ at once (for some $j$). 

1536:   In order to solve these problems, we introduce a

1537:   binary relation $\mu$, which for every $x \in U_0$ as in

1538:   (\ref{string x}) generates a binary tree of depth~$m$ with root $x$;

1539:   this will be the only relation in our string automatic structure that

1540:   causes exponential growth. This relation will mark in $x$ every

1541:   occurrence of an arbitrary counter. For this, we need two copies

1542:   $\ol 0$ and $\ul 0$ of $0$ as well as two copies $\ol 1$ and $\ul 1$

1543:   of $1$. For $b\in\{0,1\}$, define the mapping

1544:   \[

1545:     f_b : \{ \ul{0}, \ol{0}, \ul{1}, \ol{1} \}^* \{0,1\}^+ \to  

1546:           \{ \ul{0}, \ol{0}, \ul{1}, \ol{1} \}^+ \{0,1\}^*

1547:   \]

1548:   as follows (where $u \in \{ \ul{0}, \ol{0}, \ul{1}, \ol{1} \}^*$, $c

1549:   \in \{0,1\}$, and $v \in \{0,1\}^*$):

1550:   \[

1551:     f_b(u c v) = 

1552:      \begin{cases}

1553:        u \ul{c} v & \text{if $b \neq c$} \\

1554:        u \ol{c}  v & \text{if $b = c$}

1555:      \end{cases}

1556:   \]

1557:   We extend $f_b$ to a function on $((\{\ul{0}, \ol{0}, \ul{1}, \ol{1}

1558:   \}^*\{0,1\}^+\Omega)^+ \#)^*$ as follows: Let $w = w_1 a_1 \cdots

1559:   w_\ell a_\ell$ with $w_i \in \{\ul{0}, \ol{0}, \ul{1}, \ol{1}

1560:   \}^*\{0,1\}^+$ and $a_i \in \Omega \cup \Omega\#$.  Then $f_b(w) =

1561:   f_b(w_1) a_1 \cdots f_b(w_\ell) a_\ell$; this mapping can be computed with

1562:   a synchronized transducer. Hence, the relation

1563:   \[

1564:     \mu = f_0\cup f_1

1565:         = \{(u,f_b(u)) \mid 

1566:                u\in((\{\ul 0,\ol 0,\ul 1,\ol 1\}^*\{0,1\}^+\Omega)^+\#)^*, 

1567:                b\in\{0,1\}\}

1568:   \] 

1569:   can be recognized by a 2-dimensional automaton.

1570: 

1571:   Let $x\in U_0$ as in (\ref{string x}), let the word $y$ be obtained

1572:   from $x$ by overlining or underlining each bit in $x$, and let

1573:   $u\in\{0,1\}^m$ be some counter. We say \emph{the counter $u$ is

1574:     marked in $y$} if every occurrence of the counter $u$ is marked by

1575:   overlining each bit, whereas all other counters contain at least one

1576:   underlined bit.

1577: 

1578:   \medskip

1579: 

1580:   \noindent {\bf Fact 2.} Let $x \in U_0$ be as in (\ref{string x}).

1581:   \begin{itemize}

1582:   \item For all counters $u\in\{0,1\}^m$, there exists a unique

1583:     word~$y$ with $(x,y)\in\mu^m$ such that the counter $u$ is marked

1584:     in~$y$.

1585:   \item If $(x,y)\in\mu^m$, then there exists a unique counter $u \in

1586:     \{0,1\}^m$ such that $u$ is marked in $y$.

1587:     %If $(x,y)\in\mu^m$ and $\ol u\in\{\ol0,\ol1\}^m$ is a factor of

1588:     %$y$, then the counter $u$ (obtained from $u$ by replacing $\ol b$

1589:     %by $b$ for $b\in\{0,1\}$) is marked in $y$.

1590:   \end{itemize}

1591:   Now, we can achieve our final goal, namely checking whether two

1592:   successive configurations in $x \in U_0$ represent a transition of

1593:   the machine $M$. Let the counter $u \in \{0,1\}^m$ be marked in~$y$.

1594:   We describe a finite automaton $A_2$ that checks on the string~$y$,

1595:   whether at position $\val(u)$ successive configurations in~$x$ are

1596:   ``locally consistent''.  The automaton $A_2$ searches for the first

1597:   marked counter in~$y$. Then it stores the next three symbols $a_1,

1598:   a_2, a_3$ from $\Omega$ (if the separator~$\#$ is seen before, then

1599:   only one or two symbols may be stored), walks right until it finds

1600:   the next marked counter, reads the next three symbols~$b_1, b_2,

1601:   b_3$ from $\Omega$, and checks whether $(a_1a_2a_3,

1602:   b_1b_2b_3) \in \alpha_M$, where $\alpha_M$ is from (\ref{equiv alpha}).  

1603:   If this is not the case, the automaton

1604:   will reject, otherwise it will store $b_1b_2b_3$ and repeat the

1605:   procedure described above.  Let $U_2 = L(A_2)$. Together with Fact~1

1606:   and 2, the behavior of $A_2$ implies that for all $x \in U_0$ and

1607:   all $m \in \dN$, $x$ represents an accepting $2^m$-computation of

1608:   $M$ if and only if

1609:   $$

1610:    \exists y_1, y_2, y_3 \ \biggl( \delta(x,y_1) \ \wedge \ \sigma_0^{m}(y_1,y_2)  \ \wedge \ \sigma_\Omega(y_2,y_3) 

1611:    \ \wedge \ y_3 \in U_1 \biggr) \ \wedge \

1612:    \forall y \ \biggl( \mu^m(x,y) \ \to \ y \in U_2  \biggr)\ .

1613:    $$

1614:   Let us now fix some input $w = a_1 a_2 \cdots a_n \in \Sigma^*$ with

1615:   $|w|=n$, and let $a_{n+1} = \Box$ and $m = 2^n$.  Thus, $w$ is

1616:   accepted by $M$ if and only if there exists an accepting

1617:   $2^m$-computation~$x$ such that in the first configuration of $x$,

1618:   the tape content is of the form $w \Box^+$.  It remains to add some

1619:   structure that allows us to express the latter by a

1620:   formula. But this is straightforward: 

1621:   Let $\triangleright$ be a new symbol and let 

1622:   $\Pi = \Delta  \cup \{\ul{0}, \ol{0}, \ul{1}, \ol{1}, \triangleright\}$;

1623:   this is our final alphabet.  Define the binary relations

1624:   $\iota_{0,1}$ and $\iota_a$ ($a \in \Omega$) as follows:

1625:   \begin{align*}

1626:   \iota_{0,1} \ =\ & \{ (u \triangleright a v, u a \triangleright v) \mid 

1627:   a \in \{0,1\}, u,v \in \Delta^*, 

1628:   u a v \in U_0 \} \ \cup \ \{ (0 v, 0 \triangleright v) \mid  v \in

1629:   \Delta^*, 0v \in U_0 \} \\

1630:    \iota_a \ =\ & \{ (u \triangleright a v, u a \triangleright v) \mid u,v \in \Delta^*, u a v \in U_0 \} \ . 

1631:   \end{align*}

1632:   Then,

1633:   $\mcA = (\Pi^* \cup (\Pi^* \otimes \Pi^*), \delta, \sigma_0, \sigma_\Omega,

1634:   \mu, \iota_{0,1}, (\iota_a)_{a \in \Omega}, U_0, U_1, U_2)$

1635:   is a string automatic structure of bounded degree

1636:   such that $w$ is accepted by $M$ if and

1637:   only if the following formula is true in $\mcA$:

1638:   \[

1639:   \exists x \in U_0 \left\{ 

1640:   \begin{array}{l}

1641:    \exists y_1, y_2, y_3 \ \biggl( \delta(x,y_1) \ \wedge \ \sigma_0^{m}(y_1,y_2)  \ \wedge \ \sigma_\Omega(y_2,y_3) 

1642:    \ \wedge \ y_3 \in U_1 \biggr) \ \wedge \\

1643:    \forall y \ \biggl( \mu^m(x,y) \ \to \  y \in U_2   \biggr) \ \wedge

1644:    \\ 

1645:    \displaystyle

1646:    \exists y_0,z_0, \ldots, y_{n+1},z_{n+1} \biggl(  \iota_{0,1}^m(x,y_0) \

1647:    \wedge \ \iota_{q_0}(y_0,z_0) \ \wedge \ \bigwedge_{i=1}^{n+1}

1648:    \iota_{0,1}^m(z_{i-1},y_i) \, \wedge \, 

1649:    \iota_{a_i}(y_i,z_i) \biggr)

1650:   \end{array}\right\}

1651:   \]

1652:   By Lemma~\ref{L long paths} we can compute in time $O(\log(m)) =

1653:   O(n)$ an equivalent formula over the signature of $\mcA$.  This

1654:   concludes the proof.  \qed

1655: \end{proof}

1656: 

1657: The following theorem, which proves an analogous result for

1658: tree automatic structures, uses alternating Turing machines, see

1659: \cite{ChaKS81,Pap94} for more details. Roughly speaking, an

1660: \emph{alternating Turing machine} is a nondeterministic Turing

1661: machine, where the set of states is partitioned into accepting,

1662: existential, and universal states. A configuration is accepting, if

1663: either (i) the current state is accepting, or (ii) the current state

1664: is existential and at least one successor configuration is accepting,

1665: or (iii) the current state is universal and every successor

1666: configuration is accepting.  By \cite{ChaKS81}, $k${\sf EXPTIME} is the set

1667: of all problems that can be accepted in space $\exp(k-1,n^{O(1)})$ on an

1668: alternating Turing machine (for all $k \geq 1$).

1669: 

1670: \begin{theorem} \label{T 3EXPTIME} There exists a fixed tree automatic

1671:   structure $\mcA$ of bounded degree such that $\FOTh(\mcA)$ is

1672:   {\sf 3EXPTIME}-hard.

1673: \end{theorem}

1674: 

1675: \begin{proof}

1676: Let $M$ be a fixed {\em alternating} Turing machine with a 

1677: space bound of $\exp(2,n)$ such that $M$ accepts a {\sf 3EXPTIME}-complete language.

1678: W.l.o.g. every configuration, where the current state is either existential

1679: or universal has exactly two successor configurations. 

1680: Let $\Sigma$, $\Gamma$, $Q$, and $\Omega$ have the same meaning as in the

1681: previous proof. Moreover, let $\Delta = \Omega \cup \{ 0,1, \#_\exists, \#_\forall \}$.

1682: 

1683: The idea is that a binary tree $x$ over the alphabet $\Delta$ can 

1684: encode a computation tree for some input. Configurations can be encoded

1685: by linear chains over the alphabet $\Omega \cup \{0,1\}$ as in the previous proof.

1686: The separator symbol 

1687: $\#_\exists$ is used to separate an existential configuration from 

1688: a successor configuration, whereas the

1689: separator symbol $\#_\forall$ is used to separate a universal configuration from 

1690: its two successor configurations. Hence, a $\#_\exists$-labeled node has 

1691: exactly one child, whereas a $\#_\forall$-labeled node has 

1692: exactly two children.

1693: Checking whether the counters 

1694: behave correctly can be done similarly to the previous proof by introducing

1695: binary relations $\sigma_0$ and $\sigma_\Omega$, which rotate symbols within

1696: configurations. Remember that in our tree encoding, configurations are just

1697: long chains. Also the marking of some specific counter

1698: can be done in the same way as before. Finally, having marked

1699: some specific counter allows to check with a top-down tree automaton, 

1700: whether the tree $x$ represents

1701: indeed  a valid computation tree. Of course, the tree automaton 

1702: has to check whether the current configuration is existential or universal.

1703: In case of a universal configuration, the automaton branches at the next

1704: separator symbol $\#_\forall$. If e.g. the current configuration is universal but 

1705: the next separator symbol is $\#_\exists$, then the automaton rejects the tree. 

1706: \qed

1707: \end{proof}

1708: 

1709: The proof of the next result is in fact a simplification of 

1710: the proof of Theorem~\ref{T 2EXPSPACE}, since we do not need

1711: counters.

1712: 

1713: \begin{theorem} \label{T EXPSPACE}

1714: There exists a fixed string automatic structure $\mcA$ of bounded degree

1715: and polynomial growth (in fact linear growth)

1716: such that $\FOTh(\mcA)$ is {\sf EXPSPACE}-hard.

1717: \end{theorem}

1718: 

1719: \begin{proof}

1720: Let $M$ be a fixed Turing machine with a

1721: space bound of $2^n$ such that $M$ accepts an {\sf EXPSPACE}-complete language.

1722: Let $\Sigma$, $\Gamma$, $Q$, $q_0$, $q_f$, $\Box$, and $\Omega$ have

1723: the usual meaning.

1724: Let $\Delta = \{\#\} \cup \Omega$.

1725: This time, for $m \in \dN$, an {\em accepting $m$-computation} is

1726: a string $x_1 \# x_2 \# \cdots x_n \#$, where 

1727: $x_1, \ldots, x_n \in \Gamma^* Q \Gamma^+$

1728: are configurations with $|x_i| = m$ ($1 \leq i \leq n$),

1729: $x_i \vdash_M x_{i+1}$ ($1 \leq i < n$), $x_1 \in q_0 \Sigma^* \Box^*$, and

1730: $x_n \in \Gamma^* q_f \Gamma^+$.

1731: Let $U_0$ be the fixed regular language 

1732: $$

1733: U_0 \ = \  (\Gamma^* Q \Gamma^+\#)^+ \ \cap \

1734:  q_0 \Sigma^* \Box^* \# \Delta^* \ \cap \ \Delta^* q_f (\Delta \setminus

1735:  \{\#\})^* \#\ .

1736: $$

1737: The following binary relations $\delta$ and $\sigma_\Omega$

1738: can be easily recognized by 2-dimensional automata:

1739: \begin{align*}

1740: \delta \ =\ & \{ (w,\, w \otimes w) \mid w \in U_0 \} \\

1741: \sigma_\Omega \ = \ & \{ (av \otimes w, \, 

1742: va \otimes w) \mid w \in U_0, a \in \Omega, v \in \Delta^* \}  

1743: %\sigma_\# \ = \ &   \{ (\# v \otimes w, \, 

1744: %v\# \otimes w) \mid w \in U_0, v \in \Delta^* \}

1745: \end{align*}

1746: Moreover, let $U_1$ be the following regular language over $\Delta^* \otimes

1747: \Delta^*$:

1748: $$

1749: U_1 \ = \ \{ \# u \otimes v\# \mid u, v \in \Omega^+, |u|=|v|, v \vdash_M

1750: u\}^+ \{ \# u \otimes v\# \mid u, v \in \Omega^+, |u|=|v|\} \ .

1751: $$

1752: Then, for every $x \in U_0$ and $m \in \dN$ we have: $x$ is an

1753: accepting $m$-computation if and only if there exist $y_1, y_2

1754: \in \Delta^* \otimes \Delta^*$ such that $\delta(x,y_1)$,

1755: $\sigma_\Omega^{m}(y_1,y_2)$, and $y_2 \in U_1$.

1756: 

1757: Let us now fix some input $w = a_1 \cdots a_n \in \Sigma^*$ with $|w|=n$,

1758: let $a_{n+1} = \Box$, and let $m = 2^n$.

1759: Thus, $w$ is accepted by $M$ if and only if there exists 

1760: an accepting $m$-computation $x$ such that in the first configuration 

1761: of $x$, the tape content is of the form $w \Box^+$.

1762: It remains to add some structure that allows us 

1763: to express the latter by a formula.

1764: This can be done similarly to the proof of Theorem~\ref{T 2EXPSPACE}: 

1765: Let  $\Pi = \Delta \cup \{\triangleright\}$, where $\triangleright$ is a new symbol and

1766: define the binary relations $\iota_a$ 

1767: ($a \in \Sigma \cup \{\Box\}$) as follows: 

1768: $$

1769: \iota_a \ =\ 

1770: \{ (q_0 a v, q_0 a \triangleright v) \mid  v \in

1771: \Delta^*, q_0 a v \in U_0 \} \ \cup \

1772:  \{ (u \triangleright a v, u a \triangleright v) \mid u,v \in

1773: \Delta^*, u a v \in U_0 \}

1774: $$

1775: Then, 

1776: $\mcA = ( \Pi^* \cup (\Delta^* \otimes \Delta^*), \delta,

1777: \sigma_\Omega, (\iota_a)_{a \in \Sigma \cup \{\Box\}}, U_0, U_1)$

1778: is a fixed string automatic structure of bounded degree and linear growth.

1779: For the latter note that the Gaifman graph of $\mcA$ is just a

1780: disjoint union of cycles and finite paths (in fact, every node has degree

1781: at most 2). 

1782: %(for the relations $\sigma_\Omega$ and

1783: %$\sigma_\#$), where some finite paths are attached to (for the

1784: %relations $\delta$ and $\iota_a$). 

1785: Moreover, $w$ is accepted by $M$ if

1786: and only if the following statement is true in $\mcA$:

1787: \begin{equation} \label{reduction formula expspace}

1788: \exists x \in U_0 \left\{ 

1789: \begin{array}{l}

1790:  \exists y_1, y_2 \ \biggl( \delta(x,y_1) \ \wedge \ \sigma_\Omega^{m}(y_1,y_2)  

1791:  \ \wedge \ y_2 \in U_1 \biggr) \ \wedge \\ \displaystyle

1792:  \exists y_0, \ldots, y_n \biggl( \iota_{a_1}(x,y_0)  \ \wedge \

1793:   \bigwedge_{i=1}^n

1794:  \iota_{a_i}(y_{i-1},y_i)  \biggr)

1795: \end{array}\right\} \ .

1796: \end{equation}

1797: By Lemma~\ref{L long paths} this concludes the proof.

1798: \qed

1799: \end{proof}

1800: 

1801: The next result can be easily shown by combining the techniques from the proof

1802: of Theorem~\ref{T 3EXPTIME} and \ref{T EXPSPACE}. We leave the details for the reader.

1803: 

1804: \begin{theorem}

1805: There exists a fixed tree automatic structure $\mcA$ of bounded degree

1806: and polynomial growth (in fact linear growth)

1807: such that $\FOTh(\mcA)$ is {\sf 2EXPTIME}-hard.

1808: \end{theorem}

1809: 

1810: \section{Bounded quantifier alternation depth}

1811: 

1812: In this section we prove some facts about first-order fragments of

1813: fixed quantifier alternation depth. These results will follow easily

1814: from the constructions in the preceding section.

1815: 

1816: For $n \geq 0$, $\Sigma_n$-formulas and $\Pi_n$-formulas are

1817: inductively defined as follows:

1818: \begin{itemize}

1819: \item A quantifier-free first-order formula is a $\Sigma_0$-formula

1820: as well as a $\Pi_0$-formula.

1821: \item If $\varphi(x_1,\ldots,x_n,y_1,\ldots,y_m)$ 

1822: is a $\Sigma_n$-formula, then

1823: $\forall x_1 \cdots \forall x_n : \varphi(x_1,\ldots,x_n,y_1,\ldots,y_m)$

1824: is a $\Pi_{n+1}$-formula.

1825: \item If $\varphi(x_1,\ldots,x_n,y_1,\ldots,y_m)$ 

1826: is a $\Pi_n$-formula, then

1827: $\exists x_1 \cdots \exists x_n : \varphi(x_1,\ldots,x_n,y_1,\ldots,y_m)$

1828: is a $\Sigma_{n+1}$-formula.

1829: \end{itemize}

1830: The $\Sigma_n$-theory $\Sigma_n$-$\FOTh(\mcA)$ of a structure $\mcA$ is

1831: the set of all $\Sigma_n$-formulas in $\FOTh(\mcA)$; the

1832: $\Pi_n$-theory is defined analogously. For a class $\dC$ of tree

1833: automatic presentations, the \emph{$\Sigma_n$-model checking problem

1834:   $\Sigma_n$-$\Decision(\dC)$ of $\dC$} denotes the set of all pairs

1835: $(P,\varphi)$ where $P \in \dC$, and $\varphi \in \Sigma_n$-$\FOTh(\mcA(P))$.

1836: 

1837: 

1838: The following result can be found in \cite{BluG00}:

1839: 

1840: \begin{theorem}[cf.\ \cite{BluG00}]\label{T BluG00} 

1841:   The $\Sigma_1$-model checking problem

1842:   $\Sigma_1$-$\Decision(\mathsf{SA})$ for all string automatic

1843:   presentations is in {\sf PSPACE}.

1844:   Moreover, there is a fixed string automatic structure

1845:   with a {\sf PSPACE}-complete $\Sigma_1$-theory.

1846: \end{theorem}

1847: 

1848: {}From our construction in the proof of Theorem~\ref{T EXPSPACE},

1849: we can slightly sharpen the lower bound in this theorem:

1850: 

1851: \begin{theorem}

1852:   There exists a fixed string automatic structure of bounded degree

1853:   and linear growth with a {\sf PSPACE}-complete $\Sigma_1$-theory.

1854: \end{theorem}

1855: 

1856: \begin{proof}

1857: Take the structure $\mcA$ from the proof of Theorem~\ref{T EXPSPACE} and let 

1858: $M$ be a fixed linear bounded automaton with a {\sf PSPACE}-complete

1859: acceptance problem. If we replace the number $m$ in the formula

1860: (\ref{reduction formula expspace}) by the input length 

1861: $n$, then (\ref{reduction formula expspace}) is equivalent

1862: to the following formula, which is equivalent to a $\Sigma_1$-formula:

1863: $$

1864: \exists x \in U_0 \left\{ 

1865: \begin{array}{l} \displaystyle

1866:  \exists y_0, \ldots, y_{n+1} \ \biggl( \delta(x,y_0) \ \wedge \

1867:  \bigwedge_{i=0}^n \sigma_\Omega(y_i,y_{i+1})  

1868:  \ \wedge \ y_{n+1} \in U_1 \biggr) \ \wedge \\[5mm] \displaystyle

1869:  \exists y_1, \ldots, y_n \biggl( \iota_{a_1}(x,y_1)  \ \wedge \

1870:   \bigwedge_{i=2}^n

1871:  \iota_{a_i}(y_{i-1},y_i)  \biggr)

1872: \end{array}\right\} \ .

1873: $$

1874: This formula is true in $\mcA$ if and only if the linear

1875: bounded automaton accepts the input $w = a_1 \cdots a_n$.

1876: \qed

1877: \end{proof}

1878: 

1879: Let us now move on to $\Sigma_2$-formulas and structures of arbitrary growth:

1880: 

1881: \begin{theorem}\label{T Sigma2} 

1882:   The $\Sigma_2$-model checking problem

1883:   $\Sigma_2$-$\Decision(\mathsf{SA})$ for all string automatic

1884:   presentations is in {\sf EXPSPACE}.

1885:   Moreover, there is a string automatic structure of bounded

1886:   degree with an {\sf EXPSPACE}-complete $\Sigma_2$-theory.

1887: \end{theorem}

1888: 

1889: \begin{proof}

1890:   For the upper bound, let $P$ be a string automatic presentations of

1891:   the automatic structure $\mcA(P)=\mcA$ and let

1892:   $$

1893:   \psi = \exists x_1 \cdots \exists x_n \forall y_1 \cdots \forall y_m :

1894:   \varphi

1895:   $$ 

1896:   be a $\Sigma_2$-sentence. The sentence $\psi$ is equivalent to

1897:   $$

1898:   \exists x_1 \cdots \exists x_n \neg \exists y_1 \cdots \exists y_m :

1899:   \neg \varphi\ .

1900:   $$

1901:   Negations in $\neg \varphi$ can be moved down to the level of atomic

1902:   predicates.  Then, we can built an $(n+m)$-dimensional automaton for

1903:   $\neg \varphi$ with $\exp(1,|\psi|^{O(1)})$ many states. Projection

1904:   onto the tracks corresponding to the variables $x_1,\ldots,x_n$

1905:   results again into an automaton with $\exp(1,|\psi|^{O(1)})$ many

1906:   states.  Hence, for $\neg \exists y_1 \cdots \exists y_m : \neg

1907:   \varphi$ there exists an $n$-dimensional automaton with

1908:   $\exp(2,|\psi|^{O(1)})$ many states. But, we do not need to

1909:   construct this automaton explicitly but only have to check emptiness

1910:   of its language, which can be done on the fly in exponential space.

1911: 

1912:   For the lower bound, we reuse our construction from the proof of

1913:   Theorem~\ref{T 2EXPSPACE}. We start with an

1914:   $\exp(1,n)$-space-bounded machine $M$ that accepts an {\sf

1915:     EXPSPACE}-complete language. We carry out the same construction as

1916:   in the proof of Theorem~\ref{T 2EXPSPACE}, but replace $2^m$

1917:   (resp. $m$) everywhere by $m$ (resp. the input length $n$). In

1918:   addition, we need the following (trivial) analogue of Lemma~\ref{L

1919:     long paths}: Let the signature $\mcS$ contain a binary symbol $r$.

1920:   {}From a given number $n$ (encoded unary), we can construct in

1921:   linear time a $\Sigma_1$-formula $\varphi^{(n)}(x,y)$ such that for

1922:   every $\mcS$-structure $\mcA$ and all elements $a,b \in \mcA$ we

1923:   have: $(a,b) \in r^{n}$ if and only if $\mcA \models

1924:   \varphi^{(n)}(a,b)$.

1925: 

1926:   Then, the final formula from the proof of Theorem~\ref{T 2EXPSPACE}

1927:   can be written as

1928:   \[

1929:   \exists x \in U_0 \left\{ 

1930:   \begin{array}{l}

1931:    \exists y_1, y_2, y_3 \ \biggl( \delta(x,y_1) \ \wedge \ \sigma_0^{(n)}(y_1,y_2)  \ \wedge \ \sigma_\Omega(y_2,y_3) 

1932:    \ \wedge \ y_3 \in U_1 \biggr) \ \wedge \\

1933:    \forall y \ \biggl( \neg\mu^{(n)}(x,y) \ \lor \  y \in U_2   \biggr) \ \wedge

1934:    \\ 

1935:    \displaystyle

1936:    \exists y_0,z_0, \ldots, y_{n+1},z_{n+1} \biggl(  \iota_{0,1}^{(n)}(x,y_0) \

1937:    \wedge \ \iota_{q_0}(y_0,z_0) \ \wedge \ \bigwedge_{i=1}^{n+1}

1938:    \iota_{0,1}^{(n)}(z_{i-1},y_i) \, \wedge \, 

1939:    \iota_{a_i}(y_i,z_i) \biggr)

1940:   \end{array}\right\}.

1941:   \]

1942:   This formula is equivalent to a $\Sigma_2$-formula. Moreover, this 

1943:   formula is true in the string automatic structure $\mcA$ (of bounded degree)

1944:   from the proof of Theorem~\ref{T 2EXPSPACE}, if and only if the input $w = a_1

1945:   a_2 \cdots a_n$ is accepted by the machine $M$.

1946:   \qed

1947: \end{proof}

1948: 

1949: As before, Theorems~\ref{T BluG00}--\ref{T Sigma2} can be extended to

1950: tree automatic structures as follows:

1951: 

1952: \begin{theorem}

1953: The following holds:

1954:   \begin{enumerate}

1955:   \item The $\Sigma_1$-model checking problem

1956:     $\Sigma_1$-$\Decision(\mathsf{TA})$ for all tree automatic

1957:     presentations is in {\sf EXPTIME}.

1958:   \item There exists a fixed tree automatic structure of bounded

1959:     degree and linear growth with an {\sf EXPTIME}-complete

1960:     $\Sigma_1$-theory.

1961:   \item The $\Sigma_2$-model checking problem

1962:     $\Sigma_2$-$\Decision(\mathsf{TA})$ for all tree automatic

1963:     presentations is in {\sf 2EXPTIME}.

1964:   \item There exists a tree automatic structure of bounded

1965:     degree with a {\sf 2EXPTIME}-complete $\Sigma_2$-theory.

1966:   \end{enumerate}

1967: \end{theorem}

1968: 

1969: 

1970: \section{Open problems}

1971: 

1972: The most obvious open question regards the uniform first-order theory for

1973: (injective) tree automatic structures: we do not know whether it is

1974: {\sf 4EXPTIME}-hard. Moreover, we don't know

1975: an upper bound for the uniform first-order theory

1976: for arbitrary tree automatic structures. The reason is that we do not

1977: know the complexity of transforming such a presentation into an

1978: equivalent injective one (which is possible by~\cite{ColL07}).

1979: 

1980: In \cite{BluG00,KhoRS04}, it is shown that not only the

1981: first-order theory of every string automatic structure is (uniformly)

1982: decidable, but even its extension by the quantifiers ``there are

1983: infinitely many $x$ with \dots'' and ``the number of $x$ satisfying

1984: \dots is divisible by $p$''. In \cite{KusL08}, we proved that this

1985: extended theory can be decided in triply exponential time for

1986: ($\omega$)-automatic structures of bounded degree. It is not clear

1987: whether the doubly-exponential upper bound proved in this paper

1988: extends to this more expressive theory.

1989: 

1990: Recall that there are tree automatic structures which are not string

1991: automatic. Provided {\sf 2EXPSPACE} $\neq$ {\sf 3EXPTIME}, our results on the

1992: non-uniform first-order theories imply the existence of such a

1993: structure of bounded degree (namely the tree automatic structure

1994: constructed in the proof of Theorem~\ref{T 3EXPTIME}). But no example

1995: is known that does not rest on the complexity theoretic assumption

1996: {\sf 2EXPSPACE} $\neq$ {\sf 3EXPTIME}.

1997: 

1998: For $n \geq 3$, the precise complexity of the $\Sigma_n$-theory of a

1999: string/tree automatic structure of bounded degree remains open. We

2000: know that these theories belong to {\sf 2EXPSPACE} for string

2001: automatic structures and to {\sf 3EXPTIME} for tree automatic

2002: structures. Moreover, from our results for the $\Sigma_2$-fragment we

2003: obtain lower bounds of {\sf EXPSPACE} and {\sf 2EXPTIME},

2004: respectively.

2005: \begin{conjecture}

2006:   For every $n\geq3$, the problems 

2007:   $\Sigma_n$-$\Decision(\mathsf{SAb})$ and

2008:   $\Sigma_n$-$\Decision(\mathsf{TAb})$ 

2009:    belong to {\sf EXPSPACE} and {\sf 2EXPTIME}, respectively.

2010: \end{conjecture}

2011: A possible attack to this conjecture would follow the line of argument

2012: in the proof of Theorem~\ref{T-upper} and would therefore be based on

2013: Gaifman's theorem. To make this work, the exponential bound in

2014: Gaifman's theorem would have to be reduced which leads to the

2015: following conjecture.

2016: \begin{conjecture}

2017:   Let $\mcA$ be a structure, $(a_1,\ldots,a_k), (b_1,\ldots,b_k) \in

2018:   \mcA^k$, $d \geq 0$, and $D_1, \ldots, D_k \geq d\cdot 2^n$ such that

2019:   \begin{equation*}

2020:     (\mcA \rest (\bigcup_{i=1}^k S(D_i,a_i) ), \ a_1, \ldots, a_k) \simeq

2021:     (\mcA \rest (\bigcup_{i=1}^k S(D_i,b_i) ), \ b_1, \ldots, b_k)\ .

2022:   \end{equation*}

2023:   Then, for every $\Sigma_n$-formula $\varphi(x_1,\ldots,x_k)$ of

2024:   quantifier depth at most $d$, we

2025:   have: $$\mcA\models\varphi(a_1,\ldots,a_k) \ \Longleftrightarrow \

2026:   \mcA\models\varphi(b_1,\ldots,b_k) \ .$$

2027: 

2028: \end{conjecture}

2029: 

2030: \bibliographystyle{abbrv}

2031: %\bibliography{../../../BIBTEX/bib}

2032: %\bibliography{literatur}

2033: 

2034: \begin{thebibliography}{10}

2035: 

2036: \bibitem{Bar06}

2037: V.~B{\'a}r{\'a}ny.

2038: \newblock Invariants of automatic presentations and semi-synchronous

2039:   transductions.

2040: \newblock In {\em STACS'06}, Lecture Notes in Comp.\ Science vol.\ 3884, pages

2041:   289--300. Springer, 2006.

2042: 

2043: \bibitem{BarKR08}

2044: V.~B{\'a}r{\'a}ny, {\L}.~Kaiser, and S.~Rubin.

2045: \newblock Cardinality and counting quantifiers on omega-automatic structures.

2046: \newblock In {\em STACS'08}, pages 385--396. IFIB Schloss Dagstuhl, 2008.

2047: 

2048: \bibitem{BenLSS03}

2049: M.~Benedikt, L.~Libkin, T.~Schwentick, and L.~Segoufin.

2050: \newblock Definable relations and first-order query languages over strings.

2051: \newblock {\em J. ACM}, 50(5):694--751, 2003.

2052: 

2053: \bibitem{Blu99}

2054: A.~Blumensath.

2055: \newblock Automatic structures.

2056: \newblock Technical report, RWTH Aachen, 1999.

2057: 

2058: \bibitem{BluG00}

2059: A.~Blumensath and E.~Gr{\"a}del.

2060: \newblock Automatic {S}tructures.

2061: \newblock In {\em LICS'00}, pages 51--62. IEEE Computer Society Press, 2000.

2062: 

2063: \bibitem{ChaKS81}

2064: A.~K. Chandra, D.~C. Kozen, and L.~J. Stockmeyer.

2065: \newblock Alternation.

2066: \newblock {\em J.~ACM}, 28(1):114--133, 1981.

2067: 

2068: \bibitem{ColL07}

2069: T.~Colcombet and C.~L{\"o}ding.

2070: \newblock Transforming structures by set interpretations.

2071: \newblock {\em Logical Methods in Computer Science}, 3:1--36, 2007.

2072: 

2073: \bibitem{tata2007}

2074: H.~Comon, M.~Dauchet, R.~Gilleron, C.~L\"oding, F.~Jacquemard, D.~Lugiez,

2075:   S.~Tison, and M.~Tommasi.

2076: \newblock Tree automata techniques and applications.

2077: \newblock Available on: \url{http://www.grappa.univ-lille3.fr/tata}, 2007.

2078: \newblock Release October, 12th 2007.

2079: 

2080: \bibitem{ComH90}

2081: K.~Compton and C.~Henson.

2082: \newblock A uniform method for proving lower bounds on the computational

2083:   complexity of logical theories.

2084: \newblock {\em Annals of Pure and Applied Logic}, 48:1--79, 1990.

2085: 

2086: \bibitem{DelGK03}

2087: C.~Delhomm\'e, V.~Goranko, and T.~Knapik.

2088: \newblock Automatic linear orderings.

2089: \newblock Manuscript, 2003.

2090: 

2091: \bibitem{Elg61}

2092: C.~Elgot.

2093: \newblock Decision problems of finite automata design and related arithmetics.

2094: \newblock {\em Trans. Am. Math. Soc.}, 98:21--51, 1961.

2095: 

2096: \bibitem{EpsCHLPT92}

2097: D.~Epstein, J.~Cannon, D.~Holt, S.~Levy, M.~Paterson, and W.~Thurston.

2098: \newblock {\em Word Processing In Groups}.

2099: \newblock Jones and Bartlett Publishers, Boston, 1992.

2100: 

2101: \bibitem{Gai82}

2102: H.~Gaifman.

2103: \newblock On local and nonlocal properties.

2104: \newblock In J.~Stern, editor, {\em Logic Colloquium '81}, pages 105--135.

2105:   North-Holland, 1982.

2106: 

2107: \bibitem{Hod82}

2108: B.~Hodgson.

2109: \newblock On direct products of automaton decidable theories.

2110: \newblock {\em Theoretical Computer Science}, 19:331--335, 1982.

2111: 

2112: \bibitem{IshKR02}

2113: I.~Ishihara, B.~Khoussainov, and S.~Rubin.

2114: \newblock Some results on automatic structures.

2115: \newblock In {\em LICS'02}, pages 235--244. IEEE Computer Society Press, 2002.

2116: 

2117: \bibitem{KhoN95}

2118: B.~Khoussainov and A.~Nerode.

2119: \newblock Automatic presentations of structures.

2120: \newblock In {\em Logic and Computational Complexity}, Lecture Notes in Comp.\

2121:   Science vol.\ 960, pages 367--392. Springer, 1995.

2122: 

2123: \bibitem{KhoR01}

2124: B.~Khoussainov and S.~Rubin.

2125: \newblock Graphs with automatic presentations over a unary alphabet.

2126: \newblock {\em J.\ Autom.\ Lang.\ Comb.}, 6:467--480, 2001.

2127: 

2128: \bibitem{KhoRS03a}

2129: B.~Khoussainov, S.~Rubin, and F.~Stephan.

2130: \newblock On automatic partial orders.

2131: \newblock In {\em LICS'03}, pages 168--177. IEEE Computer Society Press, 2003.

2132: 

2133: \bibitem{KhoRS04}

2134: B.~Khoussainov, S.~Rubin, and F.~Stephan.

2135: \newblock Definability and regularity in automatic structures.

2136: \newblock In {\em STACS'04}, Lecture Notes in Comp.\ Science vol.\ 2996, pages

2137:   440--451. Springer, 2004.

2138: 

2139: \bibitem{Kus03}

2140: D.~Kuske.

2141: \newblock Is {C}antor's theorem automatic?

2142: \newblock In {\em LPAR'03}, Lecture Notes in Comp.\ Science vol.\ 2850, pages

2143:   332--345. Springer, 2003.

2144: 

2145: \bibitem{KusL08b}

2146: D.~Kuske and M.~Lohrey.

2147: \newblock Euler paths and ends in automatic and recursive graphs.

2148: \newblock In {\em Automata and Formal Languages 2008}, pages 245--256.

2149:   Hungarian Academy of Sciences, 2008.

2150: 

2151: \bibitem{KusL08}

2152: D.~Kuske and M.~Lohrey.

2153: \newblock First-order and counting theories of $\omega$-automatic structures.

2154: \newblock {\em Journal of Symbolic Logic}, 73:129--150, 2008.

2155: 

2156: \bibitem{KusL08a}

2157: D.~Kuske and M.~Lohrey.

2158: \newblock Hamiltonicity of automatic graphs.

2159: \newblock In G.~Ausiello, J.~Karhum\"aki, G.~Mauri, and L.~Ong, editors, {\em

2160:   IFIP-TCS'08}, pages 445--459. Springer, 2008.

2161: 

2162: \bibitem{Loh03}

2163: M.~Lohrey.

2164: \newblock Automatic structures of bounded degree.

2165: \newblock In {\em LPAR'03}, Lecture Notes in Comp.\ Science vol.\ 2850, pages

2166:   344--358. Springer, 2003.

2167: 

2168: \bibitem{Mey75}

2169: A.~Meyer.

2170: \newblock Weak monadic second order theory of one successor is not elementary

2171:   recursive.

2172: \newblock In {\em Proc. Logic Colloquium}, Lecture Notes in Mathematics vol.\

2173:   453, pages 132--154. Springer, 1975.

2174: 

2175: \bibitem{Pap94}

2176: C.~H. Papadimitriou.

2177: \newblock {\em Computational Complexity}.

2178: \newblock Addison Wesley, 1994.

2179: 

2180: \bibitem{Rub08}

2181: S.~Rubin.

2182: \newblock Automata presenting structures: A survey of the finite string case.

2183: \newblock {\em Bulletin of Symbolic Logic}, 14:169--209, 2008.

2184: 

2185: \bibitem{Sei92}

2186: H.~Seidl.

2187: \newblock Single-valuedness of tree transducers is decidable in polynomial

2188:   time.

2189: \newblock {\em Theoretical Computer Science}, 106:135--181, 1992.

2190: 

2191: \bibitem{SiSt04}

2192: P.~V. Silva and B.~Steinberg.

2193: \newblock A geometric characterization of automatic monoids.

2194: \newblock {\em The Quarterly Journal of Mathematics}, 55:333--356, 2004.

2195: 

2196: \bibitem{Web90}

2197: A.~Weber.

2198: \newblock On the valuedness of finite transducers.

2199: \newblock {\em Acta Informatica}, 27:749--780, 1990.

2200: 

2201: \end{thebibliography}

2202: 

2203: \end{document}