We have defined a generic expression language for behaviours of finite
set coalgebras based on predicate liftings, specifically on a strongly
expressive set of singleton-preserving predicate liftings. There are
mutual conversions between such sets of predicate liftings and functor
presentations, one direction being via the Moss liftings introduced by
Marti and Venema [1]}; we have however demonstrated that
these fail to be mutually inverse in one direction, i.e. in general
not all singleton-preserving predicate liftings are Moss liftings. Our
language is presumably equivalent to the set-based instance of Myer's
expression language [2]}; our alternative presentation is aimed
primarily at showing that expression languages embed naturally into
the coalgebraic \(\mu \) -calculus, generalizing well-known results on the
relational
\(\mu \) -calculus [3]}, [4]}, [5]}, [6]}. The
benefit of this insight is to tighten the connection between
expression languages and specification logics, e.g. it allows for
combining model checking, equivalence checking, and reasoning within a
single formalism. On a more technical note, we show, e.g., that one
can provide an alternative semantics of expressions by defining a
coalgebra structure on expressions, an approach pioneered by Silva et
al. [7]} and used also by Myers [2]}; in the light
of the expressions/logic correspondence, this construction is now seen
as a canonical model construction for a fragment of the coalgebraic
\(\mu \) -calculus, and the core part of the proof that the two semantics
agree becomes just a truth lemma.
