| Summary: | Trace semantics has been defined for various kinds of state-based systems,
notably with different forms of branching such as non-determinism vs.
probability. In this paper we claim to identify one underlying mathematical
structure behind these "trace semantics," namely coinduction in a Kleisli
category. This claim is based on our technical result that, under a suitably
order-enriched setting, a final coalgebra in a Kleisli category is given by an
initial algebra in the category Sets. Formerly the theory of coalgebras has
been employed mostly in Sets where coinduction yields a finer process semantics
of bisimilarity. Therefore this paper extends the application field of
coalgebras, providing a new instance of the principle "process semantics via
coinduction."
|
|---|