Generic Trace Logics

Finite trace semantics is known and well understood for classical automata and non-deterministic labelled transition systems. Jacobs et al introduced a more general definition for coalgebras which are structured in a branching type in addition to the transition type, and generalise non-deterministic and probabilistic state based transition structures. In this work we propose a class of coalgebraic logics which adequately and expressively characterise finite trace semantics and have a compositional semantics. We obtain generic trace logics from a dual adjunction on the Eilenberg-Moore category of the monad embodying the branching type.

• Type: Journal
• Year: 2011
• Where: CORR
• Authors: Christian Kissig, Alexander Kurz
• Keywords: Branching Type, CORR 2011, Education, Non-deterministic Labelled Transition, Trace Semantics