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).  Zbl1086.11015
  2. J.-M. Autebert and J. Gabarró, Iterated GSMs and Co-CFL. Acta Informatica26, 749–769 (1989).  Zbl0659.68097
  3. V. Bárány, Invariants of automatic presentations and semi-synchronous transductions. In STACS '06. Lect. Notes Comput. Sci. 3884, 289 (2006).  Zbl1136.68413
  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).  Zbl1021.68051
  7. A. Bès, Undecidable extensions of Büchi arithmetic and Cobham-Semënov theorem. Journal of Symbolic Logic62, 1280–1296 (1997).  Zbl0896.03011
  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).  Zbl1054.03025
  10. A. Blumensath and E. Grädel, Finite presentations of infinite structures: Automata and interpretations. Theor. Comput. Syst.37, 641–674 (2004).  Zbl1061.03038
  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).  Zbl0957.11015
  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).  Zbl0804.11024
  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).  Zbl0764.20017
  15. A. Carayol and A. Meyer, Context-sensitive languages, rational graphs and determinism (2005).  Zbl1126.68049
  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).  Zbl1205.03022
  17. O. Carton and W. Thomas, The monadic theory of morphic infinite words and generalizations. Information and Computation176, 51–65 (2002).  Zbl1012.03015
  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).  Zbl1045.03509
  20. D. Caucal, On infinite terms having a decidable monadic theory. In MFCS, pp. 165–176 (2002).  Zbl1014.68077
  21. Th. Colcombet, A combinatorial theorem for trees. In ICALP'07. Lect. Notes Comput. Sci. 4596, 901–912 (2007).  Zbl1171.03325
  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).  Zbl0872.03026
  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).  Zbl0929.03036
  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).  Zbl0144.24501
  26. S. Fratani and G. Sénizergues, Iterated pushdown automata and sequences of rational numbers. Annals of Pure and Applied Logic141, 363–411, (2006).  Zbl1106.03036
  27. Ch. Frougny and J. Sakarovitch, Synchronized rational relations of finite and infinite words. Theoretical Computer Science108, 45–82 (1993).  Zbl0783.68065
  28. E. Grädel, W. Thomas and T. Wilke, Eds. Automata, Logics, and Infinite Games. Lect. Notes Comput. Sci. 2500, (2002).  Zbl1011.00037
  29. B.R. Hodgson, Décidabilité par automate fini. Ann. Sci. Math. Québec7, 39–57 (1983).  Zbl0531.03007
  30. J. Honkala and M. Rigo, A note on decidability questions related to abstract numeration systems. Discrete Math.285, 329–333 (2004).  Zbl1076.68040
  31. K. Culik II and J. Karhumäki, Iterative devices generating infinite words. In STACS '92. Lect. Notes Comput. Sci. 577, 529–543 (1992).  Zbl0900.68337
  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).  Zbl1058.68070
  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).  Zbl1122.68466
  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).  Zbl1114.68048
  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).  Zbl0937.68078
  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).  Zbl0605.03005
  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).  Zbl1078.68093
  43. A. Rabinovich, On decidability of monadic logic of order over the naturals extended by monadic predicates. Unpublished note (2005).  Zbl1115.68100
  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).  Zbl1225.03013
  45. M. Rigo and A. Maes, More on generalized automatic sequences. J. Autom. Lang. Comb.7, 351–376 (2002).  Zbl1033.68069
  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).  Zbl0575.00023
  48. S. Rubin, Automatic Structures. Ph.D. thesis, University of Auckland, NZ (2004).  Zbl1122.68466
  49. S. Rubin, Automata presenting structures: A survey of the finite-string case. Manuscript.  Zbl1146.03028
  50. G. Sénizergues, Sequences of level 1, 2, 3,..., k,... In CSR'07. Lect. Notes Comput. Sci. 4649, 24–32 (2007).  Zbl1188.68219
  51. S. Shelah, The monadic theory of order. Annals of Mathematics102, 379–419 (1975).  Zbl0345.02034
  52. L. Staiger, Rich omega-words and monadic second-order arithmetic. In CSL, pp. 478–490 (1997).  Zbl0914.03058
  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).  Zbl1124.03314
  55. I. Walukiewicz, Monadic second-order logic on tree-like structures. Theoretical Computer Science275, 311–346 (2002).  Zbl1026.68087

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.