We propose a categorical framework for linear-time temporal verification of effectful higher-order programs, including probabilistic higher-order programs. Our framework provides a generic denotational reduction -- namely, a denotational product construction -- from linear-time safety verification of effectful higher-order programs to computation of weakest pre-conditions of product programs. This reduction enables us to apply existing algorithms for such well-studied computations of weakest pre-conditions, some of which are available as off-the-shelf solvers. We show the correctness of our denotational product construction by proving a preservation theorem under strong monad morphisms and an existence of suitable liftings along a fibration. We instantiate our framework with both probabilistic and angelic nondeterministic higher-order programs, and implement an automated solver for the probabilistic case based on the existing solver developed by Kura and Unno. To the best of our knowledge, this is the first automated verifier for linear-time temporal verification of probabilistic higher-order programs with recursion.

翻译：我们提出了一种用于效应高阶程序（包括概率高阶程序）线性时序验证的范畴论框架。该框架提供了一种通用的指称归约——即指称积构造——将效应高阶程序的线性时序安全性验证归约为积程序最弱前置条件的计算。这一归约使我们能够应用现有算法来处理此类经过充分研究的最弱前置条件计算，其中部分算法可作为现成求解器使用。我们通过证明在强单子态射下的保持定理以及沿着纤维化的合适提升的存在性，展示了我们指称积构造的正确性。我们使用概率性和天使非确定性高阶程序实例化了该框架，并基于Kura和Unno开发的现有求解器实现了概率情形的自动化求解器。据我们所知，这是首个支持递归概率高阶程序线性时序验证的自动化验证器。