{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T03:23:17Z","timestamp":1779074597510,"version":"3.51.4"},"reference-count":71,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"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,1,7]]},"abstract":"<jats:p>Infinite-state reactive synthesis has attracted significant attention in recent years, which has led to the emergence of novel symbolic techniques for solving infinite-state games. Temporal logics featuring variables over infinite domains offer an expressive high-level specification language for infinite-state reactive systems. Currently, the only way to translate these temporal logics into symbolic games is by naively encoding the specification to use techniques designed for the Boolean case. An inherent limitation of this approach is that it results in games in which the semantic structure of the temporal and first-order constraints present in the formula is lost. There is a clear need for techniques that leverage this information in the translation process to speed up solving the generated games.<\/jats:p>\n                  <jats:p>In this work, we propose the first approach that addresses this gap. Our technique constructs a monitor incorporating first-order and temporal reasoning at the formula level, enriching the constructed game with semantic information that leads to more efficient solving. We demonstrate that thanks to this, our method outperforms the state-of-the-art techniques across a range of benchmarks.<\/jats:p>","DOI":"10.1145\/3704888","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"1536-1567","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Translation of Temporal Logic for Efficient Infinite-State Reactive Synthesis"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-5433-8133","authenticated-orcid":false,"given":"Philippe","family":"Heim","sequence":"first","affiliation":[{"name":"CISPA Helmholtz Center for Information Security, Saarbr\u00fccken, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-2494-8690","authenticated-orcid":false,"given":"Rayna","family":"Dimitrova","sequence":"additional","affiliation":[{"name":"CISPA Helmholtz Center for Information Security, Saarbr\u00fccken, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2013.6679385"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2307.09776"},{"key":"e_1_3_2_4_2","volume-title":"Principles of model checking","author":"Baier Christel","year":"2008","unstructured":"Christel Baier and Joost-Pieter Katoen. 2008. Principles of model checking. MIT Press."},{"key":"e_1_3_2_5_2","first-page":"950","volume-title":"Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, New York, NY, USA, 9-15 July 2016","author":"Bertello Matteo","year":"2016","unstructured":"Matteo Bertello, Nicola Gigante, Angelo Montanari, and Mark Reynolds. 2016. Leviathan: A New LTL Satisfiability Checking Tool Based on a One-Pass Tree-Shaped Tableau. In Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, New York, NY, USA, 9-15 July 2016, Subbarao Kambhampati (Ed.). IJCAI\/AAAI Press, 950\u2013956. http:\/\/www.ijcai.org\/Abstract\/16\/139"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74113-8"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523429"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10703-015-0233-4"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","DOI":"10.1145\/3419404"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78800-324"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.3166\/JANCL.16.311-347"},{"key":"e_1_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.IC.2006.09.006"},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-46520-3_8"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-13188-2_9"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-0-387-36123-9"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10009-022-00663-1"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/3417995"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1609\/aaai.v37i5.25779"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.29007\/WPG3"},{"key":"e_1_3_2_20_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-38919-214"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/3158149"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99253-817"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-25540-4_35"},{"key":"e_1_3_2_24_2","doi-asserted-by":"publisher","unstructured":"Bernd Finkbeiner Kaushik Mallik Noemi Passing Malte Schledjewski and Anne-Kathrin Schmuck. 2022. BOCoSy: Small but Powerful Symbolic Output-Feedback Control. In HSCC \u201822: 25th ACM International Conference on Hybrid Systems: Computation and Control Milan Italy May 4 - 6 2022 Ezio Bartocci and Sylvie Putot (Eds.). ACM 24:1\u201324:11. https:\/\/doi.org\/10.1145\/3501710.3519535 10.1145\/3501710.3519535","DOI":"10.1145\/3501710.3519535"},{"key":"e_1_3_2_25_2","article-title":"A General Automata Model for First-Order Temporal Logics (Extended Version)","author":"Geatti Luca","year":"2024","unstructured":"Luca Geatti, Alessandro Gianola, and Nicola Gigante. 2024. A General Automata Model for First-Order Temporal Logics (Extended Version). CoRR abs\/2405.20057 (2024). https:\/\/doi.org\/10.48550\/ARXIV.2405.20057 arXiv:2405.20057 10.48550\/ARXIV.2405.20057 arXiv:2405.20057","journal-title":"CoRR"},{"key":"e_1_3_2_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-023-09691-1"},{"key":"e_1_3_2_27_2","first-page":"3","volume-title":"Protocol Specification, Testing and Verification XV, Proceedings of the Fifteenth IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification, Warsaw, Poland, June 1995 (IFIP Conference Proceedings, Vol. 38)","author":"Gerth Rob","year":"1995","unstructured":"Rob Gerth, Doron A. Peled, Moshe Y. Vardi, and Pierre Wolper. 1995. Simple on-the-fly automatic verification of linear temporal logic. In Protocol Specification, Testing and Verification XV, Proceedings of the Fifteenth IFIP WG6.1 International Symposium on Protocol Specification, Testing and Verification, Warsaw, Poland, June 1995 (IFIP Conference Proceedings, Vol. 38), Piotr Dembinski and Marek Sredniawa (Eds.). Chapman Hall, 3\u201318."},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33386-6_11"},{"key":"e_1_3_2_29_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2006.10.009"},{"key":"e_1_3_2_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571214"},{"key":"e_1_3_2_31_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-03769-7_7"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10009-021-00626-Y"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2001.989799"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","unstructured":"Philippe Heim and Rayna Dimitrova. 2024. Artifact of \u201cTranslation of Temporal Logic for Efficient Infinite-State Reactive Synthesis\u201d. https:\/\/doi.org\/10.5281\/zenodo.13939202 10.5281\/zenodo.13939202","DOI":"10.5281\/zenodo.13939202"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/3632899"},{"key":"e_1_3_2_36_2","article-title":"Translation of Temporal Logic for Efficient Infinite-State Reactive Synthesis (Full Version)","author":"Heim Philippe","year":"2024","unstructured":"Philippe Heim and Rayna Dimitrova. 2024. Translation of Temporal Logic for Efficient Infinite-State Reactive Synthesis (Full Version). CoRR abs\/2411.07078 (2024). arXiv:2411.07078 https:\/\/arxiv.org\/abs\/2411.07078","journal-title":"CoRR"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45061-0_69"},{"key":"e_1_3_2_38_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-27481-728"},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","DOI":"10.1109\/TIME.2003.1214884"},{"key":"e_1_3_2_40_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45653-81"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029847"},{"key":"e_1_3_2_42_2","article-title":"The Temporal Logic Synthesis Format TLSF v1.2","author":"Jacobs Swen","year":"2023","unstructured":"Swen Jacobs, Guillermo A. P\u00e9rez, and Philipp Schlehuber-Caissier. 2023. The Temporal Logic Synthesis Format TLSF v1.2. CoRR abs\/2303.03839 (2023). https:\/\/doi.org\/10.48550\/ARXIV.2303.03839 arXiv:2303.03839 10.48550\/ARXIV.2303.03839 arXiv:2303.03839","journal-title":"CoRR"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89963-310"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_7"},{"key":"e_1_3_2_45_2","article-title":"Fast LTL Satisfiability Checking by SAT Solvers","author":"Li Jianwen","year":"2014","unstructured":"Jianwen Li, Geguang Pu, Lijun Zhang, Moshe Y. Vardi, and Jifeng He. 2014. Fast LTL Satisfiability Checking by SAT Solvers. CoRR abs\/1401.5677 (2014). arXiv:1401.5677 http:\/\/arxiv.org\/abs\/1401.5677","journal-title":"CoRR"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","DOI":"10.1109\/TIME.2013.19"},{"key":"e_1_3_2_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/S00236-019-00349-3"},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.34727\/2022\/ISBN.978-3-85448-053-2_38"},{"key":"e_1_3_2_49_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_31"},{"key":"e_1_3_2_50_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(84)90049-5"},{"key":"e_1_3_2_51_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49674-912"},{"key":"e_1_3_2_52_2","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-3(3:5)2007"},{"key":"e_1_3_2_53_2","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_3_2_54_2","doi-asserted-by":"publisher","DOI":"10.1145\/75277.75293"},{"key":"e_1_3_2_55_2","doi-asserted-by":"publisher","unstructured":"Mark Reynolds. 2016. A New Rule for LTL Tableaux. In Proceedings of the Seventh International Symposium on Games Automata Logics and Formal Verification GandALF 2016 Catania Italy 14-16 September 2016 (EPTCS Vol. 226) Domenico Cantone and Giorgio Delzanno (Eds.). 287\u2013301. https:\/\/doi.org\/10.4204\/EPTCS.226.20 10.4204\/EPTCS.226.20","DOI":"10.4204\/EPTCS.226.20"},{"key":"e_1_3_2_56_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-37709-915"},{"key":"e_1_3_2_57_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10009-010-0140-3"},{"key":"e_1_3_2_58_2","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1988.21948"},{"key":"e_1_3_2_59_2","doi-asserted-by":"publisher","DOI":"10.1145\/3468264.3473126"},{"key":"e_1_3_2_60_2","doi-asserted-by":"publisher","DOI":"10.1109\/ASE56229.2023.00212"},{"key":"e_1_3_2_61_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-65633-0_7"},{"key":"e_1_3_2_62_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-69778-028"},{"key":"e_1_3_2_63_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-40965-617"},{"key":"e_1_3_2_64_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211865"},{"key":"e_1_3_2_65_2","doi-asserted-by":"publisher","unstructured":"IEEE Standards. 2010. IEEE Standard for Property Specification Language (PSL). IEEE Std 1850-2010 (Revision of IEEE Std 1850-2005) (2010) 1\u2013182. https:\/\/doi.org\/10.1109\/IEEESTD.2010.5446004 10.1109\/IEEESTD.2010.5446004","DOI":"10.1109\/IEEESTD.2010.5446004"},{"key":"e_1_3_2_66_2","doi-asserted-by":"publisher","DOI":"10.1145\/3571265"},{"key":"e_1_3_2_67_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57887-0116"},{"key":"e_1_3_2_68_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60915-6_6"},{"key":"e_1_3_2_69_2","doi-asserted-by":"publisher","DOI":"10.1145\/3704838"},{"key":"e_1_3_2_70_2","doi-asserted-by":"publisher","DOI":"10.1007\/S10009-012-0232-3"},{"key":"e_1_3_2_71_2","doi-asserted-by":"publisher","DOI":"10.1109\/FMCAD.2014.6987617"},{"key":"e_1_3_2_72_2","first-page":"119","article-title":"The tableau method for temporal logic: an overview","volume":"28","author":"Wolper Pierre","year":"1985","unstructured":"Pierre Wolper. 1985. The tableau method for temporal logic: an overview. Logique Et Analyse 28 (1985), 119\u2013136. https:\/\/api.semanticscholar.org\/CorpusID:118632087","journal-title":"Logique Et Analyse"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704888","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704888","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:14:41Z","timestamp":1770200081000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704888"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":71,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704888"],"URL":"https:\/\/doi.org\/10.1145\/3704888","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}