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开发的现有求解器，实现了概率情形的自动化求解器。据我们所知，这是首个针对带递归的概率高阶程序的线性时序验证的自动化验证器。