We investigate automatic presentations of -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 -words enjoying the above mentioned definability and decidability properties. We introduce -lexicographic presentations, and morphisms of level stacks and show that these are inter-translatable, thus giving rise to the same classes of -lexicographic or level morphic words. We prove that these presentations are also canonical, which implies decidability of the MSO theory of every -lexicographic word as well as closure of these classes under MSO-definable recolorings, e.g. closure under deterministic sequential mappings. The classes of -lexicographic words are shown to constitute an infinite hierarchy.
@article{ITA_2008__42_3_417_0,
author = {B\'ar\'any, Vince},
title = {A hierarchy of automatic $\omega $-words having a decidable MSO theory},
journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
volume = {42},
year = {2008},
pages = {417-450},
doi = {10.1051/ita:2008008},
mrnumber = {2434027},
zbl = {1152.03030},
language = {en},
url = {http://dml.mathdoc.fr/item/ITA_2008__42_3_417_0}
}
Bárány, Vince. A hierarchy of automatic $\omega $-words having a decidable MSO theory. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 42 (2008) pp. 417-450. doi : 10.1051/ita:2008008. http://gdmltest.u-ga.fr/item/ITA_2008__42_3_417_0/
[1] and , Automatic Sequences, Theory, Applications, Generalizations. Cambridge University Press (2003). | MR 1997038 | Zbl 1086.11015
[2] and , Iterated GSMs and Co-CFL. Acta Informatica 26, 749-769 (1989). | MR 1021789 | Zbl 0659.68097
[3] , Invariants of automatic presentations and semi-synchronous transductions. In STACS '06. Lect. Notes Comput. Sci. 3884, 289 (2006). | MR 2249377 | Zbl 1136.68413
[4] , Automatic Presentations of Infinite Structures. Ph.D. thesis, RWTH Aachen (2007).
[5] , Transductions and Context-Free Languages. Teubner, Stuttgart (1979). | MR 549481 | Zbl 0424.68040
[6] and , The monadic theory of tree-like structures. In Automata, Logics, and Infinite Games. Lect. Notes Comput. Sci. 2500, 285-301 (2002). | MR 2070747 | Zbl 1021.68051
[7] , Undecidable extensions of Büchi arithmetic and Cobham-Semënov theorem. Journal of Symbolic Logic 62, 1280-1296 (1997). | MR 1617949 | Zbl 0896.03011
[8] , Automatic Structures. Diploma thesis, RWTH-Aachen (1999).
[9] , Axiomatising Tree-interpretable Structures. In STACS. Lect. Notes Comput. Sci. 2285, 596-607 (2002). | MR 2050871 | Zbl 1054.03025
[10] and , Finite presentations of infinite structures: Automata and interpretations. Theor. Comput. Syst. 37, 641-674 (2004). | MR 2093606 | Zbl 1061.03038
[11] , Higher-order schemes and morphic words. Journées Montoises, Rennes (2006).
[12] and , Bertrand numeration systems and recognizability. Theoretical Computer Science 181, 17-43 (1997). | MR 1463527 | Zbl 0957.11015
[13] , , and , Logic and p-recognizable sets of integers. Bull. Belg. Math. Soc. Simon Stevin 1, 191-238 (1994). | MR 1318968 | Zbl 0804.11024
[14] , , , , and , Word processing in groups. Jones and Barlett Publ., Boston, MA (1992). | MR 1161694 | Zbl 0764.20017
[15] and , Context-sensitive languages, rational graphs and determinism (2005). | MR 2295771 | Zbl 1126.68049
[16] and , 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 2093642
[17] and , The monadic theory of morphic infinite words and generalizations. Information and Computation 176, 51-65 (2002). | MR 1915839 | Zbl 1012.03015
[18] , Monadic theory of term rewritings. In LICS, pp. 266-273. IEEE Computer Society (1992).
[19] , On infinite transition graphs having a decidable monadic theory. In ICALP'96. Lect. Notes Comput. Sci. 1099, 194-205 (1996). | MR 1464449 | Zbl 1045.03509
[20] , On infinite terms having a decidable monadic theory. In MFCS, pp. 165-176 (2002). | MR 2064455 | Zbl 1014.68077
[21] , A combinatorial theorem for trees. In ICALP'07. Lect. Notes Comput. Sci. 4596, 901-912 (2007). | MR 2424741 | Zbl pre05215625
[22] , On factorisation forests and some applications. arXiv:cs.LO/0701113v1 (2007).
[23] , The monadic second-order logic of graphs ix: Machines and their behaviours. Theoretical Computer Science 151, 125-162 (1995). | MR 1362151 | Zbl 0872.03026
[24] and , Monadic second-order logic, graph coverings and unfoldings of transition systems. Annals of Pure and Applied Logic 92, 35-62 (1998). | MR 1624811 | Zbl 0929.03036
[25] and , Decidability and undecidability of extensions of second (first) order theory of (generalized) successor. Journal of Symbolic Logic 31, 169-181 (1966). | Zbl 0144.24501
[26] and , Iterated pushdown automata and sequences of rational numbers. Annals of Pure and Applied Logic 141, 363-411, (2006). | MR 2234704 | Zbl 1106.03036
[27] and , Synchronized rational relations of finite and infinite words. Theoretical Computer Science 108, 45-82 (1993). | MR 1203822 | Zbl 0783.68065
[28] E. Grädel, W. Thomas and T. Wilke, Eds. Automata, Logics, and Infinite Games. Lect. Notes Comput. Sci. 2500, (2002). | Zbl 1011.00037
[29] , Décidabilité par automate fini. Ann. Sci. Math. Québec 7, 39-57 (1983). | MR 699985 | Zbl 0531.03007
[30] and , A note on decidability questions related to abstract numeration systems. Discrete Math. 285, 329-333 (2004). | MR 2062858 | Zbl 1076.68040
[31] and , Iterative devices generating infinite words. In STACS '92. Lect. Notes Comput. Sci. 577, 529-543 (1992).
[32] , and , L systems. In Handbook of Formal Languages, G. Rozenberg and A. Salomaa Eds., volume I, pp. 253-328. Springer, New York (1997). | MR 1469997 | Zbl 0281.00016
[33] and , Automatic presentations of structures. In LCC '94. Lect. Notes Comput. Sci. 960, 367-392 (1995). | MR 1449670
[34] and , Automatic structures: Overview and future directions. J. Autom. Lang. Comb. 8, 287-301 (2003). | MR 2000619 | Zbl 1058.68070
[35] , and , Definability and regularity in automatic structures. In STACS '04. Lect. Notes Comput. Sci. 2996, 440-451 (2004). | MR 2093979 | Zbl 1122.68466
[36] , Prédicats algébriques d'entiers. Rapport de stage, IRISA: Galion (2005).
[37] , Automatic Graph and D0L-Sequences of Finite Graphs. Journal of Computer and System Sciences 67, 497-545 (2003). | MR 2011476 | Zbl 1114.68048
[38] , An automata theoretic decidability proof for first-order theory of with morphic predicate . J. Autom. Lang. Comb. 4, 229-245 (1999). | MR 1719367 | Zbl 0937.68078
[39] and , Families of automata characterizing context-sensitive languages. Acta Informatica 41, 293-314 (2005). | MR 2129796 | Zbl 1067.68086
[40] and , The theory of ends, pushdown automata, and second-order logic. Theor. Comput. Sci. 37, 51-75 (1985). | MR 796313 | Zbl 0605.03005
[41] , On various classes of infinite words obtained by iterated mappings. In Automata on Infinite Words, pp. 188-197 (1984). | MR 814743 | Zbl 0571.68065
[42] and , A topological approach to transductions. Theoretical Computer Science 340, 443-456 (2005). | MR 2150765 | Zbl 1078.68093
[43] , On decidability of monadic logic of order over the naturals extended by monadic predicates. Unpublished note (2005).
[44] and , Decidable theories of the ordering of natural numbers with unary predicates. In CSL 2006. Lect. Notes Comput. Sci. 4207, 562-574 (2006). | MR 2334448 | Zbl pre05528232
[45] and , More on generalized automatic sequences. J. Autom. Lang. Comb. 7, 351-376 (2002). | MR 1957696 | Zbl 1033.68069
[46] , The synchronized graphs trace the context-sensistive languages. Elect. Notes Theoret. Comput. Sci. 68 (2002).
[47] and , The Book of L. Springer Verlag (1986). | Zbl 0575.00023
[48] , Automatic Structures. Ph.D. thesis, University of Auckland, NZ (2004).
[49] , Automata presenting structures: A survey of the finite-string case. Manuscript.
[50] , Sequences of level 1, 2, 3,..., k,... In CSR'07. Lect. Notes Comput. Sci. 4649, 24-32 (2007). | Zbl pre05282044
[51] , The monadic theory of order. Annals of Mathematics 102, 379-419 (1975). | MR 491120 | Zbl 0345.02034
[52] , Rich omega-words and monadic second-order arithmetic. In CSL, pp. 478-490 (1997). | MR 1727827 | Zbl 0914.03058
[53] , 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 1470024
[54] , Constructing infinite graphs with a decidable mso-theory. In MFCS'03. Lect. Notes Comput. Sci. 2747, 113-124 (2003). | MR 2081322 | Zbl 1124.03314
[55] , Monadic second-order logic on tree-like structures. Theoretical Computer Science 275, 311-346 (2002). | MR 1902097 | Zbl 1026.68087