{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,3]],"date-time":"2026-07-03T20:23:41Z","timestamp":1783110221081,"version":"3.54.6"},"reference-count":37,"publisher":"Elsevier BV","license":[{"start":{"date-parts":[[2026,8,1]],"date-time":"2026-08-01T00:00:00Z","timestamp":1785542400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/tdm\/userlicense\/1.0\/"},{"start":{"date-parts":[[2026,8,1]],"date-time":"2026-08-01T00:00:00Z","timestamp":1785542400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.elsevier.com\/legal\/tdmrep-license"},{"start":{"date-parts":[[2026,5,3]],"date-time":"2026-05-03T00:00:00Z","timestamp":1777766400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by-nc-nd\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100008530","name":"European Regional Development Fund","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100008530","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000780","name":"European Commission","doi-asserted-by":"publisher","award":["1058 23\/06\/2022"],"award-info":[{"award-number":["1058 23\/06\/2022"]}],"id":[{"id":"10.13039\/501100000780","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000780","name":"European Commission","doi-asserted-by":"publisher","award":["ECS00000043"],"award-info":[{"award-number":["ECS00000043"]}],"id":[{"id":"10.13039\/501100000780","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000780","name":"European Commission","doi-asserted-by":"publisher","award":["2023-T1\/COM-29001"],"award-info":[{"award-number":["2023-T1\/COM-29001"]}],"id":[{"id":"10.13039\/501100000780","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["elsevier.com","sciencedirect.com"],"crossmark-restriction":true},"short-container-title":["Artificial Intelligence"],"published-print":{"date-parts":[[2026,8]]},"DOI":"10.1016\/j.artint.2026.104553","type":"journal-article","created":{"date-parts":[[2026,5,9]],"date-time":"2026-05-09T06:45:06Z","timestamp":1778309106000},"page":"104553","update-policy":"https:\/\/doi.org\/10.1016\/elsevier_cm_policy","source":"Crossref","is-referenced-by-count":0,"special_numbering":"C","title":["An optimal pastification algorithm for LTL[X,F] and LTL[X,G]"],"prefix":"10.1016","volume":"357","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3852-9351","authenticated-orcid":false,"given":"Alessandro","family":"Artale","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7125-787X","authenticated-orcid":false,"given":"Luca","family":"Geatti","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2254-4821","authenticated-orcid":false,"given":"Nicola","family":"Gigante","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1104-7299","authenticated-orcid":false,"given":"Alessio","family":"Mansutti","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8512-1933","authenticated-orcid":false,"given":"Andrea","family":"Mazzullo","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4322-769X","authenticated-orcid":false,"given":"Angelo","family":"Montanari","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"78","reference":[{"key":"10.1016\/j.artint.2026.104553_bib0001","series-title":"KR","article-title":"A singly exponential transformation of LTL[X,F] into pure past LTL","author":"Artale","year":"2023"},{"key":"10.1016\/j.artint.2026.104553_bib0002","series-title":"SFCS","first-page":"46","article-title":"The temporal logic of programs","author":"Pnueli","year":"1977"},{"key":"10.1016\/j.artint.2026.104553_bib0003","series-title":"Workshop on Logic of Programs","article-title":"The glory of the past","author":"Lichtenstein","year":"1985"},{"key":"10.1016\/j.artint.2026.104553_bib0004","series-title":"IJCAI","article-title":"Linear temporal logic and linear dynamic logic on finite traces","author":"De Giacomo","year":"2013"},{"key":"10.1016\/j.artint.2026.104553_bib0005","series-title":"IJCAI","article-title":"Pure-past linear temporal and dynamic logic on finite traces","author":"De Giacomo","year":"2021"},{"key":"10.1016\/j.artint.2026.104553_bib0006","series-title":"TIME","article-title":"LTL over finite words can be exponentially more succinct than pure-past LTL, and vice versa","author":"Artale","year":"2023"},{"key":"10.1016\/j.artint.2026.104553_bib0007","doi-asserted-by":"crossref","DOI":"10.1016\/j.ic.2024.105262","article-title":"Succinctness issues for LTL and safety and cosafety fragments of LTL","volume":"302","author":"Artale","year":"2025","journal-title":"Inf. Comput."},{"key":"10.1016\/j.artint.2026.104553_bib0008","series-title":"ICALP","article-title":"Characterization of temporal property classes","author":"Chang","year":"1992"},{"key":"10.1016\/j.artint.2026.104553_bib0009","article-title":"Extended bounded response LTL: a new safety fragment for efficient reactive synthesis","author":"Cimatti","year":"2021","journal-title":"Form. Methods Syst. Des."},{"key":"10.1016\/j.artint.2026.104553_bib0010","doi-asserted-by":"crossref","DOI":"10.1145\/3506799","article-title":"Monitoring constraints and metaconstraints with temporal logics on finite traces","author":"De Giacomo","year":"2022","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"10.1016\/j.artint.2026.104553_bib0011","series-title":"ICAPS","article-title":"Planning for temporally extended goals in pure-past linear temporal logic: a polynomial reduction to standard planning","author":"De Giacomo","year":"2022"},{"key":"10.1016\/j.artint.2026.104553_bib0012","series-title":"Proceedings of POPL\u201989","first-page":"179","article-title":"On the synthesis of a reactive module","author":"Pnueli","year":"1989"},{"key":"10.1016\/j.artint.2026.104553_bib0013","series-title":"AAAI","article-title":"Complexity of safety and cosafety fragments of linear temporal logic","author":"Artale","year":"2023"},{"key":"10.1016\/j.artint.2026.104553_bib0014","series-title":"Modular Synthesis of Reactive Systems","author":"Rosner","year":"1992"},{"key":"10.1016\/j.artint.2026.104553_bib0015","series-title":"IJCAI","article-title":"Synthesis for LTL and LDL on finite traces","author":"De Giacomo","year":"2015"},{"key":"10.1016\/j.artint.2026.104553_bib0016","series-title":"AAAI","article-title":"Foundations of reactive synthesis for declarative process specifications","author":"Geatti","year":"2024"},{"key":"10.1016\/j.artint.2026.104553_bib0017","series-title":"BPM","article-title":"Foundations of collaborative sfDECLARE","author":"Geatti","year":"2023"},{"key":"10.1016\/j.artint.2026.104553_bib0018","series-title":"FORMATS","article-title":"Real time temporal logic: past, present, future","author":"Maler","year":"2005"},{"key":"10.1016\/j.artint.2026.104553_bib0019","series-title":"CAV","article-title":"On synthesizing controllers from bounded-response properties","author":"Maler","year":"2007"},{"key":"10.1016\/j.artint.2026.104553_bib0020","series-title":"FOSSACS","article-title":"Succinctness of cosafety fragments of LTL via combinatorial proof systems","author":"Geatti","year":"2024"},{"key":"10.1016\/j.artint.2026.104553_bib0021","doi-asserted-by":"crossref","DOI":"10.1007\/s10817-023-09691-1","article-title":"SAT meets tableaux for linear temporal logic satisfiability","author":"Geatti","year":"2024","journal-title":"J. Autom. Reason."},{"key":"10.1016\/j.artint.2026.104553_sbref0022","series-title":"OVERLAY","article-title":"BLACK: A fast, flexible and reliable LTL satisfiability checker","author":"Geatti","year":"2021"},{"issue":"3","key":"10.1016\/j.artint.2026.104553_bib0023","doi-asserted-by":"crossref","first-page":"733","DOI":"10.1145\/3828.3837","article-title":"The complexity of propositional linear temporal logics","volume":"32","author":"Sistla","year":"1985","journal-title":"J. ACM"},{"issue":"6\u20137","key":"10.1016\/j.artint.2026.104553_bib0024","doi-asserted-by":"crossref","first-page":"431","DOI":"10.1007\/s00236-003-0136-5","article-title":"Past is for free: on the complexity of verifying linear temporal properties with past","volume":"40","author":"Markey","year":"2004","journal-title":"Acta Inform."},{"key":"10.1016\/j.artint.2026.104553_bib0025","series-title":"Conference Record of the Seventh Annual ACM Symposium on Principles of Programming Languages, Las Vegas, Nevada, USA, January 1980","first-page":"163","article-title":"On the temporal analysis of fairness","author":"Gabbay","year":"1980"},{"key":"10.1016\/j.artint.2026.104553_bib0026","series-title":"Proceedings 17th Annual IEEE Symposium on Logic in Computer Science","first-page":"383","article-title":"Temporal logic with forgettable past","author":"Laroussinie","year":"2002"},{"key":"10.1016\/j.artint.2026.104553_bib0027","series-title":"Temporal Logic in Specification, Altrincham, UK, April 8\u201310, 1987, Proceedings","first-page":"409","article-title":"The declarative past and imperative future: executable temporal logic for interactive systems","volume":"Vol. 398","author":"Gabbay","year":"1987"},{"key":"10.1016\/j.artint.2026.104553_bib0028","series-title":"We Will Show Them! Essays in Honour of Dov Gabbay","first-page":"117","article-title":"Separation\u2013past, present, and future","volume":"Vol. 2","author":"Hodkinson","year":"2005"},{"key":"10.1016\/j.artint.2026.104553_bib0029","series-title":"Stepwise Refinement of Distributed Systems, Models, Formalisms, Correctness, REX Workshop, Mook, the Netherlands, May 29\u2013June 2, 1989, Proceedings","first-page":"94","article-title":"METATEM: a framework for programming in temporal logic","volume":"Vol. 430","author":"Barringer","year":"1989"},{"key":"10.1016\/j.artint.2026.104553_bib0030","first-page":"17416","article-title":"Foundations of reactive synthesis for declarative process specifications","author":"Geatti","year":"2024"},{"key":"10.1016\/j.artint.2026.104553_bib0031","series-title":"AAAI-25, Sponsored by the Association for the Advancement of Artificial Intelligence, February 2,\u2013March 4, 2025, Philadelphia, PA, USA","first-page":"14940","article-title":"First-order automata","author":"Geatti","year":"2025"},{"key":"10.1016\/j.artint.2026.104553_bib0032","series-title":"Time for Verification, Essays in Memory of Amir Pnueli","article-title":"On the Krohn-Rhodes cascaded decomposition theorem","author":"Maler","year":"2010"},{"key":"10.1016\/j.artint.2026.104553_bib0033","series-title":"FOCS","article-title":"Tight bounds on the complexity of cascaded decomposition of automata","author":"Maler","year":"1990"},{"key":"10.1016\/j.artint.2026.104553_bib0034","doi-asserted-by":"crossref","DOI":"10.1023\/A:1011254632723","article-title":"Model checking of safety properties","author":"Kupferman","year":"2001","journal-title":"Form. Methods Syst. Des."},{"key":"10.1016\/j.artint.2026.104553_bib0035","doi-asserted-by":"crossref","DOI":"10.1090\/S0002-9947-1965-0188316-1","article-title":"Algebraic theory of machines. I. Prime decomposition theorem for finite semigroups and machines","author":"Krohn","year":"1965","journal-title":"Trans. Am. Math. Soc."},{"key":"10.1016\/j.artint.2026.104553_bib0036","series-title":"Counter-Free Automata (MIT Research Monograph no. 65)","author":"McNaughton","year":"1971"},{"key":"10.1016\/j.artint.2026.104553_bib0037","series-title":"STACS","article-title":"On cascades of reset automata","author":"Borelli","year":"2025"}],"container-title":["Artificial Intelligence"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0004370226000792?httpAccept=text\/xml","content-type":"text\/xml","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/api.elsevier.com\/content\/article\/PII:S0004370226000792?httpAccept=text\/plain","content-type":"text\/plain","content-version":"vor","intended-application":"text-mining"}],"deposited":{"date-parts":[[2026,7,3]],"date-time":"2026-07-03T19:52:57Z","timestamp":1783108377000},"score":1,"resource":{"primary":{"URL":"https:\/\/linkinghub.elsevier.com\/retrieve\/pii\/S0004370226000792"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2026,8]]},"references-count":37,"alternative-id":["S0004370226000792"],"URL":"https:\/\/doi.org\/10.1016\/j.artint.2026.104553","relation":{},"ISSN":["0004-3702"],"issn-type":[{"value":"0004-3702","type":"print"}],"subject":[],"published":{"date-parts":[[2026,8]]},"assertion":[{"value":"Elsevier","name":"publisher","label":"This article is maintained by"},{"value":"An optimal pastification algorithm for and","name":"articletitle","label":"Article Title"},{"value":"Artificial Intelligence","name":"journaltitle","label":"Journal Title"},{"value":"https:\/\/doi.org\/10.1016\/j.artint.2026.104553","name":"articlelink","label":"CrossRef DOI link to publisher maintained version"},{"value":"article","name":"content_type","label":"Content Type"},{"value":"\u00a9 2026 The Author(s). Published by Elsevier B.V.","name":"copyright","label":"Copyright"}],"article-number":"104553"}}