## Eti.uni-siegen.de

**Hamiltonicity of automatic graphs**
**Abstract **It is shown that the existence of a Hamiltonian path in a planar automatic

graph of bounded degree is complete for Σ 1, the first level of the analytical hier-

archy. This sharpens a corresponding result of Hirst and Harel for highly recursivegraphs. Furthermore, we also show: (i) The Hamiltonian path problem for finite pla-nar graphs that are succinctly encoded by an automatic presentation is NEXPTIME-complete. (ii) The existence of an infinite path in an automatic successor tree is Σ 1-
complete. (iii) An infinite version of the set cover problem is decidable for automaticgraphs (it is Σ 1-complete for recursive graphs).

**1 Introduction**
The theory of

*recursive structures *has its origins in computability theory. A structureis recursive, if its domain is a recursive set of naturals, and every relation is againrecursive. Starting with the work of Manaster and Rosenstein [23] and Bean [1,2], infinite variants of classical graph problems for finite graphs were studied forrecursive graphs. It is not surprising that these problems are mostly undecidable forrecursive graphs. This motivates the search for the precise level of undecidability. Itturned out that some of the problems reside on low levels of the arithmetic hierarchy(e.g. the question whether a given recursive graph has an Eulerian path [3]), whereasothers are complete for Σ 1 — the first level of the analytic hierarchy [21]. A classical
example for the latter situation is the question whether a given recursive tree has aninfinite path. With a technically quite subtle reduction from the latter problem, Harelproved in [13] that also the existence of a

*Hamiltonian path *(i.e., a one-way infinitepath that visits every node exactly once) in a recursive graph is Σ 1-complete. Σ 1-
Dietrich KuskeInstitut f¨ur Informatik, Universit¨at Leipzig, e-mail:

[email protected]
Markus LohreyInstitut f¨ur Informatik, Universit¨at Leipzig, e-mail:

[email protected]
hardness holds already for highly recursive graphs, where a list of the neighbors ofa node

*v *can be computed effectively from

*v*.

Hamiltonian paths in infinite graphs were also studied under a purely graph the-
oretic view. An important result of Dean, Thomas, and Yu [6] states that an infiniteundirected graph

*G *has an Hamiltonian path if it is (i) planar, (ii) 4-connected, and(iii) has only one end (see [7] for definitions). This extends a result of Tutte [27] forfinite graphs.

In computer science, in particular in the area of automatic verification, focus
has shifted in recent years from arbitrary recursive graphs to subclasses that havemore amenable algorithmic properties. An important example for this is the classof

*automatic graphs *[5, 16]. A graph is called automatic if it has an

*automaticpresentation*, which consists of a finite automaton that generates the set of nodesand a two-tape automaton with synchronously moving heads, which accepts the setof edges. One of the main motivations for investigating automatic graphs is the factthat every automatic graph has a decidable first-order theory [16], this result extendsto first-order logic with infinity and modulo quantifiers [5, 19]. In contrast to thesepositive results, Khoussainov, Nies, and Rubin have shown that the isomorphismproblem for automatic graphs is Σ 1-complete [17]. Results on the model theoretic
complexity of automatic structures can be found in [15].

The main result of this paper states that the existence of a Hamiltonian path
becomes Σ 1-complete already for a quite restricted subclass of recursive graphs,
namely for automatic graphs, which are planar and of bounded degree. The lattermeans that there exists a constant

*c *such that every node has at most

*c *many neigh-bors. The proof of the Σ 1 lower bound (the non-trivial part) in Section 3 is based on
a reduction from the

*recurring tiling problem *[10, 12]. This is a variant of the clas-sical tiling problem [29, 4] that asks whether a given finite set of tiles allows a tilingof the infinite quarter plane such that a distinguished color occurs infinitely oftenat the lower border. Harel proved that the recurring tiling problem is Σ 1-complete
[10, 12]. In our reduction we use as building blocks some of the graph gadgets fromthe NP-hardness proof of the Hamiltonian path problem in finite planar graphs [9].

These gadgets have to be combined in a non-trivial way for the whole reduction.

The main purpose of automatic presentations is the finite representation of infi-
nite structures. But automatic presentations can be also used as a tool for the succinctrepresentation of large finite structures. An automatic presentation of size

*n *maygenerate a finite graph of size 2

*O*(

*n*). A straightforward adaptation of our proof forinfinite automatic graphs shows that it is NEXPTIME-complete to check whether afinite planar graph given by an automatic presentation has a Hamiltonian path, seeSection 4. Without the restriction to planar graphs, this result was already shown byVeith [28] in the slightly different context of graphs represented by ordered binarydecision diagrams (OBDDs). The special OBDDs considered by Veith in [28] canbe seen as automatic presentations of finite graphs.

Finally, in Section 5 we investigate some other graph problems in the automatic
setting. Using a proof technique from [20, 15], we prove that the fundamental Σ 1-
complete problem in recursion theory, namely the existence of an infinite path in arecursive tree remains Σ 1-complete if the input tree is automatic. For this result it
is crucial that the tree is a

*successor tree*, which means that it is an acyclic graph,where every node is reachable from a root node and every node except the roothas exactly one incoming edge. If trees are given as particular partially ordered sets(order trees), then the existence of an infinite path is decidable for automatic trees[20].

From the above results, one might get the feeling that graph problems always
have the same degree of undecidability in the recursive and in the automatic world.

To the contrary, there are problems that are Σ 1-complete for recursive graphs [14]
but decidable for automatic graphs. This applies to the existence of an infinite branchin an automatic

*order tree *(i.e., the reflexive and transitive closure of a successortree, Khoussainov, Rubin, and Stephan [20]) as well as to the existence of an infiniteclique in an automatic graph (Rubin [25]). We show that also an infinite version ofthe set cover problem is decidable for automatic graphs. This result is achieved byproviding a decision procedure for a fragment of second-order logic that allows toexpress the set cover problem as well as the two other decidable problems mentionedbefore.

Proofs, which are not included in this extended abstract will appear in the long

**2 Preliminaries**
**Infinite graphs and Hamiltonian paths**
For details on graph theory see [7]. A

*graph *is a pair

*G *= (

*V*,

*E*), where

*V *is the(possibly infinite) set of nodes and

*E *⊆

*V *×

*V *is the set of edges. It is

*undirected*if (

*u*,

*v*) ∈

*E *implies (

*v*,

*u*) ∈

*E*. The graph

*G *has

*degree at most c*, where

*c *∈ N,if every node is contained in at most

*c *many edges. If

*G *has degree at most

*c *forsome constant

*c*, then

*G *has

*bounded degree*. If it is only required that every nodeis contained in only finitely many edges then

*G *is called

*locally finite*. The graph

*G*is

*planar *if it can be embedded in the Euclidean plane without crossing edges andwithout accumulation points; any such embedding is a

*plane graph*. A

*finite path *in

*G *is a sequence [

*v*1,

*v*2, . . . ,

*vn*] of nodes such that (

*vi*,

*vi*+1) ∈

*E *for all 1 ≤

*i *≤

*n*. Thenodes

*v*1 and

*vn *are the end points of this path. The graph

*G *= (

*V*,

*E*) is

*connected*if for all

*u*,

*v *∈

*V *there exists a finite path in the undirected graph (

*V*,

*E *∪ {(

*x*,

*y*) |(

*y*,

*x*) ∈

*E*} with end points

*u *and

*v*. An

*infinite path *in

*G *is an infinite sequence[

*v*1,

*v*2, . . .] such that every initial segment is a finite path. A

*Hamiltonian path *(or

*spanning ray*) of an

*infinite *graph

*G *is an infinite path [

*v*1,

*v*2, . . .] in

*G *that visitsevery node of

*G *exactly once, i.e. the mapping

*i *→

*vi *(

*i *∈ N) is a bijection betweenN and the set of nodes.

**Recursive graphs and automatic graphs**
A

*recursive graph *is a graph

*G *= (

*V*,

*E*) such that

*V *and

*E *are recursive subsets ofN and N × N, respectively. In case

*G *is infinite, one can w.l.o.g. assume that

*V *= N.

A recursive graph

*G *is

*highly recursive *if it is locally finite and for every node

*v *alist of its finitely many neighbors can be computed from

*v*. Harel [13] has shown thefollowing result:

**Theorem 1 ([13]). ***It is *Σ 1

*-complete to determine, whether a given highly recursive*
*undirected graph of bounded degree has a Hamiltonian path.*
Recall that Σ 1 is the first level of the

*analytic hierarchy *[21]. More precisely, it is
the class of all subsets of N of the form {

*n *∈ N | ∃

*A *ϕ(

*A*)}, where ϕ(

*A*) is a formulaof first-order arithmetic. In Thm. 1, a recursive graph is encoded by a pair of G¨odelnumbers for machines for the node and edge set, respectively.

In [14], Hirst and Harel proved that for planar recursive graphs the existence
of a Hamiltonian path is still Σ 1-complete. The aim of this paper is to extend the
results from [13, 14] to the class of planar automatic graphs of bounded degree. Weintroduce this class of graphs briefly, more details can be found in [16, 5]
Let us fix

*n *∈ N and a finite alphabet Γ . Let # ∈ Γ be an additional padding
symbol. For words

*w*1, . . . ,

*wn *∈ Γ ∗ we define the

*convolution w*1 ⊗

*w*2 ⊗ · · · ⊗

*wn*,which is a word over the alphabet ∏

*n *(Γ ∪{
#}), as follows: Let

*wi *=

*ai*,1

*ai*,2 · · ·

*ai*,

*ki*
with

*ai*,

*j *∈ Γ and

*k *= max{

*k*1, . . . ,

*kn*}. For

*ki *<

*j *≤

*k *define

*ai*,

*j *= #. Then

*w*1 ⊗ · · · ⊗

*wn *= (

*a*1,1, . . . ,

*an*,1) · · · (

*a*1,

*k*, . . . ,

*an*,

*k*). Thus, for instance

*aba *⊗

*bbabb *=(

*a*,

*b*)(

*b*,

*b*)(

*a*,

*a*)(#,

*b*)(#,

*b*). An

*n*-ary relation

*R *⊆ (Γ ∗)

*n *is called automatic if thelanguage {

*w*1 ⊗ · · · ⊗

*wn *| (

*w*1, . . . ,

*wn*) ∈

*R*} is a regular language.

Now let A = (

*A*, (

*Ri*)

*i*∈

*J*) be a relational structure with finitely many relations,
where

*Ri *⊆

*Ani *. A tuple (Γ ,

*L*,

*h*) is called an

*automatic presentation *for A if (i) Γis a finite alphabet, (ii)

*L *⊆ Γ ∗ is a regular language, (iii)

*h *:

*L *→

*A *is a bijectivefunction, (iv) the relation {(

*u*,

*v*) ∈

*L *×

*L *|

*h*(

*u*) =

*h*(

*v*)} is automatic, and (v) therelation {(

*u*1, . . . ,

*un *) ∈

*Lni *| (

*h*(

*u*
*i*} is automatic for every

*i *∈

*J*.

We say that A is

*automatic *if there exists an automatic presentation for A . In therest of the paper we will mainly restrict to automatic graphs. Such a graph can berepresented by an automaton for the node set and an automaton for the edge set.

Clearly, a (locally finite) automatic graph is (highly) recursive.

In contrast to recursive graphs, automatic graphs have some nice algorithmic
properties. In [16] it was shown that the first-order theory of an automatic structureis decidable. This result extends to first-order logic with infinity and modulo quanti-fiers [5, 19]. For general automatic structures, these logics do not allow elementaryalgorithms [5]. On the other hand, for automatic structures with a Gaifman graphof bounded degree first-order logic extended by a rather general class of countingquantifiers can be decided in triply exponential space [22].

In contrast to these positive results, several strong undecidability results show
that algorithmic methods for automatic structures are quite limited. Since the con-figuration graph of a Turing machine is automatic, it follows easily that reachabilityin automatic graphs is undecidable. Khoussainov, Nies, and Rubin have shown that
the isomorphism problem for automatic graphs is Σ 1-complete [17], whereas iso-
morphism of locally finite automatic graphs is Π 0-complete [24]. Our main result

**Theorem 2. ***It is *Σ 1

*-complete to determine, whether a given planar automatic undi-*
*rected graph of bounded degree has a Hamiltonian path.*
Note that the Σ 1 upper bound in Thm. 2 follows immediately from the correspond-
ing result for general recursive graphs (Thm. 1). For the lower bound we use aspecial variant of the tiling problem [29, 4] that was introduced by Harel.

Our main tool for proving Σ 1-hardness of the existence of a Hamiltonian path in a
planar automatic graph of bounded degree is the

*recurring tiling problem *[10, 12].

An instance of the recurring tiling problem consists of (i) a finite set of

*colors C *={

*c*0,

*c*1, . . . ,

*cn*}, (ii) a distinguished color

*c*0, and (iii) a set T ⊆

*C*4 of

*tile types*. Fora tile type

*t *∈ T we write

*t *= (

*tW *,

*tN*,

*tE *,

*tS*) (“W” for west, “N” for north, “E” foreast “S” for south); a visualization looks as follows:
A mapping

*f *: N2 → T is a

*tiling *if, for every (

*i*,

*j*) ∈ N2, we have

*f *(

*i*,

*j*)

*N *=

*f *(

*i *+ 1,

*j*)

*S *and

*f *(

*i*,

*j*)

*E *=

*f *(

*i*,

*j *+ 1)

*W *. A

*recurring tiling *is a tiling

*f *such that
for infinitely many

*j *∈ N, we have

*f *(0,

*j*)

*S *=

*c*0. Now the recurring tiling problemasks whether a given problem instance has a recurring tiling. Harel has shown thefollowing result:

**Theorem 3 ([10]). ***The recurring tiling problem is *Σ 1

*-complete.*
The recurring tiling problem turned out be very useful for proving Σ 1 lower
bounds for certain satisfiability problems in logic [11].

**3 Hamiltonicity for automatic graphs**
In this section, we reduce the recurring tiling problem to the existence of a Hamil-tonian path in a planar automatic graph of bounded degree. This proves Thm. 2 byThm. 3.

**Fig. 1 **The graph

*X *, its use and abbreviation

**3.1 Building blocks**
Let us introduce several building blocks from which we assemble our final planarautomatic graph of bounded degree. These building blocks are variants of graphstaken from the NP-hardness proof for the Hamiltonian path problem in finite planargraphs [9].

**Exclusive or**
Consider the finite plane graph

*X *in Fig. 1 (first picture). It has a Hamiltonian pathfrom

*u*1 to

*u*2 (and similarly from

*v*1 to

*v*2) indicated in the second picture. Nowsuppose

*G*′ is some graph containing the edges

*u*′ and

*v*′. Then we build a graph

*G*as follows: in the disjoint union of

*G*′ and

*X *, delete the edges

*u*′ and

*v*′ and connecttheir endpoints to

*u*1 and

*u*2 (to

*v*1 and

*v*2, resp., see Fig. 1, third picture). Nowsuppose

*H *is a Hamiltonian path in

*G *with no endpoint in

*X *. Suppose

*u*1 is thefirst vertex from

*X *in

*H*. Then the restriction of

*H *to

*X *has to coincide with theHamiltonian path from

*u*1 to

*u*2. Hence

*H *gives rise to a Hamiltonian path in

*G*′ thatcoincides with

*H *on

*G*′ but passes through the edge

*u*′ instead of taking the detourthrough

*X *. Note that

*H*′ does not contain the edge

*v*′. Conversely, every Hamiltonianpath

*H*′ of

*G*′ that contains the edge

*u*′ but not the edge

*v*′ induces a Hamiltonianpath

*H *of

*G *in a similar way. Joining

*X *to the graph

*G*′ in this manner restricts theHamiltonian paths to those that either contain the edge

*u*′ or the edge

*v*′, but not both.

This also explains the name

*X *: this graph acts as an “exclusive-or”. Note that, if

*G*′is planar and the two edges

*u*′ and

*v*′ belong to the same face, then also

*G *can beconstructed as a planar graph. Since we will make repeated use of this construction,we abbreviate it as in Fig. 1, fourth picture.

**Boolean functions**
Let

*f *: {0, 1}

*n *→ {0, 1} be a Boolean function. In the NP-hardness proof of [9], aplanar graph

*G *together with distinguished edges

*e*1, . . . ,

*en *is constructed such that

*f *(

*b*1, . . . ,

*bn*) = 1 iff

*G *has a Hamiltonian cycle

*H *with

*bi *= 1 ⇔

*ei *∈

*H*. We modify

**Fig. 2 **The graph

*A *and its abbreviation

**Fig. 3 **Paths through the graph

*A*
this construction slightly in order to place the edges

*ei *and two vertices

*u *and

*v *in aspecified order at the boundary of the outer face.

**Theorem 4. ***There exists a constant c such that from given k*, ℓ,

*n *∈ N

*and F *⊆

2{1,.,

*k*+ℓ+

*n*}

*, one can construct effectively a finite plane graph GF of degree at most*

c such that:
•

*At the boundary of the outer face of GF , we find (in this counter-clockwise order)*
*edges e*1, . . .

*ek, a vertex u, edges ek*+1, . . . ,

*ek*+ℓ

*, a vertex v, and edges ek*+ℓ+1, . . . ,

*ek*+ℓ+

*n.*
•

*For every M *⊆ {1, . . . ,

*k *+ ℓ +

*n*}

*, M *∈

*F iff there is a Hamiltonian path H from*
*u to v such that M *= {

*i *|

*ei belongs to H*}

*.*
**Infinity checking**
Next consider Fig. 2 – it depicts a graph

*A *that is connected to some context viathe edges ℓ,

*a*,

*a*′,

*b*,

*b*′, and

*r*. If the complete graph has a Hamiltonian path, thenlocally, it has to be of one of the four forms depicted in Fig. 3.

Now consider Fig. 4 – it consists of infinitely many copies of the graph

*A *ar-
ranged in a line, the edges

*a*′ and

*b*′ connect these copies of

*A *with a line of nodes.

Suppose the edges

*a *and

*b *of the copies of

*A *are connected to some infinite graph

*G*. Then, every Hamiltonian path

*H *of the resulting graph has to enter and leave

**Fig. 4 **The infinite graph

*L*
**Fig. 5 **A visit of a Hamiltonian path to the graph

*L*
*L *infinitely often. Since the possibilities to pass

*A *are restricted as shown in Fig.3,any such visit has to look as described in Fig. 5, i.e., the path enters from

*a *intosome copy of

*A*, moves left to some copy of

*A *(possibly without doing any step),moves down to the third line where it goes all the way back until it can enter the first

*A*-copy via the edge

*b*′ and leave it via the edge

*b*.

**3.2 Assembling**
From an instance of the recurring tiling problem, we construct in this section aplanar automatic graph

*G *of bounded degree that has an Hamiltonian path iff theinstance of the recurring tiling problem admits a solution. So, we fix a finite set

*C *= {

*c*0,

*c*1, . . . ,

*cn*} of colors, a distinguished color

*c*0, and a set T ⊆

*C*4 of tile
V = {

*W*0,

*W*1, . . . ,

*Wn*,

*S*0,

*S*1, . . . ,

*Sn*,

*N*0,

*N*1, . . . ,

*Nn*,

*E*0,

*E*1, . . . ,

*En*}.

We will describe tile types by certain subsets of V where

*Wi *expresses that the leftcolor is

*ci*, and

*Ni *denotes that the top color is

*not ci *(

*Si *and

*Ei *refer to the bottomand right color and are to be understood similarly). More precisely, the tile

*d *=(

*ci*,

*c j*,

*ck*,

*c*ℓ) is denoted by the set S

*d *= {

*Wi*} ∪ {

*Nm *|

*m *=

*j*} ∪ {

*Em *|

*m *=

*k*} ∪ {

*S*ℓ}.

Now let

*F *= {S

*d *|

*d *∈ T } be the descriptions of all the tile types

*d *in T . Then,by Thm. 4, there are finite plane graphs

*G*1,

*G*2,

*G*3, and

*G*4 with the followingproperties: (i) at the outer face, we find edges

*e *for

*e *∈ V and nodes

*u *and

*v *in theorder indicated in Fig. 6 and (ii)

*M *∈

*F *iff there exists a Hamiltonian path

*H *of

*Gx*from

*u *to

*v *such that

*M *= {

*v *∈ V |

*v *belongs to

*H*} (for all 1 ≤

*x *≤ 4 and

*M *⊆ V ).

Next we choose mutually disjoint graphs

*G*(

*k*, ℓ) (for

*k*, ℓ ∈ N) such that

**Fig. 6 **The graphs

*Gx*
if

*k *+ ℓ is even and

*k *> 0 or

*k *= ℓ = 0
if

*k *+ ℓ is even,

*k *= 0, and ℓ > 0.

Then

*u*(

*k*, ℓ) and

*v*(

*k*, ℓ) refer to the nodes

*u *and

*v *of the graph

*G*(

*k*, ℓ); similarly,

*e*(

*k*, ℓ) for

*e *∈ V refers to the edge

*e *of the graph

*G*(

*k*, ℓ). In the disjoint union ofthese graphs

*G*(

*k*, ℓ), we connect the node

*v*(

*k*, ℓ) by a new edge with the followingnode:

*u*(

*k *+ 1, ℓ) for

*k *+ ℓ even and ℓ = 0

*u*(

*k *+ 1, ℓ − 1) for

*k *+ ℓ even and ℓ > 0

*u*(

*k *− 1, ℓ + 1) for

*k *+ ℓ odd and

*k *> 0

*u*(

*k*, ℓ + 1) for

*k *+ ℓ odd and

*k *= 0.

The result

*G*1 of this construction is visualized in Fig. 7 where the vertices

*u*(

*k*, ℓ)are denoted by empty nodes and

*v*(

*k*, ℓ) by filled nodes. From

*G*1 we construct

*G*2by replacing the edges

*Ei*(

*k*, ℓ) and

*Wi*(

*k*, ℓ + 1) as well as

*Ni*(

*k*, ℓ) and

*Si*(

*k *+ 1, ℓ)(

*k*, ℓ ∈ N, 0 ≤

*i *≤

*n*) by a copy of the exclusive-or graph

*X *, see Fig. 8. In a thirdstep, we construct

*G*3 by adding to

*G*2 the graph

*L *from Fig. 4. To connect

*L *to

*G*2,the start node of the edges

*a *and

*b*, resp., of the

*ith *copy of

*A *in

*L *is the left and right,resp., node of the edge

*S*0(0,

*i*). The final graph

*G *is obtained from

*G*3 by adding anew node ⊥ together with an edge between ⊥ and

*u*(0, 0).

**Fig. 7 **First step in global construction - the graph

*G*1

**Fig. 8 **Second step in global construction – the graph

*G*2 (for two colors

*c*0 and

*c*1)

Let us now prove that

*G *has a Hamiltonian path iff T admits a recurring tiling.

First suppose there is a recurring tiling

*f *: N × N → T . Let

*k*, ℓ ∈ N and

*f *(

*k*, ℓ) =(

*cW *,

*cN*,

*cE*,

*cS*). Then the graph

*G*(

*k*, ℓ) ∈ {

*Gx *| 1 ≤

*i *≤ 4} has a Hamiltonian path

*H*(

*k*, ℓ) from

*u*(

*k*, ℓ) to

*v*(

*k*, ℓ) such that for all 1 ≤

*i *≤

*n*
1. the edge

*Si *belongs to

*H*(

*k*, ℓ) iff

*cS *=

*ci*,2. the edge

*Wi *belongs to

*H*(

*k*, ℓ) iff

*cW *=

*ci*,3. the edge

*Ni *belongs to

*H*(

*k*, ℓ) iff

*cN *=

*ci*, and4. the edge

*Ei *belongs to

*H*(

*k*, ℓ) iff

*cE *=

*ci*.

Then we find a Hamiltonian path

*H*1 of the infinite graph

*G*1 in Fig. 7 by appendingthese Hamiltonian paths suitably:

*H*1 =

*H*(0, 0),

*H*(1, 0),

*H*(0, 1),

*H*(0, 2),

*H*(1, 1),

*H*(2, 0) . . .

∈

*H*1 ⇐⇒

*f *(

*k*, ℓ)

*E *=

*ci*
⇐⇒

*f *(

*k*, ℓ + 1)

*W *=

*ci*⇐⇒

*Wi*(

*k*, ℓ + 1) ∈

*H*1
∈

*H*1 iff

*Si*(

*k *+ 1, ℓ) ∈

*H*1. Hence the Hamiltonian path

*H*1 can
be extended to a Hamiltonian path

*H*2 of the graph

*G*2 obtained from

*G*1 by addingall the copies of the exclusive-or graph

*X *. Observe also that

*f *is recurring, i.e., thereare infinitely many ℓ ∈ N with

*f *(0, ℓ)

*S *=

*c*0. For every such ℓ, the path

*H*1 passesthrough the edge

*S*0(0, ℓ). Instead of passing through this edge, we now enter thegraph

*L *(Fig. 4) via the edge

*a *of the ℓ

*th *copy of

*A *and leave it via its edge

*b*. Wecan ensure that after this visit, all nodes of

*L *to the left of the ℓ

*th *copy of

*A *have beenvisited (cf. Fig. 5). This results in a Hamiltonian path

*H*3 of the graph

*G*3 starting in

*u*(0, 0). Prepending the node ⊥ gives a Hamiltonian path

*H *of the final graph

*G*.

Conversely, let

*H *be a Hamiltonian path of the final graph

*G*. Since ⊥ has degree
1, it has to start in ⊥ – deleting ⊥ from

*H *gives a Hamiltonian path

*H*3 of

*G*3that starts in

*u*(0, 0). Since

*G*3 contains infinitely many nodes outside of

*L*, thispath has to enter and leave

*L *infinitely often. Any such visit has to enter via theedge

*a *some copy of

*A *and leave via the edge

*b *of the same copy of

*A *(or viceversa, see Fig. 5). Hence, deleting all the vertices of

*L *from the path

*H*, we obtaina Hamiltonian path

*H*2 of the graph

*G*2 that contains infinitely many edges of theform

*S*0(0, ℓ). Recall that

*G*2 is obtained from

*G*1 by replacing some pairs of edgesby the exclusive-or graph

*X *. Hence, the restriction of

*H*2 to the nodes of

*G*1 givesrise to a Hamiltonian path

*H*1 of

*G*1 that
(a) contains infinitely many edges of the form

*S*0(0, ℓ),
(b) contains the edge

*Wi*(

*k*, ℓ + 1) iff it does not contain the edge

*Ei*(

*k*, ℓ), and
(c) contains the edge

*Si*(

*k *+ 1, ℓ) iff it does not contain the edge

*Ni*(

*k*, ℓ)
for all 0 ≤

*i *≤

*n *and

*k*, ℓ ∈ N. Since

*H*1 has to pass through all the graphs

*G*(

*k*, ℓ), ithas to be of the form

*H*(0, 0),

*H*(1, 0),

*H*(0, 1),

*H*(0, 2),

*H*(1, 1),

*H*(2, 0) . . .

where

*H*(

*k*, ℓ) is a Hamiltonian path of the graph

*G*(

*k*, ℓ) from

*u*(

*k*, ℓ) to

*v*(

*k*, ℓ). Nowwe are ready to define the mapping

*f *: N2 →

*C*4: set
(1)

*f *(

*k*, ℓ)

*W *=

*ci *iff

*H*(

*k*, ℓ) contains the edge

*Wi*(

*k*, ℓ),(2)

*f *(

*k*, ℓ)

*N *=

*ci *iff

*H*(

*k*, ℓ) does not contain the edge

*Ni*(

*k*, ℓ),(3)

*f *(

*k*, ℓ)

*E *=

*ci *iff

*H*(

*k*, ℓ) does not contain the edge

*Ei*(

*k*, ℓ), and(4)

*f *(

*k*, ℓ)

*S *=

*ci *iff

*H*(

*k*, ℓ) contains the edge

*Si*(

*k*, ℓ).

Since

*H*(

*k*, ℓ) is a Hamiltonian path of

*G*(

*k*, ℓ) from

*u*(

*k*, ℓ) to

*v*(

*k*, ℓ), we get

*f *(

*k*, ℓ) ∈T from the construction of the graphs

*G*1,

*G*2,

*G*3,

*G*4. By (1), (b), and (3), we have

*f *(

*k*, ℓ)

*W *=

*ci *⇐⇒

*Wi*(

*k*, ℓ) belongs to

*H*(

*k*, ℓ)
⇐⇒

*Ei*(

*k*, ℓ + 1) does not belong to

*H*(

*k*, ℓ + 1)⇐⇒

*f *(

*k*, ℓ + 1) =

*ci*
and similarly

*f *(

*k*, ℓ)

*N *=

*f *(

*k *+1, ℓ)

*S *follows from (2), (c), and (4). Thus,

*f *is a tiling.

Since

*H*1 contains infinitely many edges of the form

*S*0(0, ℓ), there are infinitelymany ℓ ∈ N such that

*S*0(0, ℓ) belongs to

*H*(0, ℓ), i.e.,

*f *(0, ℓ)

*S *=

*c*0.

Thus, we showed that indeed the graph

*G *contains a Hamiltonian path iff the set
of tiles T admits a recurring tiling.

Clearly, the undirected graph

*G *is planar and has bounded degree. Thus, in order
to finish the proof of Thm. 2, it remains to prove that

*G *is automatic. Note thatthe graph

*G *has a highly regular structure. It results from the infinite grid N × Nby replacing each grid point by a finite graph and connecting these finite graphs ina regular pattern. It is not surprising that such a graph is automatic, in particularsince the grid is automatic. Let us provide some more formal arguments for theautomaticity of

*G*.

Recall that

*G *can be obtained from N × N by replacing every grid point (

*k*, ℓ) ∈
N × N by a finite graph

*G*′(

*k*, ℓ). This graph is a copy of one of the graphs

*G*′ ,

*G*′ ,

*G*′ ,

*G*′ , where

*G*′ is the graph

*G*
*i *together with copies of the XOR-graph

*X *that connect

*G*(

*k*, ℓ) with

*G*(

*k *+ 1, ℓ) and

*G*(

*k*, ℓ + 1). Whether

*G*′(

*k*, ℓ) is

*G*′ only
depends on the parity of

*k *+ ℓ and whether

*k *and ℓ are zero or non-zero, respectively.

The alphabet of our presentation consists of the elements of {0, 1, #}2 \ {(#, #)}
and the nodes of the graphs

*G*′ , . . . ,

*G*′ . Then, the node set of

*G *can be represented
{(bin(

*k*) ⊗ bin(ℓ))

*v *|

*k*, ℓ ≥ 0,

*v *is a node of

*G*′(

*k*, ℓ)},
where bin(

*n*) is the binary encoding of a number

*n *(note that the parity of

*k *+ℓ can bedetermined by a finite automaton from bin(

*k*) ⊗ bin(ℓ)). Constructing from this noderepresentation an automaton that recognizes the edge set of

*G *is straightforward buttedious. This concludes the proof of Thm. 2.

There also exists the variant of two-way Hamiltonian paths in infinite graphs. A
two-way Hamiltonian path in

*G *= (

*V*,

*E*) is a two-way infinite sequence (

*vi*)

*i*∈Z suchthat (

*vi*,

*vi*+1) ∈

*E *for all

*i *∈ Z and for every node

*v *∈

*V *there is exactly one

*i *∈ Zsuch that

*v *=

*vi*. From the previous construction, it follows that also the existence ofa two-way Hamiltonian path in a given planar automatic graph of bounded degree is
Σ1-complete. Take the disjoint union of two copies of our main graph

*G *and connect
the two ⊥-nodes with an edge. The resulting graph

*G*′ has a two-way Hamiltonianpath iff

*G *has a (one-way) Hamiltonian path. Moreover, since

*G *is automatic and theclass of automatic graphs is closed under disjoint unions,

*G*′ is automatic as well.

**4 Remarks about large finite graphs**
The main purpose of automatic presentations is the finite representation of infinitestructures. But automatic presentations can be also used as a tool for the succinctrepresentation of large finite structures. Note that a finite automaton with

*n *statescan accept a finite language with 2

*O*(

*n*) elements, which may serve as the domain ofa finite structure.

In general, given an automatic presentation (Γ ,

*L*,

*h*) for a

*finite *graph (

*V*,

*E*) to-
gether with an automaton

*A *for the node set language

*L*, it is clear that |

*V *| is boundedby |Γ |

*n*, where

*n *is the number of states of

*A*. It follows that for every graph problem

*L *in NP, the succinct version of

*L*, where the input graph is given by an automaticpresentation, belongs to NEXPTIME. In particular, the Hamiltonian path problembelongs to NEXPTIME for this succinct input representation.

For the lower bound, consider for

*n *≥ 1 the finite planar graph

*Gn *that results
from our main infinite graph

*G *by restricting it to the graphs

*G*(

*k*, ℓ) for

*k *+ ℓ ≤

*n*and the connecting XOR-graphs between these graphs. Then

*Gn *has a Hamiltonianpath if and only if the finite set of tiles T admits a tiling of the “triangle”

*Dn *={(

*k*, ℓ) ∈ N × N |

*k *+ ℓ ≤

*n*} (tilings of finite parts of the grid N × N are definedanalogously to tilings of the whole grid). Now we can use a result of F¨urer [8]: Itis NEXPTIME-complete (under logspace reductions) to check for a given binaryencoded number

*n *and a finite set of tiles T whether T admits a tiling of

*Dn*. Letus make a few remarks on F¨urer’s proof before continuing:
• F¨urer proved NEXPTIME-completeness for tilings of the square {(

*k*, ℓ) ∈ N×N |

*k*, ℓ ≤

*n*} instead of the triangle

*Dn*. It is straightforward to adapt F¨urer’s prooffor

*Dn*.

• F¨urer actually does not speak about NEXPTIME-completeness in his paper, but
states explicit lower bounds. But in his proof he presents a generic reduction fromthe acceptance problem for nondeterministic exponential time Turing-machinesto the problem of tiling {(

*k*, ℓ) ∈ N × N |

*k*, ℓ ≤

*n*} for a given binary coded num-ber.

• F¨urer states that all his construction can be carried out in polynomial time, but it
is straightforward to check that they can be carried out even in logspace.

Finally, it is easy to construct from a binary coded number

*n *in logarithmic space anautomatic presentation of the graph

*Gn*. For this, we can basically use the automaticpresentation of the infinite graph

*G*, but restrict it to numbers of size at most

*n*.

Hence, we obtain:

**Theorem 5. ***It is NEXPTIME-complete under logspace reductions to check for a*

given automatic presentation of a finite planar graph, whether it has a Hamiltonian

path.
A variant of Thm. 5 was shown by Veith [28]. He considers finite structures thatare represented by OBDDs (ordered binary decision diagrams). In this context, thenode set of a graph is {0, 1}

*n *for some fixed

*n*. The edge set is represented by an
OBDD over variables

*x*1, . . . ,

*xn*,

*y*1, . . . ,

*yn*. Here the tuple (

*x*1, . . . ,

*xn*) ∈ {0, 1}

*n *rep-resents the initial vertex of an edge, whereas (

*y*1, . . . ,

*yn*) ∈ {0, 1}

*n *represents thefinal node. The variable order of the OBDDs in [28] is fixed to the interleaved or-der

*x*1,

*y*1,

*x*2,

*y*2, . . . ,

*xn*,

*yn*. Under this variable order, OBDDs exactly correspond todeterministic acyclic automata that work on the convolution (

*x*1 · · ·

*xn*) ⊗ (

*y*1 · · ·

*yn*).

In [28], the following upgrading theorem was shown (here, only formulated
for the classes NP and NEXPTIME): If a graph problem

*L *is NP-complete underquantifier free first-order reductions then obdd(

*L*) (the class of all OBDDs of theabove form that encode a graph from

*L*) is NEXPTIME-complete under polynomialtime reductions. Since the Hamiltonian path problem (HP) is NP-compete underquantifier free first-order reductions [26], it follows that obdd(HP) is NEXPTIME-complete under polynomial time reductions. Thm. 5 strengthens this result in twopoints: we obtain NEXPTIME-completeness (i) under logspace reductions and (ii)for

*planar *graphs. It is not clear for us, whether the

*planar *Hamiltonian path prob-lem is still NP-complete under quantifier free first-order reductions.

**5 Further graph problems**
An

*order tree *is a partial order (

*A*, ) with a least element such that the set {

*a *∈

*A *|

*a*
*b*} is finite and linearly ordered for every

*b *∈

*A*, a

*successor tree *is the covering
relation of an order tree. It is decidable, whether an automatic order tree has aninfinite path [20]. The following result is in sharp contrast to this positive result.

**Theorem 6. ***It is *Σ 1

*-complete to determine whether a given automatic successor*
The proof idea is to transform a recursive successor tree into an automatic one
by adding the computation (i.e., sequence of transitions) that verifies the edge (

*u*,

*v*)as a path between the nodes

*u *and

*v*; a similar idea was used in [20, 15].

Let us now present some graph problems which are Σ 1-complete for recursive
graphs, but decidable in automatic graphs. For this, we introduce, inspired by [18,25], a fragment SOr of second-order logic, which extends first-order logic with theinfinity quantifier and modulo quantifiers. Every relation that is definable in first-order logic with the infinity quantifier and modulo quantifiers has a regular set ofrepresentatives [16, 5, 19]. We will extend this result to SOr. The set of all formulasof SOr is inductively defined as follows:
• Every atomic first-order formula is an SOr-formula.

•

*X*(

*x*1, . . . ,

*xk*) for

*x*1, . . . ,

*xk *first-order variables and

*X *a

*k*-ary second-order vari-
• If ϕ and ψ are SOr-formulas, then also ϕ ∨ ψ is an SOr-formula.

• If ϕ is an SOr-formula, then also ¬ϕ, ∃

*x *ϕ, ∃∞

*x *ϕ (there are infinitely many

*x*
satisfying ϕ), ∃(

*k*,

*p*)

*x *ϕ for 0 ≤

*k *<

*p *∈ N (the number of

*x *satisfying ϕ is finiteand congruent

*k *modulo

*p *are SOr-formulas.

• If ϕ is an SOr-formula and

*X *is a second-order variable of arity

*k *such that
for every

*k*-tuple of first-order variables

*x*1, . . . ,

*xk*, ϕ contains the subformula

*X *(

*x*1, . . . ,

*xk*) only negatively (i.e. within an odd number of negations), then also∃

*X *infinite : ϕ is an SOr-formula.

Note that the restriction on ϕ in the last point means that if ϕ is satisfied for some

*k*-ary relation

*X *=

*R *and

*Q *⊆

*R*, then ϕ is also satisfied for

*X *=

*Q*.

**Theorem 7. ***From an automatic presentation *(Γ ,

*L*,

*h*)

*of an automatic structure *A

*and an *SOr

*-formula *ϕ(

*x*)

*one can compute effectively an automaton for the convo-*

lution of the relation {(

*u*1, . . . ,

*un*) ∈

*Ln *| A |= ϕ(

*h*(

*u*1), . . . ,

*h*(

*un*))}

*. Hence, if *ϕ

*is*

an SOr

*-sentence, then *A |= ϕ

*can be checked effectively.*
A variation of the proof of Thm. 7 yields the following result.

**Theorem 8. ***Let *(Γ ,

*L*,

*h*)

*be an automatic presentation of the structure *A

*and let*
α(

*X*)

*with X an n-ary relation variable be a formula of *SOr

*such that *∀

*X*,

*Y *: α(

*X *∪

*Y *) → α(

*X*)

*is a tautology and *A |= ∃

*X infinite *: α

*. Then one can construct H *⊆

*Ln*
*regular such that h*(

*H*)

*is infinite and *A |= α(

*h*(

*H*))

*.*
We use Thm. 7 and 8 to show that two problems, which are Σ 1-complete for re-
cursive structures [14], are decidable for automatic structures. First, by taking theSOr-formula ∃

*X *infinite ∀

*x*,

*y *: (

*x*,

*y *∈

*X *⇒ (

*x*,

*y*) ∈

*E*), we get:

**Corollary 1 (cf. [25, Thm. 3.20]). ***It is decidable whether a given automatic graph*

contains an infinite clique. If an infinite clique exists, a regular set of representatives

of an infinite clique can be computed.
The second problem is the infinite version of maximal set cover considered by Hirstand Harel [14]. It asks whether, given a set

*X *= {

*Xi *|

*i *∈ N} of sets

*Xi *⊆ N, thereexists

*A *⊆ N with

*a*∈

*A Xa *= N and N \

*A *infinite. Note that the collection

*X *can
be represented as a set of pairs

*E *with (

*i*,

*j*) ∈

*E *iff

*j *∈

*Xi*. Then there exists

*A *asrequired iff the directed graph (N,

*E*) satisfies ∃

*B *infinite ∀

*j*∃

*i *:

*i */
∈

*B *∧ (

*i*,

*j*) ∈

*E*
(then

*A *is the complement of

*B*). Hence we get:

**Corollary 2. ***The infinite version of maximal set cover is decidable if the collection*

X is given as an automatic set of pairs. In case a set cover as required exists, an

infinite such can be computed.
**6 Open problems**
Hirst and Harel [14] gave an extensive list of problems that are Σ 1-complete in
the recursive setting. Apart from the infinite version of the longest common subse-quence problem, all of these problems are decidable or Σ 1-complete in the automatic
setting (this follows easily from the problems considered in this paper). We are miss-ing an explanation for this phenomenon – or a natural problem that is undecidablefor automatic structures, but “simpler” than for recursive structures.

**References**
1. D. R. Bean. Effective coloration.

*J. Symbolic Logic*, 41(2):469–480, 1976.

2. D. R. Bean. Recursive Euler and Hamilton paths.

*Proc. Amer. Math. Soc.*, 55(2):385–394,
3. R. Beigel and W. I. Gasarch. unpublished results. 1986–1990.

4. R. Berger. The undecidability of the domino problem.

*Mem. Am. Math. Soc.*, 66. AMS, 1966.

5. A. Blumensath and E. Gr¨adel. Finite presentations of infinite structures: Automata and inter-
pretations.

*Theory Comput. Syst.*, 37(6):641–674, 2004.

6. N. Dean, R. Thomas, and X. Yu. Spanning paths in infinite planar graphs.

*J. Graph Theory*,
7. R. Diestel.

*Graph Theory, Third Edition*. Springer, 2006.

8. M. F¨urer. The computational complexity of the unconstrained limited domino problem (with
implications for logical decision problems). In

*Logic and machines: decision problems andcomplexity*, LNCS 171, pages 312–319. Springer, 1984.

9. M. Garey, D. Johnson, and R. E. Tarjan. The planar Hamiltonian circuit problem is NP-
complete.

*SIAM J. Comput.*, 5(4):704–714, 1976.

10. D. Harel. A simple undecidable domino problem (or, a lemma on infinite trees, with applica-
tions). In

*Proc. Logic and Computation Conference*, Victoria, Australia, 1984. Clayton.

11. D. Harel. Recurring dominoes: making the highly undecidable highly understandable.

*Ann.*
*Discrete Math.*, 24:51–72, 1985.

12. D. Harel. Effective transformations on infinite trees, with applications to high undecidability,
dominoes, and fairness.

*J. Assoc. Comput. Mach.*, 33(1):224–248, 1986.

13. D. Harel. Hamiltonian paths in infinite graphs.

*Israel J. Math.*, 76(3):317–336, 1991.

14. T. Hirst and D. Harel. Taking it to the limit: on infinite variants of NP-complete problems.

*J.*
*Comput. System Sci.*, 53:180–193, 1996.

15. B. Khoussainov and M. Minnes. Model theoretic complexity of automatic structures. In

*Proceedings of TAMC 08*. Springer, 2008. to appear.

16. B. Khoussainov and A. Nerode. Automatic presentations of structures. In

*LCC: International*
*Workshop on Logic and Computational Complexity*, LNCS 960, pages 367–392, 1994.

17. B. Khoussainov, A. Nies, S. Rubin, and F. Stephan. Automatic structures: richness and limi-
tations.

*Log. Methods Comput. Sci.*, 3(2):2:2, 18 pp. (electronic), 2007.

18. B. Khoussainov, S. Rubin, and F. Stephan. On automatic partial orders. In

*Proc. LICS 2003*,
pages 168–177. IEEE Computer Society Press, 2003.

19. B. Khoussainov, S. Rubin, and F. Stephan. Definability and regularity in automatic structures.

In

*Proc. STACS 2004*, LNCS 2996, pages 440–451. Springer, 2004.

20. B. Khoussainov, S. Rubin, and F. Stephan. Automatic linear orders and trees.

*ACM Trans.*
*Comput. Log.*, 6(4):675–700, 2005.

21. D. Kozen.

*Theory of Computation*. Springer, 2006.

22. D. Kuske and M. Lohrey. First-order and counting theories of omega-automatic structures.

*J. Symbolic Logic*, 73:129–150, 2008.

23. A. B. Manaster and J. G. Rosenstein. Effective matchmaking (recursion theoretic aspects of a
theorem of Philip Hall).

*Proc. London Math. Soc. (3)*, 25:615–654, 1972.

24. S. Rubin.

*Automatic Structures*. PhD thesis, University of Auckland, 2004.

25. S. Rubin. Automata presenting structures: A survey of the finite string case.

*Bull. Symbolic*
26. I. A. Stewart. Using the Hamiltonian path operator to capture NP.

*J. Comput. System Sci.*,
27. W. T. Tutte. A theorem on planar graphs.

*Trans. Amer. Math. Soc.*, 82:99–116, 1956.

28. H. Veith. How to encode a logical structure by an OBDD. In

*Proc. 13th Annual Conf. Com-*
*putational Complexity*, pages 122–131. IEEE Computer Society, 1998.

29. H. Wang. Proving theorems by pattern recognition.

*Bell Syst. Tech. J.*, 40:1–41, 1961.

Source: http://www.eti.uni-siegen.de/ti/veroeffentlichungen/08-ifip.pdf

Conditions générales de transport pour le transport ferroviaire des voyageurs (GCC- CIV/PRR) Applicables à partir du 1er octobre 2013 Préambule Les Conditions générales de transport pour le transport ferroviaire des voyageurs (GCC-CIV/PRR) ont pour but de garantir l’appli- cation de conditions contractuelles uniformes dans le transport national et international des voyageurs par chem

DRUG INTERACTIONS Pharmacodynamic interaction Pharmacokinetic interaction then dypiridamole, ticlopidine bleeding time (BT) by inhibiting platelet aggregation. take OCP of high progesterone content/ other contraceptive mycobacterial infections. Whether OCP is a combination of ethylinestradiol and nirethindrone . disulfirum like reactions. methonidazole therapy, alco