Please note: This master’s thesis presentation will take place online.
Mazen Khodier, Master’s candidate
David R. Cheriton School of Computer Science
Supervisor: Professor Jeffrey Shallit
Automatic sequences and morphic words lie at the intersection of automata theory, logic, and combinatorics on words. Many of their structural properties can be formulated as logical predicates over integer representations and decided using automata. This thesis presents automata-based methods for efficiently constructing and verifying deterministic finite automata corresponding to such predicates, and builds on this foundation to analyze key combinatorial properties of morphic words, including the critical exponent and subword complexity.
In the first part of this thesis, Chapters 2 to 4, we introduce the notion of self-verifying predicates, which are logical predicates capable of verifying their own correctness. We show how this property enables verification of candidate automata through a small set of inductive conditions and allows the corresponding automata to be constructed deterministically rather than through heuristic guessing. Building on Angluin’s L∗ learning algorithm, we demonstrate that for such predicates, the associated minimal automata can be generated in time polynomial in the size of both the automaton for the underlying sequence and the resulting automaton, thereby avoiding potentially extremely large intermediate automata that sometimes arise in Walnut. In particular, we give effective constructions for the equality-of-factors predicate, which is used extensively in the second half of the thesis, as well as for other self-verifying predicates, including periodicity of factors, addition relations for numeration systems, and summation of synchronized sequences.
The second part, Chapters 5 to 7, applies the previously constructed equality-of-factors predicate to investigate two central combinatorial measures of infinite words: the critical exponent and the subword complexity. Although binary 3-uniform morphisms are used as illustrative examples, the methods generalize naturally to all binary uniform morphisms. For the critical exponent, we present a decision procedure implemented in Walnut that detects whether the exponent is infinite and computes its exact rational value when finite. For subword complexity, we propose two complementary approaches: a constructive method that combines established concepts to produce exact formulas for ρ(n), and a fully deterministic procedure that implements Frid’s approach using Walnut. The new results include explicit subword-complexity formulas for twelve morphisms, and critical-exponent values for ten morphisms.
All algorithms and implementations developed in this thesis are made publicly available on the Github repository Cashew as open-source code to support and facilitate further research in combinatorics on words, and automata theory.