Document Open Access Logo

Coalgebraic Theory of Büchi and Parity Automata: Fixed-Point Specifications, Categorically (Invited Tutorial)

Author Ichiro Hasuo

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2018.5.pdf
  • Filesize: 225 kB
  • 2 pages

Document Identifiers

Author Details

Ichiro Hasuo
  • National Institute of Informatics, Japan

Funding

Supported by ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603), JST; Grants-in-Aid No. 15KT0012 & 15K11984, JSPS; and the JSPS-INRIA Bilateral Joint Research Project "CRECOGI."

Cite As Get 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

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)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. 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.
  2. Ichiro Hasuo, Bart Jacobs, and Ana Sokolova. Generic trace semantics via coinduction. Logical Methods in Comp. Sci., 3(4:11), 2007. Google Scholar
  3. 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.
  4. 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. Google Scholar
  5. 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.
  6. 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. Google Scholar
  7. J. J. M. M. Rutten. Universal coalgebra: a theory of systems. Theor. Comp. Sci., 249:3-80, 2000. Google Scholar
  8. 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|. Google Scholar
  9. Natsuki Urabe, Shunsuke Shimizu, and Ichiro Hasuo. Coalgebraic theory of Büchi and parity automata: Fixed-point specifications, categorically (tentative). forthcoming. Google Scholar
  10. 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. Google Scholar
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