Title: Generic Trace Logics

Abstract: Finite trace semantics is well-understood as a suitable semantics for non-deterministic, prob-
abilistic, or graded transition systems. In their recent works on Generic Trace Theory have
Jacobs and collaborations proposed a uniform definition of finite trace semantics for Set-based
coalgebras with a branching structure given in terms of a monad, in addition to the transition
structure from a Set-functor.
In Generic Trace Theory, finite trace semantics is defined as a final coalgebra semantics
obtained by induction along the initial sequence. The construction relies on the limit-colimit-
coincidence of Smyth and Plotkin, and requires the monad to be such that the Kleisli-category
can be locally directed completely ordered.
We lift several of the assumptions made in generic trace theory, and obtain a slightly more
general definition of finite trace semantics which works also in the restricted settings of finite
non-deterministic and finitely graded branching.
Finite trace semantics induces finite trace equivalence. We propose a coalgebraic logic which
is invariant under finite trace equivalence, and, with additional assumptions made, finitely ex-
pressive and complete. We need to assume that the monad is commutative. We obtain generic
trace logics through an adjunction on the category of algebras for the branching monad, in the
spirit of coalgebraic modal logics of Pattinson and Schr ̈der.
o