Patterns are words with terminals and variables. The language of a pattern is the set of words obtained by uniformly substituting all variables with words that contain only terminals. Length constraints restrict valid substitutions of variables by associating the variables of a pattern with a system (or disjunction of systems) of linear diophantine inequalities. Pattern languages with length constraints contain only words in which all variables are substituted to words with lengths that fulfill such a given set of length constraints. We consider membership, inclusion, and equivalence problems for erasing and non-erasing pattern languages with length constraints. Our main result shows that the erasing equivalence problem - one of the most prominent open problems in the realm of patterns - becomes undecidable if length constraints are allowed in addition to variable equality. Additionally, it is shown that the terminal-free inclusion problem, a prominent problem which has been shown to be undecidable in the binary case for patterns without any constraints, is also generally undecidable for all larger alphabets in this setting. Finally, we also show that considering regular constraints, i.e., associating variables also with regular languages as additional restrictions together with length constraints for valid substitutions, results in undecidability of the non-erasing equivalence problem. This sets a first upper bound on constraints to obtain undecidability in this case, as this problem is trivially decidable in the case of no constraints and as it has unknown decidability if only regular or only length constraints are considered.

A subsequence of a word w is a word u such that u = w [ i 1 ] w [ i 2 ] … w [ i k ] , for some set of indices 1 ≤ i 1 < i 2 < … < i k ≤ | w | . A word w is k -subsequence universal over an alphabet Σ if every word in Σ k appears in w as a subsequence. In this paper, we study the intersection between the set of k -subsequence universal words over some alphabet Σ and regular languages over Σ. We call a regular language L k- ∃ -subsequence universal if there exists a k -subsequence universal word in L , and k- ∀ -subsequence universal if every word of L is k -subsequence universal. We give algorithms solving the problems of deciding if a given regular language, represented by a finite automaton recognising it, is k- ∃ -subsequence universal and, respectively, if it is k- ∀ -subsequence universal , for a given k . The algorithms are FPT w.r.t. the size of the input alphabet, and their run-time does not depend on k ; they run in polynomial time in the number n of states of the input automaton when the size of the input alphabet is O ( log ⁡ n ) . Moreover, we show that the problem of deciding if a given regular language is k- ∃ -subsequence universal is NP-complete, when the language is over a large alphabet. Further, we provide algorithms for counting the number of k -subsequence universal words (paths) accepted by a given deterministic (respectively, non-deterministic) finite automaton, and ranking an input word (path) within the set of k -subsequence universal words accepted by a given finite automaton.

One of the most studied famous classes of words is the class of Lyndon words. Their studies are mainly motivated by the property that they factorise the free monoid as shown in the famous Chen-Fox-Lyndon Theorem. Several generalisations of Lyndon words as anti-Lyndon words, Nyldon words or inverse Lyndon words were made over time. In 2014, Grinberg introduced Nyldon words as a new perspective on the factorisation of the free monoid of words. In particular, for Nyldon words the famous Chen-Fox-Lyndon Theorem is considered w.r.t. a reversed lexicographical order, i.e., a lexicographically non-decreasing factorisation where each factor is smaller or equal than its successor. Further, a generalised lexicographical order is defined by equipping each position i in a word in Σ ⁎ with a total order ◃ i on Σ. For combining the concept of a generalised order as for generalised Lyndon words and the class of Nyldon words, we investigate a non-decreasing factorisation of the free monoid w.r.t. this generalised ordering and introduce generalised Nyldon words . We show that those words even force a unique non-decreasing factorisation, form a right Hall set, and coincide with the anti-Lyndon words.

Patterns are words with terminals and variables. The language of a pattern is the set of words obtained by uniformly substituting all variables with words that contain only terminals. Regular constraints restrict valid substitutions of variables by associating with each variable a regular language representable by, e.g., finite automata. Pattern languages with regular constraints contain only words in which each variable is substituted according to a set of regular constraints. We consider the membership, inclusion, and equivalence problems for erasing and non-erasing pattern languages with regular constraints. Our main result shows that the erasing equivalence problem-one of the most prominent open problems in the realm of patterns-becomes undecidable if regular constraints are allowed in addition to variable equality.

Abstract Word-representable graphs were introduced in 2008 by Kitaev and Pyatkin in the context of semigroup theory. Graphs are called word-representable if there exists a word with the graph’s nodes as letters such that the letters in the word alternate iff there is an edge between them in the graph. Until today numerous works investigated the word-representability of graphs but mostly from the graph perspective. In this work, we change the perspective to the words, i.e., we take classes of words and investigate the represented graphs. Our first subject of interest are the conjugates of words: we determine exactly which graphs are represented if we rotate the word. Afterwards, we look at k-local words introduced by Day et al. (FSTTCS LIPIcs, 2017) in order to gain more insights into this class of words. Here, we investigate especially which graphs are represented by 1-local words. Lastly, we prove that the language of all words representing a graph is regular. We were also able to characterise k-representable graphs, solving an open problem.

We study decision problems of the form: given a regular or linear context-free language L, is there a word of a given fixed form in L, where given fixed forms are based on word operations copy, marked copy, shuffle and their combinations.

Abstract String solvers are automated-reasoning tools that can solve combinatorial problems over formal languages. They typically operate on restricted first-order logic formulas that include operations such as string concatenation, substring relationship, and regular expression matching. String solving thus amounts to deciding the satisfiability of such formulas. While there exists a variety of different string solvers, many string problems cannot be solved efficiently by any of them. We present a new approach to string solving that encodes input problems into propositional logic and leverages incremental SAT solving. We evaluate our approach on a broad set of benchmarks. On the logical fragment that our tool supports, it is competitive with state-of-the-art solvers. Our experiments also demonstrate that an eager SAT-based approach complements existing approaches to string solving in this specific fragment.

A subsequence of a word w is a word u such that u = w[i₁] w[i₂] … w[i_k], for some set of indices 1 ≤ i₁ < i₂ < … < i_k ≤ |w|. A word w is k-subsequence universal over an alphabet Σ if every word in Σ^k appears in w as a subsequence. In this paper, we study the intersection between the set of k-subsequence universal words over some alphabet Σ and regular languages over Σ. We call a regular language L k-∃-subsequence universal if there exists a k-subsequence universal word in L, and k-∀-subsequence universal if every word of L is k-subsequence universal. We give algorithms solving the problems of deciding if a given regular language, represented by a finite automaton recognising it, is k-∃-subsequence universal and, respectively, if it is k-∀-subsequence universal, for a given k. The algorithms are FPT w.r.t. the size of the input alphabet, and their run-time does not depend on k; they run in polynomial time in the number n of states of the input automaton when the size of the input alphabet is O(log n). Moreover, we show that the problem of deciding if a given regular language is k-∃-subsequence universal is NP-complete, when the language is over a large alphabet. Further, we provide algorithms for counting the number of k-subsequence universal words (paths) accepted by a given deterministic (respectively, nondeterministic) finite automaton, and ranking an input word (path) within the set of k-subsequence universal words accepted by a given finite automaton.

Abstract The increased interest in string solving in the recent years has made it very hard to identify the right tool to address a particular user's purpose. Firstly, there is a multitude of string solvers, each addressing essentially some subset of the general problem. Generally, the addressed fragments are relevant and well motivated, but the lack of comparisons between the existing tools on an equal set of benchmarks cannot go unnoticed, especially as a common framework to compare solvers seems to be missing. In this paper, we gather a set of relevant benchmarks and introduce our new benchmarking framework to address this purpose.

We solve two long-standing open problems on word equations. Firstly, we prove that a one-variable word equation with constants has either at most three or an infinite number of solutions. The existence of such a bound had been conjectured, and the bound three is optimal. Secondly, we consider independent systems of three-variable word equations without constants. If such a system has a nonperiodic solution, then this system has at most 17 equations. Although probably not optimal, this is the first finite bound found. However, the conjecture of that bound being actually two still remains open.

Abstract We present a novel length-aware solving algorithm for the quantifier-free first-order theory over regex membership predicate and linear arithmetic over string length. We implement and evaluate this algorithm and related heuristics in the Z3 theorem prover. A crucial insight that underpins our algorithm is that real-world regex and string formulas contain a wealth of information about upper and lower bounds on lengths of strings, and such information can be used very effectively to simplify operations on automata representing regular expressions. Additionally, we present a number of novel general heuristics, such as the prefix/suffix method, that can be used to make a variety of regex solving algorithms more efficient in practice. We showcase the power of our algorithm and heuristics via an extensive empirical evaluation over a large and diverse benchmark of 57256 regex-heavy instances, almost 75% of which are derived from industrial applications or contributed by other solver developers. Our solver outperforms five other state-of-the-art string solvers, namely, CVC4, OSTRICH, Z3seq, Z3str3, and Z3-Trau, over this benchmark, in particular achieving a speedup of 2.4 $$\times $$ × over CVC4, 4.4 $$\times $$ × over Z3seq, 6.4 $$\times $$ × over Z3-Trau, 9.1 $$\times $$ × over Z3str3, and 13 $$\times $$ × over OSTRICH.

Modern cyber-physical systems pose great challenges for system engineers to keep track of the system's behavior when it comes to functions distributed all over the system. To check whether response time constraints are met, measurement data from different development stages is analyzed to track down the worst-case behavior observed.Several complex, signal dependencies have to be examined over long time periods. Therefore, computer aided approaches to support this task are strongly demanded. In this paper, we present EC.LANG, a formal language designed to specify evaluations over measurement data. It is particularly fitted to model event chains representing the data flow of system functions. To validate event chains against timing requirements, we implemented a compiler and an evaluation engine based on EC.LANG.

It is a long standing conjecture that the problem of deciding whether a quadratic word equation has a solution is in NP. It has also been conjectured that the length of a minimal solution to a quadratic equation is at most exponential in the length of the equation, with the latter conjecture implying the former. We show that both conjectures hold for some natural subclasses of quadratic equations, namely the classes of regular-reversed, k-ordered, and variable-sparse quadratic equations. We also discuss a connection of our techniques to the topic of unavoidable patterns, and the possibility of exploiting this connection to produce further similar results.

A rollercoaster is a sequence of real numbers for which every maximal contiguous subsequence---increasing or decreasing---has length at least three. By translating this sequence to a set of points in the plane, a rollercoaster can be defined as an $x$-monotone polygonal path for which every maximal subpath, with positive- or negative-slope edges, has at least three vertices. Given a sequence of distinct real numbers, the rollercoaster problem asks for a maximum-length (not necessarily contiguous) subsequence that is a rollercoaster. It was conjectured that every sequence of $n$ distinct real numbers contains a rollercoaster of length at least $\lceil n/2\rceil$ for $n>7$, while the best known lower bound is $\Omega(n/\log n)$. In this paper we prove this conjecture. Our proof is constructive and implies a linear-time algorithm for computing a rollercoaster of this length. Extending the $O(n\log n)$-time algorithm for computing a longest increasing subsequence, we show how to compute a maximum-length rollercoaster within the same time bound. A maximum-length rollercoaster in a permutation of $\{1,\dots,n\}$ can be computed in $O(n\log\log n)$ time. The search for rollercoasters was motivated by the orthogeodesic point-set embedding of caterpillars. A caterpillar is a tree such that deleting the leaves gives a path, called the spine. A top-view caterpillar is an embedded caterpillar where every vertex has degree either 4 or 1 and such that the two leaves adjacent to each spine vertex lie on opposite sides of the spine. As an application of our result on rollercoasters, we are able to find a planar drawing of every $n$-vertex top-view caterpillar on every set of $\frac{25}{3}(n+4)$ points in the plane, such that each edge is an orthogonal path with one bend. This improves the previous best known upper bound on the number of required points, which is $O(n\log n)$. We also show that such a drawing can be obtained in linear time when the points are given in sorted order.

A rollercoaster is a sequence of real numbers for which every maximal contiguous subsequence, that is increasing or decreasing, has length at least three. By translating this sequence to a set of points in the plane, a rollercoaster can be defined as a polygonal path for which every maximal sub-path, with positive- or negative-slope edges, has at least three points. Given a sequence of distinct real numbers, the rollercoaster problem asks for a maximum-length subsequence that is a rollercoaster. It was conjectured that every sequence of $n$ distinct real numbers contains a rollercoaster of length at least $\lceil n/2\rceil$ for $n>7$, while the best known lower bound is $Ω(n/\log n)$. In this paper we prove this conjecture. Our proof is constructive and implies a linear-time algorithm for computing a rollercoaster of this length. Extending the $O(n\log n)$-time algorithm for computing a longest increasing subsequence, we show how to compute a maximum-length rollercoaster within the same time bound. A maximum-length rollercoaster in a permutation of $\{1,\dots,n\}$ can be computed in $O(n \log \log n)$ time. The search for rollercoasters was motivated by orthogeodesic point-set embedding of caterpillars. A caterpillar is a tree such that deleting the leaves gives a path, called the spine. A top-view caterpillar is one of degree 4 such that the two leaves adjacent to each vertex lie on opposite sides of the spine. As an application of our result on rollercoasters, we are able to find a planar drawing of every $n$-node top-view caterpillar on every set of $\frac{25}{3}n$ points in the plane, such that each edge is an orthogonal path with one bend. This improves the previous best known upper bound on the number of required points, which is $O(n \log n)$. We also show that such a drawing can be obtained in linear time, provided that the points are given in sorted order.

We show how to prove theorems in additive number theory using a decision procedure based on finite automata. Among other things, we obtain the following analogue of Lagrange's theorem: every natural number > 686 is the sum of at most 4 natural numbers whose canonical base-2 representation is a binary square, that is, a string of the form xx for some block of bits x. Here the number 4 is optimal. While we cannot embed this theorem itself in a decidable theory, we show that stronger lemmas that imply the theorem can be embedded in decidable theories, and show how automated methods can be used to search for these stronger lemmas.

We investigate the class of regular-ordered word equations. In such equations, each variable occurs at most once in each side and the order of the variables occurring in both left and right hand sides is preserved (the variables can be, however, separated by potentially distinct constant factors). Surprisingly, we obtain that solving such simple equations, even when the sides contain exactly the same variables, is NP-hard. By considerations regarding the combinatorial structure of the minimal solutions of the more general quadratic equations we obtain that the satisfiability problem for regular-ordered equations is in NP. The complexity of solving such word equations under regular constraints is also settled. Finally, we show that a related class of simple word equations, that generalises one-variable equations, is in P.

The exchange of learnt clauses is a key feature in parallel SAT solving. We present an approach based on a communication graph. Each solver thread corresponds to a node in this graph. Communication between two solvers is allowed if the respective nodes are connected by an edge. This yields another dimension in controlling the amount of communication. We show results for this approach, gaining significant speedups for up to 256 parallel solvers.

Pseudo-repetitions are a natural generalisation of the classical notion of repetitions in sequences: they are the repeated concatenation of a word and its encoding under a certain morphism or antimorphism (anti-/morphism, for short). We approach the problem of deciding efficiently, for a word w and a literal anti-/morphism f, whether w contains an instance of a given pattern involving a variable x and its image under f, i.e., f(x). Our results generalise both the problem of finding fixed repetitive structures (e.g., squares, cubes) inside a word and the problem of finding palindromic structures inside a word. For instance, we can detect efficiently a factor of the form xx^Rxxx^R, or any other pattern of such type. We also address the problem of testing efficiently, in the same setting, whether the word w contains an arbitrary pseudo-repetition of a given exponent.

We investigate the solution set of the pseudoperiodic extension of the classical Lyndon and Sch\"utzenberger word equations. Consider u_1 ... u_l = v_1 ... v_m w_1 ... w_n, where u_i is in {u, theta(u)} for all 1 <= i <= l, v_j is in {v, theta(v)} for all 1 <= j <= m, w_k is in {w, theta(w)} for all 1 <= k <= n and u, v and w are variables, and theta is an antimorphic involution. A solution is called pseudoperiodic, if u,v,w are in {t, theta(t)}^+ for a word t. [Czeizler et al./I&C/2011] established that for small values of l, m, and n non-periodic solutions exist, and that for large enough values all solutions are pseudoperiodic. However, they leave a gap between those bounds which we close for a number of cases. Namely, we show that for l = 3 and either m,n >= 12 or m,n >= 5 and either m and n are not both even or not all u_i's are equal, all solutions are pseudoperiodic.

Pseudo-repetitions are a natural generalization of the classical notion of repetitions in sequences. We solve fundamental algorithmic questions on pseudo-repetitions by application of insightful combinatorial results on words. More precisely, we efficiently decide whether a word is a pseudo-repetition and find all the pseudo-repetitive factors of a word.

This special issue celebrates the 60th birthday of Professor Tero Harju (the actual birthday date is June 28, 2012).It consists of 20 original contributions written by his friends, colleagues and former students.The topics of this issue cover a broad spectrum of theoretical computer science and discrete mathematics, from automata theory via combinatorics on words to biomodelling -this coverage ref ects an impressive range of scientif c interest and research contributions by Tero.He made impressive scientif c contributions to many research areas including formal languages and automata theory, combinatorics on words, semigroup theory, computability theory, DNA computing, and biomodelling.Many of his results belong to highlights of those areas.His contributions to science are twofold: he solved many very challenging technical problems and he was also instrumental in shaping new research directions.One can mention here his solutions of famous open problems such as the equivalence problem of multitape f nite automata and Duval's conjecture on periodicity of words as examples of the former, and his work on regularity of splicing systems and the work on a formal framework for gene assembly in cilliates as examples of the latter.Tero is a Full Professor in the department of mathematics of University of Turku, Finland, and a member of Finnish Academy of Sciences.Although he stayed at a number of scientif c institutions abroad, his real nest is the combination of the department in Turku and his home in Lieto, not far from Turku.Still, thanks to the Internet and many travels to conferences where he presents his results, he has an impressive number of co-authors, mostly in Europe and North America.All four of us have extensive experience of working with Tero.The working sessions are long and intense, but they are often punctuated by bursts of laughing when Tero utters one of his one-liners: he has a wonderful sense of dry intellectual humor.Another characteristic feature of Tero is his remarkable modesty -he just lets his results speak for him.No wonder that Tero is popular in the scientif c community -the response to our call for papers to this special issue was enthusiastic indeed.

The relationship between the length of a word and the maximum length of its unbordered factors is investigated in this article. Consider a finite word w of length n . We call a word bordered if it has a proper prefix, which is also a suffix of that word. Let μ( w ) denote the maximum length of all unbordered factors of w , and let ∂( w ) denote the period of w . Clearly, μ( w ) ≤ ∂( w ). We establish that μ( w ) = ∂( w ), if w has an unbordered prefix of length μ( w ) and n ≥ 2μ( w ) − 1. This bound is tight and solves the stronger version of an old conjecture by Duval [1983]. It follows from this result that, in general, n ≥ 3μ( w ) − 3 implies μ( w ) = ∂( w ), which gives an improved bound for the question raised by Ehrenfeucht and Silberger in 1979.