TY - GEN
T1 - Generic trace semantics and graded monads
AU - Milius, Stefan
AU - Pattinson, Dirk
AU - Schröder, Lutz
N1 - Publisher Copyright:
© Stefan Milius, Dirk Pattinson, and Lutz Schröder; licensed under Creative Commons License CC-BY.
PY - 2015/10/1
Y1 - 2015/10/1
N2 - 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.
AB - 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.
KW - Coalgebra
KW - Monads
KW - Trace logics
KW - Traces
KW - Transition systems
UR - http://www.scopus.com/inward/record.url?scp=84958232957&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.CALCO.2015.253
DO - 10.4230/LIPIcs.CALCO.2015.253
M3 - Conference contribution
T3 - Leibniz International Proceedings in Informatics, LIPIcs
SP - 253
EP - 269
BT - 6th Conference on Algebra and Coalgebra in Computer Science, CALCO 2015
A2 - Moss, Lawrence S.
A2 - Sobocinski, Pawel
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 6th Conference on Algebra and Coalgebra in Computer Science, CALCO 2015
Y2 - 24 June 2015 through 26 June 2015
ER -