{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T00:10:12Z","timestamp":1743034212149,"version":"3.40.3"},"publisher-location":"Cham","reference-count":21,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030992521"},{"type":"electronic","value":"9783030992538"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,3,29]],"date-time":"2022-03-29T00:00:00Z","timestamp":1648512000000},"content-version":"vor","delay-in-days":87,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"Abstract<\/jats:title>Linear Temporal Logic<\/jats:italic> ($$\\mathsf {LTL}$$<\/jats:tex-math>\n LTL<\/mml:mi>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula>) is one of the most popular temporal logics, that comes into play in a variety of branches of computer science. Its widespread use is also due to its strong foundational properties. One of them is Kamp\u2019s theorem, showing that $$\\mathsf {LTL}$$<\/jats:tex-math>\n LTL<\/mml:mi>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula> and the first-order theory of one successor<\/jats:italic> ($$\\mathsf {S1S}[\\mathsf {FO}]$$<\/jats:tex-math>\n \n \n S<\/mml:mi>\n 1<\/mml:mn>\n S<\/mml:mi>\n <\/mml:mrow>\n [<\/mml:mo>\n FO<\/mml:mi>\n ]<\/mml:mo>\n <\/mml:mrow>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula>) are expressively equivalent. Safety and co-safety languages, where a finite prefix suffices to establish whether a word does not or does belong to the language, respectively, play a crucial role in lowering the complexity of problems like model checking and reactive synthesis for $$\\mathsf {LTL}$$<\/jats:tex-math>\n LTL<\/mml:mi>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula>. $$\\mathsf {Safety\\text {-} \\mathsf {LTL}}$$<\/jats:tex-math>\n \n Safety<\/mml:mi>\n -<\/mml:mo>\n LTL<\/mml:mi>\n <\/mml:mrow>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula> (resp., $$\\mathsf {coSafety\\text {-} \\mathsf {LTL}}$$<\/jats:tex-math>\n \n coSafety<\/mml:mi>\n -<\/mml:mo>\n LTL<\/mml:mi>\n <\/mml:mrow>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula>) is a fragment of $$\\mathsf {LTL}$$<\/jats:tex-math>\n LTL<\/mml:mi>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula> where only universal (resp., existential) temporal modalities are allowed, that recognises safety (resp., co-safety) languages only. In this paper, we introduce a fragment of $$\\mathsf {S1S}[\\mathsf {FO}]$$<\/jats:tex-math>\n \n \n S<\/mml:mi>\n 1<\/mml:mn>\n S<\/mml:mi>\n <\/mml:mrow>\n [<\/mml:mo>\n FO<\/mml:mi>\n ]<\/mml:mo>\n <\/mml:mrow>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, called $$\\mathsf {Safety\\text {-} FO}$$<\/jats:tex-math>\n \n Safety<\/mml:mi>\n -<\/mml:mo>\n FO<\/mml:mi>\n <\/mml:mrow>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, and its dual $$\\mathsf {coSafety\\text {-} FO}$$<\/jats:tex-math>\n \n coSafety<\/mml:mi>\n -<\/mml:mo>\n FO<\/mml:mi>\n <\/mml:mrow>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, which are expressively complete<\/jats:italic> with regards to the $$\\mathsf {LTL}$$<\/jats:tex-math>\n LTL<\/mml:mi>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula>-definable safety languages. In particular, we prove that they respectively characterise exactly $$\\mathsf {Safety\\text {-} \\mathsf {LTL}}$$<\/jats:tex-math>\n \n Safety<\/mml:mi>\n -<\/mml:mo>\n LTL<\/mml:mi>\n <\/mml:mrow>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula> and $$\\mathsf {coSafety\\text {-} \\mathsf {LTL}}$$<\/jats:tex-math>\n \n coSafety<\/mml:mi>\n -<\/mml:mo>\n LTL<\/mml:mi>\n <\/mml:mrow>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula>, a result that joins Kamp\u2019s theorem, and provides a clearer view of the charactisations of (fragments of) $$\\mathsf {LTL}$$<\/jats:tex-math>\n LTL<\/mml:mi>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula> in terms of first-order languages. In addition, it gives a direct, compact, and self-contained proof that any safety language definable in $$\\mathsf {LTL}$$<\/jats:tex-math>\n LTL<\/mml:mi>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula> is definable in $$\\mathsf {Safety\\text {-} \\mathsf {LTL}}$$<\/jats:tex-math>\n \n Safety<\/mml:mi>\n -<\/mml:mo>\n LTL<\/mml:mi>\n <\/mml:mrow>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula> as well. As a by-product, we obtain some interesting results on the expressive power of the weak tomorrow<\/jats:italic> operator of $$\\mathsf {Safety\\text {-} \\mathsf {LTL}}$$<\/jats:tex-math>\n \n Safety<\/mml:mi>\n -<\/mml:mo>\n LTL<\/mml:mi>\n <\/mml:mrow>\n <\/mml:math><\/jats:alternatives><\/jats:inline-formula> interpreted over finite and infinite traces.<\/jats:p>","DOI":"10.1007\/978-3-030-99253-8_13","type":"book-chapter","created":{"date-parts":[[2022,3,28]],"date-time":"2022-03-28T20:02:48Z","timestamp":1648497768000},"page":"244-263","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A first-order logic characterisation of safety and co-safety languages"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1315-6990","authenticated-orcid":false,"given":"Alessandro","family":"Cimatti","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7125-787X","authenticated-orcid":false,"given":"Luca","family":"Geatti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2254-4821","authenticated-orcid":false,"given":"Nicola","family":"Gigante","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"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9091-7899","authenticated-orcid":false,"given":"Stefano","family":"Tonetta","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,3,29]]},"reference":[{"doi-asserted-by":"crossref","unstructured":"Biere, A., Artho, C., Schuppan, V.: Liveness checking as safety checking. Electronic Notes in Theoretical Computer Science 66(2), 160\u2013177 (2002)","key":"13_CR1","DOI":"10.1016\/S1571-0661(04)80410-9"},{"unstructured":"Buchi, J.R.: Weak second-order arithmetic and finite automata. Journal of Symbolic Logic 28(1) (1963)","key":"13_CR2"},{"doi-asserted-by":"crossref","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. In: The collected works of J. Richard B\u00fcchi, pp. 425\u2013435. Springer (1990)","key":"13_CR3","DOI":"10.1007\/978-1-4613-8928-6_23"},{"doi-asserted-by":"publisher","unstructured":"Cern\u00e1, I., Pel\u00e1nek, R.: Relating hierarchy of temporal properties to model checking. In: Rovan, B., Vojt\u00e1s, P. (eds.) Proceedings of the 28th International Symposium on Mathematical Foundations of Computer Science 2003. Lecture Notes in Computer Science, vol.\u00a02747, pp. 318\u2013327. Springer (2003). https:\/\/doi.org\/10.1007\/978-3-540-45138-9_26","key":"13_CR4","DOI":"10.1007\/978-3-540-45138-9_26"},{"doi-asserted-by":"publisher","unstructured":"Chang, E.Y., Manna, Z., Pnueli, A.: Characterization of temporal property classes. In: Kuich, W. (ed.) Proceedings of the 19th International Colloquium on Automata, Languages and Programming. Lecture Notes in Computer Science, vol.\u00a0623, pp. 474\u2013486. Springer (1992). https:\/\/doi.org\/10.1007\/3-540-55719-9_97","key":"13_CR5","DOI":"10.1007\/3-540-55719-9_97"},{"unstructured":"De Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: Rossi, F. (ed.) Proceedings of the 23rd International Joint Conference on Artificial Intelligence. pp. 854\u2013860. IJCAI\/AAAI (2013)","key":"13_CR6"},{"unstructured":"De Giacomo, G., Vardi, M.Y.: Synthesis for LTL and LDL on finite traces. In: Yang, Q., Wooldridge, M.J. (eds.) Proceedings of the Twenty-Fourth International Joint Conference on Artificial Intelligence. pp. 1558\u20131564. AAAI Press (2015)","key":"13_CR7"},{"doi-asserted-by":"crossref","unstructured":"Gabbay, D., Pnueli, A., Shelah, S., Stavi, J.: On the temporal analysis of fairness. In: Proceedings of the 7th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. pp. 163\u2013173 (1980)","key":"13_CR8","DOI":"10.1145\/567446.567462"},{"unstructured":"Giacomo, G.D., Masellis, R.D., Montali, M.: Reasoning on LTL on finite traces: Insensitivity to infiniteness. In: Brodley, C.E., Stone, P. (eds.) Proceedings of the Twenty-Eighth AAAI Conference on Artificial Intelligence. pp. 1027\u20131033. AAAI Press (2014)","key":"13_CR9"},{"unstructured":"Kamp, J.A.W.: Tense logic and the theory of linear order. University of California, Los Angeles (1968)","key":"13_CR10"},{"doi-asserted-by":"crossref","unstructured":"Kupferman, O., Vardi, M.Y.: Model checking of safety properties. Formal Methods in System Design 19(3), 291\u2013314 (2001)","key":"13_CR11","DOI":"10.1023\/A:1011254632723"},{"doi-asserted-by":"crossref","unstructured":"Lichtenstein, O., Pnueli, A., Zuck, L.: The glory of the past. In: Workshop on Logic of Programs. pp. 196\u2013218. Springer (1985)","key":"13_CR12","DOI":"10.1007\/3-540-15648-8_16"},{"unstructured":"McNaughton, R., Papert, S.A.: Counter-Free Automata (MIT research monograph no. 65). The MIT Press (1971)","key":"13_CR13"},{"doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science (sfcs 1977). pp. 46\u201357. IEEE (1977)","key":"13_CR14","DOI":"10.1109\/SFCS.1977.32"},{"doi-asserted-by":"publisher","unstructured":"Rabinovich, A.: A Proof of Kamp\u2019s theorem. Logical Methods in Computer Science Volume 10, Issue 1 (Feb 2014). https:\/\/doi.org\/10.2168\/LMCS-10(1:14)2014, https:\/\/lmcs.episciences.org\/730","key":"13_CR15","DOI":"10.2168\/LMCS-10(1:14)2014"},{"doi-asserted-by":"publisher","unstructured":"Sherman, R., Pnueli, A., Harel, D.: Is the interesting part of process logic uninteresting? A translation from PL to PDL. SIAM J. Comput. 13(4), 825\u2013839 (1984). https:\/\/doi.org\/10.1137\/0213051","key":"13_CR16","DOI":"10.1137\/0213051"},{"doi-asserted-by":"crossref","unstructured":"Sistla, A.P.: Safety, liveness and fairness in temporal logic. Formal Aspects of Computing 6(5), 495\u2013511 (1994)","key":"13_CR17","DOI":"10.1007\/BF01211865"},{"unstructured":"Strejcek, J.: Linear temporal logic: Expressiveness and model checking. Ph.D. thesis, Faculty of Informatics, Masaryk University in Brno (2004)","key":"13_CR18"},{"doi-asserted-by":"crossref","unstructured":"Thomas, W.: Safety-and liveness-properties in propositional temporal logic: characterizations and decidability. Banach Center Publications 1(21), 403\u2013417 (1988)","key":"13_CR19","DOI":"10.4064\/-21-1-403-417"},{"doi-asserted-by":"publisher","unstructured":"Zhu, S., Tabajara, L.M., Li, J., Pu, G., Vardi, M.Y.: A Symbolic Approach to Safety LTL Synthesis. In: Strichman, O., Tzoref-Brill, R. (eds.) Proceedings of the 13th International Haifa Verification Conference. Lecture Notes in Computer Science, vol. 10629, pp. 147\u2013162. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-70389-3_10","key":"13_CR20","DOI":"10.1007\/978-3-319-70389-3_10"},{"unstructured":"Zuck, L.: Past temporal logic. Weizmann Institute of Science 67 (1986)","key":"13_CR21"}],"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-030-99253-8_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,28]],"date-time":"2022-03-28T20:08:05Z","timestamp":1648498085000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-99253-8_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783030992521","9783030992538"],"references-count":21,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-99253-8_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"29 March 2022","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":"Munich","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Germany","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 April 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"fossacs2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/etaps.org\/2022\/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":"77","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":"23","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)"}}]}}