Document Open Access Logo

Scoped MSO, Register Automata, and Expressions: Equivalence over Data Words

Author Radosław Piórkowski

PDF

File

Thumbnail PDF
PDF
LIPIcs.ICALP.2026.188.pdf
  • Filesize: 2 MB
  • 18 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Automata over infinite objects
  • Theory of computation → Logic and verification
  • Theory of computation → Regular languages
Keywords
  • register automata
  • data words
  • monadic second-order logic
  • infinite alphabets
  • Kleene theorem
  • nominal sets

Metrics

Abstract

This paper establishes logical and expression-based characterizations of the class of languages recognized by nondeterministic register automata with guessing (NRA) over infinite alphabets. We introduce Scoped MSO, a logic featuring a novel segment modality and syntactic restrictions on data comparisons. We prove this logic is expressively equivalent to NRA over data domains where "strong guessing" can be eliminated. Furthermore, we define Data Regular Expressions, a minimalist regular expression calculus built from quantifier-free regions and equipped with k-contracting concatenation, and demonstrate its equivalence to NRA over arbitrary relational structures. Together, these formalisms and the translations between them establish a robust correspondence between register automata, logic, and expressions over data words.

Cite As Get BibTex

Radosław Piórkowski. Scoped MSO, Register Automata, and Expressions: Equivalence over Data Words. In 53rd International Colloquium on Automata, Languages, and Programming (ICALP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 374, pp. 188:1-188:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.ICALP.2026.188

Author Details

Radosław Piórkowski
  • University of Warwick, Coventry, UK

Funding

  • Piórkowski, Radosław: The author is supported by the Engineering and Physical Sciences Research Council [EP/X03027X/1].

Acknowledgements

The author would like to thank Dmitry Chistikov for his valuable guidance and insightful discussions, and the Centre for Discrete Mathematics and its Applications (DIMAP) at the University of Warwick. The author also thanks the anonymous reviewers for their helpful comments and suggestions.

References

  1. Henrik Björklund and Thomas Schwentick. On notions of regularity for data languages. Theoretical Computer Science, 411(4):702-715, 2010. Fundamentals of Computation Theory. URL: https://doi.org/10.1016/j.tcs.2009.10.009.
  2. Mikołaj Bojańczyk. Slightly infinite sets. Draft of a book, version of September 11, 2019, 2019. URL: https://www.mimuw.edu.pl/~bojan/paper/atom-book.
  3. Mikołaj Bojańczyk, Claire David, Anca Muscholl, Thomas Schwentick, and Luc Segoufin. Two-variable logic on data words. ACM Trans. Comput. Logic, 12(4), 2011. URL: https://doi.org/10.1145/1970398.1970403.
  4. Mikołaj Bojańczyk and Rafał Stefański. Single-use automata and transducers for infinite alphabets. In Artur Czumaj, Anuj Dawar, and Emanuela Merelli, editors, 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020), volume 168 of Leibniz International Proceedings in Informatics (LIPIcs), pages 113:1-113:14, Dagstuhl, Germany, 2020. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ICALP.2020.113.
  5. Mikołaj Bojańczyk, Bartek Klin, and Sławomir Lasota. Automata theory in nominal sets. Logical Methods in Computer Science, Volume 10, Issue 3, August 2014. URL: https://doi.org/10.2168/LMCS-10(3:4)2014.
  6. Paul Brunet and Alexandra Silva. A kleene theorem for nominal automata. In Christel Baier, Ioannis Chatzigiannakis, Paola Flocchini, and Stefano Leonardi, editors, 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019), volume 132 of Leibniz International Proceedings in Informatics (LIPIcs), pages 107:1-107:13, Dagstuhl, Germany, 2019. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ICALP.2019.107.
  7. J. Richard Büchi. Weak second-order arithmetic and finite automata. Mathematical Logic Quarterly, 6(1-6):66-92, 1960. URL: https://doi.org/10.1002/malq.19600060105.
  8. Thomas Colcombet, Clemens Ley, and Gabriele Puppis. Logics with rigidly guarded data tests. Log. Methods Comput. Sci., 11(3), 2015. URL: https://doi.org/10.2168/LMCS-11(3:10)2015.
  9. Calvin C Elgot. Decision problems of finite automata design and related arithmetics. Transactions of the American Mathematical Society, 98(1):21-51, 1961. Google Scholar
  10. Michael Kaminski and Nissim Francez. Finite-memory automata. Proceedings [1990] 31st Annual Symposium on Foundations of Computer Science, pages 683-688 vol.2, 1990. URL: https://api.semanticscholar.org/CorpusID:205095872.
  11. Michael Kaminski and Tony Tan. Regular expressions for languages over infinite alphabets. Fundamenta Informaticae, 69:301-318, 2006. URL: https://api.semanticscholar.org/CorpusID:1411996.
  12. Stephen Cole Kleene. Representation of events in nerve nets and finite automata, volume 34. Princeton University Press Princeton, 1956. Google Scholar
  13. Bartek Klin, Sławomir Lasota, and Szymon Toruńczyk. Nondeterministic and co-nondeterministic implies deterministic, for data languages. In Stefan Kiefer and Christine Tasson, editors, Foundations of Software Science and Computation Structures, pages 365-384, Cham, 2021. Springer International Publishing. Google Scholar
  14. Frank Neven, Thomas Schwentick, and Victor Vianu. Finite state machines for strings over infinite alphabets. ACM Trans. Comput. Logic, 5(3):403-435, 2004. URL: https://doi.org/10.1145/1013560.1013562.
  15. Andrew M. Pitts. Nominal Sets: Names and Symmetry in Computer Science. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2013. Google Scholar
  16. Radosław Piórkowski. Scoped MSO, register automata, and expressions: Equivalence over data words, 2026. URL: https://doi.org/10.48550/arXiv.2602.13120.
  17. J. Richard Büchi. Symposium on decision problems: On a decision method in restricted second order arithmetic. In Ernest Nagel, Patrick Suppes, and Alfred Tarski, editors, Logic, Methodology and Philosophy of Science, volume 44 of Studies in Logic and the Foundations of Mathematics, pages 1-11. Elsevier, 1966. URL: https://doi.org/10.1016/S0049-237X(09)70564-6.
  18. Luc Segoufin. Automata and logics for words and trees over an infinite alphabet. In Zoltán Ésik, editor, Computer Science Logic, pages 41-57, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/11874683_3.
  19. B. A. Trakhtenbrot. Finite automata and the logic of one-place predicates. Sib. Mat. Zh., 3:103-131, 1962. Google Scholar
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact