This years BCTCS meeting will be held at the University of Edinburgh. I contribute a talk on the semantics of Set-based coalgebras with branching structure.

Title Trace Semantics of Coalgebras

Abstract Coalgebras for a functor T in the category Set of sets and functions generalise state-based and possibly non-terminating transition systems. Their semantics in the final T-coalgebra defines T-behaviour which identifies precisely T-bisimilar states. Previous work on generic trace theory has shown that structuring additionally in a Set-monad B introduces branching which subsumes non-determinism, probabilism and graded branching. We call coalgebras with branching type B and transition type T (B,T)-coalgebras. Semantics by BT-behaviour turns out to be unsuitable for (B,T)-coalgebras. Jacobs et al defined an alternative semantics by lifting into the Kleisli-category. The so obtained semantics is known as trace semantics. We distinguish semantics in finite and infinite traces. Jacobs gave a uniform definition for the first, but for the latter only in the case of non-deterministic branching. In this talk we present infinite trace semantics generic for a large class of branching and transition types. We characterise the codomain of infinite trace semantics as Cauchy converging sequences. The characterisation is based on a stratified axiomatisation of infinite traces from T-behaviour and a span which describes whether the continuation in a trace is plausible. Infinite trace semantics is not unique.