Related Work   As mentioned above, we owe much to work
by Marti and Venema on Moss liftings [1]}, and moreover
we use a notion of
\(\Lambda \) -bisimulation [2]} that turns out
to be an instance of their definition of bisimulation via lax
extensions. Besides the mentioned work on generic expression
languages for Kripke polynomial [3]},
weighted [4]}, and finitary [5]} functors, there
is work on expression languages for reactive
\(T\) -automata [6]}, which introduce an orthogonal
dimension of genericity: The coalgebra functor as such remains fixed
but the computational capacities of the automaton model at hand are
encapsulated as a computational
monad [7]}. Venema [8]} proves that for
weak-pullback preserving fuctors, every bisimilarity class of finite
coalgebras is expressible in coalgebraic fixpoint logic over Moss'
\(\nabla \)  modality.
