The past decade has witnessed substantial developments in string solving. Motivated by the complexity of string solving strategies adopted in existing string solvers, we investigate a simple and generic method for solving string constraints: regular constraint propagation. The method repeatedly computes pre- or postimages of regular languages under the string functions present in a string formula, inferring more and more knowledge about the possible values of string variables, until either a conflict is found or satisfiability of the string formula can be concluded. Such a propagation strategy is applicable to string constraints with multiple operations like concatenation, replace, and almost all flavors of string transductions. We demonstrate the generality and effectiveness of this method theoretically and experimentally. On the theoretical side, we show that RCP is sound and complete for a large fragment of string constraints, subsuming both straight-line and chain-free constraints, two of the most expressive decidable fragments for which some modern string solvers provide formal completeness guarantees. On the practical side, we implement regular constraint propagation within the open-source string solver OSTRICH. Our experimental evaluation shows that this addition significantly improves OSTRICH’s performance and makes it competitive with existing solvers. In fact, it substantially outperforms other solvers on random PCP and bioinformatics benchmarks. The results also suggest that incorporating regular constraint propagation alongside other techniques could lead to substantial performance gains for existing solvers.

Parikh’s Theorem is a fundamental result in automata theory with numerous applications in computer science. These include software verification (e.g. infinite-state verification, string constraints, and theory of arrays), verification of cryptographic protocols (e.g. using Horn clauses modulo equational theories) and database querying (e.g. evaluating path-queries in graph databases), among others. Parikh’s Theorem states that the letter-counting abstraction of a language recognized by finite automata or context-free grammars is definable in Linear Integer Arithmetic (a.k.a. Presburger Arithmetic). In fact, there is a linear-time algorithm computing existential Presburger formulas capturing such abstractions, which enables an efficient analysis via SMT-solvers. Unfortunately, real-world applications typically require large alphabets (e.g. Unicode, containing a million of characters) — which are well-known to be not amenable to explicit treatment of the alphabets — or even worse infinite alphabets. Symbolic automata have proven in the last decade to be an effective algorithmic framework for handling large finite or even infinite alphabets. A symbolic automaton employs an effective boolean algebra, which offers a symbolic representation of character sets (i.e. in terms of predicates) and often lends itself to an exponentially more succinct representation of a language. Instead of letter-counting, Parikh’s Theorem for symbolic automata amounts to counting the number of times different predicates are satisfied by an input sequence. Unfortunately, naively applying Parikh’s Theorem from classical automata theory to symbolic automata yields existential Presburger formulas of exponential size. In this paper, we provide a new construction for Parikh’s Theorem for symbolic automata and grammars, which avoids this exponential blowup: our algorithm computes an existential formula in polynomial-time over (quantifier-free) Presburger and the base theory. In fact, our algorithm extends to the model of parametric symbolic grammars, which are one of the most expressive models of languages over infinite alphabets. We have implemented our algorithm and show it can be used to solve string constraints that are difficult to solve by existing solvers.

Abstract Sequence theories are an extension of theories of strings with an infinite alphabet of letters, together with a corresponding alphabet theory (e.g. linear integer arithmetic). Sequences are natural abstractions of extendable arrays, which permit a wealth of operations including append, map, split, and concatenation. In spite of the growing amount of tool support for theories of sequences by leading SMT-solvers, little is known about the decidability of sequence theories, which is in stark contrast to the state of the theories of strings. We show that the decidable theory of strings with concatenation and regular constraints can be extended to the world of sequences over an alphabet theory that forms a Boolean algebra, while preserving decidability. In particular, decidability holds when regular constraints are interpreted as parametric automata (which extend both symbolic automata and variable automata), but fails when interpreted as register automata (even over the alphabet theory of equality). When length constraints are added, the problem is Turing-equivalent to word equations with length (and regular) constraints. Similar investigations are conducted in the presence of symbolic transducers, which naturally model sequence functions like map, split, filter, etc. We have developed a new sequence solver, SeCo, based on parametric automata, and show its efficacy on two classes of benchmarks: (i) invariant checking on array-manipulating programs and parameterized systems, and (ii) benchmarks on symbolic register automata.

This paper initiates the study of data-path query languages (in particular, regular data path queries (RDPQ) and conjunctive RDPQ (CRDPQ)) in the classic setting of embedded finite model theory, wherein each graph is "embedded" into a background infinite structure (with a decidable FO theory or fragments thereof). Our goal is to address the current lack of support for typed attribute data (e.g. integer arithmetics) in existing data-path query languages, which are crucial in practice. We propose an extension of register automata by allowing powerful constraints over the theory and the database as guards, and having two types of registers: registers that can store values from the active domain, and read-only registers that can store arbitrary values. We prove NL data complexity for (C)RDPQ over the Presburger arithmetic, the real-closed field, the existential theory of automatic structures and word equations with regular constraints. All these results strictly extend the known NL data complexity of RDPQ with only equality comparisons, and provides an answer to a recent open problem posed by Libkin et al. Among others, we introduce one crucial proof technique for obtaining NL data complexity for data path queries over embedded graph databases called "Restricted Register Collapse (RRC)", inspired by the notion of Restricted Quantifier Collapse (RQC) in embedded finite model theory.

A word equation with one variable in a free group is given as U = V, where both U and V are words over the alphabet of generators of the free group and X, X⁻¹, for a fixed variable X. An element of the free group is a solution when substituting it for X yields a true equality (interpreted in the free group) of left- and right-hand sides. It is known that the set of all solutions of a given word equation with one variable is a finite union of sets of the form {α wⁱ β : i ∈ ℤ}, where α, w, β are reduced words over the alphabet of generators, and a polynomial-time algorithm (of a high degree) computing this set is known. We provide a cubic time algorithm for this problem, which also shows that the set of solutions consists of at most a quadratic number of the above-mentioned sets. The algorithm uses only simple tools of word combinatorics and group theory and is simple to state. Its analysis is involved and focuses on the combinatorics of occurrences of powers of a word within a larger word.

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.

In word equation problem we are given an equation u = v, where both u and v are words of letters and variables, and ask for a substitution of variables by words that equalizes the sides of the equation. This problem was first solved by Makanin and a different solution was proposed by Plandowski only 20 years later, his solution works in PSPACE, which is the best computational complexity bound known for this problem; on the other hand, the only known lower-bound is NP-hardness. In both cases the algorithms (and proofs) employed nontrivial facts on word combinatorics. In the paper I will present an application of a recent technique of recompression, which simplifies the known proofs and (slightly) lowers the complexity to linear nondeterministic space. The technique is based on employing simple compression rules (replacement of two letters ab by a new letter c, replacement of maximal repetitions of a by a new letter), and modifying the equations (replacing a variable X by bX or Xa) so that those operations are sound and complete. In particular, no combinatorial properties of strings are used. The approach turns out to be quite robust and can be applied to various generalizations and related scenarios (context unification, i.e. equations over terms; equations over traces, i.e. partially ordered words; ...).

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.

In first-order term unification, variables represent well-formed terms over a given signature, and we are to solve equations built using function symbols from the signature and such variables; this problem is well-known to be decidable (in linear time). In second-order term unification, the variables take arguments (i.e., other terms) and a substitution uses those arguments an arbitrary number of times; for instance, an equation f ( X ( c ), X ( c )) = X ( f ( c , c )) has a solution X = •, where • is a special symbol denoting the place in which the argument is substituted. Under this substitution, both sides evaluate to f ( c , c ). There are other solutions, for instance X = f (•,•), which evaluates both sides to f ( f ( c , c ), f ( c , c )); in general, a solution that evaluates both sides to full binary tree of arbitrary height is easy to construct. Second-order unification is in general undecidable. Context unification is a natural problem in between first- and second-order unification—we deal with equations over terms, the variables take arguments, but we restrict the set of solutions: The argument is used exactly once. Formally, contexts are terms with exactly one occurrence of the special symbol • and in context unification, we are given an equation over terms with variables representing contexts and ask about the satisfiability of this equation. For instance, when the aforementioned equation f ( X ( c ), X ( c )) = X ( f ( c , c )) is treated as a context unification problem, then it has exactly one solution: X = •. Other substitutions that are solutions of it as an instance of the second-unification problem, say X = f (•, •), are not valid, as • is used more than once. Context unification also generalizes satisfiability of word equations, which is decidable (in PSPACE). The decidability status of context unification remained unknown for almost two decades. In this article, we show that context unification is in PSPACE (in EXPTIME , when tree regular constraints are also allowed). Those results are obtained by extending the recently developed recompression technique, which was previously defined for strings and used to obtain a new PSPACE algorithm for satisfiability of word equations. In this article, the technique is generalized to trees, and the corresponding algorithm is generalized from word equations to context unification. The idea of recompression is to apply simple compression rules (replacing pairs of neighboring function symbols) to the solution of the context equation; to this end, we appropriately modify the equation (without the knowledge of the actual solution) so compressing the solution can be simulated by compressing parts of the equation. It is shown that if the compression operations are appropriately chosen, then the size of the instance is polynomial during the whole algorithm, thus giving a PSPACE-upper bound.

We consider the problem of edit distance in which block operations are allowed, i.e. we ask for the minimal number of (block) operations that are needed to transform a string s to t. We give O(log n) approximation algorithms, where n is the total length of the input strings, for the variants of the problem which allow the following sets of operations: block move; block move and block delete; block move and block copy; block move, block copy, and block uncopy. The results still hold if we additionally allow any of the following operations: character insert, character delete, block reversal, or block involution (involution is a generalisation of the reversal). Previously, algorithms only for the first and last variant were known, and they had approximation ratios O(log n log^*n) and O(log n (log^*n)^2), respectively. The edit distance with block moves is equivalent, up to a constant factor, to the common string partition problem, in which we are given two strings s, t and the goal is to partition s into minimal number of parts such that they can be permuted in order to obtain t. Thus we also obtain an O(log n) approximation for this problem (compared to the previous O(log n log^* n)). The results use a simplification of the previously used technique of locally consistent parsing, which groups short substrings of a string into phrases so that similar substrings are guaranteed to be grouped in a similar way. Instead of a sophisticated parsing technique relying on a deterministic coin tossing, we use a simple one based on a partition of the alphabet into two subalphabets. In particular, this lowers the running time from O(n log^* n) to O(n). The new algorithms (for block copy or block delete) use a similar algorithm, but the analysis is based on a specially tuned combinatorial function on sets of numbers.

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

Unambiguous conjunctive grammars with 1 nonterminal symbol are shown to be strictly weaker than the grammars with 2 nonterminal symbols, which are in turn strictly weaker that the grammars with 3 or more nonterminal symbols. This hierarchy is established by considering grammars over a one-symbol al phabet, for which it is shown that 1-nonterminal grammars describe only regular languages, 2-nonterminal grammars describe some non-regular languages, but all of them are in a certain sense sparse, whereas 3-nonterminal grammars may describe some non-regular languages of non-zero density. It is also proved that one can test a 2-nonterminal grammar for equivalence with a regular language, whereas the equivalence between a pair of 2-nonterminal grammars is undecidable.

In this talk I will survey the recompression technique in case of SLPs. The technique is based on applying simple compression operations (replacement of pairs of two different letters by a new letter and replacement of maximal repetition of a letter by a new symbol) to strings represented by SLPs. To this end we modify the SLPs, so that performing such compression operations on SLPs is possible. For instance, when we want to replace ab in the string and SLP has a production X to aY and the string generated by Y is bw, then we alter the rule of Y so that it generates w and replace Y with bY in all rules. In this way the rule becomes X to abY and so ab can be replaced, similar operations are defined for the right sides of the nonterminals. As a result, we are interested mostly in the SLP representation rather than the string itself and its combinatorial properties. What we need to control, though, is the size of the SLP. With appropriate choices of substrings to be compressed it can be shown that it stays linear. The proposed method turned out to be surprisingly efficient and applicable in various scenarios: for instance it can be used to test the equality of SLPs in time O(n log N), where n is the size of the SLP and N the length of the generated string; on the other hand it can be used to approximate the smallest SLP for a given string, with the approximation ratio O(log(n/g)) where n is the length of the string and g the size of the smallest SLP for this string, matching the best known bounds.

In this paper we propose a heuristical grammar compressor, based on the well-known Re-Pair algorithm. As Re-Pair, it recursively chooses a digram of letters to be replaced with a new symbol, while Re-Pair chooses the most often digram, we propose to also employ penalties, if the chosen digrams are not coherent with a Lempel-Ziv factorisation. The idea of such penalties is motivated by analysis of recent approximation algorithms for this problem. We experimentally evaluate the proposed heuristics on established corpora, obtaining smaller grammars than the one generated by Re-Pair for English (and similar) text data and WebGraph, unfortunately for other types of data no improvement was obtained.

Satisfiability of word equations is an important problem in the intersection of formal languages and algebra: Given two sequences consisting of letters and variables we are to decide whether there is a substitution for the variables that turns this equation into true equality of strings. The computational complexity of this problem remains unknown, with the best lower and upper bounds being, respectively, NP and PSPACE. Recently, the novel technique of recompression was applied to this problem, simplifying the known proofs and lowering the space complexity to (nondeterministic) O(n log n). In this paper we show that satisfiability of word equations is in nondeterministic linear space, thus the language of satisfiable word equations is context-sensitive. We use the known recompression-based algorithm and additionally employ Huffman coding for letters. The proof, however, uses analysis of how the fragments of the equation depend on each other as well as a new strategy for nondeterministic choices of the algorithm, which uses several new ideas to limit the space occupied by the letters.

Word equations is given by two strings over disjoint alphabets of letters and variables and we ask whether there is a substitution that satisfies this equation. Recently, a new PSPACE solution to this problem was proposed, it is based on compressing simple substrings of the equation and modifying the equation so that such operations are sound. The analysis focuses on the way the equation is stored and changed rather than on the combinatorics of words. This approach greatly simplified many existing proofs and algorithms. In particular, unlike the previous solutions, it generalises to equations over contexts (known for historical reasons as context unification): contexts are terms with one special symbol that represent a missing argument and they can be applied on terms, in which case their argument replaces the special constant.

We generalise the fundamental concept of LZ77 factorisation from strings to trees. A tree is represented as a collection of edge-disjoint fragments that either consist of one node or has already occurred earlier (in the BFS order). Similarly as for strings, such a collection uniquely determines the tree, so by minimising the number of fragments we obtain a compressed representation of the tree. We show that our generalisation has several useful properties of the standard LZ77 factorisation: it can be computed in polynomial time and its simpler variant in linear time; its size is not larger than the smallest grammar for a tree; it can be transformed (in linear time) into a tree grammar of size O(rg log(n/(rg))), where n is the size of the tree, g the size of the smallest grammar for this tree and r the maximal arity of the nodes in the tree, which matches a recent bound of Jez and Lohrey [STACS 2014], but with a simpler and more modular proof.

This is an Open Access Article. It is published by Schloss Dagstuhl – Leibniz Center for Informatics under the Creative Commons Attribution 4.0 Unported Licence (CC BY). Full details of this licence are available at: http://creativecommons.org/licenses/by/4.0/

In this paper we consider word equations with one-variable (and arbitrarily many occurrences of it). A recent technique of recompression, which is applicable to general word equations, is shown to be suitable also in this case. While in general case the recompression is nondeterministic in case of one-variable it becomes deterministic and its running time is $$\mathcal {O}(n + \#_X \log n)$$ , where $$\#_X$$ is the number of occurrences of the variable in the equation. This matches the previously best algorithm due to Dąbrowski and Plandowski. Then, using a couple of heuristics as well as more detailed time analysis, the running time is lowered to $$\mathcal {O}(n)$$ in the RAM model. Unfortunately, no new properties of solutions are shown.

In this article, we present an application of a simple technique of local recompression, previously developed by the author in the context algorithms for compressed strings [Jeż 2014a, 2015b, 2015a], to word equations. The technique is based on local modification of variables (replacing X by aX or Xa ) and iterative replacement of pairs of letters occurring in the equation by a “fresh” letter, which can be seen as a bottom-up compression of the solution of the given word equation, or, to be more specific, building a Straight-Line Programme for the solution of the word equation. Using this technique, we give new, independent, and self-contained proofs of many known results for word equations. To be more specific, the presented (nondeterministic) algorithm runs in O ( n log n space and in time polynomial in n and log N , where n is the size of the input equation and N the size of the length-minimal solution of the word equation. Furthermore, for O (1) variables, the bound on the space consumption is in fact linear, that is, O ( m ), where m is the size of the space used by the input. This yields that for each k the set of satisfiable word equations with k variables is context sensitive. The presented algorithm can be easily generalised to a generator of all solutions of the given word equation (without increasing the space usage). Furthermore, a further analysis of the algorithm yields an independent proof of doubly exponential upper bound on the size of the length-minimal solution. The presented algorithm does not use exponential bound on the exponent of periodicity. Conversely, the analysis of the algorithm yields an independent proof of the exponential bound on exponent of periodicity.

In this article, a fully compressed pattern matching problem is studied. The compression is represented by straight-line programs (SLPs)—that is, context-free grammars generating exactly one string; the term fully means that both the pattern and the text are given in the compressed form. The problem is approached using a recently developed technique of local recompression: the SLPs are refactored so that substrings of the pattern and text are encoded in both SLPs in the same way. To this end, the SLPs are locally decompressed and then recompressed in a uniform way. This technique yields an O (( n + m ) log M ) algorithm for compressed pattern matching, assuming that M fits in O (1) machine words, where n ( m ) is the size of the compressed representation of the text (pattern, respectively), and M is the size of the decompressed pattern. If only m + n fits in O (1) machine words, the running time increases to O (( n + m ) log M log ( n + m )). The previous best algorithm due to Lifshits has O ( n 2 m ) running time.

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.

Let $\pi'_{w}$ denote the failure function of the Knuth-Morris-Pratt algorithm for a word w. In this paper we study the following problem: given an integer array $A'[1 \mathinner {\ldotp \ldotp }n]$ , is there a word w over an arbitrary alphabet Σ such that $A'[i]=\pi'_{w}[i]$ for all i? Moreover, what is the minimum cardinality of Σ required? We give an elementary and self-contained $\mathcal{O}(n\log n)$ time algorithm for this problem, thus improving the previously known solution (Duval et al. in Conference in honor of Donald E. Knuth, 2007), which had no polynomial time bound. Using both deeper combinatorial insight into the structure of π′ and advanced algorithmic tools, we further improve the running time to $\mathcal{O}(n)$ .

In this paper, a compressed membership problem for finite automata, both deterministic (DFAs) and non-deterministic (NFAs), with compressed transition labels is studied. The compression is represented by straight-line programs (SLPs), i.e. context-free grammars generating exactly one string. A novel technique of dealing with SLPs is employed: the SLPs are recompressed, so that substrings of the input word are encoded in SLPs labelling the transitions of the NFA (DFA) in the same way, as in the SLP representing the input text. To this end, the SLPs are locally decompressed and then recompressed in a uniform way. Furthermore, in order to reflect the recompression in the NFA, we need to modify it only a little, in particular its size stays polynomial in the input size. Using this technique it is shown that the compressed membership for NFA with compressed labels is in NP, thus confirming the conjecture of Plandowski and Rytter (Jewels Are Forever, pp. 262–272, Springer, Berlin, 1999 ) and extending the partial result of Lohrey and Mathissen (in CSR, LNCS, vol. 6651, pp. 275–288, Springer, Berlin, 2011 ); as this problem is known to be NP -hard (in Plandowski and Rytter, Jewels Are Forever, pp. 262–272, Springer, Berlin, 1999 ), we settle its exact computational complexity. Moreover, the same technique applied to the compressed membership for DFA with compressed labels yields that this problem is in P , and this problem is known to be P -hard (in Markey and Schnoebelen, Inf. Process. Lett. 90(1):3–6, 2004 ; Beaudry et al., SIAM J. Comput. 26(1):138–152, 1997 ).

We present an application of a local recompression technique, previously developed by the author in the context of compressed membership problems and compressed pattern matching, to word equations. The technique is based on local modification of variables (replacing X by aX or Xa) and replacement of pairs of letters appearing in the equation by a 'fresh' letter, which can be seen as a bottom-up compression of the solution of the given word equation, to be more specific, building an SLP (Straight-Line Programme) for the solution of the word equation. Using this technique we give new self-contained proofs of many known results for word equations: the presented nondeterministic algorithm runs in O(n log n) space and in time polynomial in log N and n, where N is the size of the length-minimal solution of the word equation. It can be easily generalised to a generator of all solutions of the word equation. A further analysis of the algorithm yields a doubly exponential upper bound on the size of the length-minimal solution. The presented algorithm does not use exponential bound on the exponent of periodicity. Conversely, the analysis of the algorithm yields a new proof of the exponential bound on exponent of periodicity. For O(1) variables with arbitrary many appearances it works in linear space.

We consider online competitive algorithms for the problem of collecting weighted items from a dynamic queue S . The content of S varies over time. An update to S can occur between any two consecutive time steps, and it consists in deleting any number of items at the front of S and inserting other items into arbitrary locations in S . At each time step we are allowed to collect one item in S . The objective is to maximize the total weight of collected items. This is a generalization of bounded-delay packet scheduling (also known as buffer management). We present several upper and lower bounds on the competitive ratio for the general case and for some restricted variants of this problem.

In this paper, a compressed membership problem for finite automata, both deterministic and non-deterministic, with compressed transition labels is studied. The compression is represented by straight-line programs (SLPs), i.e. context-free grammars generating exactly one string. A novel technique of dealing with SLPs is introduced: the SLPs are recompressed, so that substrings of the input text are encoded in SLPs labelling the transitions of the NFA (DFA) in the same way, as in the SLP representing the input text. To this end, the SLPs are locally decompressed and then recompressed in a uniform way. Furthermore, such recompression induces only small changes in the automaton, in particular, the size of the automaton remains polynomial. Using this technique it is shown that the compressed membership for NFA with compressed labels is in NP, thus confirming the conjecture of Plandowski and Rytter and extending the partial result of Lohrey and Mathissen; as it is already known, that this problem is NP-hard, we settle its exact computational complexity. Moreover, the same technique applied to the compressed membership for DFA with compressed labels yields that this problem is in P; for this problem, only trivial upper-bound PSPACE was known.

Systems of equations with sets of integers as unknowns are considered. It is shown that the class of sets representable by unique solutions of equations using the operations of union and addition, defined as S+T={m+n∣m∈S,n∈T}, and with ultimately periodic constants is exactly the class of hyper-arithmetical sets. Equations using addition only can represent every hyper-arithmetical set under a simple encoding. All hyper-arithmetical sets can also be represented by equations over sets of natural numbers equipped with union, addition and subtraction $S \mathop {\mbox {$-^{\hspace {-.5em}\cdot }\,\,$}}T=\{m-n \mid m \in S, n \in T, m \geq n\}$ . Testing whether a given system has a solution is $\varSigma ^{1}_{1}$ -complete for each model. These results, in particular, settle the expressive power of the most general types of language equations, as well as equations over subsets of free groups.

Systems of equations with sets of integers as unknowns are considered. It is shown that the class of sets representable by unique solutions of equations using the operations of union and addition $S+T=\makeset{m+n}{m \in S, \: n \in T}$ and with ultimately periodic constants is exactly the class of hyper-arithmetical sets. Equations using addition only can represent every hyper-arithmetical set under a simple encoding. All hyper-arithmetical sets can also be represented by equations over sets of natural numbers equipped with union, addition and subtraction $S \dotminus T=\makeset{m-n}{m \in S, \: n \in T, \: m \geqslant n}$. Testing whether a given system has a solution is $\Sigma^1_1$-complete for each model. These results, in particular, settle the expressive power of the most general types of language equations, as well as equations over subsets of free groups.

It is shown that equations of the form �(X) = ψ(X), in which the unknown X is a set of natural numbers and �, ψ use the operations of union, intersection and addition of sets S + T = {m + n |, m ∈ S, n ∈ T}, can simulate systems of equations � j (X 1 , …, X n ) = � j (X 1 , …, X n ) with 1 ≤ j ≤ ℓ, in the sense that solutions of any such system are encoded in the solutions of the corresponding equation. This implies computational universality of least and greatest solutions of equations �(X) = ψ(X), as well as undecidability of their basic decision problems. It is sufficient to use only singleton constants in the construction. All results equally apply to language equations over a one-letter alphabet Σ = {a}.

We consider the problem of collecting weighted items from a dynamic queue . Before each step, some items at the front of can be deleted and some other items can be added to at any place. An item, once deleted, cannot be re-inserted — in other words, it “expires”. We are allowed to collect one item from per step. Each item can be collected only once. The objective is to maximize the total weight of the collected items. We study the online version of the dynamic queue problem. It is quite easy to see that the greedy algorithm that always collects the maximum-value item is 2-competitive, and that no deterministic online algorithm can be better than 1.618-competitive. We improve both bounds: We give a 1.89-competitive algorithm for general dynamic queues and we show a lower bound of 1.632 on the competitive ratio. We also provide other upper and lower bounds for restricted versions of this problem. The dynamic queue problem is a generalization of the well-studied buffer management problem, and it is an abstraction of the buffer management problem for network links with intermittent access.

Systems of equations of the form $X=YZ$ and $X=C$ are considered, in which the unknowns are sets of natural numbers, ``$+$'' denotes pairwise sum of sets $S+T=\ensuremath{ \{ m+n \: | \: m \in S, \; n \in T \} }$, and $C$ is an ultimately periodic constant. It is shown that such systems are computationally universal, in the sense that for every recursive (r.e., co-r.e.) set $S \subseteq \mathbb{N}$ there exists a system with a unique (least, greatest) solution containing a component $T$ with $S=\ensuremath{ \{ n \: | \: 16n+13 \in T \} }$. This implies undecidability of basic properties of these equations. All results also apply to language equations over a one-letter alphabet with concatenation and regular constants.

Systems of equations over sets of natural numbers (or, equivalently, language equations over a one-letter alphabet) of the form $X_i=varphi_i(X_1, ldots, X_n)$ ($1 leqslant i leqslant n$) are considered. Expressions $varphi_i$ may contain the operations of union, intersection and pairwise sum $A plus B = {x + y mid x in A, y in B$. A system with an EXPTIME-complete least solution is constructed, and it is established that least solutions of all such systems are in EXPTIME. The general membership problem for these equations is proved to be EXPTIME-complete.