It is shown that the problem of computing the Strahler number of a binary tree given as a term is complete for the circuit complexity class uniform NC¹. For several variants, where the binary tree is given by a pointer structure or in a succinct form by a directed acyclic graph or a tree straight-line program, the complexity of computing the Strahler number is determined as well. The problem, whether a given context-free grammar in Chomsky normal form produces a derivation tree (resp., an acyclic derivation tree), whose Strahler number is at least a given number k is shown to be P-complete (resp., PSPACE-complete).

Enumerating the result set of a first-order query over a relational structure of bounded degree can be done with linear preprocessing and constant delay. In this work, we extend this result towards the compressed perspective where the structure is given in a potentially highly compressed form by a straight-line program (SLP). Our main result is an algorithm that enumerates the result set of a first-order query over a structure of bounded degree that is represented by an SLP satisfying the so-called apex condition. For a fixed formula, the enumeration algorithm has constant delay and needs a preprocessing time that is linear in the size of the SLP.

Abstract It is shown that the subgroup membership problem for a virtually free group can be decided in polynomial time when all group elements are represented by so-called power words, i.e., words of the form $$p_1^{z_1} p_2^{z_2} \cdots p_k^{z_k}$$ p 1 z 1 p 2 z 2 ⋯ p k z k . Here the $$p_i$$ p i are explicit words over the generating set of the group and all $$z_i$$ z i are binary encoded integers. As a corollary, it follows that the subgroup membership problem for the matrix group $$\textsf{GL}(2,\mathbb {Z})$$ GL ( 2 , Z ) can be decided in polynomial time when elements of $$\textsf{GL}(2,\mathbb {Z})$$ GL ( 2 , Z ) are represented by matrices with binary encoded integers. For the same input representation, it also shown that one can compute in polynomial time the index of a given finitely generated subgroup of $$\textsf{GL}(2,\mathbb {Z})$$ GL ( 2 , Z ) .

Abstract The power word problem for a group $$\varvec{G}$$ G asks whether an expression $$\varvec{u_1^{x_1} \cdots u_n^{x_n}}$$ u 1 x 1 ⋯ u n x n , where the $$\varvec{u_i}$$ u i are words over a finite set of generators of $$\varvec{G}$$ G and the $$\varvec{x_i}$$ x i binary encoded integers, is equal to the identity of $$\varvec{G}$$ G . It is a restriction of the compressed word problem, where the input word is represented by a straight-line program (i.e., an algebraic circuit over $$\varvec{G}$$ G ). We start by showing some easy results concerning the power word problem. In particular, the power word problem for a group $$\varvec{G}$$ G is $$\varvec{\textsf{uNC}^{1}}$$ uNC 1 -many-one reducible to the power word problem for a finite-index subgroup of $$\varvec{G}$$ G . For our main result, we consider graph products of groups that do not have elements of order two. We show that the power word problem in a fixed such graph product is $$\varvec{\textsf{AC} ^0}$$ AC 0 -Turing-reducible to the word problem for the free group $$\varvec{F_2}$$ F 2 and the power word problems of the base groups. Furthermore, we look into the uniform power word problem in a graph product, where the dependence graph and the base groups are part of the input. Given a class of finitely generated groups $$\varvec{\mathcal {C}}$$ C without order two elements, the uniform power word problem in a graph product can be solved in $$\varvec{\textsf{AC} ^0[\textsf{C}_=\textsf{L} ^{{{\,\textrm{UPowWP}\,}}(\mathcal {C})}]}$$ AC 0 [ C = L UPowWP ( C ) ] , where $$\varvec{{{\,\textrm{UPowWP}\,}}(\mathcal {C})}$$ UPowWP ( C ) denotes the uniform power word problem for groups from the class $$\varvec{\mathcal {C}}$$ C . As a consequence of our results, the uniform knapsack problem in right-angled Artin groups is $$\varvec{\textsf{NP}}$$ NP -complete. The present paper is a combination of the two conference papers (Lohrey and Weiß 2019b, Stober and Weiß 2022a). In Stober and Weiß (2022a) our results on graph products were wrongly stated without the additional assumption that the base groups do not have elements of order two. In the present work we correct this mistake. While we strongly conjecture that the result as stated in Stober and Weiß (2022a) is true, our proof relies on this additional assumption.

We present a linear preprocessing and output-linear delay enumeration algorithm for MSO-queries over trees that are compressed in the well-established grammar-based framework. Time bounds are measured with respect to the size of the compressed representation of the tree. Our result extends previous work on the enumeration of MSO-queries over uncompressed trees and on the enumeration of document spanners over compressed text documents.

A short version will be presented at the conference FSTTCS 2022

We consider exponent equations in finitely generated groups. These are equations, where the variables appear as exponents of group elements and take values from the natural numbers. Solvability of such (systems of) equations has been intensively studied for various classes of groups in recent years. In many cases, it turns out that the set of all solutions on an exponent equation is a semilinear set that can be constructed effectively. Such groups are called knapsack semilinear. The class of knapsack semilinear groups is quite rich and it is closed under many group theoretic constructions, e.g., finite extensions, graph products, wreath products, amalgamated free products with finite amalgamated subgroups, and HNN-extensions with finite associated subgroups. On the other hand, arbitrary HNN-extensions do not preserve knapsack semilinearity. In this paper, we consider the knapsack semilinearity of HNN-extensions, where the stable letter t acts trivially by conjugation on the associated subgroup A of the base group G. We show that under some additional technical conditions, knapsack semilinearity transfers from the base group G to the HNN-extension. These additional technical conditions are satisfied in many cases, e.g., when A is a centralizer in G or A is a quasiconvex subgroup of the hyperbolic group G.

We study deterministic and randomized streaming algorithms for word problems of finitely generated groups. For finitely generated linear groups, metabelian groups and free solvable groups we show the existence of randomized streaming algorithms with logarithmic space complexity for their word problems. We also show that the class of finitely generated groups with a logspace randomized streaming algorithm for the word problem is closed under several group theoretical constructions: finite extensions, direct products, free products and wreath products by free abelian groups. We contrast these results with several lower bound. An example of a finitely presented group, where the word problem has only a linear space randomized streaming algorithm, is Thompson’s group F.

We show that the subset sum problem, the knapsack problem and the rational subset membership problem for permutation groups are NP-complete. Concerning the knapsack problem we obtain NP-completeness for every fixed $n \geq 3$, where $n$ is the number of permutations in the knapsack equation. In other words: membership in products of three cyclic permutation groups is NP-complete. This sharpens a result of Luks, which states NP-completeness of the membership problem for products of three abelian permutation groups. We also consider the context-free membership problem in permutation groups and prove that it is PSPACE-complete but NP-complete for a restricted class of context-free grammars where acyclic derivation trees must have constant Horton-Strahler number. Our upper bounds hold for black box groups. The results for context-free membership problems in permutation groups yield new complexity bounds for various intersection non-emptiness problems for DFAs and a single context-free grammar.

It is shown that the subgroup membership problem for a virtually free group can be decided in polynomial time where all group elements are represented by so-called power words, i.e., words of the form p_1^{z_1} p_2^{z_2} ⋯ p_k^{z_k}. Here the p_i are explicit words over the generating set of the group and all z_i are binary encoded integers. As a corollary, it follows that the subgroup membership problem for the matrix group GL(2,ℤ) can be decided in polynomial time when all matrix entries are given in binary notation.

Abstract In the sliding window streaming model the goal is to compute an output value that only depends on the lastnsymbols from the data stream. Thereby, only space sublinear in the window sizenshould be used. Quite often randomization is used in order to achieve this goal. In the literature, one finds two different correctness criteria for randomized sliding window algorithms: (i) one can require that for every data stream and every time instantt, the algorithm computes a correct output value with high probability, or (ii) one can require that for every data stream the probability that the algorithm computes at every time instant a correct output value is high. Condition (ii) is stronger than (i) and is called “strict correctness” in this paper. The main result of this paper states that every strictly correct randomized sliding window algorithm can be derandomized without increasing the worst-case space consumption.

In a seminal paper, Charikar et al. derive upper and lower bounds on the approximation ratios for several grammar-based compressors, but in all cases there is a gap between the lower and upper bound. Here the gaps for LZ78 and BISECTION are closed by showing that the approximation ratio of LZ78 is Θ((n/log n)2/3), whereas the approximation ratio of BISECTION is Θ(√(n/log n)). In addition, the lower bound for RePair is improved from Ω(√(log n)) to Ω(log n/log log n). Finally, results of Arpe and Reischuk relating grammar-based compression for arbitrary alphabets and binary alphabets are improved.

We give lower bounds on the complexity of the word problem of certain non-solvable groups: for a large class of non-solvable infinite groups, including in particular free groups, Grigorchuk’s group and Thompson’s groups, we prove that their word problem is ALOGTIME-hard. For some of these groups (including Grigorchuk’s group and Thompson’s groups) we prove that the circuit value problem (which is equivalent to the circuit evaluation problem) is PSPACE-complete.

We prove new complexity results for computational problems in certain wreath products of groups and (as an application) for free solvable group. For a finitely generated group we study the so-called power word problem (does a given expression $u_1^{k_1} \ldots u_d^{k_d}$, where $u_1, \ldots, u_d$ are words over the group generators and $k_1, \ldots, k_d$ are binary encoded integers, evaluate to the group identity?) and knapsack problem (does a given equation $u_1^{x_1} \ldots u_d^{x_d} = v$, where $u_1, \ldots, u_d,v$ are words over the group generators and $x_1,\ldots,x_d$ are variables, has a solution in the natural numbers). We prove that the power word problem for wreath products of the form $G \wr \mathbb{Z}$ with $G$ nilpotent and iterated wreath products of free abelian groups belongs to $\mathsf{TC}^0$. As an application of the latter, the power word problem for free solvable groups is in $\mathsf{TC}^0$. On the other hand we show that for wreath products $G \wr \mathbb{Z}$, where $G$ is a so called uniformly strongly efficiently non-solvable group (which form a large subclass of non-solvable groups), the power word problem is $\mathsf{coNP}$-hard. For the knapsack problem we show $\mathsf{NP}$-completeness for iterated wreath products of free abelian groups and hence free solvable groups. Moreover, the knapsack problem for every wreath product $G \wr \mathbb{Z}$, where $G$ is uniformly efficiently non-solvable, is $Σ^2_p$-hard.

We prove that the power word problem for the solvable Baumslag-Solitar groups BS(1,q) = ⟨ a,t ∣ t a t^{-1} = a^q ⟩ can be solved in TC⁰. In the power word problem, the input consists of group elements g₁, …, g_d and binary encoded integers n₁, …, n_d and it is asked whether g₁^{n₁} ⋯ g_d^{n_d} = 1 holds. Moreover, we prove that the knapsack problem for BS(1,q) is NP-complete. In the knapsack problem, the input consists of group elements g₁, …, g_d,h and it is asked whether the equation g₁^{x₁} ⋯ g_d^{x_d} = h has a solution in ℕ^d.

Online fault-diagnosis is applied to various systems to enable an automatic monitoring and, if applicable, the recovery from faults to prevent the system from failing. For a sound decision on occurred faults, typically a large amount of sensor measurements and state variables has to be gathered, analyzed and evaluated in real-time. Due to the complexity and the nature of distributed systems all this data needs to be communicated among the network, which is an expensive affair in terms of communication resources and time. In this paper we present compression strategies that utilize the fact that many of these data streams are highly correlated and can be compressed simultaneously. Experimental results show that this can lead to better compression ratios compared to an individual compression of the data streams. Moreover, the algorithms support real-time constraints for time-triggered architectures and enable the data to be transmitted by means of shorter messages, leading to a reduced communication time and improved scheduling results.

We show that a context-free grammar of size that produces a single string of length (such a grammar is also called a string straight-line program) can be transformed in linear time into a context-free grammar for of size , whose unique derivation tree has depth . This solves an open problem in the area of grammar-based compression, improves many results in this area, and greatly simplifies many existing constructions. Similar results are shown for two formalisms for grammar-based tree compression: top dags and forest straight-line programs. These balancing results can be all deduced from a single meta-theorem stating that the depth of an algebraic circuit over an algebra with a certain finite base property can be reduced to with the cost of a constant multiplicative size increase. Here, refers to the size of the unfolding (or unravelling) of the circuit. In particular, this results applies to standard arithmetic circuits over (noncommutative) semirings.

We study the problem of recognizing regular languages in a variant of the streaming model of computation, called the sliding window model. In this model, we are given a size of the sliding window $n$ and a stream of symbols. At each time instant, we must decide whether the suffix of length $n$ of the current stream ("the active window") belongs to a given regular language. Recent works showed that the space complexity of an optimal deterministic sliding window algorithm for this problem is either constant, logarithmic or linear in the window size $n$ and provided natural language theoretic characterizations of the space complexity classes. Subsequently, those results were extended to randomized algorithms to show that any such algorithm admits either constant, double logarithmic, logarithmic or linear space complexity. In this work, we make an important step forward and combine the sliding window model with the property testing setting, which results in ultra-efficient algorithms for all regular languages. Informally, a sliding window property tester must accept the active window if it belongs to the language and reject it if it is far from the language. We consider deterministic and randomized sliding window property testers with one-sided and two-sided errors. In particular, we show that for any regular language, there is a deterministic sliding window property tester that uses logarithmic space and a randomized sliding window property tester with two-sided error that uses constant space.

The definition of kth-order empirical entropy of strings is extended to node-labeled binary trees. A suitable binary encoding of tree straight-line programs (that have been used for grammar-based tree compression before) is shown to yield binary tree encodings of size bounded by the kth-order empirical entropy plus some lower order terms. This generalizes recent results for grammar-based string compression to grammar-based tree compression. A long version of this paper can be found in [11].

In this work we introduce a new succinct variant of the word problem in a finitely generated group $G$, which we call the power word problem: the input word may contain powers $p^x$, where $p$ is a finite word over generators of $G$ and $x$ is a binary encoded integer. The power word problem is a restriction of the compressed word problem, where the input word is represented by a straight-line program (i.e., an algebraic circuit over $G$). The main result of the paper states that the power word problem for a finitely generated free group $F$ is AC$^0$-Turing-reducible to the word problem for $F$. Moreover, the following hardness result is shown: For a wreath product $G \wr \mathbb{Z}$, where $G$ is either free of rank at least two or finite non-solvable, the power word problem is complete for coNP. This contrasts with the situation where $G$ is abelian: then the power word problem is shown to be in TC$^0$.

We prove that the compressed word problem and the compressed simultaneous conjugacy problem are solvable in polynomial time in hyperbolic groups. In such problems, group elements are input as words defined by straight-line programs defined over a finite generating set for the group. We prove also that, for any infinite hyperbolic group G, the compressed knapsack problem in G is NP-complete.

The problem of universal source coding for binary trees is considered. Zhang, Yang, and Kieffer derived upper bounds on the average-case redundancy of codes based on directed acyclic graph (DAG) compression for binary tree sources with certain properties. In this paper, a natural class of binary tree sources is presented such that the demanded properties are fulfilled. Moreover, for both subclasses considered in the paper of Zhang, Yang, and Kieffer, their result is improved by deriving bounds on the maximal pointwise redundancy (or worst-case redundancy) instead of the average-case redundancy. Finally, using context-free tree grammars instead of DAGs, upper bounds on the maximal pointwise redundancy for certain binary tree sources are derived. This yields universal codes for new classes of binary tree sources.

A sliding window algorithm receives a stream of symbols and has to output at each time instant a certain value which only depends on the last $n$ symbols. If the algorithm is randomized, then at each time instant it produces an incorrect output with probability at most $ε$, which is a constant error bound. This work proposes a more relaxed definition of correctness which is parameterized by the error bound $ε$ and the failure ratio $ϕ$: A randomized sliding window algorithm is required to err with probability at most $ε$ at a portion of $1-ϕ$ of all time instants of an input stream. This work continues the investigation of sliding window algorithms for regular languages. In previous works a trichotomy theorem was shown for deterministic algorithms: the optimal space complexity is either constant, logarithmic or linear in the window size. The main results of this paper concerns three natural settings (randomized algorithms with failure ratio zero and randomized/deterministic algorithms with bounded failure ratio) and provide natural language theoretic characterizations of the space complexity classes.

We study the average size of the minimal directed acyclic graph (DAG) with respect to so-called leaf-centric binary tree sources as studied by Zhang, Yang, and Kieffer. A leaf-centric binary tree source induces for every n >= 2 a probability distribution on all binary trees with n leaves. We generalize a result shown by Flajolet, Gourdon, Martinez and Devroye according to which the average size of the minimal DAG of a binary tree that is produced by the binary search tree model is Theta(n / log n).

We study the space complexity of sliding window streaming algorithms that check membership of the window content in a fixed context-free language. For regular languages, this complexity is either constant, logarithmic or linear [Moses Ganardi et al., 2016]. We prove that every context-free language whose sliding window space complexity is log_2(n) - omega(1) must be regular and has constant space complexity. Moreover, for every c in N, c >= 1 we construct a (nondeterministic) context-free language whose sliding window space complexity is O(n^(1/c)) \ o(n^(1/c)). Finally, we give an example of a deterministic one-counter language whose sliding window space complexity is Theta((log n)^2).

In a recent paper we analyzed the space complexity of streaming algorithms whose goal is to decide membership of a sliding window to a fixed language. For the class of regular languages we proved a space trichotomy theorem: for every regular language the optimal space bound is either constant, logarithmic or linear. In this paper we continue this line of research: We present natural characterizations for the constant and logarithmic space classes and establish tight relationships to the concept of language growth. We also analyze the space complexity with respect to automata size and prove almost matching lower and upper bounds. Finally, we consider the decision problem whether a language given by a DFA/NFA admits a sliding window algorithm using logarithmic/constant space.

In recent years, knapsack problems for (in general non-commutative) groups have attracted attention. In this paper, the knapsack problem for wreath products is studied. It turns out that decidability of knapsack is not preserved under wreath product. On the other hand, the class of knapsack-semilinear groups, where solutions sets of knapsack equations are effectively semilinear, is closed under wreath product. As a consequence, we obtain the decidability of knapsack for free solvable groups. Finally, it is shown that for every non-trivial abelian group $G$, knapsack (as well as the related subset sum problem) for the wreath product $G \wr \mathbb{Z}$ is NP-complete.

With its ability to detect, identify and, if applicable, recover from occurred faults, online-diagnosis can help achieving fault-tolerant systems. A sound decision on an occurred fault is the foundation for fault-specific recovery actions. For this, typically a large amount of data has to be analyzed and evaluated. A diagnostic process implemented on a distributed system needs to communicate all those data among the network which is an expensive affair in terms of communication resources and time. In this paper we present an architecture for a distributed online diagnosis system with real time constraints that supports data compression to reduce the communication time. We further present a lossy compression method with a guaranteed compression ratio that is suitable for real time purposes.

Many XML documents are data-centric and do not make use of the inherent document order. Can we provide stronger compression for such documents through giving up order? We first consider compression via minimal dags (directed acyclic graphs) and study the worst case ratio of the size of the ordered dag divided by the size of the unordered dag, where the worst case is taken for all trees of size n. We prove that this worst case ratio is n / log n for the edge size and n log log n / log n for the node size. In experiments we compare several known compressors on the original document tree versus on a canonical version obtained by length-lexicographical sorting of subtrees. For some documents this difference is surprisingly large: reverse binary dags can be smaller by a factor of 3.7 and other compressors can be smaller by factors of up to 190.

We apply so-called tree straight-line programs to the problem of universal source coding for binary trees. We derive an upper bound on the maximal pointwise redundancy (or worst-case redundancy) that improve previous bounds on the average case redundancy obtained by Zhang, Yang, and Kieffer using directed acyclic graphs. Using this, we obtain universal codes for new classes of tree sources.

Probabilistic systems that accumulate quantities such as energy or cost are naturally modelled by cost chains, which are Markov chains whose transitions are labelled with a vector of numerical costs. Computing information on the probability distribution of the total accumulated cost is a fundamental problem in this model. In this paper, we study the so-called cost problem, which is to compute quantiles of the total cost, such as the median cost or the probability of large costs. While it is an open problem whether such probabilities are always computable or even rational, we present an algorithm that allows to approximate the probabilities with arbitrary precision. The algorithm is simple to state and implement, and exploits strong results from graph theory such as the so-called BEST theorem for efficiently computing the number of Eulerian circuits in a directed graph. Moreover, our algorithm enables us to show that a decision version of the cost problem lies in the counting hierarchy, a counting analogue to the polynomial-time hierarchy that contains the latter and is included in PSPACE. Finally, we demonstrate the applicability of our algorithm by evaluating it experimentally.

Given finite-state automata (or context-free grammars) A,B over the same alphabet and a Parikh vector p, we study the complexity of deciding whether the number of words in the language of A with Parikh image p is greater than the number of such words in the language of B. Recently, this problem turned out to be tightly related to the cost problem for weighted Markov chains. We classify the complexity according to whether A and B are deterministic, the size of the alphabet, and the encoding of p (binary or unary).

The circuit evaluation problem for finite semirings is considered, where semirings are not assumed to have an additive or multiplicative identity. The following dichotomy is shown: If a finite semiring R (i) has a solvable multiplicative semigroup and (ii) does not contain a subsemiring with an additive identity 0 and a multiplicative identity 1 != 0, then its circuit evaluation problem is in the complexity class DET (which is contained in NC^2). In all other cases, the circuit evaluation problem is P-complete.

Myasnikov et al. have introduced the knapsack problem for arbitrary finitely generated groups. In LohreyZ16 the authors proved that for each graph group, the knapsack problem can be solved in NP. Here, we determine the exact complexity of the problem for every graph group. While the problem is TC^0-complete for complete graphs, it is LogCFL-complete for each (non-complete) transitive forest. For every remaining graph, the problem is NP-complete.

Metric temporal logic (MTL) and timed propositional temporal logic (TPTL) are quantitative extensions of linear temporal logic, which are prominent and widely used in the verification of real-timed systems. It was recently shown that the path checking problem for MTL, when evaluated over finite timed words, is in the parallel complexity class NC. In this paper, we derive precise complexity results for the path-checking problem for MTL and TPTL when evaluated over infinite data words over the non-negative integers. Such words may be seen as the behaviours of one-counter machines. For this setting, we give a complete analysis of the complexity of the path-checking problem depending on the number of register variables and the encoding of constraint numbers (unary or binary). As the two main results, we prove that the path-checking problem for MTL is P-complete, whereas the path-checking problem for TPTL is PSPACE-complete. The results yield the precise complexity of model checking deterministic one-counter machines against formulae of MTL and TPTL.

In this paper the computational complexity of the (bi)simulation problem over restricted graph classes is studied. For trees given as pointer structures or terms the (bi)simulation problem is complete for logarithmic space or NC^1, respectively. This solves an open problem from Balcázar, Gabarró, and Sántha. We also show that the simulation problem is P-complete even for graphs of bounded path-width.

A grammar-compressed ranked tree is represented with a linear space overhead so that a single traversal step, i.e., the move to the parent or the ith child, can be carried out in constant time. The data structure is extended so that equality of subtrees can be checked in constant time.

We study the space complexity of querying regular languages over data streams in the sliding window model. The algorithm has to answer at any point of time whether the content of the sliding window belongs to a fixed regular language. A trichotomy is shown: For every regular language the optimal space requirement is either in Theta(n), Theta(log(n)), or constant, where $n$ is the size of the sliding window.

It is shown that the knapsack problem, which was introduced by Myasnikov et al. for arbitrary finitely generated groups, can be solved in NP for graph groups. This result even holds if the group elements are represented in a compressed form by SLPs, which generalizes the classical NP-completeness result of the integer knapsack problem. We also prove general transfer results: NP-membership of the knapsack problem is passed on to finite extensions, HNN-extensions over finite associated subgroups, and amalgamated products with finite identified subgroups.

Recent decidability results on the satisfiability problem for temporal logics, in particular LTL, CTL* and ECTL*, with constraints over external structures like the integers with the order or infinite trees are surveyed in this paper.

We study the satisfiability problem of the logic K 2 = K × K—the two-dimensional variant of unimodal logic, where models are restricted to asynchronous products of two Kripke frames. Gabbay and Shehtman proved in 1998 that this problem is decidable in a tower of exponentials. So far, the best-known lower bound is NEXP-hardness shown by Marx and Mikulás in 2001. Our first main result closes this complexity gap. We show that satisfiability in K 2 is nonelementary. More precisely, we prove that it is k -NEXP-complete, where k is the switching depth (the minimal modal rank among the two dimensions) of the input formula, hereby solving a conjecture of Marx and Mikulás. Using our lower-bound technique also allows us to derive nonelementary lower bounds for the two-dimensional modal logics K4 × K and S5 2 × K, for which only elementary lower bounds were previously known. Moreover, we apply our technique to prove nonelementary lower bounds for the sizes of Feferman-Vaught decompositions with respect to product for any decomposable logic that is at least as expressive as unimodal K, generalizing a recent result by the first author and Lin. For the three-variable fragment FO 3 of first-order logic, we obtain the following two immediate corollaries: the size of Feferman-Vaught decompositions with respect to disjoint sum are inherently nonelementary, and equivalent formulas in Gaifman normal form are inherently nonelementary. Our second main result consists in providing effective elementary (more precisely, doubly exponential) upper bounds for the two-variable fragment FO 2 of first-order logic both for Feferman-Vaught decompositions and for equivalent formulas in Gaifman normal form.

It is shown that every tree of size n over a fixed set of sigma different ranked symbols can be decomposed into O(n/log_sigma(n)) = O((n * log(sigma))/ log(n)) many hierarchically defined pieces. Formally, such a hierarchical decomposition has the form of a straight-line linear context-free tree grammar of size O(n/log_sigma(n)), 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(n/log^{0.19}(n)) 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 <= n different variables occur, can be transformed (in time O(n * log(n)) into an arithmetical circuit of size O((n * log(m))/log(n)) and depth O(log(n)). This refines a classical result of Brent, according to which an arithmetical formula of size n can be transformed into a logarithmic depth circuit of size O(n).

A simple linear-time algorithm for constructing a linear context-free tree grammar of size O(r^2.g.log(n)) 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 an approximation ratio polynomial in g. The analysis of the algorithm uses an extension of the recompression technique (used in the context of grammar-based string compression) from strings to trees.

A Boolean closed full trio is a class of languages that is closed under the Boolean operations (union, intersection, and complementation) and rational transductions. It is well-known that the regular languages constitute such a Boolean closed full trio. It is shown here that every such language class that contains any non-regular language already includes the whole arithmetical hierarchy (and even the one relative to this language). A consequence of this result is that aside from the regular languages, no full trio generated by one language is closed under complementation. Our construction also shows that there is a fixed rational Kripke frame such that assigning an arbitrary non-regular language to some variable allows the definition of any language from the arithmetical hierarchy in the corresponding Kripke structure using multimodal logic.

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. This is because optional elements are more likely to appear towards the end of child sequences.

We adapt the TreeRePair tree compression algorithm and use it as an intermediate step in proving termination of term rewriting systems. We introduce a cost function that approximates the size of constraint systems that specify compatibility of matrix interpretations. We show how to integrate the compression algorithm with the Dependency Pairs transformation. Experiments show that compression reduces running times of constraint solvers, and thus improves the power of automated termination provers.

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 (${\mathsf{CTL}}$) on transition systems induced by OCA. A ${\mathsf{PSPACE}}$ upper bound is inherited from the modal $\mu$-calculus for this problem proved by Serre. First, we analyze the periodic behavior of ${\mathsf{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 ${\mathsf{CTL}}$ formulas with a fixed leftward until depth is in $\mathsf{P}$. This generalizes a corresponding recent result of Göller, Mayr, and To for the expression complexity of ${\mathsf{CTL}}$'s fragment ${\mathsf{EF}}$. Second, we prove that already over some fixed OCA, ${\mathsf{CTL}}$ model checking is ${\mathsf{PSPACE}}$-hard, i.e., expression complexity is ${\mathsf{PSPACE}}$-hard. Third, we show that there already exists a fixed ${\mathsf{CTL}}$ formula for which model checking of OCA is ${\mathsf{PSPACE}}$-hard, i.e., data complexity is ${\mathsf{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 ${\mathsf{NC}}^1$ and (ii) ${\mathsf{PSPACE}}$ is $\mathsf{AC}^0$-serializable. We demonstrate that our approach can be used to obtain further results. We show that model checking ${\mathsf{CTL}}$'s fragment ${\mathsf{EF}}$ over OCA is hard for $\mathsf{P}^{\mathsf{NP}}$, thus establishing a matching lower bound. Moreover, we show that the following problem is hard for ${\mathsf{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 ${\mathsf{CTL}}$ formula for which model checking 2-clock timed automata is ${\mathsf{PSPACE}}$-hard, generalizing a ${\mathsf{PSPACE}}$-hardness result for the combined complexity by Laroussinie, Markey, and Schnoebelen.

We show that the satisfiability problem for the two-dimensional extension KxK of unimodal K is nonelementary, hereby confirming a conjecture of Marx and Mikulas from 2001. Our lower bound technique allows us to derive further lower bounds for many-dimensional modal logics for which only elementary lower bounds were previously known. We also derive nonelementary lower bounds on the sizes of Feferman-Vaught decompositions w.r.t. product for any decomposable logic that is at least as expressive as unimodal K. Finally, we study the sizes of Feferman-Vaught decompositions and formulas in Gaifman normal form for fixed-variable fragments of first-order logic.

Larsson and Moffat's RePair algorithm is generalized from strings to trees. The new algorithm (TreeRePair) produces straight-line linear context-free tree (SLT) grammars which are smaller than those produced by previous grammar-based compressors such as BPLEX. Experiments show that a Huffman-based coding of the resulting grammars gives compression ratios comparable to the best known XML file compressors. Moreover, SLT grammars can be used as efficient memory representation of trees. Our investigations show that tree traversals over TreeRePair grammars are 14 times slower than over pointer structures and 5 times slower than over succinct trees, while memory consumption is only 1/43 and 1/6, respectively.

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.

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

Several new undecidability results on isomorphism problems for automatic structures are shown: (i) The isomorphism problem for automatic equivalence relations is Π10-complete, (ii) The isomorphism problem for automatic trees of height n ≥ 2 is Π2n-30-complete, (iii) The isomorphism problem for automatic linear orders is not arithmetical.

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.

Abstract 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 ( -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 -complete, resp.).

Abstract 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 2ΕΧΡΤΙΜΕ, thus 2ΕΧΡΤΙΜΕ-complete by an existing lower bound, and (ii) infinite-state model checking of basic process algebras and pushdown systems is also 2ΕΧΡΤΙΜΕ-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 2ΕΧΡΤΙΜΕ. We prove the lower bound(s) for infinite-state model checking using an encoding of alternating Turing machines.

Tight connections between leafs languages and strings compressed via 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, a fixed linear visibly pushdown language with a PSPACE-complete compressed membership problem is obtained. For XML languages, the compressed membership problem is shown to be coNP-complete.

Abstract The logic extends first-order logic by a generalized form of counting quantifiers (“the number of elements satisfying … belongs to the setC”). 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 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.

Logical properties of iterations of relational structures are studied and these decidability results are applied to the model checking of a powerful extension of pushdown systems. It is shown that the monadic chain theory of the iteration of a structure A (in the sense of Shelah and Stupp) is decidable in case the first-order theory of the structure A is decidable. This result fails if Muchnik's clone-predicate is added. A model of pushdown automata, where the stack alphabet is given by an arbitrary (possibly infinite) relational structure, is introduced. If the stack structure has a decidable first-order theory with regular reachability predicates, then the same holds for the configuration graph of this pushdown automaton. This result follows from our decidability result for the monadic chain theory of the iteration

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.

Hierarchical graph definitions allow a modular description of graphs using modules for the specification of repeated substructures. Beside this modularity, hierarchical graph definitions allow to specify graphs of exponential size using polynomial size descriptions. In many cases, this succinctness increases the computational complexity of decision problems when input graphs 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 graphs is investigated. Several new complete problems for the levels of the polynomial time hierarchy and the exponential time hierarchy are obtained. Two restrictions on the structure of hierarchical graph definitions that lead to more efficient model-checking algorithms are presented.