preprint on behavioural covarieties available

preprint on behavioural covarieties available

[Rob Goldblatt]

[Resent message]

A preprint of a paper entitled

"A comonadic account of behavioural covarieties of coalgebras"

is available for downloading as a pdf file from

www.mcs.vuw.ac.nz/~rob

Rob Goldblatt


ABSTRACT
A class $K$ of coalgebras for an endofunctor $T:\Set\to\Set$ is a
\textit{behavioural covariety}
if it is closed under disjoint unions and images of bisimulation
relations (hence closed under
images and domains of coalgebraic morphisms, including subcoalgebras).
$K$ may be thought of as
the class of all coalgebras that satisfy some computationally
significant property. In any logical system suitable for specifying
properties of state-transition systems in the Hennessy-Milner style,
each formula will define a class of models that is a behavioural
variety.

Assume that the forgetful functor on $T$-coalgebras has a right
adjoint, providing for
the construction of cofree coalgebras, and let $\G^T$ be the comonad
arising from this
adjunction. Then we show that behavioural covarieties $K$ are
(isomorphic to) the Eilenberg-Moore categories of coalgebras for
certain comonads $\G^K$ naturally associated with $\G^T$. These are
called \textit{pure subcomonads} of $\G^T$, and a categorical
characterization of them is given,
involving a pullback condition on the naturality squares of a
transformation from $\G^K$ to $\G^T$.

We show that  there is a bijective correspondence between behavioural
covarieties of $T$-coalgebras and isomorphism classes of pure
subcomonads of $\G^T$.