Automata on $S$-adic words

Abstract

A fundamental question in logic and verification is the following: for which unary predicates $P_1, \ldots, P_k$ is the monadic second-order theory of $\langle \mathbb{N}; <, P_1, \ldots, P_k \rangle$ decidable? Equivalently, for which infinite words $α$ can we decide whether a given Büchi automaton $A$ accepts $α$? Carton and Thomas showed decidability in case $α$ is a fixed point of a letter-to-word substitution $σ$, i.e., $σ(α) = α$. However, abundantly more words, e.g., Sturmian words, are characterised by a broader notion of self-similarity that uses a set $S$ of substitutions. A word $α$ is said to be directed by a sequence $s = (σ_n)_{n \in \mathbb{N}}$ over $S$ if there is a sequence of words $(α_n)_{n \in \mathbb{N}}$ such that $α_0 = α$ and $α_n = σ_n(α_{n+1})$ for all $n$; such $α$ is called $S$-adic. We study the automaton acceptance problem for such words and prove, among others, the following. Given finite $S$ and an automaton $A$, we can compute an automaton $B$ that accepts $s \in S^ω$ if and only if $s$ directs a word $α$ accepted by $A$. Thus we can algorithmically answer questions of the form "Which $S$-adic words are accepted by a given automaton $A$?"