A Unifying Approach to Product Constructions for Quantitative Temporal Inference
summary
Presents a categorical recipe that turns a system and a temporal specification into a product via coalgebraic modelling and a natural distributive law, then proves a three‑part sufficient condition (preservation of base assignments, joins of ω‑chains, and a commuting diagram tied to modalities) that guarantees solving reachability/expectation queries on the product equals the original temporal inference. Instantiates to Markov reward models, cost‑bounded reachability, weighted optimization, and demonstrates a new weighted‑program × weighted‑property prototype for scalability; no end‑to‑end implementation yet.
AI-written summary · about
chapters (7)
- 0:00Unifying product constructions
- 2:11Temporal verification products
- 4:23Cogebra semantics
- 6:13Algebraic product definition
- 8:19Correctness criterion
- 9:44Related work
- 11:32Q&A
related talks
22mSynthesizing Efficiently Monitorable Formulas in Metric Temporal Logic
24mHigher order programming with probabilistic effects: A model of stochastic memo...
46mBlueprints for a Universal Reasoning Machine
49mSemantic Foundations for Probabilistic Programming
29mEfficient Discovery of Actual Causality in Stochastic Systems
01h 01mBrief Tutorial on Probabilistic Databases
41mWar Time Proofs and Futuristic Programs
13mTyped Abstractions for Causal Probabilistic Programming