LIPIcs.CONCUR.2018.5.pdf
- Filesize: 225 kB
- 2 pages
Document
Coalgebraic Theory of Büchi and Parity Automata: Fixed-Point Specifications, Categorically (Invited Tutorial)
Author
Ichiro Hasuo 
-
Part of:
Volume:
29th International Conference on Concurrency Theory (CONCUR 2018)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Concurrency Theory (CONCUR) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2018-08-31
File
Document Identifiers
Author Details
Cite AsGet BibTex
Ichiro Hasuo. Coalgebraic Theory of Büchi and Parity Automata: Fixed-Point Specifications, Categorically (Invited Tutorial). In 29th International Conference on Concurrency Theory (CONCUR 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 118, pp. 5:1-5:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)
https://doi.org/10.4230/LIPIcs.CONCUR.2018.5
https://doi.org/10.4230/LIPIcs.CONCUR.2018.5
Abstract
Coalgebra is a categorical modeling of state-based dynamics. Final coalgebras - as categorical greatest fixed points - play a central role in the theory; somewhat analogously, most coalgebraic proof techniques have been devoted to greatest fixed-point properties such as safety and bisimilarity. In this tutorial, I introduce our recent coalgebraic framework that accommodates those fixed-point specifications which are not necessarily the greatest. It does so specifically by characterizing the accepted languages of Büchi and parity automata in categorical terms. We present two characterizations of accepted languages. The proof for their coincidence offers a unique categorical perspective of the correspondence between (logical) fixed-point specifications and the (combinatorial) parity acceptance condition.
Subject Classification
ACM Subject Classification
- Theory of computation → Automata over infinite objects
Keywords
- Coalgebra
- category theory
- fixed-point logic
- automata
- Büchi automata
- parity automata
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- Corina Cîrstea. Canonical coalgebraic linear time logics. In Lawrence S. Moss and Pawel Sobocinski, editors, 6th Conference on Algebra and Coalgebra in Computer Science, CALCO 2015, June 24-26, 2015, Nijmegen, The Netherlands, volume 35 of LIPIcs, pages 66-85. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. URL: http://dx.doi.org/10.4230/LIPIcs.CALCO.2015.66.
-
Ichiro Hasuo, Bart Jacobs, and Ana Sokolova. Generic trace semantics via coinduction. Logical Methods in Comp. Sci., 3(4:11), 2007.
- Ichiro Hasuo, Shunsuke Shimizu, and Corina Cîrstea. Lattice-theoretic progress measures and coalgebraic model checking. In Rastislav Bodik and Rupak Majumdar, editors, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 718-732. ACM, 2016. URL: http://dx.doi.org/10.1145/2837614.2837673.
-
B. Jacobs. Trace semantics for coalgebras. In J. Adámek and S. Milius, editors, Coalgebraic Methods in Computer Science, volume 106 of Elect. Notes in Theor. Comp. Sci. Elsevier, Amsterdam, 2004.
- Bart Jacobs. Introduction to Coalgebra: Towards Mathematics of States and Observation, volume 59 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016. URL: http://dx.doi.org/10.1017/CBO9781316823187.
-
J. Power and D. Turi. A coalgebraic foundation for linear time semantics. In Category Theory and Computer Science, volume 29 of Elect. Notes in Theor. Comp. Sci. Elsevier, Amsterdam, 1999.
-
J. J. M. M. Rutten. Universal coalgebra: a theory of systems. Theor. Comp. Sci., 249:3-80, 2000.
-
Natsuki Urabe and Ichiro Hasuo. Categorical Büchi and parity conditions via alternating fixed points of functors. In Corina Cîrstea, editor, Proc. Coalgebraic Methods in Computer Science - 14th IFIP WG 1.3 International Workshop, CMCS 2018, Lect. Notes Comp. Sci., 2018. to appear, preprint available at ěrb|arxiv.org/abs/1803.06811|.
-
Natsuki Urabe, Shunsuke Shimizu, and Ichiro Hasuo. Coalgebraic theory of Büchi and parity automata: Fixed-point specifications, categorically (tentative). forthcoming.
-
Natsuki Urabe, Shunsuke Shimizu, and Ichiro Hasuo. Coalgebraic trace semantics for buechi and parity automata. In Josée Desharnais and Radha Jagadeesan, editors, 27th International Conference on Concurrency Theory, CONCUR 2016, August 23-26, 2016, Québec City, Canada, volume 59 of LIPIcs, pages 24:1-24:15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016.