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 $\alpha$ can we decide whether a given B\"uchi automaton $A$ accepts $\alpha$? Carton and Thomas showed decidability in case $\alpha$ is a fixed point of a letter-to-word substitution $\sigma$, i.e., $\sigma(\alpha) = \alpha$. 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 $\alpha$ is said to be directed by a sequence $s = (\sigma_n)_{n \in \mathbb{N}}$ over $S$ if there is a sequence of words $(\alpha_n)_{n \in \mathbb{N}}$ such that $\alpha_0 = \alpha$ and $\alpha_n = \sigma_n(\alpha_{n+1})$ for all $n$; such $\alpha$ 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^\omega$ if and only if $s$ directs a word $\alpha$ accepted by $A$. Thus we can algorithmically answer questions of the form "Which $S$-adic words are accepted by a given automaton $A$?"