Finite trace semantics is well-understood as a suitable semantics for
non-deterministic, probabilistic, 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 $\mathit{Set}$-based coalgebras with
a branching structure given in terms of a monad, in addition to the
transition structure from a $\mathit{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 expressive 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\"oder.