Search

The computational complexity of the word problem in HNN-extension of groups is studied. HNN-extension is a fundamental construction in combinatorial group theory. It is shown that the word problem for an ascending HNN-extension of a group H is logspace reducible to the so-called compressed word problem for H. The main result of the paper states that the word problem for an HNN-extension of a hyperbolic group H with cyclic associated subgroups can be solved in polynomial time. This result can be easily extended to fundamental groups of graphs of groups with hyperbolic vertex groups and cyclic edge groups. [ABSTRACT FROM AUTHOR]

We study the circuit evaluation problem (also known as the compressed word problem) for finitely generated linear groups. The best upper bound for this problem is coRP (the complements of problems in randomized polynomial time), which is shown by a reduction to polynomial identity testing for arithmetic circuits. Conversely, the compressed word problem for the linear group SL3(Z) is equivalent to polynomial identity testing. In the paper, we show that the compressed word problem for every finitely generated nilpotent group is in DET ⊆ NC2.Within the larger class of polycyclic groups we find examples where the compressed word problem is at least as hard as polynomial identity testing for skew arithmetic circuits. It is a major open problem, whether polynomial identity testing for skew arithmetic circuits can be solved in polynomial time. [ABSTRACT FROM AUTHOR]

A simple linear-time algorithm for constructing a linear context-free tree grammar of size O ( r g + r g log ⁡ ( n / r g ) ) for a given input tree T of size n is presented, where g is the size of a minimal linear context-free tree grammar for T , and r is the maximal rank of symbols in T (which is a constant in many applications). This is the first example of a grammar-based tree compression algorithm with a good, i.e. logarithmic in terms of the size of the input tree, approximation ratio. The analysis of the algorithm uses an extension of the recompression technique from strings to trees. [ABSTRACT FROM AUTHOR]

The uniform first-order theory of ground tree rewrite graphs is the set of all pairs consisting of a ground tree rewrite system and a first-order sentence that holds in the graph defined by the ground tree rewrite system. We prove that the complexity of the uniform first-order theory of ground tree rewrite graphs is in ATIME(22poly(n), O(n)). Providing a matching lower bound, we show that there is some fixed ground tree rewrite graph whose first-order theory is hard for ATIME(22poly(n), poly(n)) with respect to logspace reductions. Finally, we prove that there exists a fixed ground tree rewrite graph together with a single unary predicate in form of a regular tree language such that the resulting structure has a non-elementary first-order theory. [ABSTRACT FROM AUTHOR]

One-counter automata (OCA) are pushdown automata which operate only on a unary stack alphabet. We study the computational complexity of model checking computation tree logic (CTL) on transition systems induced by OCA. A PSPACE upper bound is inherited from the modal μ-calculus for this problem proved by Serre. First, we analyze the periodic behavior of CTL over OCA 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. In particular, model checking fixed OCA against CTL formulas with a fixed leftward until depth is in P. This generalizes a corresponding recent result of Göller, Mayr, and To for the expression complexity of CTL's fragment EF. Second, we prove that already over some fixed OCA, CTL model checking is PSPACE-hard, i.e., expression complexity is PSPACE-hard. Third, we show that there already exists a fixed CTL formula for which model checking of OCA is PSPACE-hard, i.e., data complexity is PSPACE-hard as well. To obtain the latter result, we employ two results from complexity theory: (i) Converting a natural number in Chinese remainder presentation into binary presentation is in logspace-uniform NC¹ and (ii) PSPACE is AC0-serializable. We demonstrate that our approach can be used to obtain further results. We show that model checking CTL's fragment EF over OCA is hard for PNP, thus establishing a matching lower bound. Moreover, we show that the following problem is hard for PSPACE: Given a one-counter Markov decision process, a set of target states with counter value zero each, and an initial state, to decide whether the probability that the initial state will eventually reach one of the target states is arbitrarily close to 1. This improves a recently proved lower bound for every level of the boolean hierarchy shown by Brázdil et al. Finally, we prove that there is a fixed CTL formula for which model checking 2-clock timed automata is PSPACE-hard, generalizing a PSPACE-hardness result for the combined complexity by Laroussinie, Markey, and Schnoebelen. [ABSTRACT FROM AUTHOR]

Abstract: The computational complexity of the isomorphism problem for regular trees, regular linear orders, and regular words is analyzed. A tree is regular if it is isomorphic to the prefix order on a regular language. In case regular languages are represented by NFAs (DFAs), the isomorphism problem for regular trees turns out to be -complete (resp. -complete). In case the input automata are acyclic NFAs (acyclic DFAs), the corresponding trees are (succinctly represented) finite trees, and the isomorphism problem turns out to be -complete (resp. -complete). A linear order is regular if it is isomorphic to the lexicographic order on a regular language. A polynomial time algorithm for the isomorphism problem for regular linear orders (and even regular words, which generalize the latter) given by DFAs is presented. This solves an open problem by Ésik and Bloom. Similar techniques can be used to show that one can check in polynomial time whether a given regular linear order has a non-trivial automorphism. This improves a recent decidability result of Kuske. [Copyright &y& Elsevier]

Abstract: Hierarchical graph definitions allow a modular description of structures using modules for the specification of repeated substructures. Beside this modularity, hierarchical graph definitions allow us to specify structures of exponential size using polynomial size descriptions. In many cases, this succinctness increases the computational complexity of decision problems when input structures are defined hierarchically. In this paper, the model-checking problem for first-order logic (FO), monadic second-order logic (MSO), and second-order logic (SO) on hierarchically defined input structures is investigated. It is shown that in general these model-checking problems are exponentially harder than their non-hierarchical counterparts, where the input structures are given explicitly. As a consequence, several new complete problems for the levels of the polynomial time hierarchy and the exponential time hierarchy are obtained. Based on classical results of Gaifman and Courcelle, two restrictions on the structure of hierarchical graph definitions that lead to more efficient model-checking algorithms are presented. [Copyright &y& Elsevier]

Abstract: Tight connections between leaf languages and strings compressed by straight-line programs (SLPs) are established. It is shown that the compressed membership problem for a language L is complete for the leaf language class defined by L via logspace machines. A more difficult variant of the compressed membership problem for L is shown to be complete for the leaf language class defined by L via polynomial time machines. As a corollary, it is shown that there exists a fixed linear visibly pushdown language for which the compressed membership problem is PSPACE-complete. For XML languages, it is shown that the compressed membership problem is coNP-complete.Furthermore it is shown that the embedding problem for SLP-compressed strings is hard for PP (probabilistic polynomial time). [Copyright &y& Elsevier]

Hierarchical graph definitions allow a modular description of graphs using modules for the specification of repeated substructures. Beside this modularity, hierarchical graph definitions also allow to specify graphs of exponential size using polynomial size descriptions. In many cases, this succinctness increases the computational complexity of decision problems. In this paper, the model-checking problem for the modal μ-calculus and (monadic) least fixpoint logic on hierarchically defined input graphs is investigated. In order to analyze the modal μ-calculus, parity games on hierarchically defined input graphs are investigated. Precise upper and lower complexity bounds are derived. A restriction on hierarchical graph definitions that leads to more efficient model-checking algorithms is presented. [ABSTRACT FROM AUTHOR]

We consider a compressed form of the word problem for finitely presented monoids, where the input consists of two compressed representations of words over the generators of a monoid M, and we ask whether these two words represent the same monoid element of M. Words are compressed using straight-line programs, i.e., context-free grammars that generate exactly one word. For several classes of finitely presented monoids we obtain completeness results for complexity classes in the range from P to EXPSPACE. As a by-product of our results on compressed word problems we obtain a fixed deterministic context-free language with a PSPACE-complete compressed membership problem. The existence of such a language was open so far. Finally, we will investigate the complexity of the compressed membership problem for various circuit complexity classes. [ABSTRACT FROM AUTHOR]

We study the notion of safe realizability for high-level message sequence charts (HMSCs) (Proceedings of the 28th International Colloquium on Automata, Languages and Programming (ICALP 2001), Crete (Greece), Lecture Notes in Computer Science, Vol. 2076, Springer, Berlin, 2001, pp. 797–808). We show that safe realizability is EXPSPACE-complete for bounded HMSCs but undecidable for the class of all HMSCs. This solves two open problems from Alur et al. Moreover we prove that safe realizability is also EXPSPACE-complete for the larger class of globally-cooperative HMSCs. [Copyright &y& Elsevier]