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

Vince Bárány

RAIRO - Theoretical Informatics and Applications (2008)

  • Volume: 42, Issue: 3, page 417-450
  • ISSN: 0988-3754

Abstract

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

How to cite

top

Bárány, Vince. "A Hierarchy of Automatic ω-Words having a Decidable MSO Theory." RAIRO - Theoretical Informatics and Applications 42.3 (2008): 417-450. <http://eudml.org/doc/250373>.

@article{Bárány2008,
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. },
author = {Bárány, Vince},
journal = {RAIRO - Theoretical Informatics and Applications},
keywords = {Morphic words; monadic second-order logic; automatic structures; automatic sequences.; morphic words; lexicographic word ordering; lexicographic hierarchies; finite automaton; automatic sequences; recognizability by finite automata},
language = {eng},
month = {6},
number = {3},
pages = {417-450},
publisher = {EDP Sciences},
title = {A Hierarchy of Automatic ω-Words having a Decidable MSO Theory},
url = {http://eudml.org/doc/250373},
volume = {42},
year = {2008},
}

TY - JOUR
AU - Bárány, Vince
TI - A Hierarchy of Automatic ω-Words having a Decidable MSO Theory
JO - RAIRO - Theoretical Informatics and Applications
DA - 2008/6//
PB - EDP Sciences
VL - 42
IS - 3
SP - 417
EP - 450
AB - 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.
LA - eng
KW - Morphic words; monadic second-order logic; automatic structures; automatic sequences.; morphic words; lexicographic word ordering; lexicographic hierarchies; finite automaton; automatic sequences; recognizability by finite automata
UR - http://eudml.org/doc/250373
ER -

References

top
  1. J.-P. Allouche and J. Shallit, Automatic Sequences, Theory, Applications, Generalizations. Cambridge University Press (2003).  
  2. J.-M. Autebert and J. Gabarró, Iterated GSMs and Co-CFL. Acta Informatica26, 749–769 (1989).  
  3. V. Bárány, Invariants of automatic presentations and semi-synchronous transductions. In STACS '06. Lect. Notes Comput. Sci. 3884, 289 (2006).  
  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).  
  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).  
  7. A. Bès, Undecidable extensions of Büchi arithmetic and Cobham-Semënov theorem. Journal of Symbolic Logic62, 1280–1296 (1997).  
  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).  
  10. A. Blumensath and E. Grädel, Finite presentations of infinite structures: Automata and interpretations. Theor. Comput. Syst.37, 641–674 (2004).  
  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 Science181, 17–43 (1997).  
  13. V. Bruyère, G. Hansel, Ch. Michaux and R. Villemaire, Logic and p-recognizable sets of integers. Bull. Belg. Math. Soc. Simon Stevin1, 191–238 (1994).  
  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).  
  15. A. Carayol and A. Meyer, Context-sensitive languages, rational graphs and determinism (2005).  
  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).  
  17. O. Carton and W. Thomas, The monadic theory of morphic infinite words and generalizations. Information and Computation176, 51–65 (2002).  
  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).  
  20. D. Caucal, On infinite terms having a decidable monadic theory. In MFCS, pp. 165–176 (2002).  
  21. Th. Colcombet, A combinatorial theorem for trees. In ICALP'07. Lect. Notes Comput. Sci. 4596, 901–912 (2007).  
  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 Science151, 125–162 (1995).  
  24. B. Courcelle and I. Walukiewicz, Monadic second-order logic, graph coverings and unfoldings of transition systems. Annals of Pure and Applied Logic92, 35–62 (1998).  
  25. C.C. Elgot and M.O. Rabin, Decidability and undecidability of extensions of second (first) order theory of (generalized) successor. Journal of Symbolic Logic31, 169–181 (1966).  
  26. S. Fratani and G. Sénizergues, Iterated pushdown automata and sequences of rational numbers. Annals of Pure and Applied Logic141, 363–411, (2006).  
  27. Ch. Frougny and J. Sakarovitch, Synchronized rational relations of finite and infinite words. Theoretical Computer Science108, 45–82 (1993).  
  28. E. Grädel, W. Thomas and T. Wilke, Eds. Automata, Logics, and Infinite Games. Lect. Notes Comput. Sci. 2500, (2002).  
  29. B.R. Hodgson, Décidabilité par automate fini. Ann. Sci. Math. Québec7, 39–57 (1983).  
  30. J. Honkala and M. Rigo, A note on decidability questions related to abstract numeration systems. Discrete Math.285, 329–333 (2004).  
  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).  
  33. B. Khoussainov and A. Nerode, Automatic presentations of structures. In LCC '94. Lect. Notes Comput. Sci. 960, 367–392 (1995).  
  34. B. Khoussainov and S. Rubin, Automatic structures: Overview and future directions. J. Autom. Lang. Comb.8, 287–301 (2003).  
  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).  
  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 Sciences67, 497–545 (2003).  
  38. A. Maes, An automata theoretic decidability proof for first-order theory of 〈 ℕ , < , P 〉 with morphic predicate P. J. Autom. Lang. Comb.4, 229–245 (1999).  
  39. Ch. Morvan and Ch. Rispal, Families of automata characterizing context-sensitive languages. Acta Informatica41, 293–314 (2005).  
  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).  
  41. J.-J. Pansiot, On various classes of infinite words obtained by iterated mappings. In Automata on Infinite Words, pp. 188–197 (1984).  
  42. J.-E. Pin and P.V. Silva, A topological approach to transductions. Theoretical Computer Science340, 443–456 (2005).  
  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).  
  45. M. Rigo and A. Maes, More on generalized automatic sequences. J. Autom. Lang. Comb.7, 351–376 (2002).  
  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).  
  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 Mathematics102, 379–419 (1975).  
  52. L. Staiger, Rich omega-words and monadic second-order arithmetic. In CSL, pp. 478–490 (1997).  
  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).  
  54. W. Thomas, Constructing infinite graphs with a decidable mso-theory. In MFCS'03. Lect. Notes Comput. Sci. 2747, 113–124 (2003).  
  55. I. Walukiewicz, Monadic second-order logic on tree-like structures. Theoretical Computer Science275, 311–346 (2002).  

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.