The main result of this paper is that the isomorphism for omega-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, Montalban, and Nies showing that the isomorphism problem for
omega-automatic structures is not $\Sigma^1_2$. Moreover, assuming the
continuum hypothesis CH, we can show that the isomorphism problem for
omega-automatic trees of finite height is recursively equivalent with
second-order arithmetic.
It is shown that for graph groups (right-angled Artin groups) the conjugacy
problem as well as a restricted version of the simultaneous conjugacy problem
can be solved in polynomial time even if input words are represented in a
compressed form. As a consequence it follows that the word problem for the
outer automorphism group of a graph group can be solved in polynomial time.
Automatic structures are finitely presented structures where the universe and
all relations can be recognized by finite automata. It is known that the
isomorphism problem for automatic structures is complete for $\Sigma^1_1$; the
first existential level of the analytical hierarchy. Several new results on
isomorphism problems for automatic structures are shown in this paper: (i) The
isomorphism problem for automatic equivalence relations is complete for
$\Pi^0_1$ (first universal level of the arithmetical hierarchy).
One-counter processes (OCPs) are pushdown processes which operate only on a
unary stack alphabet. We study the computational complexity of model checking
computation tree logic (CTL) over OCPs. A PSPACE upper bound is inherited from
the modal mu-calculus for this problem. First, we analyze the periodic
behaviour of CTL over OCPs and derive a model checking algorithm whose running
time is exponential only in the number of control locations and a syntactic
notion of the formula that we call leftward until depth.
One-counter processes (OCPs) are pushdown processes which operate only on a
unary stack alphabet. We study the computational complexity of model checking
computation tree logic (CTL) over OCPs. A PSPACE upper bound is inherited from
the modal mu-calculus for this problem. First, we analyze the periodic
behaviour of CTL over OCPs and derive a model checking algorithm whose running
time is exponential only in the number of control locations and a syntactic
notion of the formula that we call leftward until depth.