specifically into (the conjunctive fragment of) the coalgebraic
\(\mu \) -calculus [1]}, extending the classical result that
every bisimilarity class of states in finite labelled transition
systems is expressible by a characteristic formula in the
\(\mu \) -calculus [2]}, [3]}, [4]}, [5]}. This
result provides a direct link between descriptions of processes and
their property-oriented specification; as indicated above, the key
to lifting it to a coalgebraic level of generality are
singleton-preserving predicate liftings.
