Coalgebraic trace semantics via forgetful logics. (English) Zbl 1445.68129
Summary: We use modal logic as a framework for coalgebraic trace semantics, and show the flexibility of the approach with concrete examples such as the language semantics of weighted, alternating and tree automata, and the trace semantics of generative probabilistic systems. We provide a sufficient condition under which a logical semantics coincides with the trace semantics obtained via a given determinization construction. Finally, we consider a condition that guarantees the existence of a canonical determinization procedure that is correct with respect to a given logical semantics. That procedure is closely related to Brzozowski’s minimization algorithm.
MSC:
| 68Q55 | Semantics in the theory of computing |
| 03B45 | Modal logic (including the logic of norms) |
| 03G30 | Categorical logic, topoi |
References:
| [1] | J. Ad’amek, F. Bonchi, M. H”ulsbusch, B. K”onig, S. Milius, and A. Silva. A coalgebraic perspective on minimization and determinization. In Procs. FoSSaCS 2012, volume 7213 of LNCS, pages 58–73, 2012. · Zbl 1352.68171 |
| [2] | N. Bezhanishvili, C. Kupke, and P. Panangaden. Minimization via duality. In Procs. WoLLIC 2012, volume 7456 of LNCS, pages 191–205, 2012. · Zbl 1361.68157 |
| [3] | F. Bonchi, M. M. Bonsangue, H. H. Hansen, P. Panangaden, J. J. M. M. Rutten, and A. Silva. Algebracoalgebra duality in Brzozowski’s minimization algorithm. ACM Trans. Comput. Log., 15(1):3, 2014. · Zbl 1288.68174 |
| [4] | J. Brzozowski. Canonical regular expressions and minimal state graphs for definite events. Mathematical Theory of Automata, 12:529–561, 1962. |
| [5] | L-T. Chen and A. Jung. On a categorical framework for coalgebraic modal logic. Electr. Notes Theor. Comput. Sci., 308:109–128, 2014. · Zbl 1337.03091 |
| [6] | C. Cırstea. From branching to linear time, coalgebraically. In Procs. FICS 2013, volume 126 of EPTCS, pages 11–27, 2013. |
| [7] | C. Cırstea. A coalgebraic approach to linear-time logics. In Procs. FoSSaCS 2014, volume 8412 of LNCS, pages 426–440, 2014. · Zbl 1405.68192 |
| [8] | C. Cirstea. Canonical Coalgebraic Linear Time Logics. In Procs. CALCO 2015, volume 35 of Leibniz International Proceedings in Informatics (LIPIcs), pages 66–85, 2015. · Zbl 1366.03242 |
| [9] | C. Cırstea and D. Pattinson. Modular construction of modal logics. In Procs. CONCUR 2004, volume 3170 of LNCS, pages 258–275, 2004. · Zbl 1099.03018 |
| [10] | E. J. Dubuc. Kan extensions in enriched category theory. Lecture notes in mathematics. Springer, 1970. · Zbl 0228.18002 |
| [11] | S. Goncharov. Trace semantics via generic observations. In Procs. CALCO 2013, volume 8089 of LNCS, pages 158–174, 2013. · Zbl 1394.68218 |
| [12] | I. Hasuo, B. Jacobs, and A. Sokolova. Generic trace semantics via coinduction. Log. Meth. Comp. Sci., 3(4), 2007. · Zbl 1131.68058 |
| [13] | C. Hermida and B. Jacobs. Structural induction and coinduction in a fibrational setting. Inf. and Comp., 145:107–152, 1997. · Zbl 0941.18006 |
| [14] | B. Jacobs. Introduction to coalgebra. Towards mathematics of states and observations, 2014. Draft. |
| [15] | B. Jacobs and J. Mandemaker. Coreflections in algebraic quantum logic. Foundations of Physics, 42(7):932–958, 2012. · Zbl 1259.81010 |
| [16] | B. Jacobs, A. Silva, and A. Sokolova. Trace semantics via determinization. J. Comput. Syst. Sci., 81(5):859–879, 2015. · Zbl 1327.68158 |
| [17] | B. Jacobs and A. Sokolova. Exemplaric expressivity of modal logics. J. Log. and Comput., 20(5):1041– · Zbl 1234.03009 |
| [18] | P. Johnstone. Adjoint lifting theorems for categories of algebras. Bulletin of the London Mathematical Society, 7:294–297, 1975. · Zbl 0315.18004 |
| [19] | C. Kissig and A. Kurz. Generic trace logics. CoRR, abs/1103.3239, 2011. |
| [20] | B. Klin. Coalgebraic modal logic beyond sets. ENTCS, 173:177–201, 2007. · Zbl 1316.03017 |
| [21] | B. Klin and J. Rot. Coalgebraic trace semantics via forgetful logics. In FoSSaCS 2015. Proceedings, pages 151–166, 2015. · Zbl 1459.68114 |
| [22] | C. Kupke and D. Pattinson. Coalgebraic semantics of modal logics: An overview. Theor. Comput. Sci., 412(38):5070–5094, 2011. · Zbl 1360.03068 |
| [23] | A. Kurz, S. Milius, D. Pattinson, and L. Schr”oder. Simplified coalgebraic trace equivalence. In Software, Services, and Systems - Essays Dedicated to Martin Wirsing on the Occasion of His Retirement from the Chair of Programming and Software Engineering, pages 75–90, 2015. · Zbl 1453.68112 |
| [24] | S. Mac Lane. Categories for the working mathematician, volume 5. Springer, 1998. · Zbl 0906.18001 |
| [25] | M. Lenisa, J. Power, and H. Watanabe. Category theory for operational semantics. Theor. Comput. Sci., 327(1-2):135–154, 2004. · Zbl 1071.68059 |
| [26] | E. Manes. Monads of sets. Handbook of algebra, 3:67–153, 2003. · Zbl 1064.18003 |
| [27] | E. Manes and P. Mulry. Monad compositions I: general constructions and recursive distributive laws. Theory and Applications of Categories, 18(7):172–208, 2007. · Zbl 1131.18003 |
| [28] | S. Milius, D. Pattinson, and L. Schr”oder. Generic Trace Semantics and Graded Monads. In Procs. CALCO 2015, volume 35 of Leibniz International Proceedings in Informatics (LIPIcs), pages 253–269, 2015. · Zbl 1366.68211 |
| [29] | D. Pavlovic, M. Mislove, and J. Worrell. Testing semantics: Connecting processes and process logics. In AMAST 2006, volume 4019 of LNCS, pages 308–322, 2006. · Zbl 1236.68065 |
| [30] | J. Power and D. Turi. A coalgebraic foundation for linear time semantics. ENTCS, 29:259–274, 1999. · Zbl 0967.68102 |
| [31] | J. J. M. M. Rutten. Universal coalgebra: a theory of systems. Theor. Comput. Sci., 249(1):3–80, 2000. · Zbl 0951.68038 |
| [32] | L. Schr”oder and D. Pattinson. Modular algorithms for heterogeneous modal logics via multi-sorted coalgebra. Math. Struct. in Comp. Sci., 21(2):235–266, 2011. · Zbl 1260.03061 |
| [33] | A. Silva, F. Bonchi, M. M. Bonsangue, and J. J. M. M. Rutten. Generalizing determinization from automata to coalgebras. Log. Meth. Comp. Sci., 9(1), 2013. · Zbl 1262.18002 |
| [34] | R.J. van Glabbeek, S.A. Smolka, and B. Steffen. Reactive, generative, and stratified models of probabilistic processes. Information and Computation, 121(1):59 – 80, 1995. · Zbl 0832.68042 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
