Trace theory is concerned with assigning transition systems a semantics in trace monoids. Informally, trace monoids are word monoids generated from an independence relation, analogous to parallelism in concurrency. Generic trace theory seeks to extends trace theory to arbitrary transition systems, that formally are Set-based coalgebras.

Finite Trace Semantics for Coalgebras

Finite trace semantics is defined for (B,T)-coalgebras structured in a branching type, given by a Set-monad B, and a transition type, given by a Set-functor T. Monads are suitable branching types, because the unit defines a deterministic behaviour, and mutliplication contracts non-deterministic choices. For the latter one also needs a law distributing the transition behaviour over the branching behaviour.

The adjoint transpose of (B,T)-coalgebras in Set are coalgebras for the Kleisli-lifting of T in the Kleisli-category of B. [3] brings this idea further, interpreting (B,T)-coalgebras as T-coalgebras over free B-algebras.

Finite trace semantics are cones over the final T-sequences in B-Alg, the category of B-algebras. Full finite trace semantics exists if the final T-sequence terminates in countably many steps,  then finite trace semantics is the unique map into the final T-coalgebra.

Infinite Trace Semantics for Coalgebras

In recent work, I define infinite trace semantics in a generic form. Analogous to finite trace semantics, generic infinite trace semantics arises as cones over a (discrete) sequence for the functor T in the Kleisli-category. Contrary to finite trace semantics is that the sequence does not start with the initial (final) object, but with the B-algebra free over the singleton {*}. * (read: bud) expresses the unknown future, which is refined along the T-sequence.

There are obviously forgetful maps Tⁿ⁺¹{*}->Tⁿ{*} that make forget the last transition step, but not the last branching step, so that these cones do not commute with the sequence of these forgetful maps. To characterise the codomain of infinite trace semantics, I introduced a span which describes whether the continuation in a trace is plausible. The cones then commute with the forgetful maps laxly with respect to these spans. This yields the characterisation of the codomain of infinite trace semantics.

Then it turns out that finite trace semantics, the least, and generic infinite trace semantics, the greatest trace semantics, are both instances of infinite trace semantics.

The non-uniqueness of infinite trace semantics is also witnessed by the language theory of automata. These are pointed (P,T)-coalgebras with acceptance condition, where T is the transition type of the recognised class of input structures.  These ideas were first stated in Venema, Automata and Fixed Point Logics for Coalgebras. The acceptance condition determines which infinite traces of the transition structure of a coalgebra automaton are included.  We showed that the acceptance behaviour of a coalgebra automaton is an instance of infinite trace semantics.

Finite Trace Logics

In [3] we define finite trace logics from the adjoint transpose of the final T-coalgebra map under the adjunction induced by the ambimorphic object F1, the free B-algebra generated from a singleton 1. We use the insides of Klin (Coalgebra Modal Logics beyond Sets, 2007) to state properties of B and T under which finite trace logics are adequate and expressive.

People

• Ichiro Hasuo
• Bart Jacobs
• Alexander Kurz
• Ana Sokolova

Some Publications

1. B Jacobs, Trace Semantics for Coalgebras, 2004
2. B Jacobs, I Hasuo,  A Sokolova, Generic Trace Theory, 2006
3. C Kissig, A Kurz, Generic Trace Logics, 2010, submitted [Preprint]
4. C Kissig, Infinite Trace Semantics for Coalgebras, 2010, submitted [Preprint]

Talks

1. 03.03.2010, Infinite Traces through Coalgebras, Coalgebra Day, University of Amsterdam, NL [Slides]