{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T06:58:18Z","timestamp":1762325898285,"version":"3.40.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031572302"},{"type":"electronic","value":"9783031572319"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,4,6]],"date-time":"2024-04-06T00:00:00Z","timestamp":1712361600000},"content-version":"vor","delay-in-days":96,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>This paper focuses on succinctness results for fragments of Linear Temporal Logic with Past (<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf{LTL}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>LTL<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>) devoid of binary temporal operators like <jats:italic>until<\/jats:italic>, and provides methods to establish them. We prove that there is a family of <jats:italic>cosafety<\/jats:italic> languages <jats:inline-formula><jats:alternatives><jats:tex-math>$$(\\mathcal {L}_n)_{n \\ge 1}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:msub>\n                    <mml:mrow>\n                      <mml:mo>(<\/mml:mo>\n                      <mml:msub>\n                        <mml:mi>L<\/mml:mi>\n                        <mml:mi>n<\/mml:mi>\n                      <\/mml:msub>\n                      <mml:mo>)<\/mml:mo>\n                    <\/mml:mrow>\n                    <mml:mrow>\n                      <mml:mi>n<\/mml:mi>\n                      <mml:mo>\u2265<\/mml:mo>\n                      <mml:mn>1<\/mml:mn>\n                    <\/mml:mrow>\n                  <\/mml:msub>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> such that <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathcal {L}_n$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:msub>\n                    <mml:mi>L<\/mml:mi>\n                    <mml:mi>n<\/mml:mi>\n                  <\/mml:msub>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> can be expressed with a <jats:italic>pure future formula<\/jats:italic> of size <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\mathcal {O}(n)$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mrow>\n                    <mml:mi>O<\/mml:mi>\n                    <mml:mo>(<\/mml:mo>\n                    <mml:mi>n<\/mml:mi>\n                    <mml:mo>)<\/mml:mo>\n                  <\/mml:mrow>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, but it requires formulae of size <jats:inline-formula><jats:alternatives><jats:tex-math>$$2^{\\varOmega (n)}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:msup>\n                    <mml:mn>2<\/mml:mn>\n                    <mml:mrow>\n                      <mml:mi>\u03a9<\/mml:mi>\n                      <mml:mo>(<\/mml:mo>\n                      <mml:mi>n<\/mml:mi>\n                      <mml:mo>)<\/mml:mo>\n                    <\/mml:mrow>\n                  <\/mml:msup>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> to be captured with <jats:italic>past formulae<\/jats:italic>. As a by-product, such a succinctness result shows the optimality of the <jats:italic>pastification algorithm<\/jats:italic> proposed in <jats:italic>[Artale et al., KR, 2023]<\/jats:italic>.<\/jats:p><jats:p>We show that, in the considered case, succinctness cannot be proven by relying on the classical automata-based method introduced in\u00a0<jats:italic>[Markey, Bull.\u00a0EATCS, 2003]<\/jats:italic>. In place of this method, we devise and apply a <jats:italic>combinatorial proof system<\/jats:italic> whose deduction trees represent <jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf{LTL}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>LTL<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula> formulae. The system can be seen as a proof-centric (one-player) view on the games used by Adler and Immerman to study the succinctness\u00a0of\u00a0<jats:inline-formula><jats:alternatives><jats:tex-math>$$\\textsf{CTL}$$<\/jats:tex-math><mml:math xmlns:mml=\"http:\/\/www.w3.org\/1998\/Math\/MathML\">\n                  <mml:mi>CTL<\/mml:mi>\n                <\/mml:math><\/jats:alternatives><\/jats:inline-formula>.<\/jats:p>","DOI":"10.1007\/978-3-031-57231-9_5","type":"book-chapter","created":{"date-parts":[[2024,4,5]],"date-time":"2024-04-05T18:01:54Z","timestamp":1712340114000},"page":"95-115","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Succinctness of Cosafety Fragments of LTL via Combinatorial Proof Systems"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7125-787X","authenticated-orcid":false,"given":"Luca","family":"Geatti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1104-7299","authenticated-orcid":false,"given":"Alessio","family":"Mansutti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4322-769X","authenticated-orcid":false,"given":"Angelo","family":"Montanari","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,4,6]]},"reference":[{"key":"5_CR1","doi-asserted-by":"crossref","unstructured":"M.\u00a0Adler and N.\u00a0Immerman. An n! lower bound on formula size. ACM Transactions on Computational Logic, 4(3):296\u2013314, 2003.","DOI":"10.1145\/772062.772064"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"A.\u00a0Artale, L.\u00a0Geatti, N.\u00a0Gigante, A.\u00a0Mazzullo, and A.\u00a0Montanari. Complexity of safety and cosafety fragments of linear temporal logic. In AAAI\u201923, pages 6236\u20136244, 2023.","DOI":"10.1609\/aaai.v37i5.25768"},{"key":"5_CR3","unstructured":"A.\u00a0Artale, L.\u00a0Geatti, N.\u00a0Gigante, A.\u00a0Mazzullo, and A.\u00a0Montanari. LTL over finite words can be exponentially more succinct than pure-past LTL, and vice versa. In TIME\u201923, volume 278, pages 2:1\u20132:14, 2023."},{"key":"5_CR4","doi-asserted-by":"crossref","unstructured":"A.\u00a0Artale, L.\u00a0Geatti, N.\u00a0Gigante, A.\u00a0Mazzullo, and A.\u00a0Montanari. A singly exponential transformation of LTL[X, F] into pure past LTL. In KR\u201923, pages 65\u201374, 2023.","DOI":"10.24963\/kr.2023\/7"},{"key":"5_CR5","doi-asserted-by":"crossref","unstructured":"A.\u00a0Camacho and S.\u00a0A. McIlraith. Learning interpretable models expressed in linear temporal logic. In ICAPS\u201919, pages 621\u2013630, 2019.","DOI":"10.1609\/icaps.v29i1.3529"},{"key":"5_CR6","doi-asserted-by":"crossref","unstructured":"E.\u00a0Y. Chang, Z.\u00a0Manna, and A.\u00a0Pnueli. Characterization of temporal property classes. In ICALP\u201992, pages 474\u2013486, 1992.","DOI":"10.1007\/3-540-55719-9_97"},{"key":"5_CR7","doi-asserted-by":"crossref","unstructured":"G.\u00a0De\u00a0Giacomo, A.\u00a0Di\u00a0Stasio, F.\u00a0Fuggitti, and S.\u00a0Rubin. Pure-past linear temporal and dynamic logic on finite traces. In IJCAI\u201921, pages 4959\u20134965, 2021.","DOI":"10.24963\/ijcai.2020\/690"},{"key":"5_CR8","unstructured":"G.\u00a0De Giacomo and M.\u00a0Y. Vardi. Linear temporal logic and linear dynamic logic on finite traces. In IJCAI\u201913, pages 854\u2013860, 2013."},{"key":"5_CR9","doi-asserted-by":"crossref","unstructured":"R.\u00a0Fagin, J.\u00a0Lenchner, K.\u00a0W. Regan, and N.\u00a0Vyas. Multi-structural games and number of quantifiers. In LICS\u201921, pages 1\u201313, 2021.","DOI":"10.1109\/LICS52264.2021.9470756"},{"key":"5_CR10","unstructured":"R.\u00a0Fagin, J.\u00a0Lenchner, N.\u00a0Vyas, and R.\u00a0R. Williams. On the number of quantifiers as a complexity measure. In MFCS\u201922, pages 48:1\u201348:14, 2022."},{"key":"5_CR11","doi-asserted-by":"crossref","unstructured":"M.\u00a0Fortin, B.\u00a0Konev, V.\u00a0Ryzhikov, Y.\u00a0Savateev, F.\u00a0Wolter, and M.\u00a0Zakharyaschev. Unique characterisability and learnability of temporal instance queries. In KR\u201922, 2022.","DOI":"10.24963\/kr.2022\/17"},{"key":"5_CR12","doi-asserted-by":"crossref","unstructured":"M.\u00a0Fortin, B.\u00a0Konev, V.\u00a0Ryzhikov, Y.\u00a0Savateev, F.\u00a0Wolter, and M.\u00a0Zakharyaschev. Reverse engineering of temporal queries mediated by LTL ontologies. In IJCAI\u201923, pages 3230\u20133238, 2023.","DOI":"10.24963\/ijcai.2023\/360"},{"key":"5_CR13","doi-asserted-by":"crossref","unstructured":"L.\u00a0Geatti, A.\u00a0Mansutti, and A.\u00a0Montanari. Succinctness of Cosafety Fragments of LTL via Combinatorial Proof Systems (extended version). arXiv, cs.LO\/2401.09860, 2024.","DOI":"10.1007\/978-3-031-57231-9_5"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"M.\u00a0Grohe and N.\u00a0Schweikardt. The succinctness of first-order logic on linear orders. Log. Methods Comput. Sci., 1(1:6), 2005.","DOI":"10.2168\/LMCS-1(1:6)2005"},{"key":"5_CR15","doi-asserted-by":"crossref","unstructured":"M.\u00a0Karchmer. Communication complexity - a new approach to circuit depth. MIT Press, 1989.","DOI":"10.7551\/mitpress\/1948.001.0001"},{"key":"5_CR16","doi-asserted-by":"crossref","unstructured":"O.\u00a0Kupferman and M.\u00a0Y. Vardi. Model checking of safety properties. Formal Methods in System Design, 19(3):291\u2013314, 2001.","DOI":"10.1023\/A:1011254632723"},{"key":"5_CR17","doi-asserted-by":"crossref","unstructured":"O.\u00a0Lichtenstein, A.\u00a0Pnueli, and L.\u00a0Zuck. The glory of the past. In Workshop on Logic of Programs, pages 196\u2013218, 1985.","DOI":"10.1007\/3-540-15648-8_16"},{"key":"5_CR18","doi-asserted-by":"crossref","unstructured":"F.\u00a0M. Maggi, M.\u00a0Montali, and R.\u00a0Pe\u00f1aloza. Temporal logics over finite traces with uncertainty. In AAAI\u201920, pages 10218\u201310225, 2020.","DOI":"10.1609\/aaai.v34i06.6583"},{"key":"5_CR19","doi-asserted-by":"crossref","unstructured":"Z.\u00a0Manna and A.\u00a0Pnueli. Temporal verification of reactive systems - safety. Springer, 1995.","DOI":"10.1007\/978-1-4612-4222-2"},{"key":"5_CR20","unstructured":"N.\u00a0Markey. Temporal logic with past is exponentially more succinct, concurrency column. Bull. EATCS, 79:122\u2013128, 2003."},{"key":"5_CR21","doi-asserted-by":"crossref","unstructured":"D.\u00a0Neider and I.\u00a0Gavran. Learning linear temporal properties. In FMCAD\u201918, pages 1\u201310, 2018.","DOI":"10.23919\/FMCAD.2018.8603016"},{"key":"5_CR22","doi-asserted-by":"crossref","unstructured":"M.\u00a0Pesic and W.\u00a0M.\u00a0P. van\u00a0der Aalst. A declarative approach for flexible business processes management. In J.\u00a0Eder and S.\u00a0Dustdar, editors, BPM\u201906, pages 169\u2013180, 2006.","DOI":"10.1007\/11837862_18"},{"key":"5_CR23","doi-asserted-by":"crossref","unstructured":"A.\u00a0Pnueli. The temporal logic of programs. In FOCS (SFCS\u201977), pages 46\u201357, 1977.","DOI":"10.1109\/SFCS.1977.32"},{"key":"5_CR24","doi-asserted-by":"crossref","unstructured":"R.\u00a0Raha, R.\u00a0Roy, N.\u00a0Fijalkow, and D.\u00a0Neider. Scalable anytime algorithms for learning fragments of linear temporal logic. In TACAS\u201922, pages 263\u2013280, 2022.","DOI":"10.1007\/978-3-030-99524-9_14"},{"key":"5_CR25","doi-asserted-by":"crossref","unstructured":"L.\u00a0J. Stockmeyer and A.\u00a0R. Meyer. Cosmological lower bound on the circuit complexity of a small problem in logic. J. ACM, 49(6):753\u2013784, 2002.","DOI":"10.1145\/602220.602223"},{"key":"5_CR26","unstructured":"M.\u00a0Y. Vardi and P.\u00a0Wolper. An automata-theoretic approach to automatic program verification. In LICS\u201986, pages 322\u2013331, 1986."}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-57231-9_5","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,5,3]],"date-time":"2024-05-03T16:03:59Z","timestamp":1714752239000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-57231-9_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031572302","9783031572319"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-57231-9_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"6 April 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"FoSSaCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Foundations of Software Science and Computation Structures","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2024\/conferences\/fossacs\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"79","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"24","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}