This is joint work with Ichiro Hasuo (University of Nijmegen, The Netherlands, and Kyoto University, Japan) and Bart Jacobs (University of Nijmegen, The Netherlands)

Labelled transition systems (LTS) are a common model of concurrent systems. Semantic equivalences on LTS provide notions of behaviour. A way to verify correctness of a concurrent system with respect to a given semantics ~ is to model both the system (Sys) and the correctness property (Spec) as LTS and show that Sys ~ Spec. The spectrum of behaviour equivalences is rich, from the strongest—bisimilarity, to the weakest—trace semantics.

We work in the abstract setting of coalgebras which are generic (category theoretic) transition systems. They come equipped with a generic notion of bisimilarity obtained by coinduction. However, defining other semantics for coalgebras is not straightforward. We developed a theory of generic traces (applicable to certain coalgebras in an order enriched setting) which shows that trace equivalence is also obtained by coinduction while shifting the base category to a Kleisli category. The theory instantiates to both (possibilistic, standard) LTS and to probabilistic transition systems.

I will start the talk with a mild introduction to coalgebras and their behaviour semantics. Further, I will present the results leading to the generic trace theory.