{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T17:25:16Z","timestamp":1787592316828,"version":"build-2736575974"},"reference-count":91,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T00:00:00Z","timestamp":1744156800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/legalcode"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,4,9]]},"abstract":"<jats:p>\n                    Probabilistic programs are a powerful and convenient approach to formalising distributions over system executions. A classical verification problem for probabilistic programs is\n                    <jats:italic toggle=\"yes\">temporal inference<\/jats:italic>\n                    : 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.\n                  <\/jats:p>\n                  <jats:p>\n                    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\n                    <jats:italic toggle=\"yes\">product<\/jats:italic>\n                    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\n                    <jats:italic toggle=\"yes\">coalgebras<\/jats:italic>\n                    and 2) product constructions are\n                    <jats:italic toggle=\"yes\">distributive laws<\/jats:italic>\n                    in this context. Our categorical framework leads us to our main contribution: a sufficient condition for\n                    <jats:italic toggle=\"yes\">correctness,<\/jats:italic>\n                    which is precisely what enables to use the product construction for temporal inference.\n                  <\/jats:p>\n                  <jats:p>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. Furthermore, we demonstrate a product of weighted programs and weighted temporal properties as a new instance to show the scalability of our approach.<\/jats:p>","DOI":"10.1145\/3720501","type":"journal-article","created":{"date-parts":[[2025,4,9]],"date-time":"2025-04-09T13:48:26Z","timestamp":1744206506000},"page":"1575-1603","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["A Unifying Approach to Product Constructions for Quantitative Temporal Inference"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4167-3370","authenticated-orcid":false,"given":"Kazuki","family":"Watanabe","sequence":"first","affiliation":[{"name":"National Institute of Informatics, Tokyo, Japan"},{"name":"The Graduate University for Advanced Studies (SOKENDAI), Hayama, Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0978-8466","authenticated-orcid":false,"given":"Sebastian","family":"Junges","sequence":"additional","affiliation":[{"name":"Radboud University, Nijmegen, Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1404-6232","authenticated-orcid":false,"given":"Jurriaan","family":"Rot","sequence":"additional","affiliation":[{"name":"Radboud University, Nijmegen, Netherlands"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8300-4650","authenticated-orcid":false,"given":"Ichiro","family":"Hasuo","sequence":"additional","affiliation":[{"name":"National Institute of Informatics, Tokyo, Japan"},{"name":"The Graduate University for Advanced Studies (SOKENDAI), Hayama, Japan"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158122"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571195"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129522000330"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-40903-8_8"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06200-6_24"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_28"},{"key":"e_1_3_1_8_1","volume-title":"Principles of model checking","author":"Baier Christel","year":"2008","unstructured":"Christel Baier and CJoost-Pieter Katoen. 2008. Principles of model checking. MIT Press."},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.JCSS.2023.03.005"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_43"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603162"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","unstructured":"Christel Baier Joachim Klein Sascha Kl\u00fcppelholz and Sascha Wunderlich. 2017. Maximizing the Conditional Expected Reward for Reaching the Goal. In TACAS (2) (Lecture Notes in Computer Science Vol. 10206). 269\u2013285. https:\/\/doi.org\/10.1007\/978-3-662-54580-5_16 10.1007\/978-3-662-54580-5_16","DOI":"10.1007\/978-3-662-54580-5_16"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/0012-365X(91)90413-V"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1017\/9781108770750"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30820-8_25"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527310"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ijar.2020.08.001"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2422085.2422092"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_19"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_1"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13185-1_4"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.21"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CALCO.2019.5"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54830-7_28"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.3233\/FI-2017-1474"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068410000529"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1979.82.43"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39813-4_26"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","unstructured":"Carmine Dodaro Valeria Fionda and Gianluigi Greco. 2022. LTL on Weighted Finite Traces: Formal Foundations and Algorithms. In IJCAI. ijcai.org 2606\u20132612. https:\/\/doi.org\/10.24963\/IJCAI.2022\/361 10.24963\/IJCAI.2022\/361","DOI":"10.24963\/IJCAI.2022\/361"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2012.10.001"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","unstructured":"Manfred Droste and George Rahonis. 2016. Weighted Linear Dynamic Logic. In GandALF (EPTCS Vol. 226). 149\u2013163. https:\/\/doi.org\/10.4204\/EPTCS.226.11 10.4204\/EPTCS.226.11","DOI":"10.4204\/EPTCS.226.11"},{"key":"e_1_3_1_33_1","first-page":"39","volume-title":"Software Engineering (LNI, Vol. P-227)","author":"Filieri Antonio","year":"2014","unstructured":"Antonio Filieri, Corina S. Pasareanu, and Willem Visser. 2014. Reliability Analysis in Symbolic Pathfinder: A brief summary. In Software Engineering (LNI, Vol. P-227). GI, 39\u201340."},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_9"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_4"},{"key":"e_1_3_1_36_1","first-page":"854","volume-title":"IJCAI","author":"De Giacomo Giuseppe","year":"2013","unstructured":"Giuseppe De Giacomo and Moshe Y. Vardi. 2013. Linear Temporal Logic and Linear Dynamic Logic on Finite Traces. In IJCAI. IJCAI\/AAAI, 854\u2013860."},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571215"},{"key":"e_1_3_1_38_1","unstructured":"Noah D. Goodman Vikash K. Mansinghka Daniel M. Roy Kallista A. Bonawitz and Joshua B. Tenenbaum. 2008. Church: a language for generative models. In UAI. AUAI Press 220\u2013229."},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2593882.2593900"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.PEVA.2013.11.004"},{"key":"e_1_3_1_41_1","unstructured":"Martin Hairer and Xue-Mei Li. 2020. Markov processes. Course Notes Imperial College London (2020)."},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-020-09574-9"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-3(4:11)2007"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.JLAMP.2023.100922"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837673"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428208"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_27"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2594291.2594303"},{"key":"e_1_3_1_49_1","volume-title":"Categorical Logic and Type Theory. Studies in logic and the foundations of mathematics","author":"Jacobs Bart","year":"2001","unstructured":"Bart Jacobs. 2001. Categorical Logic and Type Theory. Studies in logic and the foundations of mathematics, Vol. 141. North-Holland. http:\/\/www.elsevierdirect.com\/product.jsp?isbn=9780444508539"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","DOI":"10.1007\/11780274_20"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781316823187"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2014.12.005"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571245"},{"key":"e_1_3_1_54_1","volume-title":"Advanced weakest precondition calculi for probabilistic programs. Ph.D. Dissertation","author":"Kaminski Benjamin Lucien","year":"2019","unstructured":"Benjamin Lucien Kaminski. 2019. Advanced weakest precondition calculi for probabilistic programs. Ph.D. Dissertation. RWTH Aachen University, Germany."},{"key":"e_1_3_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3208102"},{"key":"e_1_3_1_56_1","volume-title":"Probability theory: a comprehensive course","author":"Klenke Achim","year":"2013","unstructured":"Achim Klenke. 2013. Probability theory: a comprehensive course. Springer Science & Business Media."},{"key":"e_1_3_1_57_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.03.023"},{"key":"e_1_3_1_58_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-12(4:10)2016"},{"key":"e_1_3_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-66438-0_1"},{"key":"e_1_3_1_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37703-7_3"},{"key":"e_1_3_1_61_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13185-1_12"},{"key":"e_1_3_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/3661814.3662139"},{"key":"e_1_3_1_63_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90012-1"},{"key":"e_1_3_1_64_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.04.023"},{"key":"e_1_3_1_65_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31982-5_9"},{"key":"e_1_3_1_66_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-4721-8"},{"key":"e_1_3_1_67_1","volume-title":"Abstraction, Refinement and Proof for Probabilistic Systems","author":"McIver Annabelle","year":"2005","unstructured":"Annabelle McIver and Carroll Morgan. 2005. Abstraction, Refinement and Proof for Probabilistic Systems. Springer."},{"key":"e_1_3_1_68_1","doi-asserted-by":"publisher","DOI":"10.1609\/AAAI.V28I1.9060"},{"key":"e_1_3_1_69_1","doi-asserted-by":"publisher","DOI":"10.1145\/3156018"},{"key":"e_1_3_1_70_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511662508.004"},{"key":"e_1_3_1_71_1","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_3_1_72_1","doi-asserted-by":"publisher","DOI":"10.1002\/9780470316887"},{"key":"e_1_3_1_73_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-85248-1_16"},{"key":"e_1_3_1_74_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exab050"},{"key":"e_1_3_1_75_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00056-6"},{"key":"e_1_3_1_76_1","first-page":"27","article-title":"Relational dynamic influence diagram language (rddl): Language description","volume":"32","author":"Sanner Scott","year":"2010","unstructured":"Scott Sanner. 2010. Relational dynamic influence diagram language (rddl): Language description. Australian National University 32 (2010), 27.","journal-title":"Australian National University"},{"key":"e_1_3_1_77_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(1:9)2013"},{"key":"e_1_3_1_78_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(1:9)2013"},{"key":"e_1_3_1_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314639"},{"key":"e_1_3_1_80_1","doi-asserted-by":"publisher","DOI":"10.1613\/JAIR.5153"},{"key":"e_1_3_1_81_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563344"},{"key":"e_1_3_1_82_1","doi-asserted-by":"publisher","DOI":"10.1145\/3450967"},{"key":"e_1_3_1_83_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-23461-8_36"},{"key":"e_1_3_1_84_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1997.614955"},{"key":"e_1_3_1_85_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005151"},{"key":"e_1_3_1_86_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-00389-0_12"},{"key":"e_1_3_1_87_1","unstructured":"Jan-Willem van de Meent Brooks Paige Hongseok Yang and Frank Wood. 2018. An Introduction to Probabilistic Programming. CoRR abs\/1809.10756 (2018). arXiv:1809.10756 http:\/\/arxiv.org\/abs\/1809.10756"},{"key":"e_1_3_1_88_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(86)90026-7"},{"key":"e_1_3_1_89_1","unstructured":"Marcell Vazquez-Chanlatte Susmit Jha Ashish Tiwari Mark K. Ho and Sanjit A. Seshia. 2018. Learning Task Specifications from Demonstrations. In NeurIPS. 5372\u20135382."},{"key":"e_1_3_1_90_1","unstructured":"Marcell Vazquez-Chanlatte Ameesh Shah Gil Lederman and Sanjit A. Seshia. 2021. Demonstration Informed Specification Search. CoRR abs\/2112.10807 (2021). arXiv:2112.10807 https:\/\/arxiv.org\/abs\/2112.10807"},{"key":"e_1_3_1_91_1","unstructured":"Kazuki Watanabe Sebastian Junges Jurriaan Rot and Ichiro Hasuo. 2025. A Unifying Approach to Product Constructions for Quantitative Temporal Inference. CoRR abs\/2407.10465 (2025). A Longer Version that Includes Proofs."},{"key":"e_1_3_1_92_1","doi-asserted-by":"publisher","DOI":"10.23638\/LMCS-16(1:8)2020"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720501","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3720501","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,8,24]],"date-time":"2026-08-24T16:32:00Z","timestamp":1787589120000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3720501"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,4,9]]},"references-count":91,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2025,4,9]]}},"alternative-id":["10.1145\/3720501"],"URL":"https:\/\/doi.org\/10.1145\/3720501","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,4,9]]},"assertion":[{"value":"2024-10-16","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-02-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-04-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}