Coalgebraic Semantics for Nominal Automata | SpringerLink
Skip to main content

Coalgebraic Semantics for Nominal Automata

  • Conference paper
  • First Online:
Coalgebraic Methods in Computer Science (CMCS 2022)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 13225))

Included in the following conference series:

  • 253 Accesses

Abstract

This paper provides a coalgebraic approach to the language semantics of two types of non-deterministic automata over nominal sets: non-deterministic orbit-finite automata (NOFAs) and regular nominal non-deterministic automata (RNNAs), which were introduced in previous work. While NOFAs are a straightforward nominal version of non-deterministic automata, RNNAs feature ordinary as well as name binding transitions. Correspondingly, words accepted by RNNAs are strings formed by ordinary letters and name binding letters. Bar languages are sets of such words modulo \(\alpha \)-equivalence, and to every state of an RNNA one associates its accepted bar language. We show that the semantics of NOFAs and RNNAs, respectively, arise both as an instance of the Kleisli-style coalgebraic trace semantics as well as an instance of the coalgebraic language semantics obtained via generalized determinization. On the way we revisit coalgebraic trace semantics in general and give a new compact proof for the main result in that theory stating that an initial algebra for a functor yields the terminal coalgebra for the Kleisli extension of the functor. Our proof requires fewer assumptions on the functor than all previous ones.

Funded by the Deutsche Forschungsgemeinschaft (DFG, German Research Foundation) – project number 419850228.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 12583
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 15729
Price includes VAT (Japan)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

References

  1. Adámek, J., Milius, S., Moss, L.S.: Initial algebras without iteration. In: Gaducci, F., Silva, A. (eds.) 9th Conference on Algebra and Coalgebra in Computer Science (CALCO). LIPIcs, vol. 211, pp. 5:1–5:20. Schloss Dagstuhl (2021)

    Google Scholar 

  2. Applegate, H.: Acyclic models and resolvent functors. Ph.D. thesis, Columbia University (1965)

    Google Scholar 

  3. Bartels, F.: On generalized coinduction and probabilistic specification formats. Ph.D. thesis, Vrije Universiteit Amsterdam (2004)

    Google Scholar 

  4. Bojańczyk, M., Klin, B., Lasota, S.: Automata theory in nominal sets. Log. Methods Comput. Sci. 10(3), 1–8 (2014)

    Google Scholar 

  5. Bonchi, F., Milius, S., Silva, A., Zanasi, F.: Killing epsilons with a dagger: a coalgebraic study of systems with algebraic label structure. Theoret. Comput. Sci. 604, 102–126 (2015)

    Article  MathSciNet  Google Scholar 

  6. Bonchi, F., Pous, D.: Checking NFA equivalence with bisimulations up to congruence. In: Giacobazzi, R., Cousot, R. (eds.) Proceedings of 40th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 2013), pp. 457–468. ACM (2013)

    Google Scholar 

  7. Bonsangue, M.M., Milius, S., Silva, A.: Sound and complete axiomatizations of coalgebraic language equivalence. ACM Trans. Comput. Logic 14(1), 7:1–7:52 (2013)

    Google Scholar 

  8. Ciancia, V., Sammartino, M.: A class of automata for the verification of infinite, resource-allocating behaviours. In: Maffei, M., Tuosto, E. (eds.) TGC 2014. LNCS, vol. 8902, pp. 97–111. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-45917-1_7

    Chapter  Google Scholar 

  9. Dorsch, U., Milius, S., Schröder, L.: Graded monads and graded logics for the linear time - branching time spectrum. In: Fokkink, W.J., van Glabbeek, R. (eds.) Proceedings of 30th International Conference on Concurrency Theory (CONCUR). LIPIcs, vol. 140, pp. 36:1–36:16. Schloss Dagstuhl (2019)

    Google Scholar 

  10. Fiore, M., Plotkin, G.D., Turi, D.: Abstract syntax and variable binding. In: Proceedings of Logic in Computer Science (LICS), pp. 193–202. IEEE Computer Society (1999)

    Google Scholar 

  11. Freyd, P.: Remarks on algebraically compact categories. In: Fourman, M.P., Johnstone, P.T., Pitts, A.M. (eds.) Applications of category theory in computer science: Proceedings of the London Mathematical Society Symposium, Durham 1991. London Mathematical Society Lecture Note Series, vol. 177, pp. 95–106. Cambridge University Press (1992)

    Google Scholar 

  12. Gabbay, M.J.: Foundations of nominal techniques: logic and semantics of variables in abstract syntax. Bull. Symb. Log. 17(2), 161–229 (2011)

    Article  MathSciNet  Google Scholar 

  13. Gabbay, M.J., Pitts, A.M.: A new approach to abstract syntax involving binders. In: Logic in Computer Science, LICS 1999, pp. 214–224. IEEE Computer Society (1999)

    Google Scholar 

  14. van Glabbeek, R.: The linear time - branching time spectrum i; the semantics of concrete, sequential processes. In: Bergstra, J., Ponse, A., Smolka, S. (eds.) Handbook of Process Algebra, pp. 3–99. Elsevier (2001)

    Google Scholar 

  15. Goncharov, S., Milius, S., Silva, A.: Towards a uniform theory of effectful state machines. ACM Trans. Comput. Log.21(3), 63 (2020). (article 23)

    Google Scholar 

  16. Grigore, R., Distefano, D., Petersen, R.L., Tzevelekos, N.: Runtime verification based on register automata. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 260–276. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-36742-7_19

    Chapter  Google Scholar 

  17. Hasuo, I.: Tracing Anonymity with Coalgebras. Ph.D. thesis, Radboud University Nijmegen (2008)

    Google Scholar 

  18. Hasuo, I., Jacobs, B., Sokolova, A.: Generic trace semantics via coinduction. Log. Methods Comput. Sci. 3(4:11), 1–36 (2007)

    Google Scholar 

  19. Hermida, C., Jacobs, B.: Structural induction and conduction in a fibrational setting. Inform. Comput. 145, 107–152 (1998)

    Article  MathSciNet  Google Scholar 

  20. Jacobs, B.: Introduction to Coalgebra. Towards Mathematics of States and Observation, Cambridge University Press, Cambridge (2016)

    Book  Google Scholar 

  21. Jacobs, B., Silva, A., Sokolova, A.: Trace semantics via determinization. J. Comput. System Sci. 81, 859–879 (2015)

    Article  MathSciNet  Google Scholar 

  22. Johnstone, P.T.: Adjoint lifting theorems for categories of algebras. Bull. London Math. Soc. 7, 294–297 (1975)

    Article  MathSciNet  Google Scholar 

  23. Joyal, A.: Une théorie combinatoire des séries formelles. Adv. Math. 42, 1–82 (1981)

    Article  MathSciNet  Google Scholar 

  24. Joyal, A.: Foncteurs analytiques et espèces de structures. Lect. Notes Math. 1234, 126–159 (1986)

    Article  Google Scholar 

  25. Kaminski, M., Francez, N.: Finite-memory automata. Theor. Comput. Sci. 134(2), 329–363 (1994)

    Article  MathSciNet  Google Scholar 

  26. Kock, A.: Monads on symmetric monoidal closed categories. Arch. Math. (Basel) 21, 1–10 (1970)

    Article  MathSciNet  Google Scholar 

  27. Kozen, D., Mamouras, K., Petrişan, D., Silva, A.: Nominal Kleene coalgebra. In: Halldórsson, M.M., Iwama, K., Kobayashi, N., Speckmann, B. (eds.) ICALP 2015. LNCS, vol. 9135, pp. 286–298. Springer, Heidelberg (2015). https://doi.org/10.1007/978-3-662-47666-6_23

    Chapter  Google Scholar 

  28. Kürtz, K., Küsters, R., Wilke, T.: Selecting theories and nonce generation for recursive protocols. In: Formal methods in security engineering, FMSE 2007, pp. 61–70. ACM (2007)

    Google Scholar 

  29. Lambek, J.: A fixpoint theorem for complete categories. Math. Z. 103, 151–161 (1968)

    Article  MathSciNet  Google Scholar 

  30. Milius, S., Palm, T., Schwencke, D.: Complete iterativity for algebras with effects. In: Kurz, A., Lenisa, M., Tarlecki, A. (eds.) CALCO 2009. LNCS, vol. 5728, pp. 34–48. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-03741-2_4

    Chapter  Google Scholar 

  31. Milius, S., Pattinson, D., Wißmann, T.: A new foundation for finitary corecursion and iterative algebras. Inform. and Comput. 271, 104456 (2020)

    Google Scholar 

  32. Moggi, E.: Notions of computations and monads. Inform. Comput. 93(1), 55–92 (1991)

    Article  MathSciNet  Google Scholar 

  33. Mulry, P.S.: Lifting theorems for Kleisli categories. In: Brookes, S., Main, M., Melton, A., Mislove, M., Schmidt, D. (eds.) MFPS 1993. LNCS, vol. 802, pp. 304–319. Springer, Heidelberg (1994). https://doi.org/10.1007/3-540-58027-1_15

    Chapter  Google Scholar 

  34. Pitts, A.M.: Nominal Sets: Names and Symmetry in Computer Science. Cambridge University Press (2013)

    Google Scholar 

  35. Plotkin, G.D., Turi, D.: Towards a mathematical operational semantics. In: Proceedings of Logic in Computer Science (LICS) (1997)

    Google Scholar 

  36. Rot, J., Bonsangue, M., Rutten, J.: Coalgebraic bisimulation-up-to. In: van Emde Boas, P., Groen, F.C.A., Italiano, G.F., Nawrocki, J., Sack, H. (eds.) SOFSEM 2013. LNCS, vol. 7741, pp. 369–381. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-35843-2_32

    Chapter  Google Scholar 

  37. Rutten, J.J.M.M.: Automata and coinduction (an exercise in coalgebra). In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 194–218. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0055624

    Chapter  Google Scholar 

  38. Rutten, J.: Universal coalgebra: a theory of systems. Theoret. Comput. Sci. 249(1), 3–80 (2000)

    Article  MathSciNet  Google Scholar 

  39. Schröder, L., Kozen, D., Milius, S., Wißmann, T.: Nominal automata with name binding. In: Esparza, J., Murawski, A.S. (eds.) FoSSaCS 2017. LNCS, vol. 10203, pp. 124–142. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54458-7_8

    Chapter  Google Scholar 

  40. Silva, A., Bonchi, F., Bonsangue, M.M., Rutten, J.J.M.M.: Generalizing determinization from automata to coalgebras. Log. Methods Comput. Sci. 9(1:9), 1–22 (2013)

    Google Scholar 

  41. Silva, A., Westerbaan, B.: A coalgebraic view of \(\epsilon \)-transitions. In: Heckel, R., Milius, S. (eds.) CALCO 2013. LNCS, vol. 8089, pp. 267–281. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-40206-7_20

    Chapter  Google Scholar 

  42. Smyth, M.B., Plotkin, G.D.: The category-theoretic solution of recursive domain equations. SIAM J. Comput. 11(4), 761–783 (1982)

    Article  MathSciNet  Google Scholar 

  43. Winter, J., Bonsangue, M., Rutten, J.: Coalgebraic characterizations of context-free languages. Log. Methods Comput. Sci. 9(3:14), 39 (2013)

    Google Scholar 

  44. Winter, J., Bonsangue, M., Rutten, J.: Context-free coalgebras. J. Comput. System Sci. 81, 911–939 (2015)

    Article  MathSciNet  Google Scholar 

  45. Wißmann, T.: Coalgebraic Semantics and Minimization in Sets and Beyond. Ph.D. thesis, Friedrich-Alexander-Universität Erlangen-Nürnberg (FAU) (2020). https://opus4.kobv.de/opus4-fau/frontdoor/index/index/docId/14222

Download references

Author information

Authors and Affiliations

Authors

Corresponding author

Correspondence to Stefan Milius .

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2022 IFIP International Federation for Information Processing

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Frank, F., Milius, S., Urbat, H. (2022). Coalgebraic Semantics for Nominal Automata. In: Hansen, H.H., Zanasi, F. (eds) Coalgebraic Methods in Computer Science. CMCS 2022. Lecture Notes in Computer Science, vol 13225. Springer, Cham. https://doi.org/10.1007/978-3-031-10736-8_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-10736-8_3

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-10735-1

  • Online ISBN: 978-3-031-10736-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics