{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T07:01:13Z","timestamp":1762326073718,"version":"build-2065373602"},"publisher-location":"California","reference-count":0,"publisher":"International Joint Conferences on Artificial Intelligence Organization","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025,11]]},"abstract":"<jats:p>Recently, the Manna-Pnueli Hierarchy has been used to define the temporal logics LTLf+ and PPLTL+, which allow to use finite-trace LTLf\/PPLTL techniques in infinite-trace settings while achieving the expressiveness of full LTL. \n\n\n\nIn this paper, we present the first actual solvers for reactive synthesis in these logics. These are based on games on graphs that leverage DFA-based techniques from LTLf\/PPLTL to construct the game arena. We start with a symbolic solver based on Emerson-Lei games, which reduces lower-class properties (guarantee, safety) to higher ones (recurrence, persistence) before solving the game.\n\n\n\nWe then introduce Manna-Pnueli games, which natively embed Manna-Pnueli objectives into the arena. These games are solved by composing solutions to a DAG of simpler Emerson-Lei games, resulting in a provably more efficient approach.\n\n\n\nWe implemented the solvers and practically evaluated their performance on a range of representative formulas. The results show that Manna-Pnueli games often offer significant advantages, though not universally, indicating that combining both approaches could further enhance practical performance.<\/jats:p>","DOI":"10.24963\/kr.2025\/78","type":"proceedings-article","created":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T06:10:44Z","timestamp":1762323044000},"page":"810-820","source":"Crossref","is-referenced-by-count":0,"title":["Emerson-Lei and Manna-Pnueli Games for LTLf+ and PPLTL+ Synthesis"],"prefix":"10.24963","author":[{"given":"Daniel","family":"Hausmann","sequence":"first","affiliation":[{"name":"University of Liverpool"}]},{"given":"Shufang","family":"Zhu","sequence":"additional","affiliation":[{"name":"University of Liverpool"}]},{"given":"Gianmarco","family":"Parretti","sequence":"additional","affiliation":[{"name":"Sapienza Universit\u00e0 di Roma"}]},{"given":"Christoph","family":"Weinhuber","sequence":"additional","affiliation":[{"name":"University of Oxford"}]},{"given":"Giuseppe","family":"De Giacomo","sequence":"additional","affiliation":[{"name":"University of Oxford"},{"name":"Sapienza Universit\u00e0 di Roma"}]},{"given":"Nir","family":"Piterman","sequence":"additional","affiliation":[{"name":"University of Gothenburg"},{"name":"Chalmers University of Technology"}]}],"member":"10584","event":{"name":"22nd International Conference on Principles of Knowledge Representation and Reasoning {KR-2025}","theme":"Artificial Intelligence","location":"Melbourne, Australia","acronym":"KR-2025","number":"22","sponsor":["Artificial Intelligence Journal","Principles of Knowledge Representation and Reasoning Inc.","Academic College of Tel-Aviv","European Association for Artificial Intelligence","National Science Foundation"],"start":{"date-parts":[[2025,11,11]]},"end":{"date-parts":[[2025,11,17]]}},"container-title":["Proceedings of the TwentySecond International Conference on Principles of Knowledge Representation and Reasoning"],"original-title":[],"deposited":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T06:11:26Z","timestamp":1762323086000},"score":1,"resource":{"primary":{"URL":"https:\/\/proceedings.kr.org\/2025\/78"}},"subtitle":[],"proceedings-subject":"Artificial Intelligence Research Articles","short-title":[],"issued":{"date-parts":[[2025,11]]},"references-count":0,"URL":"https:\/\/doi.org\/10.24963\/kr.2025\/78","relation":{},"subject":[],"published":{"date-parts":[[2025,11]]}}}