{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,18]],"date-time":"2026-01-18T00:00:35Z","timestamp":1768694435655,"version":"3.49.0"},"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":[[2023,9]]},"abstract":"<jats:p>Confronting the past can be hard. This is true even in Linear Temporal Logic (LTL), interpreted on either infinite or finite traces, when faced with the problem of transforming a temporally future formula into an equivalent one that contains past temporal modalities only. To our knowledge, the best among the available pastification procedures for full LTL, as well as for expressive enough fragments of it (that is, containing at least one temporal modality other than tomorrow), are triply exponential in the size of the input. In this paper, we focus on the fragment of LTL that features the tomorrow and eventually modalities, and provide a singly exponential pastification algorithm for it. The transformation is based on a normalisation procedure that requires a non-trivial complexity analysis, and on the subsequent generation of a pure past formula from suitably-defined dependency tree structures. Moreover, leveraging its purely syntactic nature, we present an implementation of our procedure in a temporal satisfiability checking tool that deals with both future and past modalities.<\/jats:p>","DOI":"10.24963\/kr.2023\/7","type":"proceedings-article","created":{"date-parts":[[2023,7,31]],"date-time":"2023-07-31T22:27:47Z","timestamp":1690842467000},"page":"65-74","source":"Crossref","is-referenced-by-count":1,"title":["A Singly Exponential Transformation of LTL[X, F] into Pure Past LTL"],"prefix":"10.24963","author":[{"given":"Alessandro","family":"Artale","sequence":"first","affiliation":[{"name":"Free University of Bozen-Bolzano"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Luca","family":"Geatti","sequence":"additional","affiliation":[{"name":"University of Udine"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Nicola","family":"Gigante","sequence":"additional","affiliation":[{"name":"Free University of Bozen-Bolzano, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrea","family":"Mazzullo","sequence":"additional","affiliation":[{"name":"Free University of Bozen-Bolzano, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Angelo","family":"Montanari","sequence":"additional","affiliation":[{"name":"University of Udine"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"10584","event":{"name":"20th International Conference on Principles of Knowledge Representation and Reasoning {KR-2023}","theme":"Artificial Intelligence","location":"Rhodes, Greece","acronym":"KR-2023","number":"20","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":[[2023,9,2]]},"end":{"date-parts":[[2023,9,8]]}},"container-title":["Proceedings of the Twentieth International Conference on Principles of Knowledge Representation and Reasoning"],"original-title":[],"deposited":{"date-parts":[[2023,7,31]],"date-time":"2023-07-31T22:27:56Z","timestamp":1690842476000},"score":1,"resource":{"primary":{"URL":"https:\/\/proceedings.kr.org\/2023\/7"}},"subtitle":[],"proceedings-subject":"Artificial Intelligence Research Articles","short-title":[],"issued":{"date-parts":[[2023,9]]},"references-count":0,"URL":"https:\/\/doi.org\/10.24963\/kr.2023\/7","relation":{},"subject":[],"published":{"date-parts":[[2023,9]]}}}