We introduce continuation semantics for both fixpoint modal logic (FML) and Computation Tree Logic* (CTL*), parameterised by a choice of branching type and quantitative predicate lifting. Our main contribution is proving that they are equivalent to coalgebraic semantics, for all branching types. Our continuation semantics is defined over coalgebras of the continuation monad whose answer type coincides with the domain of truth values of the formulas. By identifying predicates and continuations, such a coalgebra has a canonical interpretation of the modality by evaluation of continuations. We show that this continuation semantics is equivalent to the coalgebraic semantics for fixpoint modal logic. We then reformulate the current construction for coalgebraic models of CTL*. These models are usually required to have an infinitary trace/maximal execution map, characterized as the greatest fixpoint of a special operator. Instead, we allow coalgebraic models of CTL* to employ non-maximal fixpoints, which we call execution maps. Under this reformulation, we establish a general result on transferring execution maps via monad morphisms. From this result, we obtain that continuation semantics is equivalent to the coalgebraic semantics for CTL*. We also identify a sufficient condition under which CTL can be encoded into fixpoint modal logic under continuation semantics.

翻译：本文针对不动点模态逻辑（FML）与计算树逻辑*（CTL*）引入了延续语义，其参数化依赖于分支类型与定量谓词提升的选择。我们的主要贡献在于证明：对于所有分支类型，该延续语义均等价于余代数语义。我们的延续语义定义在延续单子的余代数上，其应答类型与公式真值域一致。通过将谓词与延续相统一，此类余代数可通过延续求值对模态算子给出典范解释。我们证明该延续语义等价于不动点模态逻辑的余代数语义。随后，我们将现有构造重新表述为CTL*的余代数模型。这类模型通常要求具备无穷迹/极大执行映射，其特性可表征为特定算子的最大不动点。与之相对，我们允许CTL*的余代数模型采用非极大不动点，并将其称为执行映射。在此重构框架下，我们建立了关于通过单子态射传递执行映射的一般性结果。基于该结果，我们得出延续语义等价于CTL*的余代数语义的结论。同时，我们还确定了在延续语义下CTL可编码至不动点模态逻辑的充分条件。