Sciweavers

Share
ENTCS
2006

Generic Trace Theory

8 years 10 months ago
Generic Trace Theory
Trace semantics has been defined for various non-deterministic systems with different input/output types, or with different types of "non-determinism" such as classical non-determinism (with a set of possible choices) vs. probabilistic nondeterminism. In this paper we claim that these various forms of "trace semantics" are instances of a single categorical construction, namely coinduction in a Kleisli category. This claim is based on our main technical result that an initial algebra in the category of sets and functions yields a final coalgebra in the Kleisli category, for monads with a suitable order structure. The proof relies on coincidence of limits and colimits, like in the work of Smyth and Plotkin. Key words: coalgebra, trace semantics, linear time semantics, monad, Kleisli category, non-determinism, probability
Ichiro Hasuo, Bart Jacobs, Ana Sokolova
Added 12 Dec 2010
Updated 12 Dec 2010
Type Journal
Year 2006
Where ENTCS
Authors Ichiro Hasuo, Bart Jacobs, Ana Sokolova
Comments (0)
books