The Monadic Theory of Morphic Infinite Words and Generalizations

  • Olivier Carton
  • Wolfgang Thomas
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1893)


We present new examples of infinite words which have a decidable monadic theory. Formally, we consider structures 〈ℕ,<P〉 which expand the ordering 〈ℕ,<〉 of the natural numbers by a unary predicate P; the corresponding infinite word is the characteristic 0-1-sequence xP of P. We show that for a morphic predicate P the associated monadic second-order theory MThhℕ,<P〉 is decidable, thus extending results of Elgot and Rabin (1966) and Maes (1999). The solution is obtained in the framework of semigroup theory, which is then connected to the known automata theoretic approach of Elgot and Rabin. Finally, a large class of predicates P is exhibited such that the monadic theory MTh〈ℕ〈, P〉 is decidable, which unifies and extends the previously known examples.


Decision Problem Fibonacci Number Characteristic Word Unary Predicate Contraction Method 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    Jorge Almeida. Finite Semigroups and Universal Algebra. World Scientific, 1994.Google Scholar
  2. [2]
    Frédérique Bassino, Marie-Pierre Béal, and Dominique Perrin. Length distributions and regular sequences. Technical report, IGM, 2000.Google Scholar
  3. [3]
    P. T. Bateman, C. G. Jockusch, and A. R. Woods. Decidability and undecidibility of theories of with a predicate for the primes. J. Symb. Logic, 58:672–687, 1993.zbMATHCrossRefMathSciNetGoogle Scholar
  4. [4]
    Jean Berstel. Axel Thue’s work on repetitions in words. In P. Leroux and C. Reutenauer, editors, Séries formelles et combinatoire algébrique, pages 65–80. Publications du LaCIM, Université du Québec á Montréal, 1990.Google Scholar
  5. [5]
    Jean Berstel and Patrice Séébold. Algebraic Combinatorics on Words, chapter 2, pages 40–96. Cambridge University Press, 2000.Google Scholar
  6. [6]
    J. Richard Büchi. On a decision method in the restricted second-order arithmetic. In Proc. Int. Congress Logic, Methodology and Philosophy of science, Berkeley 1960, pages 1–14. Stanford University Press, 1962.Google Scholar
  7. [7]
    J. Richard Büchi and L. H. Landweber. Definability in the monadic second-order theory of successor. J. Symb. Logic, 31:169–181, 1966.CrossRefGoogle Scholar
  8. [8]
    Calvin C. Elgot and Micheal O. Rabin. Decidability and undecidibility of extensions of second (first) order theory of (generalized) successor. J. Symb. Logic, 31(2):169–181, 1966.zbMATHCrossRefGoogle Scholar
  9. [9]
    F. A. Hosch. Decision Problems in Büchi’s Sequential Calculus. Dissertation, University of New Orleans, Louisiana, 1971.Google Scholar
  10. [10]
    Arnaud Maes. An automata theoretic decidability proof for the first-order theory of 〈ℕ〈, P〉 with morphic predicate P. Journal of Automata, Languages and Combinatorics, 4:229–245, 1999.zbMATHMathSciNetGoogle Scholar
  11. [11]
    C. Michaux and R. Villemaire. Open questions around Büchi and presburger arithmetics. In Wilfrid Hodges et al., editors, Logic: from foundations to applications. European logic colloquium, pages 353–383, Oxford, 1996. Clarendon Press.Google Scholar
  12. [12]
    Arto Salomaa and Matti Soittola. Automata-Theoric Aspects of Formal Power Series. Springer-Verlag, New York, 1978.Google Scholar
  13. [13]
    D. Siefkes. Decidable extensions of monadic second order successor arithmetic. In J. Doerr and G. Hotz, editors, Automatentheorie und Formale Sprachen, pages 441–472, Mannheim, 1970. B.I. Hochschultaschenbücher.Google Scholar
  14. [14]
    Wolfgang Thomas. The theory of successor with an extra predicate. Math. Ann., 237 (121–132), 1978.zbMATHCrossRefMathSciNetGoogle Scholar
  15. [15]
    Wolfgang Thomas. On the bounded monadic theory of well-ordered structures. J. Symb. Logic, 45:334–338, 1980.zbMATHCrossRefGoogle Scholar
  16. [16]
    Wolfgang Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, chapter 4, pages 133–191. Elsevier, 1990.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • Olivier Carton
    • 1
  • Wolfgang Thomas
    • 2
  1. 1.Institut Gaspard Monge and CNRSUniversité de Marne-la-ValléeMarne-la-Vallée Cedex 2France
  2. 2.Lehrstuhl für Informatik VIIAachenGermany

Personalised recommendations