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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
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)
Applegate, H.: Acyclic models and resolvent functors. Ph.D. thesis, Columbia University (1965)
Bartels, F.: On generalized coinduction and probabilistic specification formats. Ph.D. thesis, Vrije Universiteit Amsterdam (2004)
Bojańczyk, M., Klin, B., Lasota, S.: Automata theory in nominal sets. Log. Methods Comput. Sci. 10(3), 1–8 (2014)
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)
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)
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)
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
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)
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)
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)
Gabbay, M.J.: Foundations of nominal techniques: logic and semantics of variables in abstract syntax. Bull. Symb. Log. 17(2), 161–229 (2011)
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)
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)
Goncharov, S., Milius, S., Silva, A.: Towards a uniform theory of effectful state machines. ACM Trans. Comput. Log.21(3), 63 (2020). (article 23)
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
Hasuo, I.: Tracing Anonymity with Coalgebras. Ph.D. thesis, Radboud University Nijmegen (2008)
Hasuo, I., Jacobs, B., Sokolova, A.: Generic trace semantics via coinduction. Log. Methods Comput. Sci. 3(4:11), 1–36 (2007)
Hermida, C., Jacobs, B.: Structural induction and conduction in a fibrational setting. Inform. Comput. 145, 107–152 (1998)
Jacobs, B.: Introduction to Coalgebra. Towards Mathematics of States and Observation, Cambridge University Press, Cambridge (2016)
Jacobs, B., Silva, A., Sokolova, A.: Trace semantics via determinization. J. Comput. System Sci. 81, 859–879 (2015)
Johnstone, P.T.: Adjoint lifting theorems for categories of algebras. Bull. London Math. Soc. 7, 294–297 (1975)
Joyal, A.: Une théorie combinatoire des séries formelles. Adv. Math. 42, 1–82 (1981)
Joyal, A.: Foncteurs analytiques et espèces de structures. Lect. Notes Math. 1234, 126–159 (1986)
Kaminski, M., Francez, N.: Finite-memory automata. Theor. Comput. Sci. 134(2), 329–363 (1994)
Kock, A.: Monads on symmetric monoidal closed categories. Arch. Math. (Basel) 21, 1–10 (1970)
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
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)
Lambek, J.: A fixpoint theorem for complete categories. Math. Z. 103, 151–161 (1968)
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
Milius, S., Pattinson, D., Wißmann, T.: A new foundation for finitary corecursion and iterative algebras. Inform. and Comput. 271, 104456 (2020)
Moggi, E.: Notions of computations and monads. Inform. Comput. 93(1), 55–92 (1991)
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
Pitts, A.M.: Nominal Sets: Names and Symmetry in Computer Science. Cambridge University Press (2013)
Plotkin, G.D., Turi, D.: Towards a mathematical operational semantics. In: Proceedings of Logic in Computer Science (LICS) (1997)
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
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
Rutten, J.: Universal coalgebra: a theory of systems. Theoret. Comput. Sci. 249(1), 3–80 (2000)
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
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)
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
Smyth, M.B., Plotkin, G.D.: The category-theoretic solution of recursive domain equations. SIAM J. Comput. 11(4), 761–783 (1982)
Winter, J., Bonsangue, M., Rutten, J.: Coalgebraic characterizations of context-free languages. Log. Methods Comput. Sci. 9(3:14), 39 (2013)
Winter, J., Bonsangue, M., Rutten, J.: Context-free coalgebras. J. Comput. System Sci. 81, 911–939 (2015)
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
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2022 IFIP International Federation for Information Processing
About this paper
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)