  The analysis of concurrent and reactive systems is based to a large degree on
various notions of process equivalence, ranging, on the so-called
linear-time/branching-time spectrum, from fine-grained equivalences such as
strong bisimilarity to coarse-grained ones such as trace equivalence. The
theory of concurrent systems at large has benefited from developments in
coalgebra, which has enabled uniform definitions and results that provide a
common umbrella for seemingly disparate system types including
non-deterministic, weighted, probabilistic, and game-based systems. In
particular, there has been some success in identifying a generic coalgebraic
theory of bisimulation that matches known definitions in many concrete cases.
The situation is currently somewhat less settled regarding trace equivalence. A
number of coalgebraic approaches to trace equivalence have been proposed, none
of which however cover all cases of interest; notably, all these approaches
depend on explicit termination, which is not always imposed in standard
systems, e.g. LTS. Here, we discuss a joint generalization of these approaches
based on embedding functors modelling various aspects of the system, such as
transition and braching, into a global monad; this approach appears to cover
all cases considered previously and some additional ones, notably standard LTS
and probabilistic labelled transition systems.
