Generic Trace Semantics via Coinduction

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 mathematicalstructure behind these "trace semantics," namely coinduction in a Kleislicategory. This claim is based on our technical result that, under a suitablyorder-enriched setting, a final coalgebra in a Kleisli category is given by aninitial algebra in the category Sets. Formerly the theory of coalgebras hasbeen employed mostly in Sets where coinduction yields a finer process semanticsof bisimilarity. Therefore this paper extends the application field ofcoalgebras, providing a new instance of the principle "process semantics viacoinduction."Comment: To appear in Logical Methods in Computer Science. 36 page