From T-Coalgebras to Filter Structures and Transition Systems

Abstract. For any set-endofunctor T : Set → Set there exists a largest subcartesian transformation µ to the filter functor F : Set → Set. Thus we can associate with every T-coalgebra A a certain filter-coalgebra AF. Precisely, when T weakly preserves preimages, µ is natural, and when T weakly preserves intersections, µ factors through the covariant powerset functor P, thus providing for every T-coalgebra A a Kripke structure AP. The paper characterizes weak preservation of preimages, of intersections, and preservation of both preimages and intersections by a functor T via the existence of transformations from T to either F or P. Moreover, we define for arbitrary T-coalgebras A a next-time operator A with associated modal operators 2 and 3 and relate their properties to weak limit preservation properties of T. In particular, for any T-coalgebra A there is a transition system K with A = K if and only if T weakly preserves intersections.

• Type: Conference
• Year: 2005
• Where: CALCO
• Authors: H. Peter Gumm
• Keywords: CALCO 2005, Covariant Powerset Functor, Largest Subcartesian Transformation, filter Functor