Document Open Access Logo

Supported Sets - A New Foundation for Nominal Sets and Automata

Author Thorsten Wißmann

PDF
Thumbnail PDF

File

LIPIcs.CSL.2023.38.pdf
  • Filesize: 0.84 MB
  • 19 pages

Document Identifiers

Author Details

Thorsten Wißmann
  • Radboud University, Nijmegen, the Netherlands

Funding

  • Wißmann, Thorsten: Supported by the NWO TOP project 612.001.852.

Acknowledgements

The author thanks Jurriaan Rot, Joshua Moerman, and Frits Vaandrager for inspiring discussions. The definition of supported sets originated from discussions with Lutz Schröder, Dexter Kozen, and Stefan Milius.

Cite As Get BibTex

Thorsten Wißmann. Supported Sets - A New Foundation for Nominal Sets and Automata. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 38:1-38:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023) https://doi.org/10.4230/LIPIcs.CSL.2023.38

Abstract

The present work proposes and discusses the category of supported sets which provides a uniform foundation for nominal sets of various kinds, such as those for equality symmetry, for the order symmetry, and renaming sets. We show that all these differently flavoured categories of nominal sets are monadic over supported sets. Thus, supported sets provide a canonical finite way to represent nominal sets and the automata therein, e.g. register automata and coalgebras in general. Name binding in supported sets is modelled by a functor following the idea of de Bruijn indices. This functor lifts to the well-known abstraction functor in nominal sets. Together with the monadicity result, this gives rise to a transformation process from finite coalgebras in supported sets to orbit-finite coalgebras in nominal sets. One instance of this process transforms the finite representation of a register automaton in supported sets into its configuration automaton in nominal sets.

Subject Classification

ACM Subject Classification
  • Theory of computation
Keywords
  • Nominal Sets
  • Monads
  • LFP-Category
  • Supported Sets
  • Coalgebra

Metrics

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

Related Versions

References

  1. Jiří Adámek, Stefan Milius, Lurdes Sousa, and Thorsten Wißmann. Finitely presentable algebras for finitary monads. Theory and Applications of Categories, 34(37):1179-1195, November 2019. URL: http://www.tac.mta.ca/tac/volumes/34/37/34-37abs.html.
  2. Jiří Adámek, Horst Herrlich, and George E. Strecker. Abstract and concrete categories. the joy of cats, 2004. Google Scholar
  3. Jiří Adámek and Jiří Rosický. Locally Presentable and Accessible Categories. Cambridge University Press, 1994. Google Scholar
  4. Steve Awodey. Category Theory. Oxford Logic Guides. OUP Oxford, 2010. Google Scholar
  5. Brian E. Aydemir, Aaron Bohannon, and Stephanie Weirich. Nominal reasoning techniques in coq: (extended abstract). Electron. Notes Theor. Comput. Sci., 174(5):69-77, 2007. URL: https://doi.org/10.1016/j.entcs.2007.01.028.
  6. Falk Bartels. On generalized coinduction and probabilistic specification formats: Distributive laws in coalgebraic modelling. PhD thesis, Vrije Universiteit Amsterdam, 2004. Google Scholar
  7. Mikolaj Bojanczyk, Bartek Klin, and Slawomir Lasota. Automata theory in nominal sets. Log. Methods Comput. Sci., 10, 2014. URL: https://doi.org/10.2168/LMCS-10(3:4)2014.
  8. Sofia Cassel, Falk Howar, Bengt Jonsson, and Bernhard Steffen. Extending automata learning to extended finite state machines. In Amel Bennaceur, Reiner Hähnle, and Karl Meinke, editors, Machine Learning for Dynamic Software Analysis: Potentials and Limits - International Dagstuhl Seminar 16172, volume 11026 of LNCS, pages 149-177. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-96562-8_6.
  9. Vincenzo Ciancia and Ugo Montanari. A name abstraction functor for named sets. In Jirí Adámek and Clemens Kupke, editors, Proceedings of the Ninth Workshop on Coalgebraic Methods in Computer Science, CMCS 2008, volume 203, 5 of Electronic Notes in Theoretical Computer Science, pages 49-70. Elsevier, 2008. URL: https://doi.org/10.1016/j.entcs.2008.05.019.
  10. Ranald Clouston. Generalised name abstraction for nominal sets. In Frank Pfenning, editor, Foundations of Software Science and Computation Structures - 16th International Conference, FOSSACS 2013, volume 7794 of Lecture Notes in Computer Science, pages 434-449. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-37075-5_28.
  11. N.G de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae (Proceedings), 75(5):381-392, 1972. URL: https://doi.org/10.1016/1385-7258(72)90034-0.
  12. Hans-Peter Deifel, Stefan Milius, Lutz Schröder, and Thorsten Wißmann. Generic partition refinement and weighted tree automata. In Formal Methods - The Next 30 Years, Proc. 3rd World Congress on Formal Methods (FM 2019), volume 11800 of LNCS, pages 280-297. Springer, October 2019. Google Scholar
  13. 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.
  14. Ulrich Dorsch, Stefan Milius, Lutz Schröder, and Thorsten Wißmann. Efficient coalgebraic partition refinement. In Proc. 28th International Conference on Concurrency Theory (CONCUR 2017), LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. Google Scholar
  15. Gian Luigi Ferrari, Ugo Montanari, and Marco Pistore. Minimizing transition systems for name passing calculi: A co-algebraic formulation. In Mogens Nielsen and Uffe Engberg, editors, Foundations of Software Science and Computation Structures, 5th International Conference, FOSSACS 2002, volume 2303 of Lecture Notes in Computer Science, pages 129-158. Springer, 2002. URL: https://doi.org/10.1007/3-540-45931-6_10.
  16. Marcelo Fiore, Gordon Plotkin, and Daniele Turi. Abstract syntax and variable binding (extended abstract). In Proc. 14^th LICS Conf., pages 193-202. IEEE, Computer Society Press, 1999. Google Scholar
  17. Marcelo P. Fiore and Sam Staton. Comparing operational models of name-passing process calculi. Inf. Comput., 204(4):524-560, 2006. URL: https://doi.org/10.1016/j.ic.2005.08.004.
  18. Murdoch Gabbay and James Cheney. A sequent calculus for nominal logic. In 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 14-17 July 2004, Turku, Finland, Proceedings, pages 139-148. IEEE Computer Society, 2004. URL: https://doi.org/10.1109/LICS.2004.1319608.
  19. Murdoch Gabbay and Andrew M. Pitts. A new approach to abstract syntax involving binders. In 14th Annual IEEE Symposium on Logic in Computer Science, Trento, Italy, July 2-5, 1999, pages 214-224. IEEE Computer Society, 1999. URL: https://doi.org/10.1109/LICS.1999.782617.
  20. Murdoch Gabbay and Andrew M. Pitts. A new approach to abstract syntax with variable binding. Formal Aspects Comput., 13(3-5):341-363, 2002. URL: https://doi.org/10.1007/s001650200016.
  21. Murdoch James Gabbay and Martin Hofmann. Nominal renaming sets. In Iliano Cervesato, Helmut Veith, and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, 15th International Conference, LPAR 2008, volume 5330 of LNCS, pages 158-173. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-89439-1_11.
  22. Peter Gabriel and Friedrich Ulmer. Lokal präsentierbare Kategorien, volume 221 of Lecture Notes Math. Springer-Verlag, 1971. Google Scholar
  23. Fabio Gadducci, Marino Miculan, and Ugo Montanari. About permutation algebras, (pre)sheaves and named sets. Higher Order Symbol. Comput., 19(2-3):283-304, September 2006. URL: https://doi.org/10.1007/s10990-006-8749-3.
  24. Jules Jacobs and Thorsten Wißmann. Fast coalgebraic bisimilarity minimization. In Principles of Programming Languages, POPL '23. ACM, 2023. to appear. URL: https://arxiv.org/abs/2204.12368.
  25. Peter T. Johnstone. Adjoint Lifting Theorems for Categories of Algebras. Bull. London Math. Soc., 7(3):294-297, November 1975. Google Scholar
  26. Peter T Johnstone. Sketches of an elephant: a Topos theory compendium. Oxford logic guides. Oxford Univ. Press, New York, NY, 2002. Google Scholar
  27. 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.
  28. Barbara König and Sebastian Küpper. Generic partition refinement algorithms for coalgebras and an instantiation to weighted automata. In Theoretical Computer Science, IFIP TCS 2014, volume 8705 of LNCS, pages 311-325. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-44602-7.
  29. Dexter Kozen, Konstantinos Mamouras, Daniela Petrisan, and Alexandra Silva. Nominal kleene coalgebra. In Magnús M. Halldórsson, Kazuo Iwama, Naoki Kobayashi, and Bettina Speckmann, editors, ICALP 2015, Proceedings, volume 9135 of LNCS, pages 286-298. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-47666-6_23.
  30. Alexander Kurz, Daniela Petrisan, Paula Severi, and Fer-Jan de Vries. Nominal coalgebraic data types with applications to lambda calculus. Logical Methods in Computer Science, 9(4), 2013. URL: https://doi.org/10.2168/LMCS-9(4:20)2013.
  31. Alexander Kurz, Daniela Petrisan, and Jiri Velebil. Algebraic theories over nominal sets. CoRR, abs/1006.3027, 2010. URL: http://arxiv.org/abs/1006.3027,
  32. Saunders Mac Lane. Categories for the Working Mathematician. Graduate Texts in Mathematics. Springer New York, 1998. URL: http://books.google.de/books?id=eBvhyc4z8HQC.
  33. Stefan Milius, Lutz Schröder, and Thorsten Wißmann. Regular behaviours with names. Applied Categorical Structures, 24(5):663-701, 2016. URL: https://doi.org/10.1007/s10485-016-9457-8.
  34. Joshua Moerman and Jurriaan Rot. Separation and Renaming in Nominal Sets. In Maribel Fernández and Anca Muscholl, editors, CSL 2020, volume 152 of LIPIcs, pages 31:1-31:17, Dagstuhl, Germany, 2020. LIPIcs. URL: https://doi.org/10.4230/LIPIcs.CSL.2020.31.
  35. Joshua Moerman, Matteo Sammartino, Alexandra Silva, Bartek Klin, and Michal Szynwelski. Learning nominal automata. In Giuseppe Castagna and Andrew D. Gordon, editors, POPL 2017, pages 613-625. ACM, 2017. URL: https://doi.org/10.1145/3009837.3009879.
  36. Ugo Montanari and Marco Pistore. History-dependent automata: An introduction. In Marco Bernardo and Alessandro Bogliolo, editors, SFM-Moby 2005: Formal Methods for Mobile Computing, volume 3465 of Lecture Notes in Computer Science, pages 1-28. Springer, 2005. URL: https://doi.org/10.1007/11419822_1.
  37. Daniela Petrişan. Investigations into Algebra and Topology over Nominal Sets. dissertation, University of Leicester, 2011. Google Scholar
  38. 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
  39. Lutz Schröder, Dexter Kozen, Stefan Milius, and Thorsten Wissmann. Nominal automata with name binding. In Javier Esparza and Andrzej Murawski, editors, FoSSaCS 2017, volume 10203 of LNCS, pages 124-142. Springer, 2017. URL: https://doi.org/10.1007/978-3-662-54458-7_8.
  40. 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), 2013. URL: https://doi.org/10.2168/LMCS-9(1:9)2013.
  41. Sam Staton. Name-passing process calculi: operational models and structural operational semantics. Technical Report UCAM-CL-TR-688, University of Cambridge, Computer Laboratory, June 2007. URL: https://doi.org/10.48456/tr-688.
  42. Christian Urban and Christine Tasson. Nominal techniques in isabelle/hol. In Robert Nieuwenhuis, editor, CADE-20, volume 3632 of LNCS, pages 38-53. Springer, 2005. URL: https://doi.org/10.1007/11532231_4.
  43. Henning Urbat and Lutz Schröder. Automata learning: An algebraic approach. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, LICS '20: 35th Annual ACM/IEEE Symposium on Logic in Computer Science, pages 900-914. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394775.
  44. Frits W. Vaandrager and Abhisek Midya. A myhill-nerode theorem for register automata and symbolic trace languages. In Violet Ka I Pun, Volker Stolz, and Adenilso Simão, editors, ICTAC 2020, volume 12545 of LNCS, pages 43-63. Springer, 2020. URL: https://doi.org/10.1007/978-3-030-64276-1_3.
  45. Frits W. Vaandrager and Abhisek Midya. A myhill-nerode theorem for register automata and symbolic trace languages. Theor. Comput. Sci., 912:37-55, 2022. URL: https://doi.org/10.1016/j.tcs.2022.01.015.
  46. David Venhoek, Joshua Moerman, and Jurriaan Rot. Fast computations on ordered nominal sets. In Bernd Fischer and Tarmo Uustalu, editors, ICTAC 2018, volume 11187 of LNCS, pages 493-512. Springer, 2018. URL: https://doi.org/10.1007/978-3-030-02508-3_26.
  47. David Venhoek, Joshua Moerman, and Jurriaan Rot. Fast computations on ordered nominal sets. Theor. Comput. Sci., 935:82-104, 2022. URL: https://doi.org/10.1016/j.tcs.2022.09.002.
  48. Thorsten Wißmann, Hans-Peter Deifel, Stefan Milius, and Lutz Schröder. From generic partition refinement to weighted tree automata minimization. Formal Aspects of Computing, pages 1-33, March 2021. URL: https://doi.org/10.1007/s00165-020-00526-z.
  49. Thorsten Wißmann, Ulrich Dorsch, Stefan Milius, and Lutz Schröder. Efficient and modular coalgebraic partition refinement. Logical Methods in Computer Science, 16:1:8:1-8:63, January 2020. URL: https://doi.org/10.23638/LMCS-16(1:8)2020.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

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