{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,23]],"date-time":"2025-09-23T22:40:22Z","timestamp":1758667222960,"version":"3.44.0"},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2025,8,21]],"date-time":"2025-08-21T00:00:00Z","timestamp":1755734400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,8,21]],"date-time":"2025-08-21T00:00:00Z","timestamp":1755734400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"name":"\"Aspirant\" FNRS Grant"},{"name":"Senior Research associate at F.R.S-FNRS"},{"name":"F.R.S.-FNRS","award":["F451019F"],"award-info":[{"award-number":["F451019F"]}]},{"name":"EOS project Verifying Learning Artificial Intelligence Systems"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2025,9]]},"DOI":"10.1007\/s10817-025-09737-6","type":"journal-article","created":{"date-parts":[[2025,8,21]],"date-time":"2025-08-21T07:22:14Z","timestamp":1755760934000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["LTL Reactive Synthesis with a Few Hints"],"prefix":"10.1007","volume":"69","author":[{"given":"Mrudula","family":"Balachander","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Emmanuel","family":"Filiot","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jean-Fran\u00e7ois","family":"Raskin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,8,21]]},"reference":[{"key":"9737_CR1","doi-asserted-by":"publisher","unstructured":"Abadi, M., Lamport, L., Wolper, P.: Realizable and unrealizable specifications of reactive systems. In: Automata, Languages and Programming, 16th International Colloquium, ICALP89, Stresa, Italy, July 11-15, 1989, Proceedings. Lecture Notes in Computer Science, vol. 372, pp. 1\u201317. Springer, Stresa, Italy (1989). https:\/\/doi.org\/10.1007\/BFb0035748","DOI":"10.1007\/BFb0035748"},{"key":"9737_CR2","doi-asserted-by":"crossref","unstructured":"Almagor, S., Avni, G., Kupferman, O.: Automatic generation of quality specifications. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification, pp. 479\u2013494. Springer, Berlin, Heidelberg (2013)","DOI":"10.1007\/978-3-642-39799-8_32"},{"key":"9737_CR3","doi-asserted-by":"crossref","unstructured":"Almagor, S., Boker, U., Kupferman, O.: Formalizing and reasoning about quality. Journal of the ACM 63(3), 24 (2016)","DOI":"10.1145\/2875421"},{"key":"9737_CR4","doi-asserted-by":"publisher","unstructured":"Almagor, S., Kupferman, O., Velner, Y.: Minimizing expected cost under hard boolean constraints, with applications to quantitative synthesis. In: 27th International Conference on Concurrency Theory, CONCUR 2016, August 23-26, 2016, Qu\u00e9bec City, Canada. LIPIcs, vol. 59, pp. 9\u20131915. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Qu\u00e9bec City, Canada (2016). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2016.9","DOI":"10.4230\/LIPIcs.CONCUR.2016.9"},{"key":"9737_CR5","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/978-3-642-39799-8_32","volume-title":"Computer Aided Verification","author":"S Almagor","year":"2013","unstructured":"Almagor, S., Avni, G., Kupferman, O.: Automatic generation of quality specifications. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification, pp. 479\u2013494. Springer, Berlin, Heidelberg (2013)"},{"issue":"3","key":"9737_CR6","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1145\/2875421","volume":"63","author":"S Almagor","year":"2016","unstructured":"Almagor, S., Boker, U., Kupferman, O.: Formalizing and reasoning about quality. J. ACM 63(3), 24 (2016)","journal-title":"J. ACM"},{"key":"9737_CR7","doi-asserted-by":"publisher","unstructured":"Alur, R., Bod\u00edk, R., Dallal, E., Fisman, D., Garg, P., Juniwal, G., Kress-Gazit, H., Madhusudan, P., Martin, M.M.K., Raghothaman, M., Saha, S., Seshia, S.A., Singh, R., Solar-Lezama, A., Torlak, E., Udupa, A.: Syntax-guided synthesis. In: Dependable Software Systems Engineering, pp. 1\u201325 (2015). https:\/\/doi.org\/10.3233\/978-1-61499-495-4-1","DOI":"10.3233\/978-1-61499-495-4-1"},{"key":"9737_CR8","doi-asserted-by":"publisher","unstructured":"Alur, R., Martin, M.M.K., Raghothaman, M., Stergiou, C., Tripakis, S., Udupa, A.: Synthesizing finite-state protocols from scenarios and requirements. In: Hardware and Software: Verification and Testing - 10th International Haifa Verification Conference, HVC 2014, Haifa, Israel, November 18-20, 2014. Proceedings. Lecture Notes in Computer Science, vol. 8855, pp. 75\u201391. Springer, Haifa, Israel (2014). https:\/\/doi.org\/10.1007\/978-3-319-13338-6_7","DOI":"10.1007\/978-3-319-13338-6_7"},{"key":"9737_CR9","doi-asserted-by":"publisher","unstructured":"Bloem, R., Chatterjee, K., Henzinger, T.A., Jobstmann, B.: Better quality in synthesis through quantitative objectives. In: Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings. Lecture Notes in Computer Science, vol. 5643, pp. 140\u2013156. Springer, Grenoble, France (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_14","DOI":"10.1007\/978-3-642-02658-4_14"},{"key":"9737_CR10","doi-asserted-by":"publisher","unstructured":"Bloem, R., Chatterjee, K., Jobstmann, B.: Graph games and reactive synthesis. In: Handbook of Model Checking, pp. 921\u2013962. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_27","DOI":"10.1007\/978-3-319-10575-8_27"},{"key":"9737_CR11","doi-asserted-by":"publisher","unstructured":"Bloem, R., Chockler, H., Ebrahimi, M., Strichman, O.: Synthesizing non-vacuous systems. In: Bouajjani, A., Monniaux, D. (eds.) Verification, Model Checking, and Abstract Interpretation, pp. 55\u201372. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-52234-0_4","DOI":"10.1007\/978-3-319-52234-0_4"},{"key":"9737_CR12","doi-asserted-by":"publisher","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","DOI":"10.1016\/j.ic.2016.10.011"},{"issue":"1","key":"9737_CR13","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1145\/322234.322243","volume":"28","author":"AK Chandra","year":"1981","unstructured":"Chandra, A.K., Kozen, D., Stockmeyer, L.J.: Alternation. J. ACM 28(1), 114\u2013133 (1981). https:\/\/doi.org\/10.1145\/322234.322243","journal-title":"J. ACM"},{"issue":"1","key":"9737_CR14","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1145\/322234.322243","volume":"28","author":"AK Chandra","year":"1981","unstructured":"Chandra, A.K., Kozen, D., Stockmeyer, L.J.: Alternation. J. ACM 28(1), 114\u2013133 (1981). https:\/\/doi.org\/10.1145\/322234.322243","journal-title":"J. ACM"},{"key":"9737_CR15","doi-asserted-by":"publisher","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.): Handbook of Model Checking. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8","DOI":"10.1007\/978-3-319-10575-8"},{"key":"9737_CR16","doi-asserted-by":"publisher","unstructured":"Damas, C., Lambeau, B., Lamsweerde, A.: Scenarios, goals, and state machines: a win-win partnership for model synthesis. In: Proceedings of the 14th ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2006, Portland, Oregon, USA, November 5-11, 2006, pp. 197\u2013207. ACM, Portland, Oregon, USA (2006). https:\/\/doi.org\/10.1145\/1181775.1181800","DOI":"10.1145\/1181775.1181800"},{"issue":"1","key":"9737_CR17","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1145\/2430536.2430543","volume":"22","author":"N D\u2019Ippolito","year":"2013","unstructured":"D\u2019Ippolito, N., Braberman, V.A., Piterman, N., Uchitel, S.: Synthesizing nonanomalous event-based controllers for liveness goals. ACM Trans. Softw. Eng. Methodol. 22(1), 9\u20131936 (2013). https:\/\/doi.org\/10.1145\/2430536.2430543","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"issue":"1","key":"9737_CR18","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1145\/2430536.2430543","volume":"22","author":"N D\u2019Ippolito","year":"2013","unstructured":"D\u2019Ippolito, N., Braberman, V.A., Piterman, N., Uchitel, S.: Synthesizing nonanomalous event-based controllers for liveness goals. ACM Trans. Softw. Eng. Methodol. 22(1), 9\u20131936 (2013). https:\/\/doi.org\/10.1145\/2430536.2430543","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"key":"9737_CR19","doi-asserted-by":"publisher","unstructured":"Dupont, P., Lambeau, B., Damas, C., 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"},{"issue":"1 &2","key":"9737_CR20","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1080\/08839510701853200","volume":"22","author":"P Dupont","year":"2008","unstructured":"Dupont, P., Lambeau, B., Damas, C., 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","journal-title":"Appl. Artif. Intell."},{"key":"9737_CR21","doi-asserted-by":"publisher","unstructured":"Duret-Lutz, A., Renault, E., Colange, M., Renkin, F., Gbaguidi, A., Schlehuber-Caissier, P., Medioni, T., Martin, A., Dubois, J., Gillard, C., Lauko, H.: From spot 2.0 to spot 2.10: What\u2019s new? CoRR abs\/2206.11366 (2022) https:\/\/doi.org\/10.48550\/arXiv.2206.11366arXiv:2206.11366","DOI":"10.48550\/arXiv.2206.11366"},{"key":"9737_CR22","doi-asserted-by":"publisher","unstructured":"Filiot, E., Jin, N., Raskin, J.: An antichain algorithm for LTL realizability. In: Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings. Lecture Notes in Computer Science, vol. 5643, pp. 263\u2013277. Springer, Grenoble, France (2009). https:\/\/doi.org\/10.1007\/978-3-642-02658-4_22","DOI":"10.1007\/978-3-642-02658-4_22"},{"key":"9737_CR23","doi-asserted-by":"publisher","unstructured":"Filiot, E., Jin, N., Raskin, J.: Antichains and compositional algorithms for LTL synthesis. Formal Methods Syst. Des. 39(3), 261\u2013296 (2011) https:\/\/doi.org\/10.1007\/s10703-011-0115-3","DOI":"10.1007\/s10703-011-0115-3"},{"issue":"3","key":"9737_CR24","doi-asserted-by":"publisher","first-page":"261","DOI":"10.1007\/s10703-011-0115-3","volume":"39","author":"E Filiot","year":"2011","unstructured":"Filiot, E., Jin, N., Raskin, J.: Antichains and compositional algorithms for LTL synthesis. Formal Methods Syst. Des. 39(3), 261\u2013296 (2011). https:\/\/doi.org\/10.1007\/s10703-011-0115-3","journal-title":"Formal Methods Syst. Des."},{"key":"9737_CR25","doi-asserted-by":"publisher","unstructured":"Giantamidis, G., Tripakis, S., Basagiannis, S.: Learning Moore machines from input-output traces. Int. J. Softw. Tools Technol. Transf. 23(1), 1\u201329 (2021) https:\/\/doi.org\/10.1007\/978-3-319-48989-6_18","DOI":"10.1007\/978-3-319-48989-6_18"},{"issue":"1","key":"9737_CR26","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-319-48989-6_18","volume":"23","author":"G Giantamidis","year":"2021","unstructured":"Giantamidis, G., Tripakis, S., Basagiannis, S.: Learning Moore machines from input-output traces. Int. J. Softw. Tools Technol. Transf. 23(1), 1\u201329 (2021). https:\/\/doi.org\/10.1007\/978-3-319-48989-6_18","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"9737_CR27","doi-asserted-by":"publisher","unstructured":"Heinz, J., Higuera, C., 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":"9737_CR28","unstructured":"https:\/\/strix.model.in.tum.de\/try\/"},{"key":"9737_CR29","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-25 October 2005, Pittsburgh, PA, USA, Proceedings, pp. 531\u2013542. IEEE Computer Society, Pittsburgh, PA, USA (2005). https:\/\/doi.org\/10.1109\/SFCS.2005.66","DOI":"10.1109\/SFCS.2005.66"},{"key":"9737_CR30","doi-asserted-by":"publisher","unstructured":"Kupferman, O.: On high-quality synthesis. In: Computer Science - Theory and Applications - 11th International Computer Science Symposium in Russia, CSR 2016, St. Petersburg, Russia, June 9-13, 2016, Proceedings. Lecture Notes in Computer Science, vol. 9691, pp. 1\u201315. Springer, St.Petersburg, Russia (2016). https:\/\/doi.org\/10.1007\/978-3-319-34171-2_1","DOI":"10.1007\/978-3-319-34171-2_1"},{"key":"9737_CR31","doi-asserted-by":"publisher","unstructured":"Meyer, P.J., Sickert, S., Luttenberger, M.: Strix: Explicit reactive synthesis strikes back! In: Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I. Lecture Notes in Computer Science, vol. 10981, pp. 578\u2013586. Springer, Oxford, UK (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_31","DOI":"10.1007\/978-3-319-96145-3_31"},{"key":"9737_CR32","doi-asserted-by":"publisher","unstructured":"Muskardin, E., Aichernig, B.K., Pill, I., Pferscher, A., Tappler, M.: Aalpy: An active automata learning library. In: Hou, Z., Ganesh, V. (eds.) Automated Technology for Verification and Analysis - 19th International Symposium, ATVA 2021, Gold Coast, QLD, Australia, October 18-22, 2021, Proceedings. Lecture Notes in Computer Science, vol. 12971, pp. 67-73. Springer, Gold Coast, QLD, Australia (2021). https:\/\/doi.org\/10.1007\/978-3-030-88885-5_5","DOI":"10.1007\/978-3-030-88885-5_5"},{"key":"9737_CR33","doi-asserted-by":"publisher","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of an asynchronous reactive module. In: Automata, Languages and Programming, 16th International Colloquium, ICALP89, Stresa, Italy, July 11-15, 1989, Proceedings. Lecture Notes in Computer Science, vol. 372, pp. 652\u2013671. Springer, Stresa, Italy (1989). https:\/\/doi.org\/10.1007\/BFb0035790","DOI":"10.1007\/BFb0035790"},{"key":"9737_CR34","doi-asserted-by":"publisher","unstructured":"Raha, R., Roy, R., Fijalkow, N., Neider, D.: Scalable anytime algorithms for learning fragments of linear temporal logic. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I. Lecture Notes in Computer Science, vol. 13243, pp. 263\u2013280. Springer, Munich, Germany (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_14","DOI":"10.1007\/978-3-030-99524-9_14"},{"key":"9737_CR35","doi-asserted-by":"publisher","unstructured":"Schewe, S., Finkbeiner, B.: Bounded synthesis. In: Automated Technology for Verification and Analysis, 5th International Symposium, ATVA 2007, Tokyo, Japan, October 22-25, 2007, Proceedings. Lecture Notes in Computer Science, vol. 4762, pp. 474\u2013488. Springer, Tokyo, Japan (2007). https:\/\/doi.org\/10.1007\/978-3-540-75596-8_33","DOI":"10.1007\/978-3-540-75596-8_33"},{"key":"9737_CR36","doi-asserted-by":"publisher","unstructured":"Solar-Lezama, A., Tancau, L., Bod\u00edk, R., Seshia, S.A., Saraswat, V.A.: Combinatorial sketching for finite programs. In: Shen, J.P., Martonosi, M. (eds.) Proceedings of the 12th International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2006, San Jose, CA, USA, October 21-25, 2006, pp. 404\u2013415. ACM, San Jose, CA, USA (2006). https:\/\/doi.org\/10.1145\/1168857.1168907","DOI":"10.1145\/1168857.1168907"},{"issue":"5\u20136","key":"9737_CR37","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/s10009-012-0249-7","volume":"15","author":"A Solar-Lezama","year":"2013","unstructured":"Solar-Lezama, A.: Program sketching. STTT 15(5\u20136), 475\u2013495 (2013). https:\/\/doi.org\/10.1007\/s10009-012-0249-7","journal-title":"STTT"},{"issue":"5\u20136","key":"9737_CR38","doi-asserted-by":"publisher","first-page":"475","DOI":"10.1007\/s10009-012-0249-7","volume":"15","author":"A Solar-Lezama","year":"2013","unstructured":"Solar-Lezama, A.: Program sketching. STTT 15(5\u20136), 475\u2013495 (2013). https:\/\/doi.org\/10.1007\/s10009-012-0249-7","journal-title":"STTT"},{"key":"9737_CR39","doi-asserted-by":"publisher","unstructured":"Thomas, W.: Automata on infinite objects. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (1991). https:\/\/doi.org\/10.1016\/B978-0-444-88074-1.50009-3","DOI":"10.1016\/B978-0-444-88074-1.50009-3"},{"key":"9737_CR40","unstructured":"https:\/\/github.com\/mrudu\/synth-learn"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09737-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10817-025-09737-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-025-09737-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,23]],"date-time":"2025-09-23T22:02:26Z","timestamp":1758664946000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10817-025-09737-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,8,21]]},"references-count":40,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,9]]}},"alternative-id":["9737"],"URL":"https:\/\/doi.org\/10.1007\/s10817-025-09737-6","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2025,8,21]]},"assertion":[{"value":"6 September 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 July 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 August 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors declare no competing interests.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Competing interests"}}],"article-number":"24"}}