Coalgebraic CTL: Fixpoint Characterization and Polynomial-Time Model Checking

We introduce a path-based coalgebraic temporal logic, Coalgebraic CTL (CCTL), as a categorical abstraction of standard Computation Tree Logic (CTL). Our logic can be used to formalize properties of systems modeled as coalgebras with branching. We present the syntax and path-based semantics of CCTL, and show how to encode this logic into a coalgebraic fixpoint logic with a step-wise semantics. Our main result shows that this encoding is semantics-preserving. We also present a polynomial-time model-checking algorithm for CCTL, inspired by the standard model-checking algorithm for CTL but described in categorical terms. A key contribution of our paper is to identify the categorical essence of the standard encoding of CTL into the modal mu-calculus. This categorical perspective also explains the absence of a similar encoding of PCTL (Probabilistic CTL) into the probabilistic mu-calculus.