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可编码为不动点模态逻辑。