Floating-point arithmetic provides a fast but inexact way of computing geometric predicates. In order for these predicates to be exact, it is important to rule out all the numerical situations where floating-point computations could lead to wrong results. Taking into account all the potential problems is a tedious work to do by hand. We study in this paper a floating-point implementation of a filter for the orientation-2 predicate, and how a formal and partially automatized verification of this algorithm avoided many pitfalls. The presented method is not limited to this particular predicate, it can easily be used to produce correct semi-static floating-point filters for other geometric predicates.

The properties characterizing Sturmian words are considered for words on multiliteral alphabets. We summarize various generalizations of Sturmian words to multiliteral alphabets and enlarge the list of known relationships among these generalizations. We provide a new equivalent definition of rich words and make use of it in the study of generalizations of Sturmian words based on palindromes. We also collect many examples of infinite words to illustrate differences in the generalized definitions of Sturmian words.

We show that Dejean's conjectureholds for n ≥ 27. This brings the final resolution of the conjecture by the approach of Moulin Ollagnier within range of the computationally feasible.

Right (left, two-sided) extendable part of a language consists of all words having infinitely many right (resp. left, two-sided) extensions within the language. We prove that for an arbitrary factorial language each of these parts has the same growth rate of complexity as the language itself. On the other hand, we exhibit a factorial language which grows superpolynomially, while its two-sided extendable part grows only linearly.

We investigate the density of critical factorizations of infinite sequences of words. The density of critical factorizations of a word is the ratio between the number of positions that permit a critical factorization, and the number of all positions of a word. We give a short proof of the Critical Factorization Theorem and show that the maximal number of noncritical positions of a word between two critical ones is less than the period of that word. Therefore, we consider only words of index one, that is words where the shortest period is larger than one half of their total length, in this paper. On one hand, we consider words with the lowest possible number of critical points and show, as an example, that every Fibonacci word longer than five has exactly one critical factorization and every palindrome has at least two critical factorizations. On the other hand, sequences of words with a high density of critical points are considered. We show how to construct an infinite sequence of words in four letters where every point in every word is critical. We construct an infinite sequence of words in three letters with densities of critical points approaching one, using square-free words, and an infinite sequence of words in two letters with densities of critical points approaching one half, using Thue–Morse words. It is shown that these bounds are optimal.

Arithmetical complexity of a sequence is the number of words of length n that can be extracted from it according to arithmetic progressions. We study uniformly recurrent words of low arithmetical complexity and describe the family of such words having lowest complexity.

In this paper, we solve some open problems related to (pseudo)palindrome closure operators and to the infinite words generated by their iteration, that is, standard episturmian and pseudostandard words. We show that if ϑ is an involutory antimorphism of A*, then the right and left ϑ-palindromic closures of any factor of a ϑ-standard word are also factors of some ϑ-standard word. We also introduce the class of pseudostandard words with “seed”, obtained by iterated pseudopalindrome closure starting from a nonempty word. We show that pseudostandard words with seed are morphic images of standard episturmian words. Moreover, we prove that for any given pseudostandard word s with seed, all sufficiently long left special factors of s are prefixes of it.

A square is the concatenation of a nonempty word with itself. A word has period p if its letters at distance p match. The exponent of a nonempty word is the quotient of its length over its smallest period. In this article we give a proof of the fact that there exists an infinite binary word which contains finitely many squares and simultaneously avoids words of exponent larger than 7/3. Our infinite word contains 12 squares, which is the smallest possible number of squares to get the property, and 2 factors of exponent 7/3. These are the only factors of exponent larger than 2. The value 7/3 introduces what we call the finite-repetition threshold of the binary alphabet. We conjecture it is 7/4 for the ternary alphabet, like its repetitive threshold.

Here we give a characterization of Arnoux–Rauzy sequences by the way of the lexicographic orderings of their alphabet.

Since recognizable tree languages are closed under the rational operations, every regular tree expression denotes a recognizable tree language. We provide an alternative proof to this fact that results in smaller tree automata. To this aim, we transfer Antimirov's partial derivatives from regular word expressions to regular tree expressions. For an analysis of the size of the resulting automaton as well as for algorithmic improvements, we also transfer the methods of Champarnaud and Ziadi from words to trees.

Consider partial maps ∑* → $\mathbb R$ with a rational domain. We show that two families of such series are actually the same: the unambiguous rational series on the one hand, and the max-plus and min-plus rational series on the other hand. The decidability of equality was known to hold in both families with different proofs, so the above unifies the picture. We give an effective procedure to build an unambiguous automaton from a max-plus automaton and a min-plus one that recognize the same series.

The theorem of Fraenkel and Simpson states that the maximum number of distinct squares that a word w of length n can contain is less than 2n. This is based on the fact that no more than two squares can have their last occurrences starting at the same position. In this paper we show that the maximum number of the last occurrences of squares per position in a partial word containing one hole is 2k, where k is the size of the alphabet. Moreover, we prove that the number of distinct squares in a partial word with one hole and of length n is less than 4n, regardless of the size of the alphabet. For binary partial words, this upper bound can be reduced to 3n.

We show that many classical decision problems about1-counter ω-languages, context free ω-languages, or infinitary rational relations, are Π½ -complete, hence located at the second level of the analytical hierarchy, and “highly undecidable”.In particular, the universalityproblem, the inclusion problem, the equivalence problem, the determinizability problem, the complementability problem, and theunambiguity problem are all Π½ -complete for context-free ω-languages or for infinitary rational relations. Topological and arithmetical properties of1-counter ω-languages, context free ω-languages, or infinitary rational relations, are also highly undecidable.These very surprising results provide the first examples of highly undecidable problems about the behaviour of verysimple finite machines like 1-counter automata or 2-tapeautomata.

The specification of the data structures used in EAT, a software system for symbolic computation in algebraic topology, is based on an operation that defines a link among different specification frameworks like hidden algebras and coalgebras. In this paper, this operation is extended using the notion of institution, giving rise to three institution encodings. These morphisms define a commutative diagram which shows three possible views of the same construction, placing it in an equational algebraic institution, in a hidden institution or in a coalgebraic institution. Moreover, these morphisms can be used to obtain a new description of the final objects of the categories of algebras in these frameworks, which are suitable abstract models for the EAT data structures. Thus, our main contribution is a formalization allowing us to encode a family of data structures by means of a single algebra (which can be described as a coproduct on the image of the institution morphisms). With this aim, new particular definitions of hidden and coalgebraic institutions are presented.

String rewriting reductions of the form $t\to_R^+ utv$ , called loops, are the most frequent cause of infinite reductions (non-termination). Regarded as a model of computation, infinite reductions are unwanted whence their static detection is important. There are string rewriting systems which admit infinite reductions although they admit no loops. Their non-termination is particularly difficult to uncover. We present a few necessary conditions for the existence of loops, and thus establish a means to recognize the difficult case. We show in detail four relevant criteria: (i) the existence of loops is characterized by the existence of looping forward closures; (ii) dummy elimination, a non-termination preserving transformation method, also preserves the existence of loops; (iii) dummy introduction, a transformation method that supports subsequent dummy elimination, likewise preserves loops; (iv) bordered systems can be reduced to smaller systems on a larger alphabet, preserving the existence and the non-existence of loops. We illustrate the power of the four methods by giving a two-rule string rewriting system over a two-letter alphabet which admits an infinite reduction but no loop. So far, the least known such system had three rules.

In our main result, we establish a formal connection between Lindström quantifiers with respect to regular languages and the double semidirect product of finite monoids with a distinguished set of generators. We use this correspondence to characterize the expressive power of Lindström quantifiers associated with a class of regular languages.

We consider numeration systems where the base is anegative integer, or a complex number which is a root of anegative integer.We give parallel algorithms for addition in these numeration systems,from which we derive on-line algorithms realized by finite automata. A general construction relating addition in base βand addition in base βm is given.Results on addition in base $\beta=\sqrt[m]{b}$ , where b is a relative integer, follow.We also show that addition in base the golden ratiois computable by an on-line finite automaton, but is notparallelizable.

We initiate the theory and applications of biautomata. A biautomaton can read a word alternately from the left and from the right. We assign to each regular language L its canonical biautomaton. This structure plays, among all biautomata recognizing the language L, the same role as the minimal deterministic automaton has among all deterministic automata recognizing the language L. We expect that from the graph structure of this automaton one could decide the membership of a given language for certain significant classes of languages. We present the first two results of this kind: namely, a language L is piecewise testable if and only if the canonical biautomaton of L is acyclic. From this result Simon’s famous characterization of piecewise testable languages easily follows. The second class of languages characterizable by the graph structure of their biautomata are prefix-suffix testable languages.

In the paper we study abelian versions of the critical factorization theorem. We investigate both similarities and differences between the abelian powers and the usual powers. The results we obtained show that the constraints for abelian powers implying periodicity should be quite strong, but still natural analogies exist.

This paper offers characteristic formula constructions in the real-time logic Lν for several behavioural relations between (states of) timed automata. The behavioural relations studied in this work are timed (bi)similarity, timed ready simulation, faster-than bisimilarity and timed trace inclusion. The characteristic formulae delivered by our constructions have size which is linear in that of the timed automaton they logically describe. This also applies to the characteristic formula for timed bisimulation equivalence, for which an exponential space construction was previously offered by Laroussinie, Larsen and Weise.