Hostname: page-component-586b7cd67f-t7fkt Total loading time: 0 Render date: 2024-11-24T12:02:49.477Z Has data issue: false hasContentIssue false
  • English
  • Français

A Hierarchy of Automatic ω-Words having a Decidable MSO Theory

Published online by Cambridge University Press:  03 June 2008

Vince Bárány
Vince Bárány*
Affiliation:
Mathematische Grundlagen der Informatik, RWTH Aachen, Aachen, Germany; [email protected]
Get access

Abstract

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 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.

Keywords

Morphic wordsmonadic second-order logicautomatic structuresautomatic sequences.
Type
Research Article
Information
RAIRO - Theoretical Informatics and Applications , Volume 42 , Issue 3: JM'06 , July 2008 , pp. 417 - 450
Copyright
© EDP Sciences, 2008

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

J.-P. Allouche and J. Shallit, Automatic Sequences, Theory, Applications, Generalizations. Cambridge University Press (2003).
J.-M. Autebert and J. Gabarró, Iterated GSMs and Co-CFL. Acta Informatica 26, 749–769 (1989).
V. Bárány, Invariants of automatic presentations and semi-synchronous transductions. In STACS '06. Lect. Notes Comput. Sci. 3884, 289 (2006).
V. Bárány, Automatic Presentations of Infinite Structures. Ph.D. thesis, RWTH Aachen (2007).
J. Berstel, Transductions and Context-Free Languages. Teubner, Stuttgart (1979).
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).
A. Bès, Undecidable extensions of Büchi arithmetic and Cobham-Semënov theorem. Journal of Symbolic Logic 62, 1280–1296 (1997).
A. Blumensath, Automatic Structures. Diploma thesis, RWTH-Aachen (1999).
A. Blumensath, Axiomatising Tree-interpretable Structures. In STACS. Lect. Notes Comput. Sci. 2285, 596–607 (2002). CrossRef
A. Blumensath and E. Grädel, Finite presentations of infinite structures: Automata and interpretations. Theor. Comput. Syst. 37, 641–674 (2004).
L. Braud, Higher-order schemes and morphic words. Journées Montoises, Rennes (2006).
V. Bruyère and G. Hansel, Bertrand numeration systems and recognizability. Theoretical Computer Science 181, 17–43 (1997).
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).
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).
A. Carayol and A. Meyer, Context-sensitive languages, rational graphs and determinism (2005).
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).
O. Carton and W. Thomas, The monadic theory of morphic infinite words and generalizations. Information and Computation 176, 51–65 (2002).
D. Caucal, Monadic theory of term rewritings. In LICS, pp. 266–273. IEEE Computer Society (1992).
D. Caucal, On infinite transition graphs having a decidable monadic theory. In ICALP'96. Lect. Notes Comput. Sci. 1099, 194–205 (1996).
D. Caucal, On infinite terms having a decidable monadic theory. In MFCS, pp. 165–176 (2002).
Th. Colcombet, A combinatorial theorem for trees. In ICALP'07. Lect. Notes Comput. Sci. 4596, 901–912 (2007).
Th. Colcombet, On factorisation forests and some applications. arXiv:cs.LO/0701113v1 (2007).
B. Courcelle, The monadic second-order logic of graphs ix: Machines and their behaviours. Theoretical Computer Science 151, 125–162 (1995).
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).
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).
S. Fratani and G. Sénizergues, Iterated pushdown automata and sequences of rational numbers. Annals of Pure and Applied Logic 141, 363–411, (2006).
Ch. Frougny and J. Sakarovitch, Synchronized rational relations of finite and infinite words. Theoretical Computer Science 108, 45–82 (1993).
E. Grädel, W. Thomas and T. Wilke, Eds. Automata, Logics, and Infinite Games. Lect. Notes Comput. Sci. 2500, (2002).
B.R. Hodgson, Décidabilité par automate fini. Ann. Sci. Math. Québec 7, 39–57 (1983).
J. Honkala and M. Rigo, A note on decidability questions related to abstract numeration systems. Discrete Math. 285, 329–333 (2004).
K. Culik II and J. Karhumäki, Iterative devices generating infinite words. In STACS '92. Lect. Notes Comput. Sci. 577, 529–543 (1992).
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).
B. Khoussainov and A. Nerode, Automatic presentations of structures. In LCC '94. Lect. Notes Comput. Sci. 960, 367–392 (1995).
B. Khoussainov and S. Rubin, Automatic structures: Overview and future directions. J. Autom. Lang. Comb. 8, 287–301 (2003).
B. Khoussainov, S. Rubin and F. Stephan, Definability and regularity in automatic structures. In STACS '04. Lect. Notes Comput. Sci. 2996, 440–451 (2004).
T. Lavergne, Prédicats algébriques d'entiers. Rapport de stage, IRISA: Galion (2005).
O. Ly, Automatic Graph and D0L-Sequences of Finite Graphs. Journal of Computer and System Sciences 67, 497–545 (2003).
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).
Ch. Morvan and Ch. Rispal, Families of automata characterizing context-sensitive languages. Acta Informatica 41, 293–314 (2005).
D.E. Muller and P.E. Schupp, The theory of ends, pushdown automata, and second-order logic. Theor. Comput. Sci. 37, 51–75 (1985).
J.-J. Pansiot, On various classes of infinite words obtained by iterated mappings. In Automata on Infinite Words, pp. 188–197 (1984).
J.-E. Pin and P.V. Silva, A topological approach to transductions. Theoretical Computer Science 340, 443–456 (2005).
A. Rabinovich, On decidability of monadic logic of order over the naturals extended by monadic predicates. Unpublished note (2005).
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).
M. Rigo and A. Maes, More on generalized automatic sequences. J. Autom. Lang. Comb. 7, 351–376 (2002).
Ch. Rispal, The synchronized graphs trace the context-sensistive languages. Elect. Notes Theoret. Comput. Sci. 68 (2002).
G. Rozenberg and A. Salomaa, The Book of L. Springer Verlag (1986).
S. Rubin, Automatic Structures. Ph.D. thesis, University of Auckland, NZ (2004).
S. Rubin, Automata presenting structures: A survey of the finite-string case. Manuscript.
G. Sénizergues, Sequences of level 1, 2, 3,..., k,... In CSR'07. Lect. Notes Comput. Sci. 4649, 24–32 (2007).
S. Shelah, The monadic theory of order. Annals of Mathematics 102, 379–419 (1975).
L. Staiger, Rich omega-words and monadic second-order arithmetic. In CSL, pp. 478–490 (1997).
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).
W. Thomas, Constructing infinite graphs with a decidable mso-theory. In MFCS'03. Lect. Notes Comput. Sci. 2747, 113–124 (2003). CrossRef
I. Walukiewicz, Monadic second-order logic on tree-like structures. Theoretical Computer Science 275, 311–346 (2002).