Document Open Access Logo

Coalgebraic Trace Semantics for Buechi and Parity Automata

Authors Natsuki Urabe, Shunsuke Shimizu, Ichiro Hasuo

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2016.24.pdf
  • Filesize: 0.6 MB
  • 15 pages

Document Identifiers

Author Details

Natsuki Urabe
Shunsuke Shimizu
Ichiro Hasuo

Cite AsGet BibTex

Natsuki Urabe, Shunsuke Shimizu, and Ichiro Hasuo. Coalgebraic Trace Semantics for Buechi and Parity Automata. In 27th International Conference on Concurrency Theory (CONCUR 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 59, pp. 24:1-24:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.CONCUR.2016.24

Abstract

Despite its success in producing numerous general results on state-based dynamics, the theory of coalgebra has struggled to accommodate the Buechi acceptance condition---a basic notion in the theory of automata for infinite words or trees. In this paper we present a clean answer to the question that builds on the "maximality" characterization of infinite traces (by Jacobs and Cirstea): the accepted language of a Buechi automaton is characterized by two commuting diagrams, one for a least homomorphism and the other for a greatest, much like in a system of (least and greatest) fixed-point equations. This characterization works uniformly for the nondeterministic branching and the probabilistic one; and for words and trees alike. We present our results in terms of the parity acceptance condition that generalizes Buechi's.
Keywords
  • coalgebra
  • Buechi automaton
  • parity automaton
  • probabilistic automaton
  • tree automaton

Metrics

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

References

  1. Jir'1 Adámek, Filippo Bonchi, Mathias Hülsbusch, Barbara König, Stefan Milius, and Alexandra Silva. A coalgebraic perspective on minimization and determinization. In Proc. FoSSaCS'12, volume 7213 of LNCS, pages 58-73. Springer, 2012. URL: http://dx.doi.org/10.1007/978-3-642-28729-9_4.
  2. André Arnold and Damian Niwiński. Rudiments of μ-Calculus, volume 146 of Studies in Logic and the Foundations of Mathematics. North-Holland, 2001. URL: http://dx.doi.org/10.1016/S0049-237X(01)80001-X.
  3. Christel Baier and Marcus Größer. Recognizing omega-regular languages with probabilistic automata. In Proc. LICS'05, pages 137-146. IEEE Computer Society, 2005. URL: http://dx.doi.org/10.1109/LICS.2005.41,
  4. Arnaud Carayol, Axel Haddad, and Olivier Serre. Randomization in automata on infinite trees. ACM Trans. Comp. Logic, 15(3):24:1-24:33, 2014. URL: http://dx.doi.org/10.1145/2629336.
  5. Vincenzo Ciancia and Yde Venema. Stream automata are coalgebras. In Selected Papers of CMCS'12, volume 7399 of LNCS, pages 90-108. Springer, 2012. URL: http://dx.doi.org/10.1007/978-3-642-32784-1_6.
  6. Corina Cîrstea. Generic infinite traces and path-based coalgebraic temporal logics. Electr. Notes in Theor. Comp. Sci., 264(2):83-103, 2010. URL: http://dx.doi.org/10.1016/j.entcs.2010.07.015.
  7. Corina Cîrstea, Alexander Kurz, Dirk Pattinson, Lutz Schröder, and Yde Venema. Modal logics are coalgebraic. Comp. Journ., 54(1):31-41, 2011. URL: http://dx.doi.org/10.1093/comjnl/bxp004.
  8. Rance Cleaveland, Marion Klein, and Bernhard Steffen. Faster model checking for the modal mu-calculus. In Proc. CAV'92, volume 663 of LNCS, pages 410-422. Springer, 1992. URL: http://dx.doi.org/10.1007/3-540-56496-9_32.
  9. Ernst-Erich Doberkat. Stochastic Coalgebraic Logic. Monographs in Theoretical Computer Science. An EATCS Series. Springer, 2009. URL: http://dx.doi.org/10.1007/978-3-642-02995-0.
  10. Michèle Giry. Categorical aspects of topology and analysis. In A categorical approach to probability theory, an Intl. Conference at Carleton University, 1981, Proceedings, volume 915 of Lect. Notes in Math., pages 68-85. Springer, 1982. URL: http://dx.doi.org/10.1007/BFb0092872.
  11. Sergey Goncharov and Dirk Pattinson. Coalgebraic weak bisimulation from recursive equations over monads. In Proc. ICALP'14, Part II, volume 8573 of LNCS, pages 196-207. Springer, 2014. URL: http://dx.doi.org/10.1007/978-3-662-43951-7_17.
  12. Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors. Automata, Logics, and Infinite Games: A Guide to Current Research, volume 2500 of LNCS. Springer, 2002. URL: http://dx.doi.org/10.1007/3-540-36387-4.
  13. Ichiro Hasuo, Bart Jacobs, and Ana Sokolova. Generic trace semantics via coinduction. Logical Methods in Comp. Sci., 3(4):11:1-11:36, 2007. URL: http://dx.doi.org/10.2168/LMCS-3(4:11)2007.
  14. Ichiro Hasuo, Shunsuke Shimizu, and Corina Cîrstea. Lattice-theoretic progress measures and coalgebraic model checking. In Proc. POPL'16, pages 718-732. ACM, 2016. URL: http://dx.doi.org/10.1145/2837614.2837673.
  15. Bart Jacobs. Trace semantics for coalgebras. Electr. Notes in Theor. Comp. Sci., 106:167-184, 2004. URL: http://dx.doi.org/10.1016/j.entcs.2004.02.031.
  16. Bart Jacobs. Introduction to coalgebra. Towards mathematics of states and observations. Draft of a book (ver. 2.0), available online, 2012. URL: http://www.cs.ru.nl/B.Jacobs/CLG/JacobsCoalgebraIntro.pdf.
  17. Bart Jacobs, Alexandra Silva, and Ana Sokolova. Trace semantics via determinization. J. Comp. &Syst. Sci., 81(5):859-879, 2015. URL: http://dx.doi.org/10.1016/j.jcss.2014.12.005.
  18. Bartek Klin. Bialgebraic methods and modal logic in structural operational semantics. Inf. &Comp., 207(2):237-257, 2009. URL: http://dx.doi.org/10.1016/j.ic.2007.10.006.
  19. Nancy Lynch and Frits Vaandrager. Forward and backward simulations. Inf. &Comp., 121(2):214-233, 1995. URL: http://dx.doi.org/10.1006/inco.1995.1134.
  20. Philip S. Mulry. Lifting theorems for Kleisli categories. In Proc. MFPS'93, volume 802 of LNCS, pages 304-319. Springer, 1994. URL: http://dx.doi.org/10.1007/3-540-58027-1_15.
  21. John Power and Hayo Thielecke. Environments, continuation semantics and indexed categories. In Proc. TACS'97, volume 1281 of LNCS, pages 391-414. Springer, 1997. URL: http://dx.doi.org/10.1007/BFb0014560.
  22. Jan J. M. M. Rutten. Universal coalgebra: a theory of systems. Theor. Comp. Sci., 249(1):3-80, 2000. URL: http://dx.doi.org/10.1016/S0304-3975(00)00056-6.
  23. Christoph Schubert. Terminal coalgebras for measure-polynomial functors. In Proc. TAMC'09, volume 5532 of LNCS, pages 325-334. Springer, 2009. URL: http://dx.doi.org/10.1007/978-3-642-02017-9_35.
  24. Alexandra Silva. A short introduction to the coalgebraic method. ACM SIGLOG News, 2(2):16-27, April 2015. URL: http://dx.doi.org/10.1145/2766189.2766193.
  25. Natsuki Urabe and Ichiro Hasuo. Coalgebraic infinite traces and kleisli simulations. In Lawrence S. Moss and Pawel Sobocinski, editors, Proc. CALCO'15, volume 35 of LIPIcs, pages 320-335. Schloss Dagstuhl, 2015. URL: http://dx.doi.org/10.4230/LIPIcs.CALCO.2015.320.
  26. Natsuki Urabe and Ichiro Hasuo. Quantitative simulations by matrices. Inf. &Comp., 2016. In press. URL: http://dx.doi.org/10.1016/j.ic.2016.03.007.
  27. Natsuki Urabe, Shunsuke Shimizu, and Ichiro Hasuo. Coalgebraic trace semantics for Büchi and parity automata. arXiv preprint, 2016. Google Scholar
  28. Natsuki Urabe, Shunsuke Shimizu, and Ichiro Hasuo. Fair simulation for nondeterministic and probabilistic Büchi automata: a coalgebraic perspective. CoRR, abs/1606.04680, 2016. URL: http://arxiv.org/abs/1606.04680.
  29. R.J. van Glabbeek. The linear time - branching time spectrum I: The semantics of concrete, sequential processes. In J.A. BergstraA. PonseS.A. Smolka, editor, Handbook of Process Algebra, chapter 1, pages 3-99. Elsevier, 2001. URL: http://dx.doi.org/10.1016/B978-044482830-9/50019-9.
  30. Moshe Y. Vardi. An automata-theoretic approach to linear temporal logic. In Logics for Concurrency, the of 8th Banff Higher Order Workshop, 1995, Proceedings, volume 1043 of LNCS, pages 238-266. Springer, 1995. URL: http://dx.doi.org/10.1007/3-540-60915-6_6.
  31. Yde Venema. Automata and fixed point logic: A coalgebraic perspective. Inf. &Comp., 204(4):637-678, 2006. URL: http://dx.doi.org/10.1016/j.ic.2005.06.003.
  32. James Worrell. On the final sequence of a finitary set functor. Theor. Comp. Sci., 338(1-3):184-199, 2005. URL: http://dx.doi.org/10.1016/j.tcs.2004.12.009.
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 Imprint Privacy Contact