Abstract
We show that the existence of a first-order formula separating two monadic second order formulas over countable ordinal words is decidable. This extends the work of Henckell and Almeida on finite words, and of Place and Zeitoun on \(\omega \)-words. For this, we develop the algebraic concept of monoid (resp. \(\omega \)-semigroup, resp. ordinal monoid) with aperiodic merge, an extension of monoids (resp. \(\omega \)-semigroup, resp. ordinal monoid) that explicitly includes a new operation capturing the loss of precision induced by first-order indistinguishability. We also show the computability of FO-pointlike sets, and the decidability of the covering problem for first-order logic on countable ordinal words.
This work was supported by the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (ERC DuaLL, grant agreement No. 670624), and by the DeLTA ANR project (ANR-16-CE40-0007).
A full version of this paper can be found on arXiv. This document contains internal hyperlinks, and is best read on an electronic device.
Chapter PDF
Similar content being viewed by others
Keywords
References
Adsul, B., Sarkar, S., Sreejith, A.V.: First-order logic and its infinitary quantifier extensions over countable words (2021)
Almeida, J.: Some algorithmic problems for pseudovarieties. Publ. Math. Debrecen 54(1), 531–552 (1999)
Almeida, J., Zeitoun, M.: The pseudovariety J is hyperdecidable. RAIRO-Theoretical Informatics and Applications 31(5), 457–482 (1997)
Ash, C.J.: Inevitable graphs: a proof of the type II conjecture and some related decision procedures. International Journal of Algebra and Computation 1(01), 127–146 (1991)
Bedon, N.: Finite automata and ordinals. Theoretical Computer Science 156(1), 119–144 (1996). https://doi.org/10.1016/0304-3975(95)00006-2
Bedon, N.: Langages reconnaissables de mots indexés par des ordinaux. Theses, Université de Marne la Vallée (Jan 1998), https://tel.archives-ouvertes.fr/tel-00003586
Bedon, N.: Logic over words on denumerable ordinals. Journal of Computer and System Sciences 63(3), 394–431 (2001). https://doi.org/10.1006/jcss.2001.1782
Bedon, N., Carton, O.: An Eilenberg theorem for words on countable ordinals. In: Lucchesi, C.L., Moura, A.V. (eds.) LATIN’98: Theoretical Informatics. pp. 53–64. Springer Berlin Heidelberg, Berlin, Heidelberg (1998). https://doi.org/10.1007/BFb0054310
Bedon, N., Rispal, C.: Schützenberger and Eilenberg theorems for words on linear orderings. Journal of Computer and System Sciences 78(2), 517–536 (Mar 2012). https://doi.org/10.1016/j.jcss.2011.06.003
Bès, A., Carton, O.: Algebraic Characterization of FO for Scattered Linear Orderings. In: Bezem, M. (ed.) Computer Science Logic (CSL’11) - 25th International Workshop/20th Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), vol. 12, pp. 67–81. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2011). https://doi.org/10.4230/LIPIcs.CSL.2011.67
Bojańczyk, M.: Recognisable languages over monads. In: Potapov, I. (ed.) Developments in Language Theory. pp. 1–13. Springer International Publishing, Cham (2015), https://arxiv.org/abs/1502.04898v1
Büchi, J.R.: On a decision method in restricted second order arithmetic. In: Logic, Methodology and Philosophy of Science (Proc. 1960 Internat. Congr .), pp. 1–11. Stanford Univ. Press, Stanford, Calif. (1962)
Büchi, J.R.: The monadic second order theory of \(\omega {_1}\), pp. 1–127. Springer Berlin Heidelberg (1973). https://doi.org/10.1007/BFb0082721
Carton, O., Colcombet, T., Puppis, G.: An algebraic approach to MSO-definability on countable linear orderings (May 2018). https://doi.org/10.1017/jsl.2018.7
Choueka, Y.: Finite automata, definable sets, and regular expressions over \(\omega \)n-tapes. Journal of Computer and System Sciences 17(1), 81–97 (1978)
Colcombet, T., Sreejith, A.V.: Limited set quantifiers over countable linear orderings. In: Proceedings, Part II, of the 42nd International Colloquium on Automata, Languages, and Programming - Volume 9135. pp. 146–158. ICALP 2015, Springer-Verlag, Berlin, Heidelberg (2015). https://doi.org/10.1007/978-3-662-47666-6_12
van Gool, S.J., Steinberg, B.: Merge decompositions, two-sided Krohn–Rhodes, and aperiodic pointlikes. Canadian Mathematical Bulletin 62(1), 199–208 (2019). https://doi.org/10.4153/CMB-2018-014-8
Gool, S., Steinberg, B.: Pointlike sets for varieties determined by groups. Advances in Mathematics 348, 18–50 (2019). https://doi.org/10.1016/j.aim.2019.03.020
Henckell, K.: Pointlike sets: the finest aperiodic cover of a finite semigroup. Journal of Pure and Applied Algebra 55(1), 85–126 (1988). https://doi.org/10.1016/0022-4049(88)90042-4
Makowsky, J.A.: Algorithmic uses of the Feferman–Vaught theorem. Annals of Pure and Applied Logic 126(1-3), 159–213 (2004). https://doi.org/10.1016/j.apal.2003.11.002
Manuel, A., Sreejith, A.V.: Two-variable logic over countable linear orderings. In: Faliszewski, P., Muscholl, A., Niedermeier, R. (eds.) 41st International Symposium on Mathematical Foundations of Computer Science, MFCS 2016, August 22-26, 2016 - Kraków, Poland. LIPIcs, vol. 58, pp. 66:1–66:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016). https://doi.org/10.4230/LIPIcs.MFCS.2016.66, https://doi.org/10.4230/LIPIcs.MFCS.2016.66
McNaughton, R., Papert, S.A.: Counter-Free Automata. The MIT Press (1971)
Perrin, D.: Recent results on automata and infinite words. In: International Symposium on Mathematical Foundations of Computer Science. pp. 134–148. Springer (1984). https://doi.org/10.1007/BFb0030294
Pin, J.E., Perrin, D.: Infinite Words: Automata, Semigroups, Logic and Games. Elsevier (2004), https://hal.archives-ouvertes.fr/hal-00112831
Place, T., Zeitoun, M.: Separating regular languages with first-order logic. Logical Methods in Computer Science 12 (2016). https://doi.org/10.2168/LMCS-12(1:5)2016
Place, T., Zeitoun, M.: The complexity of separation for levels in concatenation hierarchies. In: Ganguly, S., Pandya, P. (eds.) 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018). Leibniz International Proceedings in Informatics (LIPIcs), vol. 122, pp. 47:1–47:17. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany (2018). https://doi.org/10.4230/LIPIcs.FSTTCS.2018.47
Place, T., Zeitoun, M.: The covering problem. Logical Methods in Computer Science Volume 14, Issue 3 (Jul 2018). https://doi.org/10.23638/LMCS-14(3:1)2018
Place, T., Zeitoun, M.: On all things star-free. In: 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2019), https://arxiv.org/abs/1904.11863v1
Place, T., Zeitoun, M.: Separation for dot-depth two. Logical Methods in Computer Science Volume 17, Issue 3 (Sep 2021). https://doi.org/10.46298/lmcs-17(3:24)2021
Rabin, M.O.: Decidability of second-order theories and automata on infinite trees. Trans. Amer. Math. Soc. 141, 1–35 (1969)
Rispal, C.: Automates sur les ordres linéaires : Complémentation. Theses, Université de Marne la Vallée (Dec 2004), https://tel.archives-ouvertes.fr/tel-00720658
Rispal, C., Carton, O.: Complementation of Rational Sets on Countable Scattered Linear Orderings. International Journal of Foundations of Computer Science 16(4), 767–786 (2005), https://hal.archives-ouvertes.fr/hal-00160985
Rosenstein, J.G.: Linear orderings. Academic press (1982)
Schützenberger, M.: On finite monoids having only trivial subgroups. Information and Control 8(2), 190–194 (1965). https://doi.org/10.1016/S0019-9958(65)90108-7
Shelah, S.: The monadic theory of order. Ann. of Math. (2) 102(3), 379–419 (1975)
Simon, I.: Piecewise testable events. In: Brakhage, H. (ed.) Automata Theory and Formal Languages. pp. 214–222. Springer Berlin Heidelberg, Berlin, Heidelberg (1975)
Wilke, T.: An algebraic theory for regular languages of finite and infinite words. International Journal of Algebra and Computation 03(04), 447–489 (1993). https://doi.org/10.1142/S0218196793000287
Wilke, T.: Classifying discrete temporal properties. In: Meinel, C., Tison, S. (eds.) STACS 99. pp. 32–46. Springer Berlin Heidelberg, Berlin, Heidelberg (1999). https://doi.org/10.1007/3-540-49116-3_3
Wojciechowski, J.: Classes of transfinite sequences accepted by nondeterministic finite automata. Fundamenta informaticæ 7(2), 191–223 (1984)
Wojciechowski, J.: Finite automata on transfinite sequences and regular expressions. Fundamenta informaticæ 8(3-4), 379–396 (1985)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2022 The Author(s)
About this paper
Cite this paper
Colcombet, T., van Gool, S., Morvan, R. (2022). First-order separation over countable ordinals. In: Bouyer, P., Schröder, L. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2022. Lecture Notes in Computer Science, vol 13242. Springer, Cham. https://doi.org/10.1007/978-3-030-99253-8_14
Download citation
DOI: https://doi.org/10.1007/978-3-030-99253-8_14
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-99252-1
Online ISBN: 978-3-030-99253-8
eBook Packages: Computer ScienceComputer Science (R0)