A Categorical Approach to Coalgebraic Fixpoint Logic
Ezra Schoen, Clemens Kupke, Jurriaan Rot, Ruben Turkenburg
TL;DR
The paper addresses how to give a generic, abstract treatment of alternation-free coalgebraic fixpoint logics within a purely categorical setting. It introduces unfolding systems in order-enriched categories to define a least-solution semantics and an initial algebra semantics, and proves their equivalence. It then shows how to instantiate the framework to the positive coalgebraic $\mu$-calculus, PDL, and probabilistic logics, and outlines a method to add negations while preserving an initial-algebra semantics. The resulting approach provides a unified, diagrammatic foundation for invariance under behavioural equivalence and sets the stage for further proof-theoretic developments and filtrations across a range of coalgebraic logics.
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 $μ$-calculus in this framework, as well as PDL and a logic with a probabilistic dynamic modality.