Positive Data Languages

Authors Florian Frank , Stefan Milius , Henning Urbat

Thumbnail PDF


  • Filesize: 0.81 MB
  • 15 pages

Document Identifiers

Author Details

Florian Frank
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany
Stefan Milius
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany
Henning Urbat
  • Friedrich-Alexander-Universität Erlangen-Nürnberg, Germany


The authors wish to thank Bartek Klin for pointing out the example in Remark 2.10.

Cite AsGet BibTex

Florian Frank, Stefan Milius, and Henning Urbat. Positive Data Languages. In 48th International Symposium on Mathematical Foundations of Computer Science (MFCS 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 272, pp. 48:1-48:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


Positive data languages are languages over an infinite alphabet closed under possibly non-injective renamings of data values. Informally, they model properties of data words expressible by assertions about equality, but not inequality, of data values occurring in the word. We investigate the class of positive data languages recognizable by nondeterministic orbit-finite nominal automata, an abstract form of register automata introduced by Bojańczyk, Klin, and Lasota. As our main contribution we provide a number of equivalent characterizations of that class in terms of positive register automata, monadic second-order logic with positive equality tests, and finitely presentable nondeterministic automata in the categories of nominal renaming sets and of presheaves over finite sets.

Subject Classification

ACM Subject Classification
  • Theory of computation → Formal languages and automata theory
  • Data Languages
  • Register Automata
  • MSO
  • Nominal Sets
  • Presheaves


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Jiří Adámek, Stefan Milius, Lurdes Sousa, and Thorsten Wißmann. On finitary functors. Theory Appl. Categ., 34(37):1134-1164, 2019. Google Scholar
  2. Jiří Adámek and Jiří Rosický. Locally Presentable and Accessible Categories. London Mathematical Society Lecture Note Series. Cambridge University Press, 1994. Google Scholar
  3. Michał Bielecki, Jan Hidders, Jan Paredaens, Jerzy Tyszkiewicz, and Jan Van den Bussche. Navigating with a browser. In Proc. 29th International Colloquium on Automata, Languages and Programming (ICALP 2002), volume 2380 of Lect. Notes Comput. Sci., pages 764-775. Springer, 2002. Google Scholar
  4. Mikołaj Bojańczyk. Nominal monoids. Theory Comput. Syst., 53(2):194-222, 2013. URL: https://doi.org/10.1007/s00224-013-9464-1.
  5. Mikołaj Bojańczyk, Claire David, Anca Muscholl, Thomas Schwentick, and Luc Segoufin. Two-variable logic on data trees and XML reasoning. In Proc. 25th ACM SIGACT-SIGMOD-SIGART Symposium on Principles of Database Systems (PODS 2006), pages 10-19. ACM, 2006. Google Scholar
  6. Mikołaj Bojańczyk, Bartek Klin, and Sławomir Lasota. Automata theory in nominal sets. Log. Methods Comput. Sci., 10(3), 2014. URL: https://doi.org/10.2168/LMCS-10(3:4)2014.
  7. Mikołaj Bojańczyk, Anca Muscholl, Thomas Schwentick, Luc Segoufin, and Claire David. Two-variable logic on words with data. In Proc. 21th IEEE Symposium on Logic in Computer Science (LICS 2006), pages 7-16. IEEE Computer Society, 2006. Google Scholar
  8. Mikołaj Bojańczyk and Rafał Stefański. Single-use automata and transducers for infinite alphabets. In Proc. 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020), 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.
  9. Thomas Colcombet, Clemens Ley, and Gabriele Puppis. Logics with rigidly guarded data tests. Log. Methods Comput. Sci., 11(3), 2015. Google Scholar
  10. Marcelo P. Fiore, Gordon D. Plotkin, and Daniele Turi. Abstract syntax and variable binding. In Proc. 14th Annual IEEE Symposium on Logic in Computer Science (LICS 1999), pages 193-202. IEEE Computer Society, 1999. Google Scholar
  11. Murdoch J. Gabbay. Nominal renaming sets (technical report), 2007. URL: http://gabbay.org.uk/papers/nomrs-tr.pdf.
  12. Murdoch J. Gabbay and Martin Hofmann. Nominal renaming sets. In Proc. 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2008), pages 158-173. Springer, 2008. Google Scholar
  13. Murdoch J. Gabbay and Andrew M. Pitts. A new approach to abstract syntax involving binders. In Proc. 14th Annual IEEE Symposium on Logic in Computer Science (LICS 1999), pages 214-224. IEEE Computer Society, 1999. Google Scholar
  14. Fabio Gadducci, Marino Miculan, and Ugo Montanari. About permutation algebras, (pre)sheaves and named sets. High. Order Symb. Comput., 19(2-3):283-304, 2006. Google Scholar
  15. Ichiro Hasuo, Bart Jacobs, and Ana Sokolova. Generic trace semantics via coinduction. Log. Methods Comput. Sci., 3(4:11):1-36, 2007. Google Scholar
  16. Peter T. Johnstone. Sketches of an Elephant: A Topos Theory Compendium. Oxford Logic Guides. Oxford Univ. Press, 2002. Google Scholar
  17. 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.
  18. Michael Kaminski and Tony Tan. Regular expressions for languages over infinite alphabets. Fundam. Informaticae, 69(3):301-318, 2006. Google Scholar
  19. Michael Kaminski and Daniel Zeitlin. Finite-memory automata with non-deterministic reassignment. Int. J. Found. Comput. Sci., 21(5):741-760, 2010. Google Scholar
  20. Bartek Klin, Sławomir Lasota, and Szymon Torunczyk. Nondeterministic and co-nondeterministic implies deterministic, for data languages. In Proc. 24th International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2021), volume 12650 of Lect. Notes Comput. Sci., pages 365-384. Springer, 2021. Google Scholar
  21. Klaas Kürtz, Ralf Küsters, and Thomas Wilke. Selecting theories and nonce generation for recursive protocols. In Proc. 2007 ACM Workshop on Formal Methods in Security Engineering (FMSE 2007), pages 61-70. ACM, 2007. Google Scholar
  22. Saunders Mac Lane. Categories for the Working Mathematician. Springer, 1971. Google Scholar
  23. Stefan Milius and Henning Urbat. Equational axiomatization of algebras with structure. In Proc. 22nd International Conference on Foundations of Software Science and Computation Structures (FOSSACS 2019), volume 11425 of Lect. Notes Comput. Sci., pages 400-417. Springer, 2019. URL: https://doi.org/10.1007/978-3-030-17127-8_23.
  24. Joshua Moerman and Jurriaan Rot. Separation and Renaming in Nominal Sets. In Proc. 28th EACSL Annual Conference on Computer Science Logic (CSL 2020), volume 152 of Leibniz International Proceedings in Informatics (LIPIcs), pages 31:1-31:17. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2020. Google Scholar
  25. Frank Neven, Thomas Schwentick, and Victor Vianu. Finite state machines for strings over infinite alphabets. ACM Trans. Comput. Logic, 5(3):403-435, 2004. Google Scholar
  26. Daniela Petrişan. Investigations into Algebra and Topology over Nominal Sets. PhD thesis, University of Leicester, 2012. Google Scholar
  27. Andrew M. Pitts. Nominal Sets: Names and Symmetry in Computer Science, volume 57 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2013. Google Scholar
  28. Jan J. M. M. Rutten. Universal coalgebra: A theory of systems. Theor. Comput. Sci., 249(1):3-80, 2000. Google Scholar
  29. Lutz Schröder, Dexter Kozen, Stefan Milius, and Thorsten Wißmann. Nominal automata with name binding. In Proc. 20th International Conference on Foundations of Software Science and Computation Structures, (FOSSACS 2017), volume 10203 of Lect. Notes Comput. Sci., pages 124-142, 2017. Google Scholar
  30. Alexandra Silva, Filippo Bonchi, Marcello M. Bonsangue, and Jan J. M. M. Rutten. Generalizing determinization from automata to coalgebras. Log. Methods Comput. Sci., 9(1:9), 2013. Google Scholar
  31. Ian Stark. Categorical models for local names. LISP Symb. Comput., 9(1):77-107, 1996. Google Scholar
  32. A. Tal. Decidability of inclusion for unification based automata. Master’s thesis, Department of Computer Science, Technion – Israel Institute of Technology, 1999. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail