{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:22:03Z","timestamp":1751660523288,"version":"3.40.3"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030591519"},{"type":"electronic","value":"9783030591526"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-59152-6_23","type":"book-chapter","created":{"date-parts":[[2020,10,11]],"date-time":"2020-10-11T23:02:35Z","timestamp":1602457355000},"page":"413-428","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":6,"title":["Explainable Reactive Synthesis"],"prefix":"10.1007","author":[{"given":"Tom","family":"Baumeister","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernd","family":"Finkbeiner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Hazem","family":"Torfah","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,10,12]]},"reference":[{"key":"23_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1007\/978-3-642-28756-5_8","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Babiak","year":"2012","unstructured":"Babiak, T., K\u0159et\u00ednsk\u00fd, M., \u0158eh\u00e1k, V., Strej\u010dek, J.: LTL to B\u00fcchi automata translation: fast and more deterministic. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 95\u2013109. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-28756-5_8"},{"issue":"11","key":"23_CR2","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1016\/S0065-2458(03)58003-2","volume":"58","author":"A Biere","year":"2003","unstructured":"Biere, A., Cimatti, A., Clarke, E.M., Strichman, O., Zhu, Y., et al.: Bounded model checking. Adv. Comput. 58(11), 117\u2013148 (2003)","journal-title":"Adv. Comput."},{"key":"23_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/978-3-030-31784-3_25","volume-title":"Automated Technology for Verification and Analysis","author":"B Bonakdarpour","year":"2019","unstructured":"Bonakdarpour, B., Finkbeiner, B.: Program repair for hyperproperties. In: Chen, Y.-F., Cheng, C.-H., Esparza, J. (eds.) ATVA 2019. LNCS, vol. 11781, pp. 423\u2013441. Springer, Cham (2019). \nhttps:\/\/doi.org\/10.1007\/978-3-030-31784-3_25"},{"key":"23_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/978-3-662-54577-5_20","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P Faymonville","year":"2017","unstructured":"Faymonville, P., Finkbeiner, B., Rabe, M.N., Tentrup, L.: Encodings of bounded synthesis. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 354\u2013370. Springer, Heidelberg (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-662-54577-5_20"},{"key":"23_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-319-63390-9_17","volume-title":"Computer Aided Verification","author":"P Faymonville","year":"2017","unstructured":"Faymonville, P., Finkbeiner, B., Tentrup, L.: BoSy: an experimentation framework for bounded synthesis. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 325\u2013332. Springer, Cham (2017). \nhttps:\/\/doi.org\/10.1007\/978-3-319-63390-9_17"},{"key":"23_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/978-3-642-27940-9_15","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"B Finkbeiner","year":"2012","unstructured":"Finkbeiner, B., Jacobs, S.: Lazy synthesis. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 219\u2013234. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-27940-9_15"},{"key":"23_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"118","DOI":"10.1007\/978-3-319-41528-4_7","volume-title":"Computer Aided Verification","author":"B Finkbeiner","year":"2016","unstructured":"Finkbeiner, B., Klein, F.: Bounded cycle synthesis. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9779, pp. 118\u2013135. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-41528-4_7"},{"key":"23_CR8","unstructured":"Finkbeiner, B., Klein, F.: Reactive synthesis: towards output-sensitive algorithms. In: Pretschner, A., Peled, D., Hutzelmann, T. (eds.) Dependable Software Systems Engineering, Volume 50 of NATO Science for Peace and Security Series, D: Information and Communication Security, pp. 25\u201343. IOS Press (2017)"},{"issue":"5\u20136","key":"23_CR9","doi-asserted-by":"publisher","first-page":"519","DOI":"10.1007\/s10009-012-0228-z","volume":"15","author":"B Finkbeiner","year":"2013","unstructured":"Finkbeiner, B., Schewe, S.: Bounded synthesis. Int. J. Softw. Tools Technol. Transf. 15(5\u20136), 519\u2013539 (2013). \nhttps:\/\/doi.org\/10.1007\/s10009-012-0228-z","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"23_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-319-46520-3_18","volume-title":"Automated Technology for Verification and Analysis","author":"B Finkbeiner","year":"2016","unstructured":"Finkbeiner, B., Torfah, H.: Synthesizing skeletons for reactive systems. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 271\u2013286. Springer, Cham (2016). \nhttps:\/\/doi.org\/10.1007\/978-3-319-46520-3_18"},{"key":"23_CR11","doi-asserted-by":"crossref","unstructured":"Jacobs, S., et al.: The 4th reactive synthesis competition (SYNTCOMP 2017): benchmarks, participants and results. In: SYNT 2017, Volume 260 of EPTCS, pp. 116\u2013143 (2017)","DOI":"10.4204\/EPTCS.260.10"},{"key":"23_CR12","unstructured":"Jacobs, S., et al.: The 5th reactive synthesis competition (SYNTCOMP 2018): benchmarks, participants & results. CoRR, abs\/1904.07736 (2019)"},{"key":"23_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/11513988_23","volume-title":"Computer Aided Verification","author":"B Jobstmann","year":"2005","unstructured":"Jobstmann, B., Griesmayer, A., Bloem, R.: Program repair as a game. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 226\u2013238. Springer, Heidelberg (2005). \nhttps:\/\/doi.org\/10.1007\/11513988_23"},{"key":"23_CR14","doi-asserted-by":"crossref","unstructured":"Kress-Gazit, H., Torfah, H.: The challenges in specifying and explaining synthesized implementations of reactive systems. In: Proceedings CREST@ETAPS, EPTCS, pp. 50\u201364 (2018)","DOI":"10.4204\/EPTCS.286.5"},{"key":"23_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/11817963_6","volume-title":"Computer Aided Verification","author":"O Kupferman","year":"2006","unstructured":"Kupferman, O., Piterman, N., Vardi, M.Y.: Safraless compositional synthesis. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 31\u201344. Springer, Heidelberg (2006). \nhttps:\/\/doi.org\/10.1007\/11817963_6"},{"key":"23_CR16","doi-asserted-by":"crossref","unstructured":"Nilsson, P., Ozay, N.: Incremental synthesis of switching protocols via abstraction refinement. In: 53rd IEEE Conference on Decision and Control, pp. 6246\u20136253 (2014)","DOI":"10.1109\/CDC.2014.7040368"},{"key":"23_CR17","doi-asserted-by":"crossref","unstructured":"Peter, H.J., Mattm\u00fcller, R.: Component-based abstraction refinement for timed controller synthesis. In: Baker, T. (ed.) Proceedings of the 30th IEEE Real-Time Systems Symposium, RTSS 2009, Washington, D.C., USA, 1\u20134 December 2009, pp. 364\u2013374, Los Alamitos, CA, USA, December 2009. IEEE Computer Society (2009)","DOI":"10.1109\/RTSS.2009.14"},{"key":"23_CR18","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/BFb0035760","volume":"372","author":"A Pnueli","year":"1989","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. Automata Lang. Program. 372, 179\u2013190 (1989)","journal-title":"Automata Lang. Program."},{"key":"23_CR19","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science, SFCS 1977, USA, pp. 46\u201357. IEEE Computer Society (1977)","DOI":"10.1109\/SFCS.1977.32"},{"issue":"4","key":"23_CR20","doi-asserted-by":"publisher","first-page":"1781","DOI":"10.1109\/TAC.2016.2593947","volume":"62","author":"G Reissig","year":"2017","unstructured":"Reissig, G., Weber, A., Rungger, M.: Feedback refinement relations for the synthesis of symbolic controllers. IEEE Trans. Autom. Control 62(4), 1781\u20131796 (2017)","journal-title":"IEEE Trans. Autom. Control"},{"key":"23_CR21","doi-asserted-by":"crossref","unstructured":"Ryzhyk, L., Walker, A.: Developing a practical reactive synthesis tool: experience and lessons learned. In: Piskac, R., Dimitrova, R. (eds.) Proceedings Fifth Workshop on Synthesis, SYNT@CAV 2016, Toronto, Canada, 17\u201318 July 2016, Volume 229 of EPTCS, pp. 84\u201399 (2016)","DOI":"10.4204\/EPTCS.229.8"},{"key":"23_CR22","doi-asserted-by":"publisher","first-page":"733","DOI":"10.1145\/3828.3837","volume":"32","author":"A Sistla","year":"1985","unstructured":"Sistla, A., Clarke, E.: The complexity of propositional linear temporal logics. J. ACM 32, 733\u2013749 (1985)","journal-title":"J. ACM"},{"key":"23_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1007\/978-3-642-02777-2_24","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2009","author":"M Soos","year":"2009","unstructured":"Soos, M., Nohl, K., Castelluccia, C.: Extending SAT solvers to cryptographic problems. In: Kullmann, O. (ed.) SAT 2009. LNCS, vol. 5584, pp. 244\u2013257. Springer, Heidelberg (2009). \nhttps:\/\/doi.org\/10.1007\/978-3-642-02777-2_24"}],"container-title":["Lecture Notes in Computer Science","Automated Technology for Verification and Analysis"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-59152-6_23","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,10,11]],"date-time":"2020-10-11T23:07:48Z","timestamp":1602457668000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-59152-6_23"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030591519","9783030591526"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-59152-6_23","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"12 October 2020","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":"Hanoi","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Vietnam","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"19 October 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23 October 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"18","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"atva2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/fit.uet.vnu.edu.vn\/atva2020\/","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":"75","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":"27","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":"36% - 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":"6","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)"}}]}}