{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,20]],"date-time":"2025-10-20T20:01:12Z","timestamp":1760990472910,"version":"3.41.0"},"reference-count":101,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2024,4,16]],"date-time":"2024-04-16T00:00:00Z","timestamp":1713225600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"MUR PNRR project FAIR - Future AI Research","award":["PE00000013"],"award-info":[{"award-number":["PE00000013"]}]},{"name":"NextGenerationEU"},{"DOI":"10.13039\/501100005416","name":"Research Council of Norway","doi-asserted-by":"crossref","award":["316022"],"award-info":[{"award-number":["316022"]}],"id":[{"id":"10.13039\/501100005416","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2024,4,30]]},"abstract":"<jats:p>\n            Formalisms based on temporal logics interpreted over finite strict linear orders, known in the literature as\n            <jats:italic>finite traces<\/jats:italic>\n            , have been used for temporal specification in automated planning, process modelling, (runtime) verification and synthesis of programs, as well as in knowledge representation and reasoning. In this article, we focus on\n            <jats:italic>first-order temporal logic on finite traces<\/jats:italic>\n            . We first investigate preservation of equivalences and satisfiability of formulas between finite and infinite traces, by providing a set of semantic and syntactic conditions to guarantee when the distinction between reasoning in the two cases can be blurred. Moreover, we show that the satisfiability problem on finite traces for several decidable fragments of first-order temporal logic is\n            <jats:sc>ExpSpace<\/jats:sc>\n            -complete, as in the infinite trace case, while it decreases to\n            <jats:sc>NExpTime<\/jats:sc>\n            when finite traces bounded in the number of instants are considered. This leads also to new complexity results for temporal description logics over finite traces. Finally, we investigate applications to planning and verification, in particular by establishing connections with the notions of insensitivity to infiniteness and safety from the literature.\n          <\/jats:p>","DOI":"10.1145\/3651161","type":"journal-article","created":{"date-parts":[[2024,3,5]],"date-time":"2024-03-05T12:11:17Z","timestamp":1709640677000},"page":"1-43","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["First-Order Temporal Logic on Finite Traces: Semantic Properties, Decidable Fragments, and Applications"],"prefix":"10.1145","volume":"25","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3852-9351","authenticated-orcid":false,"given":"Alessandro","family":"Artale","sequence":"first","affiliation":[{"name":"Faculty of Engineering, Free University of Bozen-Bolzano, Bolzano, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8512-1933","authenticated-orcid":false,"given":"Andrea","family":"Mazzullo","sequence":"additional","affiliation":[{"name":"Faculty of Engineering, Free University of Bozen-Bolzano, Bolzano, Italy and Department of Information Engineering and Computer Science, University of Trento, Trento, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3889-6207","authenticated-orcid":false,"given":"Ana","family":"Ozaki","sequence":"additional","affiliation":[{"name":"Department of Informatics, University of Bergen, Bergen, Norway and Department of Informatics, University of Oslo, Oslo, Norway"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,4,16]]},"reference":[{"key":"e_1_3_3_2_2","volume-title":"Proceedings of the 30th International Workshop on Description Logics","author":"Aalst Wil van der","year":"2017","unstructured":"Wil van der Aalst, Alessandro Artale, Marco Montali, and Simone Tritini. 2017. Object-centric behavioral constraints: Integrating data and declarative process modelling. In Proceedings of the 30th International Workshop on Description Logics. CEUR-WS.org."},{"key":"e_1_3_3_3_2","first-page":"1","volume-title":"Proceedings of the International Workshop on Web Services and Formal Methods.","author":"Aalst Wil van der","year":"2006","unstructured":"Wil van der Aalst and Maja Pesic. 2006. DecSerFlow: Towards a truly declarative service flow language. In Proceedings of the International Workshop on Web Services and Formal Methods.Springer, 1\u201323."},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.1145\/585265.585270"},{"key":"e_1_3_3_5_2","doi-asserted-by":"crossref","first-page":"375","DOI":"10.1016\/S1574-6526(05)80014-8","volume-title":"Proceedings of the Handbook of Temporal Reasoning in Artificial Intelligence","author":"Artale Alessandro","year":"2005","unstructured":"Alessandro Artale and Enrico Franconi. 2005. Temporal description logics. In Proceedings of the Handbook of Temporal Reasoning in Artificial Intelligence. Elsevier, 375\u2013388."},{"key":"e_1_3_3_6_2","first-page":"98","volume-title":"Proceedings of the 8th European Workshop on Logics in Artificial Intelligence on Logics in Artificial Intelligence","author":"Artale Alessandro","year":"2002","unstructured":"Alessandro Artale, Enrico Franconi, Frank Wolter, and Michael Zakharyaschev. 2002. A temporal description logic for reasoning over conceptual schemas and queries. In Proceedings of the 8th European Workshop on Logics in Artificial Intelligence on Logics in Artificial Intelligence. Springer-Verlag, 98\u2013110."},{"key":"e_1_3_3_7_2","first-page":"85","volume-title":"Short Paper Proceedings of the 5th Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis","author":"Artale Alessandro","year":"2023","unstructured":"Alessandro Artale, Luca Geatti, Nicola Gigante, and Andrea Mazzullo. 2023. A landscape of first-order linear temporal logics in infinite-state verification and temporal ontologies. In Short Paper Proceedings of the 5th Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis. CEUR-WS.org, 85\u201392."},{"key":"e_1_3_3_8_2","volume-title":"Proceedings of the 37th AAAI Conference on Artificial Intelligence (AAAI\u201923)","author":"Artale Alessandro","year":"2023","unstructured":"Alessandro Artale, Luca Geatti, Nicola Gigante, Andrea Mazzullo, and Angelo Montanari. 2023. Complexity of safety and coSafety fragments of linear temporal logic. In Proceedings of the 37th AAAI Conference on Artificial Intelligence (AAAI\u201923). AAAI Press."},{"key":"e_1_3_3_9_2","first-page":"1:1\u20131:37","volume-title":"Proceedings of the 24th Int. Symposium on Temporal Representation and Reasoning.","author":"Artale Alessandro","year":"2017","unstructured":"Alessandro Artale, Roman Kontchakov, Alisa Kovtunova, Vladislav Ryzhikov, Frank Wolter, and Michael Zakharyaschev. 2017. Temporal ontology-mediated querying: A survey. In Proceedings of the 24th Int. Symposium on Temporal Representation and Reasoning.Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Mons, Belgium, 1:1\u20131:37."},{"issue":"3","key":"e_1_3_3_10_2","first-page":"25:1\u201325:50","article-title":"A cookbook for temporal conceptual data modelling with description logics","volume":"15","author":"Artale Alessandro","year":"2014","unstructured":"Alessandro Artale, Roman Kontchakov, Vladislav Ryzhikov, and Michael Zakharyaschev. 2014. A cookbook for temporal conceptual data modelling with description logics. ACM Transactions on Computational Logic 15, 3 (2014), 25:1\u201325:50.","journal-title":"ACM Transactions on Computational Logic"},{"key":"e_1_3_3_11_2","doi-asserted-by":"crossref","unstructured":"Alessandro Artale Alisa Kovtunova Marco Montali and Wil M. P. van der Aalst. 2019. Modeling and reasoning over declarative data-aware processes with object-centric behavioral constraints. In Business Process Management: 17th International Conference BPM 2019 Vienna Austria September 16 2019 Proceedings 17. Springer.","DOI":"10.1007\/978-3-030-26619-6_11"},{"key":"e_1_3_3_12_2","volume-title":"Proceedings of the 31st International Workshop on Description Logics.","author":"Artale Alessandro","year":"2018","unstructured":"Alessandro Artale, Andrea Mazzullo, and Ana Ozaki. 2018. Temporal description logics over finite traces. In Proceedings of the 31st International Workshop on Description Logics. CEUR-WS.org."},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.5555\/3367243.3367249"},{"key":"e_1_3_3_14_2","volume-title":"Proceedings of the 32nd International Workshop on Description Logics","author":"Artale Alessandro","year":"2019","unstructured":"Alessandro Artale, Andrea Mazzullo, and Ana Ozaki. 2019. Temporal DL-Lite over finite traces (preliminary results). In Proceedings of the 32nd International Workshop on Description Logics. CEUR-WS.org."},{"key":"e_1_3_3_15_2","first-page":"23","volume-title":"Proceedings of the 2nd Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis","author":"Artale Alessandro","year":"2020","unstructured":"Alessandro Artale, Andrea Mazzullo, and Ana Ozaki. 2020. Finite vs. infinite traces in temporal logics. In Proceedings of the 2nd Workshop on Artificial Intelligence and Formal Verification, Logic, Automata, and Synthesis. CEUR-WS.org, 23\u201327."},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.5555\/1807707.1807718"},{"key":"e_1_3_3_17_2","doi-asserted-by":"crossref","first-page":"60","DOI":"10.1007\/978-3-319-66167-4_4","volume-title":"Proceedings of the 11th Int. Symposium on Frontiers of Combining Systems","author":"Baader Franz","year":"2017","unstructured":"Franz Baader, Stefan Borgwardt, Patrick Koopmann, Ana Ozaki, and Veronika Thost. 2017. Metric temporal description logics with interval-rigid names. In Proceedings of the 11th Int. Symposium on Frontiers of Combining Systems. Springer, 60\u201376."},{"issue":"4","key":"e_1_3_3_18_2","first-page":"30:1\u201330:46","article-title":"Metric temporal description logics with interval-rigid names","volume":"21","author":"Baader Franz","year":"2020","unstructured":"Franz Baader, Stefan Borgwardt, Patrick Koopmann, Ana Ozaki, and Veronika Thost. 2020. Metric temporal description logics with interval-rigid names. ACM Transactions on Computational Logic 21, 4 (2020), 30:1\u201330:46.","journal-title":"ACM Transactions on Computational Logic"},{"key":"e_1_3_3_19_2","volume-title":"The Description Logic Handbook: Theory, Implementation, and Applications","author":"Baader F.","year":"2003","unstructured":"F. Baader, D. Calvanese, D. L. McGuinness, D. Nardi, and P. F. Patel-Schneider (Eds.). 2003. The Description Logic Handbook: Theory, Implementation, and Applications. Cambridge University Press."},{"issue":"3","key":"e_1_3_3_20_2","first-page":"21:1\u201321:32","article-title":"LTL over description logic axioms","volume":"13","author":"Baader Franz","year":"2012","unstructured":"Franz Baader, Silvio Ghilardi, and Carsten Lutz. 2012. LTL over description logic axioms. ACM Transactions on Computational Logic 13, 3 (2012), 21:1\u201321:32.","journal-title":"ACM Transactions on Computational Logic"},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.5555\/885746.885753"},{"key":"e_1_3_3_22_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jal.2014.09.001"},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.1023\/A:1018985923441"},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0004-3702(99)00071-5"},{"key":"e_1_3_3_25_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_3_26_2","first-page":"788","volume-title":"Proceedings of the 21st National Conference on Artificial Intelligence","author":"Baier Jorge A.","year":"2006","unstructured":"Jorge A. Baier and Sheila A. McIlraith. 2006. Planning with first-order temporally extended goals using heuristic search. In Proceedings of the 21st National Conference on Artificial Intelligence. AAAI Press, 788\u2013795."},{"key":"e_1_3_3_27_2","first-page":"173","volume-title":"Proceedings of the 13th Annual ACM Symposium on Principles of Programming Languages","author":"Barringer Howard","year":"1986","unstructured":"Howard Barringer, Ruurd Kuiper, and Amir Pnueli. 1986. A really abstract concurrent model and its temporal logic. In Proceedings of the 13th Annual ACM Symposium on Principles of Programming Languages. ACM, 173\u2013183."},{"key":"e_1_3_3_28_2","doi-asserted-by":"crossref","first-page":"547","DOI":"10.1007\/978-3-319-96145-3_29","volume-title":"Proceedings of the 30th International Conference on Computer Aided Verification.","author":"Bartocci Ezio","year":"2018","unstructured":"Ezio Bartocci, Roderick Bloem, Dejan Nickovic, and Franz R\u00f6ck. 2018. A counting semantics for monitoring LTL specifications over finite traces. In Proceedings of the 30th International Conference on Computer Aided Verification.Springer, 547\u2013564."},{"key":"e_1_3_3_29_2","first-page":"881","volume-title":"Proceedings of the 19th European Conference on Artificial Intelligence.","author":"Bauer Andreas","year":"2010","unstructured":"Andreas Bauer and Patrik Haslum. 2010. LTL goal specifications revisited. In Proceedings of the 19th European Conference on Artificial Intelligence.IOS Press, 881\u2013886."},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exn075"},{"key":"e_1_3_3_31_2","doi-asserted-by":"publisher","DOI":"10.5555\/2351776.2351780"},{"key":"e_1_3_3_32_2","doi-asserted-by":"publisher","DOI":"10.5555\/2444851.2444852"},{"key":"e_1_3_3_33_2","doi-asserted-by":"publisher","DOI":"10.5555\/3304415.3304428"},{"key":"e_1_3_3_34_2","doi-asserted-by":"crossref","unstructured":"Francesco Belardinelli Alessio Lomuscio Aniello Murano and Sasha Rubin. 2019. Imperfect information in alternating-time temporal logic on finite traces. In PRIMA 2019: Principles and Practice of Multi-Agent Systems: 22nd International Conference Turin Italy October 2831 2019 Proceedings 22. Springer 469\u2013477.","DOI":"10.1007\/978-3-030-33792-6_31"},{"key":"e_1_3_3_35_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-59207-2"},{"key":"e_1_3_3_36_2","doi-asserted-by":"crossref","first-page":"148","DOI":"10.1007\/978-3-030-20528-7_12","volume-title":"Proceedings of the 15th International Conference on Logic Programming and Nonmonotonic Reasoning.","author":"Cabalar Pedro","year":"2019","unstructured":"Pedro Cabalar, Mart\u00edn Di\u00e9guez, and Torsten Schaub. 2019. Towards dynamic answer set programming over finite traces. In Proceedings of the 15th International Conference on Logic Programming and Nonmonotonic Reasoning.Springer, 148\u2013162."},{"issue":"3","key":"e_1_3_3_37_2","doi-asserted-by":"crossref","first-page":"406","DOI":"10.1017\/S1471068418000297","article-title":"Temporal answer set programming on finite traces","volume":"18","author":"Cabalar Pedro","year":"2018","unstructured":"Pedro Cabalar, Roland Kaminski, Torsten Schaub, and Anna Schuhmann. 2018. Temporal answer set programming on finite traces. Theory and Practice of Logic Programming 18, 3-4 (2018), 406\u2013420.","journal-title":"Theory and Practice of Logic Programming"},{"key":"e_1_3_3_38_2","first-page":"3","volume-title":"Proceedings of the 3rd International Workshop on the Resurgence of Datalog in Academia and Industry.","author":"Cabalar Pedro","year":"2019","unstructured":"Pedro Cabalar and Torsten Schaub. 2019. Dynamic and temporal answer set programming on linear finite traces. In Proceedings of the 3rd International Workshop on the Resurgence of Datalog in Academia and Industry.. CEUR-WS.org, 3\u20136."},{"key":"e_1_3_3_39_2","first-page":"593","volume-title":"Proceedings of the 8th International Conference on Principles of Knowledge Representation and Reasoning","author":"Calvanese Diego","year":"2002","unstructured":"Diego Calvanese, Giuseppe De Giacomo, and Moshe Y. Vardi. 2002. Reasoning about actions and planning in LTL action theories. In Proceedings of the 8th International Conference on Principles of Knowledge Representation and Reasoning. 593\u2013602."},{"key":"e_1_3_3_40_2","first-page":"29","volume-title":"Proceedings of the 28th International Conference on Automated Planning and Scheduling","author":"Camacho Alberto","year":"2018","unstructured":"Alberto Camacho, Jorge A. Baier, Christian J. Muise, and Sheila A. McIlraith. 2018. Finite LTL synthesis as planning. In Proceedings of the 28th International Conference on Automated Planning and Scheduling. AAAI Press, 29\u201338."},{"key":"e_1_3_3_41_2","first-page":"454","volume-title":"Proceedings of the 16th International Conference on Principles of Knowledge Representation and Reasoning","author":"Camacho Alberto","year":"2018","unstructured":"Alberto Camacho, Meghyn Bienvenu, and Sheila A. McIlraith. 2018. Finite LTL synthesis with environment assumptions and quality measures. In Proceedings of the 16th International Conference on Principles of Knowledge Representation and Reasoning. AAAI Press, 454\u2013463."},{"key":"e_1_3_3_42_2","first-page":"3716","volume-title":"Proceedings of the 31st National Conference on Artificial Intelligence","author":"Camacho Alberto","year":"2017","unstructured":"Alberto Camacho, Eleni Triantafillou, Christian J. Muise, Jorge A. Baier, and Sheila A. McIlraith. 2017. Non-deterministic planning with temporally extended goals: LTL over finite and infinite traces. In Proceedings of the 31st National Conference on Artificial Intelligence. AAAI Press, 3716\u20133724."},{"key":"e_1_3_3_43_2","doi-asserted-by":"crossref","first-page":"124","DOI":"10.1007\/3-540-69778-0_18","volume-title":"Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods.","author":"Cerrito Serenella","year":"1998","unstructured":"Serenella Cerrito and Marta Cialdea Mayer. 1998. Bounded model search in linear temporal logic and its application to planning. In Proceedings of the International Conference on Automated Reasoning with Analytic Tableaux and Related Methods.Springer, 124\u2013140."},{"key":"e_1_3_3_44_2","first-page":"141","volume-title":"Proceedings of the 8th International Conference on Artificial Intelligence: Methodology, Systems, and Applications.","author":"Cerrito Serenella","year":"1998","unstructured":"Serenella Cerrito and Marta Cialdea Mayer. 1998. Using linear temporal logic to model and solve planning problems. In Proceedings of the 8th International Conference on Artificial Intelligence: Methodology, Systems, and Applications.Springer, 141\u2013152."},{"key":"e_1_3_3_45_2","doi-asserted-by":"publisher","DOI":"10.5555\/645709.756558"},{"issue":"3","key":"e_1_3_3_46_2","article-title":"A first-order logic characterization of safety and co-safety languages","volume":"19","author":"Cimatti Alessandro","year":"2023","unstructured":"Alessandro Cimatti, Luca Geatti, Nicola Gigante, Angelo Montanari, and Stefano Tonetta. 2023. A first-order logic characterization of safety and co-safety languages. Log. Methods Comput. Sci. 19, 3 (2023), 13:1\u201313:29.","journal-title":"Log. Methods Comput. Sci."},{"key":"e_1_3_3_47_2","first-page":"1","volume-title":"Proceedings of the 12th International Conference on Business Process Management","author":"Giacomo Giuseppe De","year":"2014","unstructured":"Giuseppe De Giacomo, Riccardo De Masellis, Marco Grasso, Fabrizio Maria Maggi, and Marco Montali. 2014. Monitoring business metaconstraints based on LTL and LDL for finite traces. In Proceedings of the 12th International Conference on Business Process ManagementSpringer, 1\u201317."},{"key":"e_1_3_3_48_2","first-page":"1027","volume-title":"Proceedings of the 28th National Conference on Artificial Intelligence","author":"Giacomo Giuseppe De","year":"2014","unstructured":"Giuseppe De Giacomo, Riccardo De Masellis, and Marco Montali. 2014. Reasoning on LTL on finite traces: Insensitivity to infiniteness. In Proceedings of the 28th National Conference on Artificial Intelligence. AAAI Press, 1027\u20131033."},{"key":"e_1_3_3_49_2","first-page":"854","volume-title":"Proceedings of the 23rd International Joint Conference on Artificial Intelligence","author":"Giacomo Giuseppe De","year":"2013","unstructured":"Giuseppe De Giacomo and Moshe Y. Vardi. 2013. Linear temporal logic and linear dynamic logic on finite traces. In Proceedings of the 23rd International Joint Conference on Artificial Intelligence. IJCAI\/AAAI, 854\u2013860."},{"key":"e_1_3_3_50_2","first-page":"1558","volume-title":"Proceedings of the 24th International Joint Conference on Artificial Intelligence","author":"Giacomo Giuseppe De","year":"2015","unstructured":"Giuseppe De Giacomo and Moshe Y. Vardi. 2015. Synthesis for LTL and LDL on finite traces. In Proceedings of the 24th International Joint Conference on Artificial Intelligence. AAAI Press, 1558\u20131564."},{"key":"e_1_3_3_51_2","first-page":"6346","volume-title":"Proceedings of the 37th AAAI Conference on Artificial Intelligence","author":"Felli Paolo","year":"2023","unstructured":"Paolo Felli, Marco Montali, Fabio Patrizi, and Sarah Winkler. 2023. Monitoring arithmetic temporal properties on finite traces. In Proceedings of the 37th AAAI Conference on Artificial Intelligence. Brian Williams, Yiling Chen, and Jennifer Neville (Eds.), AAAI Press, 6346\u20136354."},{"key":"e_1_3_3_52_2","first-page":"971","volume-title":"Proceedings of the 30th National Conference on Artificial Intelligence","author":"Fionda Valeria","year":"2016","unstructured":"Valeria Fionda and Gianluigi Greco. 2016. The complexity of LTL on finite traces: Hard and easy fragments. In Proceedings of the 30th National Conference on Artificial Intelligence. AAAI Press, 971\u2013977."},{"key":"e_1_3_3_53_2","doi-asserted-by":"publisher","DOI":"10.1613\/jair.1.11256"},{"key":"e_1_3_3_54_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0013976"},{"key":"e_1_3_3_55_2","volume-title":"Many-dimensional Modal Logics: Theory and Applications","author":"Gabbay Dov M.","year":"2003","unstructured":"Dov M. Gabbay, Agi Kurucz, Frank Wolter, and Michael Zakharyaschev. 2003. Many-dimensional Modal Logics: Theory and Applications. Elsevier."},{"key":"e_1_3_3_56_2","first-page":"2641","volume-title":"Proceedings of the 31st International Joint Conference on Artificial Intelligence","author":"Geatti Luca","year":"2022","unstructured":"Luca Geatti, Alessandro Gianola, and Nicola Gigante. 2022. Linear temporal logic modulo theories over finite traces. In Proceedings of the 31st International Joint Conference on Artificial Intelligence. ijcai.org, 2641\u20132647."},{"key":"e_1_3_3_57_2","first-page":"811","volume-title":"Proceedings of the 26th European Conference on Artificial Intelligence","author":"Geatti Luca","year":"2023","unstructured":"Luca Geatti, Alessandro Gianola, Nicola Gigante, and Sarah Winkler. 2023. Decidable fragments of LTL \\(_f\\) modulo theories. In Proceedings of the 26th European Conference on Artificial Intelligence. IOS Press, 811\u2013818."},{"key":"e_1_3_3_58_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.artint.2008.10.012"},{"key":"e_1_3_3_59_2","first-page":"227","volume-title":"Proceedings of the 18th International Conference on Principles of Knowledge Representation and Reasoning","author":"Giacomo Giuseppe De","year":"2021","unstructured":"Giuseppe De Giacomo, Aniello Murano, Fabio Patrizi, and Giuseppe Perelli. 2021. Timed trace alignment with metric temporal logic over finite traces. In Proceedings of the 18th International Conference on Principles of Knowledge Representation and Reasoning. 227\u2013236."},{"key":"e_1_3_3_60_2","first-page":"4959","volume-title":"Proceedings of the 29th Internatinal Joint Conference on Artificial Intelligence.","author":"Giacomo Giuseppe De","year":"2020","unstructured":"Giuseppe De Giacomo, Antonio Di Stasio, Francesco Fuggitti, and Sasha Rubin. 2020. Pure-past linear temporal and dynamic logic on finite traces. In Proceedings of the 29th Internatinal Joint Conference on Artificial Intelligence. ijcai.org, 4959\u20134965."},{"key":"e_1_3_3_61_2","first-page":"1852","volume-title":"Proceedings of the 30th International Joint Conference on Artificial Intelligence.","author":"Giacomo Giuseppe De","year":"2021","unstructured":"Giuseppe De Giacomo, Antonio Di Stasio, Lucas M. Tabajara, Moshe Y. Vardi, and Shufang Zhu. 2021. Finite-trace and generalized-reactivity specifications in temporal synthesis. In Proceedings of the 30th International Joint Conference on Artificial Intelligence. ijcai.org, 1852\u20131858."},{"key":"e_1_3_3_62_2","first-page":"304","volume-title":"Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning","author":"Giacomo Giuseppe De","year":"2020","unstructured":"Giuseppe De Giacomo, Antonio Di Stasio, Moshe Y. Vardi, and Shufang Zhu. 2020. Two-stage technique for LTL \\(_f\\) synthesis under LTL assumptions. In Proceedings of the 17th International Conference on Principles of Knowledge Representation and Reasoning. 304\u2013314."},{"key":"e_1_3_3_63_2","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2001.989841"},{"key":"e_1_3_3_64_2","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/9.2.273"},{"key":"e_1_3_3_65_2","doi-asserted-by":"publisher","DOI":"10.5555\/24401"},{"key":"e_1_3_3_66_2","doi-asserted-by":"publisher","DOI":"10.5555\/3091125.3091225"},{"key":"e_1_3_3_67_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2020.104555"},{"key":"e_1_3_3_68_2","first-page":"1074","volume-title":"Proceedings of the 26th International Joint Conference on Artificial Intelligence.","author":"Guti\u00e9rrez-Basulto V\u00edctor","year":"2017","unstructured":"V\u00edctor Guti\u00e9rrez-Basulto and Jean Christoph Jung. 2017. Combining DL-Lite \\(_{\\mathit {bool}}^{\\mathcal {N}}\\) with branching time: A gentle marriage. In Proceedings of the 26th International Joint Conference on Artificial Intelligence. ijcai.org, 1074\u20131080."},{"key":"e_1_3_3_69_2","doi-asserted-by":"publisher","DOI":"10.5555\/3007337.3007408"},{"key":"e_1_3_3_70_2","first-page":"837","volume-title":"Proceedings of the 22nd European Conference on Artificial Intelligence","author":"Guti\u00e9rrez-Basulto V\u00edctor","year":"2016","unstructured":"V\u00edctor Guti\u00e9rrez-Basulto, Jean Christoph Jung, and Ana Ozaki. 2016. On metric temporal description logics. In Proceedings of the 22nd European Conference on Artificial Intelligence. IOS Press, 837\u2013845."},{"key":"e_1_3_3_71_2","volume-title":"Proceedings of the 14th International Conference on Principles of Knowledge Representation and Reasoning.","author":"Guti\u00e9rrez-Basulto V\u00edctor","year":"2014","unstructured":"V\u00edctor Guti\u00e9rrez-Basulto, Jean Christoph Jung, and Thomas Schneider. 2014. Lightweight description logics and branching time: A troublesome marriage. In Proceedings of the 14th International Conference on Principles of Knowledge Representation and Reasoning. AAAI Press."},{"key":"e_1_3_3_72_2","doi-asserted-by":"publisher","DOI":"10.5555\/2832581.2832670"},{"key":"e_1_3_3_73_2","first-page":"382","volume-title":"Proceedings of the 11th Conference on Advances in Modal Logic","author":"Hampson Christopher","year":"2016","unstructured":"Christopher Hampson. 2016. Decidable first-order modal logics with counting quantifiers. In Proceedings of the 11th Conference on Advances in Modal Logic. College Publications, 382\u2013400."},{"issue":"3","key":"e_1_3_3_74_2","first-page":"27:1\u201327:36","article-title":"Undecidable propositional bimodal logics and one-variable first-order linear temporal logics with counting","volume":"16","author":"Hampson Christopher","year":"2015","unstructured":"Christopher Hampson and Agi Kurucz. 2015. Undecidable propositional bimodal logics and one-variable first-order linear temporal logics with counting. ACM Transactions on Computational Logic 16, 3 (2015), 27:1\u201327:36.","journal-title":"ACM Transactions on Computational Logic"},{"key":"e_1_3_3_75_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(98)00039-6"},{"key":"e_1_3_3_76_2","first-page":"91","volume-title":"Proceedings of the 10th International Symposium on Temporal Representation and Reasoning \/ 4th International Conference on Temporal Logic","author":"Hodkinson Ian M.","year":"2003","unstructured":"Ian M. Hodkinson, Roman Kontchakov, Agi Kurucz, Frank Wolter, and Michael Zakharyaschev. 2003. On the computational complexity of decidable fragments of first-order linear temporal logics. In Proceedings of the 10th International Symposium on Temporal Representation and Reasoning \/ 4th International Conference on Temporal Logic. IEEE Computer Society, 91\u201398."},{"key":"e_1_3_3_77_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(00)00018-X"},{"key":"e_1_3_3_78_2","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664589"},{"key":"e_1_3_3_79_2","doi-asserted-by":"publisher","DOI":"10.5555\/3237383.3237414"},{"issue":"76","key":"e_1_3_3_80_2","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1023\/B:STUD.0000027468.28935.6d","article-title":"Temporalising tableaux","author":"Kontchakov Roman","year":"2004","unstructured":"Roman Kontchakov, Carsten Lutz, Frank Wolter, and Michael Zakharyaschev. 2004. Temporalising tableaux. Studia Logica76, 1 (2004), 91\u2013134.","journal-title":"Studia Logica"},{"key":"e_1_3_3_81_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"e_1_3_3_82_2","doi-asserted-by":"publisher","DOI":"10.5555\/647768.733927"},{"key":"e_1_3_3_83_2","first-page":"513","volume-title":"Proceedings of the 21st European Conference on Artificial Intelligence","author":"Li Jianwen","year":"2014","unstructured":"Jianwen Li, Lijun Zhang, Geguang Pu, Moshe Y. Vardi, and Jifeng He. 2014. LTL \\(_f\\) satisfiability checking. In Proceedings of the 21st European Conference on Artificial Intelligence. IOS Press, 513\u2013518."},{"key":"e_1_3_3_84_2","doi-asserted-by":"crossref","first-page":"611","DOI":"10.1007\/978-3-319-42634-1_49","volume-title":"Proceedings of the 22nd International Conference on Computing and Combinatorics.","author":"Liu Yao","year":"2016","unstructured":"Yao Liu, Zhenhua Duan, Cong Tian, and Bin Cui. 2016. Satisfiability of linear time mu-calculus on finite traces. In Proceedings of the 22nd International Conference on Computing and Combinatorics.Springer, 611\u2013622."},{"key":"e_1_3_3_85_2","first-page":"3","volume-title":"Proceedings of the 15th International Symposium on Temporal Representation and Reasoning","author":"Lutz Carsten","year":"2008","unstructured":"Carsten Lutz, Frank Wolter, and Michael Zakharyaschev. 2008. Temporal description logics: A survey. In Proceedings of the 15th International Symposium on Temporal Representation and Reasoning. IEEE Computer Society, 3\u201314."},{"key":"e_1_3_3_86_2","first-page":"10218","volume-title":"Proceedings of the 34th National Conference on Artificial Intelligence.","author":"Maggi Fabrizio Maria","year":"2020","unstructured":"Fabrizio Maria Maggi, Marco Montali, and Rafael Pe\u00f1aloza. 2020. Temporal logics over finite traces with uncertainty. In Proceedings of the 34th National Conference on Artificial Intelligence.AAAI Press, 10218\u201310225."},{"key":"e_1_3_3_87_2","doi-asserted-by":"crossref","first-page":"132","DOI":"10.1007\/978-3-642-23059-2_13","volume-title":"Proceedings of the 9th International Conference on Business Process Management.","author":"Maggi Fabrizio Maria","year":"2011","unstructured":"Fabrizio Maria Maggi, Marco Montali, Michael Westergaard, and Wil M. P. van der Aalst. 2011. Monitoring business constraints with linear temporal logic: An approach based on colored automata. In Proceedings of the 9th International Conference on Business Process Management.Springer, 132\u2013147."},{"key":"e_1_3_3_88_2","doi-asserted-by":"publisher","DOI":"10.5555\/211468"},{"key":"e_1_3_3_89_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2014.03.001"},{"key":"e_1_3_3_90_2","volume-title":"Proceedings of the DL","author":"Ozaki Ana","year":"2018","unstructured":"Ana Ozaki, Markus Kr\u00f6tzsch, and Sebastian Rudolph. 2018. Happy ever after: Temporally attributed description logics. In Proceedings of the DL."},{"key":"e_1_3_3_91_2","volume-title":"Proceedings of the Description Logic, Theory Combination, and All That - Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday","author":"Ozaki Ana","year":"2019","unstructured":"Ana Ozaki, Markus Kr\u00f6tzsch, and Sebastian Rudolph. 2019. Temporally attributed description logics. In Proceedings of the Description Logic, Theory Combination, and All That - Essays Dedicated to Franz Baader on the Occasion of His 60th Birthday."},{"key":"e_1_3_3_92_2","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1977.32"},{"key":"e_1_3_3_93_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-018-0321-3"},{"key":"e_1_3_3_94_2","doi-asserted-by":"publisher","DOI":"10.5555\/647838.738513"},{"key":"e_1_3_3_95_2","first-page":"1","volume-title":"Proceedings of the 27th Asia-Pacific Software Engineering Conference.","author":"Shi Yingying","year":"2020","unstructured":"Yingying Shi, Shengping Xiao, Jianwen Li, Jian Guo, and Geguang Pu. 2020. SAT-based automata construction for LTL over finite traces. In Proceedings of the 27th Asia-Pacific Software Engineering Conference.IEEE, 1\u201310."},{"key":"e_1_3_3_96_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211865"},{"key":"e_1_3_3_97_2","doi-asserted-by":"publisher","DOI":"10.5555\/646332.687492"},{"key":"e_1_3_3_98_2","first-page":"331","volume-title":"Proceedings of the Complexity, Logic, and Recursion Theory","author":"Boas Peter van Emde","year":"1997","unstructured":"Peter van Emde Boas. 1997. The convenience of tilings. In Proceedings of the Complexity, Logic, and Recursion Theory. CRC Press, 331\u2013363."},{"key":"e_1_3_3_99_2","first-page":"104","volume-title":"Proceedings of the 2nd International Symposium on Frontiers of Combining Systems.","author":"Wolter Frank","year":"1998","unstructured":"Frank Wolter and Michael Zakharyaschev. 1998. Temporalizing description logics. In Proceedings of the 2nd International Symposium on Frontiers of Combining Systems.Research Studies Press\/Wiley, 104\u2013109."},{"key":"e_1_3_3_100_2","doi-asserted-by":"publisher","DOI":"10.2307\/2695115"},{"issue":"1","key":"e_1_3_3_101_2","doi-asserted-by":"crossref","first-page":"133","DOI":"10.1016\/S0168-0072(01)00124-5","article-title":"Axiomatizing the monodic fragment of first-order temporal logic","author":"Wolter Frank","year":"2002","unstructured":"Frank Wolter and Michael Zakharyaschev. 2002. Axiomatizing the monodic fragment of first-order temporal logic. Annals of Pure and Applied logic1-2 (2002), 133\u2013145.","journal-title":"Annals of Pure and Applied logic"},{"key":"e_1_3_3_102_2","first-page":"6530","volume-title":"Proceedings of the 35th National Conference on Artificial Intelligence","author":"Xiao Shengping","year":"2021","unstructured":"Shengping Xiao, Jianwen Li, Shufang Zhu, Yingying Shi, Geguang Pu, and Moshe Y. Vardi. 2021. On-the-fly synthesis for LTL over finite traces. In Proceedings of the 35th National Conference on Artificial Intelligence. AAAI Press, 6530\u20136537."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3651161","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3651161","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T22:49:53Z","timestamp":1750286993000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3651161"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,4,16]]},"references-count":101,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2024,4,30]]}},"alternative-id":["10.1145\/3651161"],"URL":"https:\/\/doi.org\/10.1145\/3651161","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2024,4,16]]},"assertion":[{"value":"2022-02-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-02-15","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-04-16","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}