A Unifying Approach to Product Constructions for Quantitative Temporal Inference

TL;DR

This work presents a general coalgebraic framework for temporal inference in probabilistic and weighted programs by introducing a product construction between systems and temporal properties. The core insight is that a distributive law induces a coalgebraic product, and a sufficient correctness criterion guarantees that inference on the product yields the intended query on the original components. The framework unifies a broad set of problems—ranging from partial rewards and cost-bounded reachability to conditional probabilities and optimization—through concrete case studies that instantiate the product for Markov chains, reward machines, and weighted systems. This approach enables efficient, exact or approximate inference by reducing temporal questions to product semantics that can be tackled with standard inference engines. The work also outlines avenues for extending to non-terminating systems, weighted regular properties, and continuous distributions, with an eye toward practical product-program implementations and tooling.

Abstract

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.

Figures (11)

• Figure 1: Temporal inference: its problem definition (black) and its tractable solution by product construction (red).
• Figure 2: Instances of coalgebraic inference with coalgebraic product construction. RSP denotes the regular safety property.
• Figure 3: Robot moves in the $5\times 3$ grid world. The requirement of the robot is given by the DFA. The state $y_0$ is the initial state, and $y_1$ is the unique accepting state in the DFA. We omit all self-loops for readability. For instance, we omit the self-loops on the states $y_2$ and $y_3$ whose assigned character is $\textcolor{blue!50!black}{lake}$.
• Figure 4: Reactive gridworld: Robot moves in the $5\times 3$ grid world in any direction, the program never halts. The requirement expresses that we want to reach a charging station without reaching a volcano.
• Figure 5: Travelling problem. The functions $\textcolor{orange}{\mathrm{min}}$ and $\textcolor{orange}{\mathrm{add}}$ in the weighted program are the primary operations on the costs (or weights in general). The state $y_0$ is the initial state, and $y_1$ is the unique accepting state in the NFA $d$. The characters $\mathrm{P},\mathrm{B},\mathrm{T}$ correspond to taking a plane, a bus, and a train, respectively.

Theorems & Definitions (63)

• Remark 1
• definition 1: functor
• definition 2: coalgebra
• definition 3: semantic structure, predicate transformer
• definition 4: semantics of coalgebras
• definition 5: coalgebraic inference
• definition 6: coalgebraic product
• definition 7: distributive law $\lambda$
• Remark 2: map that is not natural
• definition 8: correctness