Summary: Recent progress on defining abstract trace semantics for coalgebras rests upon two observations: (i) coalgebraic bisimulation for deterministic automata coincides with trace equivalence, and (ii) the classical powerset construction for automata determinization instantiates the generic idea of lifting a functor to the Eilenberg-Moore category of an appropriate monad \(\mathbb{T}\). We take this approach one step further by rebasing the latter kind of trace semantics on the novel notion of \(\mathbb{T}-observer\), which is just a certain natural transformation of the form \(F \rightarrow GT\), and thus allowing for elimination of assumptions about the structure of the coalgebra functor. As a specific application of this idea we demonstrate how it can be used for capturing trace semantics of push-down automata. Furthermore, we show how specific forms of observers can be used for coalgebra-based treatment of internal automata transitions as well as weak bisimilarity of processes.
For the entire collection see [Zbl 1271.68041].