{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,22]],"date-time":"2025-10-22T23:36:06Z","timestamp":1761176166618,"version":"build-2065373602"},"reference-count":0,"publisher":"IOS Press","isbn-type":[{"value":"9781643686318","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,10,21]],"date-time":"2025-10-21T00:00:00Z","timestamp":1761004800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc\/4.0\/"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2025,10,21]]},"abstract":"<jats:p>Reactive synthesis addresses the problem of generating a controller for a temporal specification in an adversarial environment; it was typically studied for LTL. Driven by applications ranging from AI to business process management, LTL modulo first order-theories over finite traces (LTLMTf) has recently gained traction, where propositional variables in properties are replaced by first-order constraints. Though reactive synthesis for LTLf with some first-order features has been addressed, existing work in this direction strongly restricts or excludes the possibility to compare variables across instants, a limitation that severely limits expressiveness and applicability. In this work we present a reactive synthesis procedure for LTLMTf, where properties support lookback to model cross-instant comparison of variables, subsuming the fragments of LTLMTf for which realizability was studied earlier. While we prove soundness of our approach for arbirary background theories, termination is in general not guaranteed. This is because the setting with cross-instant comparison is inherently highly complex, as realizability is undecidable even over decidable background theories. Nevertheless, we show completeness of the procedure if a bound on the strategy length exists. Moreover, the presented approach is proven a decision procedure for several relevant fragments of LTLMTf, at once re-proving known decidability results and identifying new decidable classes.<\/jats:p>","DOI":"10.3233\/faia250987","type":"book-chapter","created":{"date-parts":[[2025,10,22]],"date-time":"2025-10-22T09:47:49Z","timestamp":1761126469000},"source":"Crossref","is-referenced-by-count":0,"title":["First-Order LTLf Synthesis with Lookback"],"prefix":"10.3233","author":[{"given":"Sarah","family":"Winkler","sequence":"first","affiliation":[{"name":"Free University of Bozen-Bolzano, Italy"}]}],"member":"7437","container-title":["Frontiers in Artificial Intelligence and Applications","ECAI 2025"],"original-title":[],"link":[{"URL":"https:\/\/ebooks.iospress.nl\/pdf\/doi\/10.3233\/FAIA250987","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,22]],"date-time":"2025-10-22T09:47:49Z","timestamp":1761126469000},"score":1,"resource":{"primary":{"URL":"https:\/\/ebooks.iospress.nl\/doi\/10.3233\/FAIA250987"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,21]]},"ISBN":["9781643686318"],"references-count":0,"URL":"https:\/\/doi.org\/10.3233\/faia250987","relation":{},"ISSN":["0922-6389","1879-8314"],"issn-type":[{"value":"0922-6389","type":"print"},{"value":"1879-8314","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,21]]}}}