{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T12:04:32Z","timestamp":1770293072874,"version":"3.49.0"},"publisher-location":"Cham","reference-count":37,"publisher":"Springer Nature Switzerland","isbn-type":[{"value":"9783031453281","type":"print"},{"value":"9783031453298","type":"electronic"}],"license":[{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,1,1]],"date-time":"2023-01-01T00:00:00Z","timestamp":1672531200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023]]},"DOI":"10.1007\/978-3-031-45329-8_11","type":"book-chapter","created":{"date-parts":[[2023,10,21]],"date-time":"2023-10-21T18:02:40Z","timestamp":1697911360000},"page":"227-247","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":4,"title":["Model Checking Strategies from\u00a0Synthesis over Finite Traces"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0405-073X","authenticated-orcid":false,"given":"Suguman","family":"Bansal","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7301-9234","authenticated-orcid":false,"given":"Yong","family":"Li","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9608-1404","authenticated-orcid":false,"given":"Lucas M.","family":"Tabajara","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0661-5773","authenticated-orcid":false,"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7780-2122","authenticated-orcid":false,"given":"Andrew","family":"Wells","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,10,22]]},"reference":[{"key":"11_CR1","unstructured":"Baier, J.A., McIlraith, S.: Planning with temporally extended goals using heuristic search. In: ICAPS, pp. 342\u2013345. AAAI Press (2006)"},{"key":"11_CR2","doi-asserted-by":"crossref","unstructured":"Bansal, S., Li, Y., Tabajara, L., Vardi, M.: Hybrid compositional reasoning for reactive synthesis from finite-horizon specifications. In: AAAI, vol. 34, pp. 9766\u20139774 (2020)","DOI":"10.1609\/aaai.v34i06.6528"},{"key":"11_CR3","doi-asserted-by":"publisher","unstructured":"Bansal, S., Li, Y., Tabajara, L.M., Vardi, M.Y., Wells, A.M.: Model checking strategies from synthesis over finite traces. CoRR abs\/2305.08319 (2023). https:\/\/doi.org\/10.48550\/arXiv.2305.08319","DOI":"10.48550\/arXiv.2305.08319"},{"key":"11_CR4","first-page":"1","volume":"4","author":"S Bansal","year":"2019","unstructured":"Bansal, S., Namjoshi, K.S., Sa\u2019ar, Y.: Synthesis of coordination programs from linear temporal specifications. Proc. ACM Program. Lang. (POPL) 4, 1\u201327 (2019)","journal-title":"Proc. ACM Program. Lang. (POPL)"},{"key":"11_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/978-3-319-96145-3_20","volume-title":"Computer Aided Verification","author":"S Bansal","year":"2018","unstructured":"Bansal, S., Namjoshi, K.S., Sa\u2019ar, Y.: Synthesis of asynchronous reactive programs from temporal specifications. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 367\u2013385. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_20"},{"issue":"1","key":"11_CR6","doi-asserted-by":"publisher","first-page":"269","DOI":"10.1145\/200836.200880","volume":"42","author":"M Blum","year":"1995","unstructured":"Blum, M., Kannan, S.: Designing programs that check their work. J. ACM 42(1), 269\u2013291 (1995)","journal-title":"J. ACM"},{"key":"11_CR7","doi-asserted-by":"crossref","unstructured":"Brafman, R.I., De Giacomo, G.: Planning for LTLf\/LDLf goals in non-Markovian fully observable nondeterministic domains. In: IJCAI, pp. 1602\u20131608 (2019)","DOI":"10.24963\/ijcai.2019\/222"},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Camacho, A., Icarte, R.T., Klassen, T.Q., Valenzano, R.A., McIlraith, S.A.: LTL and beyond: formal languages for reward function specification in reinforcement learning. In: IJCAI, vol. 19, pp. 6065\u20136073 (2019)","DOI":"10.24963\/ijcai.2019\/840"},{"key":"11_CR9","doi-asserted-by":"crossref","unstructured":"De Giacomo, G., Favorito, M.: Compositional approach to translate LTLf\/LDLf into deterministic finite automata. In: Proceedings of the International Conference on Automated Planning and Scheduling, vol. 31, pp. 122\u2013130 (2021)","DOI":"10.1609\/icaps.v31i1.15954"},{"key":"11_CR10","doi-asserted-by":"crossref","unstructured":"De Giacomo, G., Favorito, M., Li, J., Vardi, M.Y., Xiao, S., Zhu, S.: LTLf synthesis as AND-OR graph search: knowledge compilation at work. In: Proceedings of IJCAI (2022)","DOI":"10.24963\/ijcai.2022\/359"},{"key":"11_CR11","doi-asserted-by":"crossref","unstructured":"De Giacomo, G., Iocchi, L., Favorito, M., Patrizi, F.: Foundations for restraining bolts: reinforcement learning with LTLf\/LDLf restraining specifications. In: ICAPS, vol. 29, pp. 128\u2013136 (2019)","DOI":"10.1609\/icaps.v29i1.3549"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"De Giacomo, G., Rubin, S.: Automata-theoretic foundations of fond planning for LTLf and LDLf goals. In: IJCAI, pp. 4729\u20134735 (2018)","DOI":"10.24963\/ijcai.2018\/657"},{"key":"11_CR13","unstructured":"De Giacomo, G., Vardi, M.: Synthesis for LTL and LDL on finite traces. In: IJCAI, pp. 1558\u20131564. AAAI Press (2015)"},{"key":"11_CR14","unstructured":"De Giacomo, G., Vardi, M.Y.: Linear temporal logic and linear dynamic logic on finite traces. In: IJCAI, pp. 854\u2013860. AAAI Press (2013)"},{"key":"11_CR15","unstructured":"De Giacomo, G., Vardi, M.Y.: LTLf and LDLf synthesis under partial observability. In: IJCAI, vol. 2016, pp. 1044\u20131050 (2016)"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"174","DOI":"10.1007\/978-3-031-13188-2_9","volume-title":"Computer Aided Verification","author":"A Duret-Lutz","year":"2022","unstructured":"Duret-Lutz, A., et al.: From spot 2.0 to spot 2.10: What\u2019s new? In: Shoham, S., Vizel, Y. (eds.) CAV 2022, Part II. Lecture Notes in Computer Science, vol. 13372, pp. 174\u2013187. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_9"},{"issue":"6","key":"11_CR17","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3417995","volume":"67","author":"J Esparza","year":"2020","unstructured":"Esparza, J., K\u0159et\u00ednsk\u1ef3, J., Sickert, S.: A unified translation of linear temporal logic to $$\\omega $$-automata. J. ACM (JACM) 67(6), 1\u201361 (2020)","journal-title":"J. ACM (JACM)"},{"key":"11_CR18","unstructured":"Favorito, M.: Forward LTLf synthesis: DPLL at work. arXiv preprint arXiv:2302.13825 (2023)"},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"He, K., Lahijanian, M., Kavraki, L.E., Vardi, M.Y.: Reactive synthesis for finite tasks under resource constraints. In: IROS, pp. 5326\u20135332. IEEE (2017)","DOI":"10.1109\/IROS.2017.8206426"},{"key":"11_CR20","unstructured":"Jacobs, S., Perez, G.A., Schlehuber-Caissier, P.: The temporal logic synthesis format TLSF v1.2 (2023)"},{"key":"11_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1007\/978-3-030-01090-4_34","volume-title":"Automated Technology for Verification and Analysis","author":"J K\u0159et\u00ednsk\u00fd","year":"2018","unstructured":"K\u0159et\u00ednsk\u00fd, J., Meggendorfer, T., Sickert, S.: Owl: a library for $$\\omega $$-words, automata, and LTL. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 543\u2013550. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_34"},{"key":"11_CR22","series-title":"The Springer International Series in Engineering and Computer Science","doi-asserted-by":"publisher","first-page":"343","DOI":"10.1007\/978-1-4615-0817-5_13","volume-title":"Logic Synthesis and Verification","author":"A Kuehlmann","year":"2002","unstructured":"Kuehlmann, A., van Eijk, C.A.: Combinational and sequential equivalence checking. In: Hassoun, S., Sasao, T. (eds.) Logic Synthesis and Verification. The Springer International Series in Engineering and Computer Science, vol. 654, pp. 343\u2013372. Springer, Boston (2002). https:\/\/doi.org\/10.1007\/978-1-4615-0817-5_13"},{"key":"11_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"407","DOI":"10.1007\/3-540-53479-2_17","volume-title":"Semantics of Systems of Concurrent Processes","author":"R De Nicola","year":"1990","unstructured":"De Nicola, R., Vaandrager, F.: Action versus state based logics for transition systems. In: Guessarian, I. (ed.) LITP 1990. LNCS, vol. 469, pp. 407\u2013419. Springer, Heidelberg (1990). https:\/\/doi.org\/10.1007\/3-540-53479-2_17"},{"key":"11_CR24","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46\u201357. IEEE (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"11_CR25","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: POPL, pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"key":"11_CR26","doi-asserted-by":"crossref","unstructured":"Safra, S.: On the complexity of omega -automata. In: FOCS, pp. 319\u2013327 (1988)","DOI":"10.1109\/SFCS.1988.21948"},{"key":"11_CR27","doi-asserted-by":"crossref","unstructured":"Siegel, M., Pnueli, A., Singerman, E.: Translation validation. In: Proceedings of TACAS, pp. 151\u2013166 (1998)","DOI":"10.1007\/BFb0054170"},{"issue":"3","key":"11_CR28","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"AP Sistla","year":"1985","unstructured":"Sistla, A.P., Clarke, E.M.: The complexity of propositional linear temporal logics. J. ACM (JACM) 32(3), 733\u2013749 (1985)","journal-title":"J. ACM (JACM)"},{"key":"11_CR29","doi-asserted-by":"crossref","unstructured":"Tabajara, L.M., Vardi, M.Y.: Partitioning techniques in LTLf synthesis. In: IJCAI, pp. 5599\u20135606. AAAI Press (2019)","DOI":"10.24963\/ijcai.2019\/777"},{"issue":"3","key":"11_CR30","doi-asserted-by":"publisher","first-page":"236","DOI":"10.1007\/s10703-011-0139-8","volume":"41","author":"D Tabakov","year":"2012","unstructured":"Tabakov, D., Rozier, K., Vardi, M.Y.: Optimized temporal monitors for SystemC. Formal Meth. Syst. Des. 41(3), 236\u2013268 (2012)","journal-title":"Formal Meth. Syst. Des."},{"key":"11_CR31","volume-title":"Automata, Logics, and Infinite Games: A Guide to Current Research","author":"W Thomas","year":"2002","unstructured":"Thomas, W., et al.: Automata, Logics, and Infinite Games: A Guide to Current Research, vol. 2500. Springer, Berlin (2002)"},{"key":"11_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"12","DOI":"10.1007\/978-3-540-70918-3_2","volume-title":"STACS 2007","author":"MY Vardi","year":"2007","unstructured":"Vardi, M.Y.: The b\u00fcchi complementation saga. In: Thomas, W., Weil, P. (eds.) STACS 2007. LNCS, vol. 4393, pp. 12\u201322. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-70918-3_2"},{"key":"11_CR33","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: LICS. IEEE Computer Society (1986)"},{"issue":"1","key":"11_CR34","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"MY Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Inf. Comput. 115(1), 1\u201337 (1994)","journal-title":"Inf. Comput."},{"key":"11_CR35","doi-asserted-by":"crossref","unstructured":"Wells, A.M., Lahijanian, M., Kavraki, L.E., Vardi, M.Y.: LTLf synthesis on probabilistic systems. arXiv preprint arXiv:2009.10883 (2020)","DOI":"10.4204\/EPTCS.326.11"},{"key":"11_CR36","doi-asserted-by":"crossref","unstructured":"Wolper, P., Vardi, M.Y., Sistla, A.P.: Reasoning about infinite computation paths. In: FOCS, pp. 185\u2013194. IEEE (1983)","DOI":"10.1109\/SFCS.1983.51"},{"key":"11_CR37","doi-asserted-by":"crossref","unstructured":"Zhu, S., Tabajara, L.M., Li, J., Pu, G., Vardi, M.Y.: Symbolic LTLf synthesis. In: IJCAI, pp. 1362\u20131369. AAAI Press (2017)","DOI":"10.24963\/ijcai.2017\/189"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-45329-8_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,10,31]],"date-time":"2024-10-31T15:56:08Z","timestamp":1730390168000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-45329-8_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023]]},"ISBN":["9783031453281","9783031453298"],"references-count":37,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-45329-8_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023]]},"assertion":[{"value":"22 October 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ATVA","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Symposium on Automated Technology for Verification and Analysis","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Singapore","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Singapore","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2023","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 October 2023","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 October 2023","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"21","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"atva2023","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/atva-conference.org\/2023\/","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":"115","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":"30","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":"26% - 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.05","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)"}},{"value":"7 tool papers","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}