Hostname: page-component-7b7567c8c-fvjsw Total loading time: 0 Render date: 2026-11-12T08:57:52.990Z Has data issue: false hasContentIssue false

A comonadic account of behavioural covarieties of coalgebras

Published online by Cambridge University Press:  14 March 2005

ROBERT GOLDBLATT
Affiliation:
Centre for Logic, Language and Computation, Victoria University, P.O. Box 600, Wellington, New Zealand Email: Rob.Goldblatt@vuw.ac.nz
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

A class $K$ of coalgebras for an endofunctor $T\,{:}\,\Set\to\Set$ is a 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 covariety.

Assuming that the forgetful functor on $T$-coalgebras has a right adjoint, providing for the construction of cofree coalgebras, and letting $\G^T$ be the comonad arising from this adjunction, 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 pure subcomonads of $\G^T$, and a categorical characterisation of them is given that involves 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$.

Information

Type
Paper
Copyright
2005 Cambridge University Press