{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T21:46:58Z","timestamp":1742939218623,"version":"3.40.3"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031562211"},{"type":"electronic","value":"9783031562228"}],"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:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"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":[[2024]]},"DOI":"10.1007\/978-3-031-56222-8_3","type":"book-chapter","created":{"date-parts":[[2024,3,19]],"date-time":"2024-03-19T08:02:30Z","timestamp":1710835350000},"page":"51-71","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["SynthLearn: A Tool for\u00a0Guided Reactive Synthesis"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8688-3550","authenticated-orcid":false,"given":"Mrudula","family":"Balachander","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2520-5630","authenticated-orcid":false,"given":"Emmanuel","family":"Filiot","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3673-1097","authenticated-orcid":false,"given":"Jean-Fran\u00e7ois","family":"Raskin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,3,20]]},"reference":[{"key":"3_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BFb0035748","volume-title":"Automata, Languages and Programming","author":"M Abadi","year":"1989","unstructured":"Abadi, M., Lamport, L., Wolper, P.: Realizable and unrealizable specifications of reactive systems. In: Ausiello, G., Dezani-Ciancaglini, M., Della Rocca, S.R. (eds.) ICALP 1989. LNCS, vol. 372, pp. 1\u201317. Springer, Heidelberg (1989). https:\/\/doi.org\/10.1007\/BFb0035748"},{"key":"3_CR2","doi-asserted-by":"publisher","unstructured":"Alur, R., Fisman, D., Singh, R., Solar-Lezama, A.: Results and analysis of sygus-comp\u201915. In: Cern\u00fd, P., Kuncak, V., Madhusudan, P. (eds.) Proceedings Fourth Workshop on Synthesis, SYNT 2015, San Francisco, CA, USA, 18th July 2015. EPTCS, vol. 202, pp. 3\u201326 (2015). https:\/\/doi.org\/10.4204\/EPTCS.202.3","DOI":"10.4204\/EPTCS.202.3"},{"key":"3_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1007\/978-3-319-13338-6_7","volume-title":"Hardware and Software: Verification and Testing","author":"R Alur","year":"2014","unstructured":"Alur, R., Martin, M., Raghothaman, M., Stergiou, C., Tripakis, S., Udupa, A.: Synthesizing finite-state protocols from scenarios and requirements. In: Yahav, E. (ed.) HVC 2014. LNCS, vol. 8855, pp. 75\u201391. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-13338-6_7"},{"key":"3_CR4","doi-asserted-by":"publisher","unstructured":"Backus, J.W., et al.: Revised report on the algorithmic language ALGOL 60. Comput. J. 5(4), 349\u2013367 (1963). https:\/\/doi.org\/10.1093\/comjnl\/5.4.349","DOI":"10.1093\/comjnl\/5.4.349"},{"key":"3_CR5","doi-asserted-by":"publisher","unstructured":"Balachander, M., Filiot, E., Raskin, J.: LTL reactive synthesis with a few hints. In: Sankaranarayanan, S., Sharygina, N. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, 22\u201327 April 2023, Proceedings, Part II. LNCS, vol. 13994, pp. 309\u2013328. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-30820-8_20","DOI":"10.1007\/978-3-031-30820-8_20"},{"key":"3_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-02658-4_14","volume-title":"Computer Aided Verification","author":"R Bloem","year":"2009","unstructured":"Bloem, R., Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Better quality in synthesis through quantitative objectives. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 140\u2013156. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_14"},{"key":"3_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"55","DOI":"10.1007\/978-3-319-52234-0_4","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"R Bloem","year":"2017","unstructured":"Bloem, R., Chockler, H., Ebrahimi, M., Strichman, O.: Synthesizing non-vacuous systems. In: Bouajjani, A., Monniaux, D. (eds.) VMCAI 2017. LNCS, vol. 10145, pp. 55\u201372. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-52234-0_4"},{"key":"3_CR8","doi-asserted-by":"publisher","unstructured":"Bohy, A., Bruy\u00e8re, V., Filiot, E., Jin, N., Raskin, J.: Acacia+, a tool for LTL synthesis. In: Madhusudan, P., Seshia, S.A. (eds.) Computer Aided Verification - 24th International Conference, CAV 2012, Berkeley, CA, USA, 7\u201313 July 2012 Proceedings. LNCS, vol. 7358, pp. 652\u2013657. Springer (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_45","DOI":"10.1007\/978-3-642-31424-7_45"},{"key":"3_CR9","doi-asserted-by":"publisher","first-page":"259","DOI":"10.1016\/j.ic.2016.10.011","volume":"254","author":"V Bruy\u00e8re","year":"2017","unstructured":"Bruy\u00e8re, V., Filiot, E., Randour, M., Raskin, J.: Meet your expectations with guarantees: beyond worst-case synthesis in quantitative games. Inf. Comput. 254, 259\u2013295 (2017). https:\/\/doi.org\/10.1016\/j.ic.2016.10.011","journal-title":"Inf. Comput."},{"key":"3_CR10","doi-asserted-by":"crossref","unstructured":"Cadilhac, M., P\u00e9rez, G.A.: Acacia-bonsai: A modern implementation of downset-based ltl realizability (2022)","DOI":"10.1007\/978-3-031-30820-8_14"},{"key":"3_CR11","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.): Handbook of Model Checking. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8","DOI":"10.1007\/978-3-319-10575-8"},{"key":"3_CR12","doi-asserted-by":"publisher","unstructured":"Damas, C., Lambeau, B., van Lamsweerde, A.: Scenarios, goals, and state machines: a win-win partnership for model synthesis. In: Young, M., Devanbu, P.T. (eds.) Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2006, Portland, Oregon, USA, 5\u201311 November 2006, pp. 197\u2013207. ACM (2006). https:\/\/doi.org\/10.1145\/1181775.1181800","DOI":"10.1145\/1181775.1181800"},{"key":"3_CR13","doi-asserted-by":"publisher","unstructured":"Dupont, P., Lambeau, B., Damas, C., van Lamsweerde, A.: The QSM algorithm and its application to software behavior model induction. Appl. Artif. Intell. 22(1 &2), 77\u2013115 (2008). https:\/\/doi.org\/10.1080\/08839510701853200","DOI":"10.1080\/08839510701853200"},{"key":"3_CR14","doi-asserted-by":"publisher","unstructured":"Duret-Lutz, A., et al.: From spot 2.0 to spot 2.10: what\u2019s new? In: Shoham, S., Vizel, Y. (eds.) Computer Aided Verification - 34th International Conference, CAV 2022, Haifa, Israel, 7\u201310 August 2022, Proceedings, Part II. LNCS, vol. 13372, pp. 174\u2013187. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_9","DOI":"10.1007\/978-3-031-13188-2_9"},{"key":"3_CR15","doi-asserted-by":"publisher","unstructured":"Duret-Lutz, A., et al.: From Spot 2.0 to Spot 2.10: What\u2019s new? In: Proceedings of the 34th International Conference on Computer Aided Verification (CAV 2022). LNCS, vol. 13372, pp. 174\u2013187. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-13188-2_9","DOI":"10.1007\/978-3-031-13188-2_9"},{"key":"3_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"192","DOI":"10.1007\/978-3-319-08867-9_13","volume-title":"Computer Aided Verification","author":"J Esparza","year":"2014","unstructured":"Esparza, J., K\u0159et\u00ednsk\u00fd, J.: From LTL to deterministic automata: a safraless compositional approach. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 192\u2013208. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_13"},{"key":"3_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"426","DOI":"10.1007\/978-3-662-54577-5_25","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J Esparza","year":"2017","unstructured":"Esparza, J., K\u0159et\u00ednsk\u00fd, J., Raskin, J.-F., Sickert, S.: From LTL and limit-deterministic b\u00fcchi automata to deterministic parity automata. In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10205, pp. 426\u2013442. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_25"},{"key":"3_CR18","doi-asserted-by":"publisher","unstructured":"Esparza, J., Kret\u00ednsk\u00fd, J., Sickert, S.: One theorem to rule them all: A unified translation of LTL into $$\\omega $$-automata. In: Dawar, A., Gr\u00e4del, E. (eds.) Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, 09\u201312 July 2018, pp. 384\u2013393. ACM (2018). https:\/\/doi.org\/10.1145\/3209108.3209161","DOI":"10.1145\/3209108.3209161"},{"key":"3_CR19","doi-asserted-by":"publisher","unstructured":"Esparza, J., Kret\u00ednsk\u00fd, J., Sickert, S.: A unified translation of linear temporal logic to $$\\omega $$-automata. J. ACM 67(6), 33:1\u201333:61 (2020). https:\/\/doi.org\/10.1145\/3417995","DOI":"10.1145\/3417995"},{"key":"3_CR20","doi-asserted-by":"publisher","unstructured":"Esparza, J., Rubio, R., Sickert, S.: A simple rewrite system for the normalization of linear temporal logic (2023). https:\/\/doi.org\/10.48550\/ARXIV.2304.08872, CoRR abs\/ arXiv: 2304.08872","DOI":"10.48550\/ARXIV.2304.08872"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Faymonville, P., Finkbeiner, B., Tentrup, L.: Bosy: An experimentation framework for bounded synthesis (2018)","DOI":"10.1007\/978-3-319-63390-9_17"},{"key":"3_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-642-02658-4_22","volume-title":"Computer Aided Verification","author":"E Filiot","year":"2009","unstructured":"Filiot, E., Jin, N., Raskin, J.-F.: An antichain algorithm for LTL realizability. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 263\u2013277. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_22"},{"key":"3_CR23","doi-asserted-by":"publisher","unstructured":"Harel, D., Pnueli, A.: On the development of reactive systems. In: Apt, K.R. (ed.) Logics and Models of Concurrent Systems - Conference proceedings, Colle-sur-Loup (near Nice), France, 8\u201319 October 1984. NATO ASI Series, vol. 13, pp. 477\u2013498. Springer (1984). https:\/\/doi.org\/10.1007\/978-3-642-82453-1_17","DOI":"10.1007\/978-3-642-82453-1_17"},{"key":"3_CR24","doi-asserted-by":"publisher","unstructured":"Heinz, J., de la Higuera, C., van Zaanen, M.: Grammatical Inference for Computational Linguistics. Synthesis Lectures on Human Language Technologies, Morgan & Claypool Publishers (2015). https:\/\/doi.org\/10.2200\/S00643ED1V01Y201504HLT028","DOI":"10.2200\/S00643ED1V01Y201504HLT028"},{"key":"3_CR25","doi-asserted-by":"publisher","unstructured":"Hoare, C.A.R.: An overview of some formal methods for program design. Computer 20(9), 85\u201391 (1987). https:\/\/doi.org\/10.1109\/MC.1987.1663697","DOI":"10.1109\/MC.1987.1663697"},{"key":"3_CR26","doi-asserted-by":"crossref","unstructured":"Oncina, J., Garcia, P.: Inferring regular languages in polynomial updated time. Pattern Recogn. Image Anal., 49\u201361 (1992)","DOI":"10.1142\/9789812797902_0004"},{"key":"3_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/978-3-642-31424-7_7","volume-title":"Computer Aided Verification","author":"J K\u0159et\u00ednsk\u00fd","year":"2012","unstructured":"K\u0159et\u00ednsk\u00fd, J., Esparza, J.: Deterministic automata for the (F,G)-fragment of LTL. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 7\u201322. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_7"},{"key":"3_CR28","doi-asserted-by":"publisher","unstructured":"Kupferman, O., Vardi, M.Y.: Safraless decision procedures. In: 46th Annual IEEE Symposium on Foundations of Computer Science (FOCS 2005), 23\u201325 October 2005, Pittsburgh, PA, USA, Proceedings, pp. 531\u2013542. IEEE Computer Society (2005). https:\/\/doi.org\/10.1109\/SFCS.2005.66","DOI":"10.1109\/SFCS.2005.66"},{"key":"3_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"578","DOI":"10.1007\/978-3-319-96145-3_31","volume-title":"Computer Aided Verification","author":"PJ Meyer","year":"2018","unstructured":"Meyer, P.J., Sickert, S., Luttenberger, M.: Strix: explicit reactive synthesis strikes back! In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 578\u2013586. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_31"},{"key":"3_CR30","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-030-88885-5_5","volume-title":"Automated Technology for Verification and Analysis","author":"E Mu\u0161kardin","year":"2021","unstructured":"Mu\u0161kardin, E., Aichernig, B.K., Pill, I., Pferscher, A., Tappler, M.: AALpy: an active automata learning library. In: Hou, Z., Ganesh, V. (eds.) ATVA 2021. LNCS, vol. 12971, pp. 67\u201373. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-88885-5_5"},{"key":"3_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"652","DOI":"10.1007\/BFb0035790","volume-title":"Automata, Languages and Programming","author":"A Pnueli","year":"1989","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of an asynchronous reactive module. In: Ausiello, G., Dezani-Ciancaglini, M., Della Rocca, S.R. (eds.) ICALP 1989. LNCS, vol. 372, pp. 652\u2013671. Springer, Heidelberg (1989). https:\/\/doi.org\/10.1007\/BFb0035790"},{"key":"3_CR32","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-030-99524-9_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Raha","year":"2022","unstructured":"Raha, R., Roy, R., Fijalkow, N., Neider, D.: Scalable anytime algorithms for learning fragments of linear temporal logic. In: TACAS 2022. LNCS, vol. 13243, pp. 263\u2013280. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_14"},{"key":"3_CR33","unstructured":"Ren, Z.: LTL synthesis problem with examples (Master Thesis). Master\u2019s thesis, Universit\u00e9 libre de Bruxelles (2023)"},{"key":"3_CR34","doi-asserted-by":"publisher","unstructured":"Safra, S.: On the complexity of omega-automata. In: 29th Annual Symposium on Foundations of Computer Science, White Plains, New York, USA, 24\u201326 October 1988, pp. 319\u2013327. IEEE Computer Society (1988). https:\/\/doi.org\/10.1109\/SFCS.1988.21948","DOI":"10.1109\/SFCS.1988.21948"},{"key":"3_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1007\/978-3-540-75596-8_33","volume-title":"Automated Technology for Verification and Analysis","author":"S Schewe","year":"2007","unstructured":"Schewe, S., Finkbeiner, B.: Bounded synthesis. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 474\u2013488. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-75596-8_33"},{"key":"3_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-319-41540-6_17","volume-title":"Computer Aided Verification","author":"S Sickert","year":"2016","unstructured":"Sickert, S., Esparza, J., Jaax, S., K\u0159et\u00ednsk\u00fd, J.: Limit-Deterministic B\u00fcchi automata for linear temporal logic. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 312\u2013332. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_17"}],"container-title":["Lecture Notes in Computer Science","Taming the Infinities of Concurrency"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-56222-8_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,6]],"date-time":"2024-11-06T22:02:55Z","timestamp":1730930575000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-56222-8_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031562211","9783031562228"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-56222-8_3","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":"20 March 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}}]}}