The logic L (Qu) extends first-order logic by a generalized form of counting quantifiers ("the number of elements satisfying... belongs to the set C"). This logic is investigated for structures with an injectively ω-automatic presentation. If first-order logic is extended by an infinity-quantifier, the resulting theory of any such structure is known to be decidable [6]. It is shown that, as in the case of automatic structures [21], also modulo-counting quantifiers as well as infinite cardinality quantifiers ("there are χ many (...) elements satisfying...") lead to decidable theories. For a structure of bounded degree with injective ω-automatic presentation, the fragment of L(Qu) that contains only effective quantifiers is shown to be decidable and an elementary algorithm for this decision is presented. Both assumptions (ω-automaticity and bounded degree) are necessary for this result to hold. (shrink)

The first-order theory of a string automatic structure is known to be decidable, but there are examples of string automatic structures with nonelementary first-order theories. We prove that the first-order theory of a string automatic structure of bounded degree is decidable in doubly exponential space (for injective automatic presentations, this holds even uniformly). This result is shown to be optimal since we also present a string automatic structure of bounded degree whose first-order theory is hard for 2EXPSPACE. We prove similar (...) results also for tree automatic structures. These findings close the gaps left open in [28] by improving both the lower and the upper bounds. (shrink)

We study satisfiability and infinite-state model checking in ICPDL, which extends Propositional Dynamic Logic (PDL) with intersection and converse operators on programs. The two main results of this paper are that (i) satisfiability is in 2EXPTIME, thus 2EXPTIME-complete by an existing lower bound, and (ii) infinite-state model checking of basic process algebras and pushdown systems is also 2EXPTIME-complete. Both upper bounds are obtained by polynomial time computable reductions to ω-regular tree satisfiability in ICPDL, a reasoning problem that we introduce specifically (...) for this purpose. This problem is then reduced to the emptiness problem for alternating two-way automata on infinite trees. Our approach to (i) also provides a shorter and more elegant proof of Danecki's difficult result that satisfiability in IPDL is in 2EXPTIME. We prove the lower bound(s) for infinite-state model checking using an encoding of alternating Turing machines. (shrink)

We prove that a finitely generated group is context-free whenever its Cayley-graph has a decidable monadic second-order theory. Hence, by the seminal work of Muller and Schupp, our result gives a logical characterization of context-free groups and also proves a conjecture of Schupp. To derive this result, we investigate general graphs and show that a graph of bounded degree with a high degree of symmetry is context-free whenever its monadic second-order theory is decidable. Further, it is shown that the word (...) problem of a finitely generated group is decidable if and only if the first-order theory of its Cayley-graph is decidable. (shrink)

For automatic and recursive graphs, we investigate the following problems: (A) existence of a Hamiltonian path and existence of an infinite path in a tree (B) existence of an Euler path, bounding the number of ends, and bounding the number of infinite branches in a tree (C) existence of an infinite clique and an infinite version of set cover The complexity of these problems is determined for automatic graphs and, supplementing results from the literature, for recursive graphs. Our results show (...) that these problems (A) are equally complex for automatic and for recursive graphs ( $\Sigma _{1}^{1}\text{-complete}$ ), (B) are moderately less complex for automatic than for recursive graphs (complete for different levels of the arithmetic hierarchy), (C) are much simpler for automatic than for recursive graphs (decidable and $\Sigma _{1}^{1}\text{-complete}$ , resp.). (shrink)

The main result of this paper states that the isomorphism problem for ω-automatic trees of finite height is at least has hard as second-order arithmetic and therefore not analytical. This strengthens a recent result by Hjorth, Khoussainov, Montalbán, and Nies showing that the isomorphism problem for ω-automatic structures is not in . Moreover, assuming the continuum hypothesis CH, we can show that the isomorphism problem for ω-automatic trees of finite height is recursively equivalent with second-order arithmetic. On the way to (...) our main results, we show lower and upper bounds for the isomorphism problem for ω-automatic trees of every finite height: It is decidable , for height 1 , -hard and in for height 3, and - and -hard and in for height . All proofs are elementary and do not rely on theorems from set theory. (shrink)