A Categorical Approach to Coalgebraic Fixpoint Logic

TL;DR

This paper develops a categorical framework for coalgebraic fixpoint logics, unifying semantics and extending to various modal and probabilistic logics.

Contribution

It introduces a novel order-enriched categorical approach to coalgebraic fixpoint logics, establishing semantics equivalence and integrating multiple modal logics.

Findings

Established equivalence of least-solution and initial algebra semantics

Placed the coalgebraic μ-calculus within the framework

Extended the framework to probabilistic and dynamic modalities

Abstract

We define a framework for incorporating alternation-free fixpoint logics into the dual-adjunction setup for coalgebraic modal logics. We achieve this by using order-enriched categories. We give a least-solution semantics as well as an initial algebra semantics, and prove they are equivalent. We also show how to place the alternation-free coalgebraic $\mu$-calculus in this framework, as well as PDL and a logic with a probabilistic dynamic modality.