A hierarchy of automatic $\omega$-words having a decidable MSO theory

Bárány, Vince

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 42 (2008) no. 3, pp. 417-450.

We investigate automatic presentations of $\omega$-words. Starting points of our study are the works of Rigo and Maes, Caucal, and Carton and Thomas concerning lexicographic presentation, MSO-interpretability in algebraic trees, and the decidability of the MSO theory of morphic words. Refining their techniques we observe that the lexicographic presentation of a (morphic) word is in a certain sense canonical. We then generalize our techniques to a hierarchy of classes of $\omega$-words enjoying the above mentioned definability and decidability properties. We introduce $k$-lexicographic presentations, and morphisms of level $k$ stacks and show that these are inter-translatable, thus giving rise to the same classes of $k$-lexicographic or level $k$ morphic words. We prove that these presentations are also canonical, which implies decidability of the MSO theory of every $k$-lexicographic word as well as closure of these classes under MSO-definable recolorings, e.g. closure under deterministic sequential mappings. The classes of $k$-lexicographic words are shown to constitute an infinite hierarchy.

Classification : 03D05, 68Q42, 68Q45, 68R15
Mots clés : morphic words, monadic second-order logic, automatic structures, automatic sequences

[1] J.-P. Allouche and J. Shallit, Automatic Sequences, Theory, Applications, Generalizations. Cambridge University Press (2003). | MR | Zbl

[2] J.-M. Autebert and J. Gabarró, Iterated GSMs and Co-CFL. Acta Informatica 26, 749-769 (1989). | MR | Zbl

[3] V. Bárány, Invariants of automatic presentations and semi-synchronous transductions. In STACS '06. Lect. Notes Comput. Sci. 3884, 289 (2006). | MR | Zbl

[4] V. Bárány, Automatic Presentations of Infinite Structures. Ph.D. thesis, RWTH Aachen (2007).

[5] J. Berstel, Transductions and Context-Free Languages. Teubner, Stuttgart (1979). | MR | Zbl

[6] D. Berwanger and A. Blumensath, The monadic theory of tree-like structures. In Automata, Logics, and Infinite Games. Lect. Notes Comput. Sci. 2500, 285-301 (2002). | MR | Zbl

[7] A. Bès, Undecidable extensions of Büchi arithmetic and Cobham-Semënov theorem. Journal of Symbolic Logic 62, 1280-1296 (1997). | MR | Zbl

[8] A. Blumensath, Automatic Structures. Diploma thesis, RWTH-Aachen (1999).

[9] A. Blumensath, Axiomatising Tree-interpretable Structures. In STACS. Lect. Notes Comput. Sci. 2285, 596-607 (2002). | MR | Zbl

[10] A. Blumensath and E. Grädel, Finite presentations of infinite structures: Automata and interpretations. Theor. Comput. Syst. 37, 641-674 (2004). | MR | Zbl

[11] L. Braud, Higher-order schemes and morphic words. Journées Montoises, Rennes (2006).

[12] V. Bruyère and G. Hansel, Bertrand numeration systems and recognizability. Theoretical Computer Science 181, 17-43 (1997). | MR | Zbl

[13] V. Bruyère, G. Hansel, Ch. Michaux and R. Villemaire, Logic and p-recognizable sets of integers. Bull. Belg. Math. Soc. Simon Stevin 1, 191-238 (1994). | MR | Zbl

[14] J.W. Cannon, D.B.A. Epstein, D.F. Holt, S.V.F. Levy, M.S. Paterson and W.P. Thurston, Word processing in groups. Jones and Barlett Publ., Boston, MA (1992). | MR | Zbl

[15] A. Carayol and A. Meyer, Context-sensitive languages, rational graphs and determinism (2005). | MR | Zbl

[16] A. Carayol and S. Wöhrle, The Caucal hierarchy of infinite graphs in terms of logic and higher-order pushdown automata. In FSTTCS. Lect. Notes Comput. Sci. 2914, 112-123 (2003). | MR

[17] O. Carton and W. Thomas, The monadic theory of morphic infinite words and generalizations. Information and Computation 176, 51-65 (2002). | MR | Zbl

[18] D. Caucal, Monadic theory of term rewritings. In LICS, pp. 266-273. IEEE Computer Society (1992).

[19] D. Caucal, On infinite transition graphs having a decidable monadic theory. In ICALP'96. Lect. Notes Comput. Sci. 1099, 194-205 (1996). | MR | Zbl

[20] D. Caucal, On infinite terms having a decidable monadic theory. In MFCS, pp. 165-176 (2002). | MR | Zbl

[21] Th. Colcombet, A combinatorial theorem for trees. In ICALP'07. Lect. Notes Comput. Sci. 4596, 901-912 (2007). | MR

[22] Th. Colcombet, On factorisation forests and some applications. arXiv:cs.LO/0701113v1 (2007).

[23] B. Courcelle, The monadic second-order logic of graphs ix: Machines and their behaviours. Theoretical Computer Science 151, 125-162 (1995). | MR | Zbl

[24] B. Courcelle and I. Walukiewicz, Monadic second-order logic, graph coverings and unfoldings of transition systems. Annals of Pure and Applied Logic 92, 35-62 (1998). | MR | Zbl

[25] C.C. Elgot and M.O. Rabin, Decidability and undecidability of extensions of second (first) order theory of (generalized) successor. Journal of Symbolic Logic 31, 169-181 (1966). | Zbl

[26] S. Fratani and G. Sénizergues, Iterated pushdown automata and sequences of rational numbers. Annals of Pure and Applied Logic 141, 363-411, (2006). | MR | Zbl

[27] Ch. Frougny and J. Sakarovitch, Synchronized rational relations of finite and infinite words. Theoretical Computer Science 108, 45-82 (1993). | MR | Zbl

[28] E. Grädel, W. Thomas and T. Wilke, Eds. Automata, Logics, and Infinite Games. Lect. Notes Comput. Sci. 2500, (2002). | Zbl

[29] B.R. Hodgson, Décidabilité par automate fini. Ann. Sci. Math. Québec 7, 39-57 (1983). | MR | Zbl

[30] J. Honkala and M. Rigo, A note on decidability questions related to abstract numeration systems. Discrete Math. 285, 329-333 (2004). | MR | Zbl

[31] K. Culik Ii and J. Karhumäki, Iterative devices generating infinite words. In STACS '92. Lect. Notes Comput. Sci. 577, 529-543 (1992).

[32] L. Kari, G. Rozenberg and A. Salomaa, L systems. In Handbook of Formal Languages, G. Rozenberg and A. Salomaa Eds., volume I, pp. 253-328. Springer, New York (1997). | MR | Zbl

[33] B. Khoussainov and A. Nerode, Automatic presentations of structures. In LCC '94. Lect. Notes Comput. Sci. 960, 367-392 (1995). | MR

[34] B. Khoussainov and S. Rubin, Automatic structures: Overview and future directions. J. Autom. Lang. Comb. 8, 287-301 (2003). | MR | Zbl

[35] B. Khoussainov, S. Rubin and F. Stephan, Definability and regularity in automatic structures. In STACS '04. Lect. Notes Comput. Sci. 2996, 440-451 (2004). | MR | Zbl

[36] T. Lavergne, Prédicats algébriques d'entiers. Rapport de stage, IRISA: Galion (2005).

[37] O. Ly, Automatic Graph and D0L-Sequences of Finite Graphs. Journal of Computer and System Sciences 67, 497-545 (2003). | MR | Zbl

[38] A. Maes, An automata theoretic decidability proof for first-order theory of $\langle \mathbb{N},<,P\rangle$ with morphic predicate $P$. J. Autom. Lang. Comb. 4, 229-245 (1999). | MR | Zbl

[39] Ch. Morvan and Ch. Rispal, Families of automata characterizing context-sensitive languages. Acta Informatica 41, 293-314 (2005). | MR | Zbl

[40] D.E. Muller and P.E. Schupp, The theory of ends, pushdown automata, and second-order logic. Theor. Comput. Sci. 37, 51-75 (1985). | MR | Zbl

[41] J.-J. Pansiot, On various classes of infinite words obtained by iterated mappings. In Automata on Infinite Words, pp. 188-197 (1984). | MR | Zbl

[42] J.-E. Pin and P.V. Silva, A topological approach to transductions. Theoretical Computer Science 340, 443-456 (2005). | MR | Zbl

[43] A. Rabinovich, On decidability of monadic logic of order over the naturals extended by monadic predicates. Unpublished note (2005).

[44] A. Rabinovich and W. Thomas, Decidable theories of the ordering of natural numbers with unary predicates. In CSL 2006. Lect. Notes Comput. Sci. 4207, 562-574 (2006). | MR

[45] M. Rigo and A. Maes, More on generalized automatic sequences. J. Autom. Lang. Comb. 7, 351-376 (2002). | MR | Zbl

[46] Ch. Rispal, The synchronized graphs trace the context-sensistive languages. Elect. Notes Theoret. Comput. Sci. 68 (2002).

[47] G. Rozenberg and A. Salomaa, The Book of L. Springer Verlag (1986). | Zbl

[48] S. Rubin, Automatic Structures. Ph.D. thesis, University of Auckland, NZ (2004).

[49] S. Rubin, Automata presenting structures: A survey of the finite-string case. Manuscript.

[50] G. Sénizergues, Sequences of level 1, 2, 3,..., k,... In CSR'07. Lect. Notes Comput. Sci. 4649, 24-32 (2007).

[51] S. Shelah, The monadic theory of order. Annals of Mathematics 102, 379-419 (1975). | MR | Zbl

[52] L. Staiger, Rich omega-words and monadic second-order arithmetic. In CSL, pp. 478-490 (1997). | MR | Zbl

[53] W. Thomas, Languages, automata, and logic. In Handbook of Formal Languages, G. Rozenberg and A. Salomaa, Eds., Vol. III, pp. 389-455. Springer, New York (1997). | MR

[54] W. Thomas, Constructing infinite graphs with a decidable mso-theory. In MFCS'03. Lect. Notes Comput. Sci. 2747, 113-124 (2003). | MR | Zbl

[55] I. Walukiewicz, Monadic second-order logic on tree-like structures. Theoretical Computer Science 275, 311-346 (2002). | MR | Zbl