Probabilistic programs are a powerful and convenient approach to formalise distributions over system executions. A classical verification problem for probabilistic programs is temporal inference: to compute the likelihood that the execution traces satisfy a given temporal property. This paper presents a general framework for temporal inference, which applies to a rich variety of quantitative models including those that arise in the operational semantics of probabilistic and weighted programs. The key idea underlying our framework is that in a variety of existing approaches, the main construction that enables temporal inference is that of a product between the system of interest and the temporal property. We provide a unifying mathematical definition of product constructions, enabled by the realisation that 1) both systems and temporal properties can be modelled as coalgebras and 2) product constructions are distributive laws in this context. Our categorical framework leads us to our main contribution: a sufficient condition for correctness, which is precisely what enables to use the product construction for temporal inference. We show that our framework can be instantiated to naturally recover a number of disparate approaches from the literature including, e.g., partial expected rewards in Markov reward models, resource-sensitive reachability analysis, and weighted optimization problems. Further, we demonstrate a product of weighted programs and weighted temporal properties as a new instance to show the scalability of our approach.

翻译：概率程序是形式化系统执行分布的一种强大而便捷的方法。概率程序的一个经典验证问题是时序推断：计算执行轨迹满足给定时序属性的可能性。本文提出了一个适用于时序推断的通用框架，该框架可应用于包括概率与加权程序操作语义中产生的各类定量模型。我们框架的核心思想在于：在多种现有方法中，实现时序推断的关键构造是目标系统与时序属性之间的乘积构造。通过认识到1）系统与时序属性均可建模为余代数，2）乘积构造在此背景下表现为分配律，我们给出了乘积构造的统一数学定义。我们的范畴化框架引出了主要贡献：一个确保正确性的充分条件，这正是利用乘积构造进行时序推断的关键所在。我们证明该框架可实例化以自然恢复文献中多种不同方法，包括马尔可夫奖励模型中的部分期望奖励、资源敏感可达性分析以及加权优化问题。此外，我们通过构建加权程序与加权时序属性的乘积作为新实例，展示了本方法良好的可扩展性。