{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T05:20:59Z","timestamp":1776316859164,"version":"3.50.1"},"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\/"}],"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.   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.   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.\n          <\/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":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0978-8466","authenticated-orcid":false,"given":"Sebastian","family":"Junges","sequence":"additional","affiliation":[{"name":"Radboud University, Nijmegen, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1404-6232","authenticated-orcid":false,"given":"Jurriaan","family":"Rot","sequence":"additional","affiliation":[{"name":"Radboud University, Nijmegen, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"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":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,4,9]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158122"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571195"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129522000330"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-40903-8_8"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-06200-6_24"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_28"},{"key":"e_1_2_1_7_1","volume-title":"Principles of model checking","author":"Baier Christel","unstructured":"Christel Baier and Joost-Pieter Katoen. 2008. Principles of model checking. MIT Press. isbn:978-0-262-02649-9"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.JCSS.2023.03.005"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54862-8_43"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603162"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54580-5_16"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/0012-365X(91)90413-V"},{"key":"e_1_2_1_13_1","volume-title":"Foundations of probabilistic programming","author":"Barthe Gilles","unstructured":"Gilles Barthe, Joost-Pieter Katoen, and Alexandra Silva. 2020. Foundations of probabilistic programming. Cambridge University Press."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-30820-8_25"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527310"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ijar.2020.08.001"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2422085.2422092"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_19"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_1"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13185-1_4"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2009.21"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPICS.CALCO.2019.5"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54830-7_28"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.3233\/FI-2017-1474"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068410000529"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1979.82.43"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-39813-4_26"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_2_1_29_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_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2012.10.001"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.226.11"},{"key":"e_1_2_1_32_1","volume-title":"Software Engineering (LNI","author":"Filieri Antonio","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_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_9"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_4"},{"key":"e_1_2_1_35_1","volume-title":"Vardi","author":"Giacomo Giuseppe De","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_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571215"},{"key":"e_1_2_1_37_1","volume-title":"Tenenbaum","author":"Goodman Noah D.","year":"2008","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_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2593882.2593900"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.PEVA.2013.11.004"},{"key":"e_1_2_1_40_1","volume-title":"Markov processes. Course Notes","author":"Hairer Martin","unstructured":"Martin Hairer and Xue-Mei Li. 2020. Markov processes. Course Notes, Imperial College London."},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-020-09574-9"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-3(4:11)2007"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1016\/J.JLAMP.2023.100922"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","unstructured":"Ichiro Hasuo Shunsuke Shimizu and Corina C\u00eerstea. 2016. Lattice-theoretic progress measures and coalgebraic model checking. In POPL. ACM 718\u2013732. https:\/\/doi.org\/10.1145\/2837614.2837673 10.1145\/2837614.2837673","DOI":"10.1145\/2837614.2837673"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428208"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_27"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","unstructured":"Chung-Kil Hur Aditya V. Nori Sriram K. Rajamani and Selva Samuel. 2014. Slicing probabilistic programs. In PLDI. ACM 133\u2013144. https:\/\/doi.org\/10.1145\/2594291.2594303 10.1145\/2594291.2594303","DOI":"10.1145\/2594291.2594303"},{"key":"e_1_2_1_48_1","volume-title":"Categorical Logic and Type Theory (Studies in logic and the foundations of mathematics","author":"Jacobs Bart","unstructured":"Bart Jacobs. 2001. Categorical Logic and Type Theory (Studies in logic and the foundations of mathematics, Vol. 141). North-Holland. isbn:978-0-444-50853-9 http:\/\/www.elsevierdirect.com\/product.jsp?isbn=9780444508539"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/11780274_20"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781316823187"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jcss.2014.12.005"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571245"},{"key":"e_1_2_1_53_1","volume-title":"Advanced weakest precondition calculi for probabilistic programs. Ph. D. Dissertation","author":"Kaminski Benjamin Lucien","unstructured":"Benjamin Lucien Kaminski. 2019. Advanced weakest precondition calculi for probabilistic programs. Ph. D. Dissertation. RWTH Aachen University, Germany."},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3208102"},{"key":"e_1_2_1_55_1","volume-title":"Probability theory: a comprehensive course","author":"Klenke Achim","unstructured":"Achim Klenke. 2013. Probability theory: a comprehensive course. Springer Science & Business Media."},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.03.023"},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-12(4:10)2016"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-66438-0_1"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37703-7_3"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13185-1_12"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/3661814.3662139"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90012-1"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.04.023"},{"key":"e_1_2_1_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31982-5_9"},{"key":"e_1_2_1_65_1","volume-title":"Categories for the working mathematician","author":"Lane Saunders Mac","unstructured":"Saunders Mac Lane. 1978. Categories for the working mathematician (second ed.) (Graduate Texts in Mathematics, Vol. 5). Springer-Verlag, New York."},{"key":"e_1_2_1_66_1","volume-title":"Refinement and Proof for Probabilistic Systems","author":"McIver Annabelle","unstructured":"Annabelle McIver and Carroll Morgan. 2005. Abstraction, Refinement and Proof for Probabilistic Systems. Springer."},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","DOI":"10.1609\/AAAI.V28I1.9060"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1145\/3156018"},{"key":"e_1_2_1_69_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511662508.004"},{"key":"e_1_2_1_70_1","volume-title":"The Temporal Logic of Programs","author":"Pnueli Amir","unstructured":"Amir Pnueli. 1977. The Temporal Logic of Programs. In FOCS. IEEE Computer Society, 46\u201357."},{"key":"e_1_2_1_71_1","volume-title":"Markov Decision Processes: Discrete Stochastic Dynamic Programming","author":"Puterman Martin L.","unstructured":"Martin L. Puterman. 1994. Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley."},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-85248-1_16"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exab050"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00056-6"},{"key":"e_1_2_1_75_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_2_1_76_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-9(1:9)2013"},{"key":"e_1_2_1_77_1","doi-asserted-by":"publisher","unstructured":"Steffen Smolka Praveen Kumar Nate Foster Dexter Kozen and Alexandra Silva. 2017. Cantor meets Scott: semantic foundations for probabilistic networks. In POPL. ACM 557\u2013571. https:\/\/doi.org\/10.2168\/LMCS-9(1:9)2013 10.2168\/LMCS-9(1:9)2013","DOI":"10.2168\/LMCS-9(1:9)2013"},{"key":"e_1_2_1_78_1","doi-asserted-by":"publisher","unstructured":"Steffen Smolka Praveen Kumar David M. Kahn Nate Foster Justin Hsu Dexter Kozen and Alexandra Silva. 2019. Scalable verification of probabilistic networks. In PLDI. ACM 190\u2013203. https:\/\/doi.org\/10.1145\/3314221.3314639 10.1145\/3314221.3314639","DOI":"10.1145\/3314221.3314639"},{"key":"e_1_2_1_79_1","doi-asserted-by":"publisher","DOI":"10.1613\/JAIR.5153"},{"key":"e_1_2_1_80_1","doi-asserted-by":"publisher","DOI":"10.1145\/3563344"},{"key":"e_1_2_1_81_1","doi-asserted-by":"publisher","DOI":"10.1145\/3450967"},{"key":"e_1_2_1_82_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-23461-8_36"},{"key":"e_1_2_1_83_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1997.614955"},{"key":"e_1_2_1_84_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005151"},{"key":"e_1_2_1_85_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-00389-0_12"},{"key":"e_1_2_1_86_1","volume-title":"An Introduction to Probabilistic Programming. CoRR, abs\/1809.10756","author":"van de Meent Jan-Willem","year":"2018","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. arxiv:1809.10756"},{"key":"e_1_2_1_87_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(86)90026-7"},{"key":"e_1_2_1_88_1","volume-title":"Seshia","author":"Vazquez-Chanlatte Marcell","year":"2018","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_2_1_89_1","volume-title":"Seshia","author":"Vazquez-Chanlatte Marcell","year":"2021","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. arxiv:2112.10807"},{"key":"e_1_2_1_90_1","volume-title":"A Unifying Approach to Product Constructions for Quantitative Temporal Inference. CoRR, abs\/2407.10465","author":"Watanabe Kazuki","year":"2025","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_2_1_91_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":[[2025,10,9]],"date-time":"2025-10-09T17:14:23Z","timestamp":1760030063000},"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"}}]}}