Markus Lohrey

  1. The Isomorphism Problem for omega-Automatic Trees.

    Authors: Markus Lohrey, Dietrich Kuske, Jiamou Liu
    Subjects: Logic in Computer Science
    Abstract

    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.

  2. Compressed conjugacy and the word problem for outer automorphism groups of graph groups.

    Authors: Markus Lohrey, Christian Mathissen, Niko Haubold
    Subjects: Group Theory
    Abstract

    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.

  3. The Isomorphism Problem On Classes of Automatic Structures.

    Authors: Markus Lohrey, Dietrich Kuske, Jiamou Liu
    Subjects: Logic in Computer Science
    Abstract

    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).

  4. Branching-time model checking of one-counter processes.

    Authors: Stefan Göller, Markus Lohrey
    Subjects: Logic in Computer Science
    Abstract

    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.

  5. Branching-time model checking of one-counter processes.

    Authors: Stefan Göller, Markus Lohrey
    Subjects: Logic in Computer Science
    Abstract

    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.

RSS-материал