Automata on S-Adic Words

Abstract

A fundamental question in logic and verification is the following: for which unary predicates P_1, …, P_k is the monadic second-order theory of ⟨ℕ;<,P_1,…,P_k⟩ decidable? Equivalently, for which infinite words α can we decide whether a given Büchi automaton 𝒜 accepts α? Carton and Thomas showed decidability in the case that α 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 involves a set S of substitutions. A word α is said to be directed by a sequence s = (σ_n)_{n ∈ ℕ} over S if there is a sequence of words (α_n)_{n ∈ ℕ} such that α₀ = α and α_n = σ_n(α_{n+1}) for all n; such α are called S-adic. We study the automaton acceptance problem for such words and prove, among others, the following: given finite S and an automaton 𝒜, we can compute an automaton ℬ that accepts s ∈ S^ω if and only if s directs a word α accepted by 𝒜. Thus we can algorithmically answer questions of the form "Which S-adic words are accepted by a given automaton 𝒜?"