Search

Recently, we have shown that satisfiability for $\mathsf{ECTL}^*$ with constraints over $\mathbb{Z}$ is decidable using a new technique. This approach reduces the satisfiability problem of $\mathsf{ECTL}^*$ with constraints over some structure A (or class of structures) to the problem whether A has a certain model theoretic property that we called EHD (for "existence of homomorphisms is decidable"). Here we apply this approach to concrete domains that are tree-like and obtain several results. We show that satisfiability of $\mathsf{ECTL}^*$ with constraints is decidable over (i) semi-linear orders (i.e., tree-like structures where branches form arbitrary linear orders), (ii) ordinal trees (semi-linear orders where the branches form ordinals), and (iii) infinitely branching trees of height h for each fixed $h\in \mathbb{N}$. We prove that all these classes of structures have the property EHD. In contrast, we introduce Ehrenfeucht-Fraisse-games for $\mathsf{WMSO}+\mathsf{B}$ (weak $\mathsf{MSO}$ with the bounding quantifier) and use them to show that the infinite (order) tree does not have property EHD. As a consequence, a different approach has to be taken in order to settle the question whether satisfiability of $\mathsf{ECTL}^*$ (or even $\mathsf{LTL}$) with constraints over the infinite (order) tree is decidable.

It is shown that every tree of size $n$ over a fixed set of $\sigma$ different ranked symbols can be decomposed (in linear time as well as in logspace) into $O\big(\frac{n}{\log_\sigma n}\big) = O\big(\frac{n \log \sigma}{\log n}\big)$ many hierarchically defined pieces. Formally, such a hierarchical decomposition has the form of a straight-line linear context-free tree grammar of size $O\big(\frac{n}{\log_\sigma n}\big)$, which can be used as a compressed representation of the input tree. This generalizes an analogous result for strings. Previous grammar-based tree compressors were not analyzed for the worst-case size of the computed grammar, except for the top dag of Bille et al., for which only the weaker upper bound of $O\big(\frac{n}{\log_\sigma^{0.19} n}\big)$ (which was very recently improved to $O\big(\frac{n \cdot \log \log_\sigma n}{\log_\sigma n}\big)$ by H\"ubschle-Schneider and Raman) for unranked and unlabelled trees has been derived. The main result is used to show that every arithmetical formula of size $n$, in which only $m \leq n$ different variables occur, can be transformed (in linear time as well as in logspace) into an arithmetical circuit of size $O\big(\frac{n \cdot \log m}{\log n}\big)$ and depth $O(\log n)$. This refines a classical result of Brent from 1974, according to which an arithmetical formula of size $n$ can be transformed into a logarithmic depth circuit of size $O(n)$., Comment: A short version of this paper appeared in the Proceedings of FSTTCS 2014

We study the complexity of algorithmic problems for matrices that are represented by multi-terminal decision diagrams (MTDD). These are a variant of ordered decision diagrams, where the terminal nodes are labeled with arbitrary elements of a semiring (instead of 0 and 1). A simple example shows that the product of two MTDD-represented matrices cannot be represented by an MTDD of polynomial size. To overcome this deficiency, we extended MTDDs to MTDD_+ by allowing componentwise symbolic addition of variables (of the same dimension) in rules. It is shown that accessing an entry, equality checking, matrix multiplication, and other basic matrix operations can be solved in polynomial time for MTDD_+-represented matrices. On the other hand, testing whether the determinant of a MTDD-represented matrix vanishes PSPACE$-complete, and the same problem is NP-complete for MTDD_+-represented diagonal matrices. Computing a specific entry in a product of MTDD-represented matrices is #P-complete., Comment: An extended abstract of this paper will appear in the Proceedings of CSR 2014

Unranked trees can be represented using their minimal dag (directed acyclic graph). For XML this achieves high compression ratios due to their repetitive mark up. Unranked trees are often represented through first child/next sibling (fcns) encoded binary trees. We study the difference in size (= number of edges) of minimal dag versus minimal dag of the fcns encoded binary tree. One main finding is that the size of the dag of the binary tree can never be smaller than the square root of the size of the minimal dag, and that there are examples that match this bound. We introduce a new combined structure, the hybrid dag, which is guaranteed to be smaller than (or equal in size to) both dags. Interestingly, we find through experiments that last child/previous sibling encodings are much better for XML compression via dags, than fcns encodings. We determine the average sizes of unranked and binary dags over a given set of labels (under uniform distribution) in terms of their exact generating functions, and in terms of their asymptotical behavior., Comment: A short version of this paper appeared in the Proceedings of ICDT 2013

A simple linear-time algorithm for constructing a linear context-free tree grammar of size O(rg + 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., Comment: 45 pages, published in Information and Computation. Approximation ratio improved since the first version, figures improved, some examples added. A small calculation error corrected since the previous version (all claims hold as previously)

We show that satisfiability for CTL* with equality-, order-, and modulo-constraints over Z is decidable. Previously, decidability was only known for certain fragments of CTL*, e.g., the existential and positive fragments and EF., Comment: To appear at Concur 2013

It is shown that membership in rational subsets of wreath products H \wr V with H a finite group and V a virtually free group is decidable. On the other hand, it is shown that there exists a fixed finitely generated submonoid in the wreath product Z \wr Z with an undecidable membership problem.

We investigate tree-automatic well-founded trees. Using Delhomme's decomposition technique for tree-automatic structures, we show that the (ordinal) rank of a tree-automatic well-founded tree is strictly below omega^omega. Moreover, we make a step towards proving that the ranks of tree-automatic well-founded partial orders are bounded by omega^omega^omega: we prove this bound for what we call upwards linear partial orders. As an application of our result, we show that the isomorphism problem for tree-automatic well-founded trees is complete for level Delta^0_{omega^omega} of the hyperarithmetical hierarchy with respect to Turing-reductions., Comment: Will appear in Logical Methods of Computer Science

Computing normal forms in groups (or monoids) is in general harder than solving the word problem (equality testing). However, normal form computation has a much wider range of applications. It is therefore interesting to investigate the complexity of computing normal forms for important classes of groups. For Coxeter groups we show that the following algorithmic tasks can be solved by a deterministic Turing machine using logarithmic work space, only: 1. Compute the length of any geodesic normal form. 2. Compute the set of letters occurring in any geodesic normal form. 3. Compute the Parikh-image of any geodesic normal form in case that all defining relations have even length (i.e., in even Coxeter groups.) 4. For right-angled Coxeter groups we can do actually compute the short length normal form in logspace. (Note that short length normal forms are geodesic.) Next, we apply the results to right-angled Artin groups. They are also known as free partially commutative groups or as graph groups. As a consequence of our result on right-angled Coxeter groups we show that shortlex normal forms in graph groups can be computed in logspace, too. Graph groups play an important role in group theory, and they have a close connection to concurrency theory. As an application of our results we show that the word problem for free partially commutative inverse monoids is in logspace. This result generalizes a result of Ondrusch and the third author on free inverse monoids. Concurrent systems which are deterministic and co-deterministic can be studied via inverse monoids., Comment: An extended abstract of this paper appears in Proceedings of LATIN 2012

We prove that the complexity of the uniform first-order theory of ground tree rewrite graphs is in ATIME(2^{2^{poly(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(2^{2^{poly(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., Comment: accepted for Logical Methods in Computer Science

The compressed word problem for a finitely generated monoid M asks whether two given compressed words over the generators of M represent the same element of M. For string compression, straight-line programs, i.e., context-free grammars that generate a single string, are used in this paper. It is shown that the compressed word problem for a free inverse monoid of finite rank at least two is complete for Pi^p_2 (second universal level of the polynomial time hierarchy). Moreover, it is shown that there exists a fixed finite idempotent presentation (i.e., a finite set of relations involving idempotents of a free inverse monoid), for which the corresponding quotient monoid has a PSPACE-complete compressed word problem. It was shown previously that the ordinary uncompressed word problem for such a quotient can be solved in logspace. Finally, a PSPACE-algorithm that checks whether a given element of a free inverse monoid belongs to a given rational subset is presented. This problem is also shown to be PSPACE-complete (even for a fixed finitely generated submonoid instead of a variable rational subset)., Comment: A short version will appear in Proceedings of MFCS 2011

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 EXPTIME-complete (resp. P-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 PSPACE-complete (resp. P-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 Esik and Bloom.

In this work we introduce a new linear time compression algorithm, called "Re-pair for Trees", which compresses ranked ordered trees using linear straight-line context-free tree grammars. Such grammars generalize straight-line context-free string grammars and allow basic tree operations, like traversal along edges, to be executed without prior decompression. Our algorithm can be considered as a generalization of the "Re-pair" algorithm developed by N. Jesper Larsson and Alistair Moffat in 2000. The latter algorithm is a dictionary-based compression algorithm for strings. We also introduce a succinct coding which is specialized in further compressing the grammars generated by our algorithm. This is accomplished without loosing the ability do directly execute queries on this compressed representation of the input tree. Finally, we compare the grammars and output files generated by a prototype of the Re-pair for Trees algorithm with those of similar compression algorithms. The obtained results show that that our algorithm outperforms its competitors in terms of compression ratio, runtime and memory usage.

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. On the way to our main results, we show lower and upper bounds for the isomorphism problem for omega-automatic trees of every finite height: (i) It is decidable ($\Pi^0_1$-complete, resp,) for height 1 (2, resp.), (ii) $\Pi^1_1$-hard and in $\Pi^1_2$ for height 3, and (iii) $\Pi^1_{n-3}$- and $\Sigma^1_{n-3}$-hard and in $\Pi^1_{2n-4}$ (assuming CH) for all n > 3. All proofs are elementary and do not rely on theorems from set theory.

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). (ii) The isomorphism problem for automatic trees of height $n \geq 2$ is $\Pi^0_{2n-3}$-complete. (iii) The isomorphism problem for automatic linear orders is not arithmetical. This solves some open questions of Khoussainov, Rubin, and Stephan.

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. Thus, model checking fixed OCPs against CTL formulas with a fixed leftward until depth is in P. This generalizes a result of the first author, Mayr, and To for the expression complexity of CTL's fragment EF. Second, we prove that already over some fixed OCP, CTL model checking is PSPACE-hard. Third, we show that there already exists a fixed CTL formula for which model checking of OCPs is PSPACE-hard. For the latter, we employ two results from complexity theory: (i) Converting a natural number in Chinese remainder presentation into binary presentation is in logspace-uniform NC^1 and (ii) PSPACE is AC^0-serializable. We demonstrate that our approach can be used to answer further open questions.

In this paper we show that the membership problems for finitely generated submonoids and for rational subsets are recursively equivalent for groups with two or more ends.

We give a simpler proof using automata theory of a recent result of Kapovich, Weidmann and Myasnikov according to which so-called benign graphs of groups preserve decidability of the generalized word problem. These include graphs of groups in which edge groups are polycyclic-by-finite and vertex groups are either locally quasiconvex hyperbolic or polycyclic-by-finite and so in particular chordal graph groups (right-angled Artin groups).

In this paper we show that membership in finitely generated submonoids is undecidable for the free metabelian group of rank 2 and for the wreath product $\mathbb Z\wr (\mathbb Z\times \mathbb Z)$. We also show that subsemimodule membership is undecidable for finite rank free $(\mathbb Z\times \mathbb Z)$-modules. The proof involves an encoding of Turing machines via tilings. We also show that rational subset membership is undecidable for two-dimensional lamplighter groups.

It is shown that the compressed word problem for an HNN-extension with base group H and finite associated subgroups is polynomial time Turing-reducible to the compressed word problem for H. An analogous result for amalgamated free products is shown as well.

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 a previous paper of the second author by improving both, the lower and the upper bounds., Comment: 26 pages

We show that the membership problem in a finitely generated submonoid of a graph group (also called a right-angled Artin group or a free partially commutative group) is decidable if and only if the independence graph (commutation graph) is a transitive forest. As a consequence we obtain the first example of a finitely presented group with a decidable generalized word problem that does not have a decidable membership problem for finitely generated submonoids. We also show that the rational subset membership problem is decidable for a graph group if and only if the independence graph is a transitive forest, answering a question of Kambites, Silva, and the second author. Finally we prove that for certain amalgamated free products and HNN-extensions the rational subset and submonoid membership problems are recursively equivalent. In particular, this applies to finitely generated groups with two or more ends that are either torsion-free or residually finite.