Generic Trace Semantics via Coinduction

TL;DR

This paper unifies various trace semantics for state-based systems using coinduction in Kleisli categories, extending coalgebra theory to encompass different forms of branching such as non-determinism and probability.

Contribution

It establishes a general mathematical framework linking trace semantics to coinduction in Kleisli categories, broadening coalgebra applications beyond Sets.

Findings

Final coalgebra in Kleisli category equals initial algebra in Sets under certain conditions

Unified approach applies to non-deterministic and probabilistic systems

Extends coalgebra theory to encompass trace semantics with branching

Abstract

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."