Der Koalgebratag ist ein jaehrliches informelles Treffen zwischen verschiedenen akademischen Institutionen in den Niederlanden. Das Treffen in diesem Jahr findet in Amsterdam statt und wird organisiert von Yde Venema, Vincenzo Ciancia, und Raul Leal.

Zu diesem Treffen stelle ich meine neuere Arbeit zu unendlichen Traces in Koalgebren vor. In dieser Arbeit setze ich das gemeinsame Projekt zu koalgebraischen Trace Logiken mit Alexander Kurz fort, und erweitere eine fruehere Publikation von Bart Jacobs zur unendlichen Trace Semantik nicht-deterministischer Koalgebren.

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.