Generic Trace Semantics and Graded Monads
Models of concurrent systems employ a wide variety of semantics inducing various notions of process equivalence, ranging from linear-time semantics such as trace equivalence to branching-time semantics such as strong bisimilarity. Many of these generalize to system types beyond standard transition systems, featuring, for example, weighted, probabilistic, or game-based transitions; this motivates the search for suitable coalgebraic abstractions of process equivalence that cover these orthogonal dimensions of generality, i.e. are generic both in the system type and in the notion of system equivalence. In recent joint work with Kurz, we have proposed a parametrization of system equivalence over an embedding of the coalgebraic type functor into a monad. In the present paper, we refine this abstraction to use graded monads, which come with a notion of depth that corresponds, e.g., to trace length or bisimulation depth. We introduce a notion of graded algebras and show how they play the role of formulas in trace logics.
transition systems
monads
coalgebra
trace logics
253-269
Regular Paper
Stefan
Milius
Stefan Milius
Dirk
Pattinson
Dirk Pattinson
Lutz
Schröder
Lutz Schröder
10.4230/LIPIcs.CALCO.2015.253
Luca Aceto, Anna Ingólfsdóttir, Kim Larsen, and Jiři Srba. Reactive systems: modelling, specification and verification. Cambridge Univ. Press, 2007.
Jiř\'ıAdámek, Jiř\'ıRosický, and Enrico Vitale. Algebraic Theories. Cambridge Univ. Press, 2011.
Marco Bernardo and Stefania Botta. A survey of modal logics characterising behavioural equivalences for non-deterministic and stochastic systems. Math. Struct. Comput. Sci., 18:29-55, 2008.
Nick Bezhanishvili and Silvio Ghilardi. The bounded proof property via step algebras and step frames. Ann. Pure Appl. Logic, 165:1832-1863, 2014.
Marcello Bonsangue, Stefan Milius, and Alexandra Silva. Sound and complete axiomatizations of coalgebraic language equivalence. ACM Trans. Comput. Log., 14, 2013.
Ivan Christoff. Testing equivalences and fully abstract models for probabilistic processes. In Theories of Concurrency, CONCUR 1990, volume 458 of LNCS, pages 126-140. Springer, 1990.
Corina Cîrstea. A coalgebraic approach to linear-time logics. In Foundations of Software Science and Computation Structures, FoSSaCS 2014, volume 8412 of LNCS, pages 426-440. Springer, 2014.
Corina Cîrstea. Canonical coalgebraic linear time logics. In Proc. CALCO, 2015. This volume.
Silvio Ghilardi. An algebraic theory of normal forms. Ann. Pure Appl. Logic, 71:189-245, 1995.
Valentin Goranko and Martin Otto. Model theory of modal logic. In P. Blackburn, J. van Benthem, and F. Wolter, editors, Handbook of Modal Logic, pages 249-329. Elsevier, 2006.
Daniel Gorín and Lutz Schröder. Simulations and bisimulations for coalgebraic modal logics. In Algebra and Coalgebra in Computer Science, CALCO 2013, volume 8089 of LNCS, pages 253-266. Springer, 2013.
Ichiro Hasuo, Bart Jacobs, and Ana Sokolova. Generic trace semantics via coinduction. Log. Meth. Comput. Sci., 3, 2007.
Antony Hoare. Communicating sequential processes. Prentice Hall, 1985.
Bart Jacobs, Alexandra Silva, and Ana Sokolova. Trace semantics via determinization. In Coalgebraic Methods in Computer Science, CMCS 2012, volume 7399 of LNCS, pages 109-129. Springer, 2012.
Peter Johnstone. Adjoint lifting theorems for categories of algebras. Bull. London Math. Soc., 7:294-297, 1975.
Shin-ya Katsumata. Parametric effect monads and semantics of effect systems. In Principles of Programming Languages, POPL 2014, pages 633-646. ACM, 2014.
Christian Kissig and Alexander Kurz. Generic trace logics. arXiv preprint 1103.3239, 2011.
Bartek Klin and Juriaan Rot. Coalgebraic trace semantics via forgetful logics. In Foundations of Software Science and Computation Structures, FoSSaCS'15, 2015.
Alexander Kurz, Stefan Milius, Dirk Pattinson, and Lutz Schröder. Simplified coalgebraic trace equivalence. In Software, Services, and Systems, volume 8950 of LNCS, pages 75-90. Springer, 2015.
A. Mazurkiewicz. Concurrent Program Schemes and Their Interpretation. Aarhus University, Comp. Sci. Depart., DAIMI PB-78, July 1977.
P.-A. Mellies. The parametric continuation monad. Preprint, 2015.
Eugenio Moggi. Notions of computation and monads. Inf. Comput., 93:55-92, 1991.
Philip Mulry. Lifting theorems for Kleisli categories. In Mathematical Foundations of Programming Semantics, MFPS 1993, volume 802 of LNCS, pages 304-319. Springer, 1994.
D. Pattinson. Expressive logics for coalgebras via terminal sequence induction. Notre Dame J. Formal Logic, 45:19-33, 2004.
J. Rutten. Universal coalgebra: A theory of systems. Theor. Comput. Sci., 249:3-80, 2000.
L. Schröder and D. Pattinson. PSPACE bounds for rank-1 modal logics. ACM Trans. Comput. Log., 10:13:1-13:33, 2009.
L. Schröder and D. Pattinson. Rank-1 modal logics are coalgebraic. J. Log. Comput., 20, 2010.
Lutz Schröder. Expressivity of coalgebraic modal logic: The limits and beyond. Theor. Comput. Sci., 390:230-247, 2008.
Lutz Schröder and Dirk Pattinson. Coalgebraic correspondence theory. In Foundations of Software Structures and Computer Science, FoSSaCS 2010, volume 6014 of LNCS, pages 328-342. Springer, 2010.
Alexandra Silva, Filippo Bonchi, Marcello Bonsangue, and Jan Rutten. Generalizing determinization from automata to coalgebras. Log. Meth. Comput. Sci, 9(1:9), 2013.
A. Smirnov. Graded monads and rings of polynomials. J. Math. Sci., 151:3032-3051, 2008.
Sam Staton. Relating coalgebraic notions of bisimulation. Log. Meth. Comput. Sci., 7, 2011.
Rob van Glabbeek. The linear time-branching time spectrum (extended abstract). In Theories of Concurrency, CONCUR'90, volume 458 of LNCS, pages 278-297. Springer, 1990.
James Worrell. On the final sequence of a finitary set functor. Theor. Comput. Sci., 338:184-199, 2005.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode