The Coalgebra Day is an annual informal meeting of researchers in coalgebra between academic institutions in the Netherlands. This years meeting is held in Amsterdam and organised by Yde Venema, Vincenzo Ciancia, and Raul Leal.

At this meeting I will give a talk on my recent work on infinite trace semantics of coaglebras with branching and transition type. The work extends my previous work with Alexander Kurz on generic trace logics and generalises previous work of Bart Jacobs on trace semantics of coalgebras.

Title: Infinite Traces through 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 an additional structuring
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 as (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 give a first exposition of 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. In particular cases we can reconstruct a coalgebra
structure on the codomain of infinite trace semantics. The coalgebra structure
is not final, as infinite trace semantics is not unique.

The most prominent application of infinite trace semantics is in the language
theory of automata. We show that the acceptance behaviour of non-deterministic
coalgebra automata is an infinite trace semantics. The infinite trace semantics
of Jacobs arises as a special case where the automata have a trivial acceptance
condition.