Document Open Access Logo

Set Automata and Limits of Decidability of Two-Variable Logic on Data Words

Authors Shibashis Guha , Amaldev Manuel , S P Rishal

PDF

File

Thumbnail PDF
PDF
LIPIcs.ICALP.2026.181.pdf
  • Filesize: 0.9 MB
  • 21 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Formal languages and automata theory
Keywords
  • Data words
  • Two-variable FO
  • Class automata
  • Finite semigroups
  • Decidability

Metrics

Abstract

We extend the two-variable logic on data words [Bojańczyk et al., 2011] with guarded regular binary predicates of the form L̃(x,y) that is true if positions x and y have the same data value and the factor strictly between x and y is in the regular language L. We characterise the class of aperiodic monoids for which the extension of the two-variable logic with guarded predicates recognised by the monoid is decidable, namely the class of idempotent monoids whose two-sided ideals are linearly ordered, called linear bands. For this, we introduce an automata formalism, set automata, that is equivalent to the class automata of Bojańczyk and Lasota and thus has an undecidable emptiness problem. The set updates used in the automaton form a semigroup of relations. We identify a subclass of set automata called ordered quasi-normal set automata that has a decidable emptiness problem by reduction to the emptiness problem of ordered multicounter automata. We show that the two-variable logic extended with guarded regular predicates recognised by a monoid M is expressively equivalent to a quasi-normal set automaton with the monoid of relations M. In particular, if M is a linear band then the resulting automaton is ordered, and the decidability result follows.

Cite As Get BibTex

Shibashis Guha, Amaldev Manuel, and S P Rishal. Set Automata and Limits of Decidability of Two-Variable Logic on Data Words. In 53rd International Colloquium on Automata, Languages, and Programming (ICALP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 374, pp. 181:1-181:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.ICALP.2026.181

Author Details

Shibashis Guha
  • Tata Institute of Fundamental Research, Mumbai, India
Amaldev Manuel
  • Indian Institute of Technology Goa, India
S P Rishal
  • Sarva Labs, Lewes, DE, USA

Funding

  • Guha, Shibashis: Partially supported by CEFIPRA project no. 7302-I and by the Department of Atomic Energy, Government of India, under project no. RTI4014.

References

  1. Ansuman Banerjee, Kingshuk Chatterjee, and Shibashis Guha. Set augmented finite automata over infinite alphabets. In DLT, volume 13911 of LNCS, pages 36-50. Springer, 2023. URL: https://doi.org/10.1007/978-3-031-33264-7_4.
  2. Henrik Björklund and Thomas Schwentick. On notions of regularity for data languages. In Fundamentals of Computation Theory, pages 88-99. Springer Berlin Heidelberg, 2007. URL: https://doi.org/10.1007/978-3-540-74240-1_9.
  3. Mikołaj Bojańczyk. Data monoids. In STACS, volume 9 of LIPIcs, pages 105-116. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011. URL: https://doi.org/10.4230/LIPIcs.STACS.2011.105.
  4. 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), July 2011. URL: https://doi.org/10.1145/1970398.1970403.
  5. Mikołaj Bojańczyk and Rafał Stefański. Single-Use Automata and Transducers for Infinite Alphabets. In ICALP, volume 168 of LIPIcs, pages 113:1-113:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. URL: https://doi.org/10.4230/LIPIcs.ICALP.2020.113.
  6. Mikolaj Bojańczyk and Sławomir Lasota. An extension of data automata that captures xpath. In LICS, pages 243-252, 2010. Google Scholar
  7. Thomas Colcombet, Clemens Ley, and Gabriele Puppis. On the use of guards for logics with data. In MFCS, volume 6907 of LNCS, pages 243-255. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22993-0_24.
  8. Thomas Colcombet and Amaldev Manuel. Fragments of Fixpoint Logic on Data Words. In FSTTCS, volume 45 of LIPIcs, pages 98-111. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2015.98.
  9. Stephane Demri and Paul Gastin. Specification and verification using temporal logics. In Modern Applications of Automata Theory, 2012. Google Scholar
  10. Stéphane Demri and Ranko Lazic. LTL with the freeze quantifier and register automata. ACM Trans. Comput. Log., 10(3):16:1-16:30, 2009. URL: https://doi.org/10.1145/1507244.1507246.
  11. Radu Grigore and Nikos Tzevelekos. History-register automata. Log. Methods Comput. Sci., 12(1), 2016. URL: https://doi.org/10.2168/LMCS-12(1:7)2016.
  12. Erich Grädel, Phokion G. Kolaitis, and Moshe Y. Vardi. On the decision problem for two-variable first-order logic. The Bulletin of Symbolic Logic, 3(1):53-69, 1997. URL: https://doi.org/10.2307/421196.
  13. Shibashis Guha, Amaldev Manuel, and S P Rishal. Set automata and limits of decidability of two-variable logic on data words. CoRR, abs/2605.09077, 2026. URL: https://arxiv.org/abs/2605.09077.
  14. Sabína Gulčíková and Ondřej Lengál. Register set automata (technical report), 2022. URL: https://arxiv.org/abs/2205.12114.
  15. Michael Kaminski and Nissim Francez. Finite-memory automata. Theor. Comput. Sci., 134(2):329-363, 1994. URL: https://doi.org/10.1016/0304-3975(94)90242-9.
  16. Ahmet Kara, Thomas Schwentick, and Tony Tan. Feasible automata for two-variable logic with successor on data words. In LATA, volume 7183 of LNCS, pages 351-362. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-28332-1_30.
  17. Gerard Lallement. Semigroups and combinatorial applications. Wiley, New York, 1979. Google Scholar
  18. Martin Leucker and César Sánchez. Regular linear temporal logic. In Theoretical Aspects of Computing - ICTAC 2007, pages 291-305. Springer Berlin Heidelberg, 2007. URL: https://doi.org/10.1007/978-3-540-75292-9_20.
  19. Amaldev Manuel and Ramaswamy Ramanujam. Class counting automata on data words. International Journal of Foundations of Computer Science, 22, November 2011. URL: https://doi.org/10.1142/S0129054111008465.
  20. Marvin L. Minsky. Computation: finite and infinite machines. Prentice-Hall, Inc., 1967. Google Scholar
  21. Frank Neven, Thomas Schwentick, and Victor Vianu. Finite state machines for strings over infinite alphabets. ACM Trans. Comput. Logic, 5(3):403-435, July 2004. URL: https://doi.org/10.1145/1013560.1013562.
  22. Jean-Éric Pin. Mathematical Foundations of Automata Theory, 2022. Google Scholar
  23. Thomas Place and Marc Zeitoun. All about unambiguous polynomial closure. TheoretiCS, Volume 2, January 2024. Google Scholar
  24. Klaus Reinhardt. Reachability in petri nets with inhibitor arcs. Electron. Notes Theor. Comput. Sci., 223:239-264, December 2008. URL: https://doi.org/10.1016/J.ENTCS.2008.12.042.
  25. Luc Segoufin. Automata and logics for words and trees over an infinite alphabet. In CSL, pages 41-57. Springer Berlin Heidelberg, 2006. URL: https://doi.org/10.1007/11874683_3.
  26. Pierre Wolper. Temporal logic can be more expressive. Information and Control, 56(1):72-99, 1983. URL: https://doi.org/10.1016/S0019-9958(83)80051-5.
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