2025/06/20 by Berthé, Valérie, Karimov, Toghrul, Vahanwala, Mihir
#FOS: Computer and information sciences #Formal Languages and Automata Theory (cs.FL) #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.2506.17460
A fundamental question in logic and verification is the following: for which unary predicates P1, …, Pk is the monadic second-order theory of ⟨ ℕ; <, P1, …, Pk ⟩ 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 ∈ ℕ over S if there is a sequence of words (αn)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 ∈ 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?"