The Least Fibred Lifting and the Expressivity of Coalgebraic Modal Logic

Every endofunctor B on the category Set can be lifted to a fibred functor on the category (fibred over Set) of equivalence relations and relation-preserving functions. In this paper, the least (fibre-wise) of such liftings, L(B), is characterized for essentially any B. The lifting has all the useful properties of the relation lifting due to Jacobs, without the usual assumption of weak pullback preservation; if B preserves weak pullbacks, the two liftings coincide. Equivalence relations can be viewed as Boolean algebras of subsets (predicates, tests). This correspondence relates L(B) to the least test suite lifting T(B), which is defined in the spirit of predicate lifting as used in coalgebraic modal logic. Properties of T(B) translate to a general expressivity result for a modal logic for B-coalgebras. In the resulting logic, modal operators of any arity can appear.

• Type: Conference
• Year: 2005
• Where: CALCO
• Authors: Bartek Klin
• Keywords: CALCO 2005, Equivalence Relations, Modal Logic, Weak Pullbacks