{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,5,18]],"date-time":"2026-05-18T07:02:05Z","timestamp":1779087725927,"version":"3.51.4"},"reference-count":64,"publisher":"Springer Science and Business Media LLC","issue":"5","license":[{"start":{"date-parts":[[2024,6,11]],"date-time":"2024-06-11T00:00:00Z","timestamp":1718064000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,6,11]],"date-time":"2024-06-11T00:00:00Z","timestamp":1718064000000},"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":["Int J Softw Tools Technol Transfer"],"published-print":{"date-parts":[[2024,10]]},"DOI":"10.1007\/s10009-024-00754-1","type":"journal-article","created":{"date-parts":[[2024,6,11]],"date-time":"2024-06-11T10:02:21Z","timestamp":1718100141000},"page":"551-567","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["The Reactive Synthesis Competition (SYNTCOMP): 2018\u20132021"],"prefix":"10.1007","volume":"26","author":[{"given":"Swen","family":"Jacobs","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Guillermo A.","family":"P\u00e9rez","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Remco","family":"Abraham","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"V\u00e9ronique","family":"Bruy\u00e8re","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Micha\u00ebl","family":"Cadilhac","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Maximilien","family":"Colange","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Charly","family":"Delfosse","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tom","family":"van Dijk","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alexandre","family":"Duret-Lutz","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Peter","family":"Faymonville","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Bernd","family":"Finkbeiner","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ayrat","family":"Khalimov","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Felix","family":"Klein","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Michael","family":"Luttenberger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Klara","family":"Meyer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thibaud","family":"Michaud","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adrien","family":"Pommellet","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Florian","family":"Renkin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Philipp","family":"Schlehuber-Caissier","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mouhammad","family":"Sakr","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Salomon","family":"Sickert","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ga\u00ebtan","family":"Staquet","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cl\u00e9ment","family":"Tamines","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Leander","family":"Tentrup","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adam","family":"Walker","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,6,11]]},"reference":[{"key":"754_CR1","unstructured":"Abraham, R.: Symbolic LTL reactive synthesis (2021). http:\/\/essay.utwente.nl\/87386\/"},{"key":"754_CR2","volume-title":"Lectures in Game Theory for Computer Scientists","year":"2011","unstructured":"Apt, K.R., Gr\u00e4del, E. (eds.): Lectures in Game Theory for Computer Scientists Cambridge University Press, Cambridge (2011). http:\/\/www.cambridge.org\/gb\/knowledge\/isbn\/item5760379"},{"key":"754_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/978-3-642-39176-7_6","volume-title":"Proceedings of the 20th International SPIN Symposium on Model Checking of Software (SPIN\u201913)","author":"T. Babiak","year":"2013","unstructured":"Babiak, T., Badie, T., Duret-Lutz, A., et al.: Compositional approach to suspension and other improvements to LTL translation. In: Proceedings of the 20th International SPIN Symposium on Model Checking of Software (SPIN\u201913). Lecture Notes in Computer Science, vol.\u00a07976, pp.\u00a081\u201398. Springer, Berlin (2013). https:\/\/doi.org\/10.1007\/978-3-642-39176-7_6"},{"key":"754_CR4","series-title":"Proceedings, Part I, Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/978-3-319-21690-4_31","volume-title":"Computer Aided Verification \u2013 27th International Conference, CAV 2015","author":"T. Babiak","year":"2015","unstructured":"Babiak, T., Blahoudek, F., Duret-Lutz, A., et al.: The Hanoi omega-automata format. In: Kroening, D., Pasareanu, C.S. (eds.) Computer Aided Verification \u2013 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015. Proceedings, Part I, Lecture Notes in Computer Science, vol.\u00a09206, pp.\u00a0479\u2013486. Springer, Berlin (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_31"},{"key":"754_CR5","volume-title":"Principles of Model Checking","author":"C. Baier","year":"2008","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"key":"754_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"586","DOI":"10.1007\/978-3-642-25566-3_46","volume-title":"Selected Papers","author":"A. Balint","year":"2011","unstructured":"Balint, A., Diepold, D., Gall, D., et al.: EDACC \u2013 an advanced platform for the experiment design, administration and analysis of empirical algorithms. In: Coello, C.A.C. (ed.) Selected Papers, Learning and Intelligent Optimization \u2013 5th International Conference, LION 5, Rome, Italy, January 17\u201321, 2011. Lecture Notes in Computer Science, vol.\u00a06683, pp.\u00a0586\u2013599. Springer, Berlin (2011). https:\/\/doi.org\/10.1007\/978-3-642-25566-3_46"},{"key":"754_CR7","unstructured":"Biere, A.: Hardware model checking competition (2007). http:\/\/fmv.jku.at\/hwmcc\/"},{"key":"754_CR8","unstructured":"Biere, A.: Aiger format and toolbox (2011). http:\/\/fmv.jku.at\/aiger\/"},{"key":"754_CR9","series-title":"Proceedings, Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-54013-4_1","volume-title":"Verification, Model Checking, and Abstract Interpretation - 15th International Conference, VMCAI 2014","author":"R. Bloem","year":"2014","unstructured":"Bloem, R., K\u00f6nighofer, R., Seidl, M.: Sat-based synthesis methods for safety specs. In: McMillan, K.L., Rival, X. (eds.) Verification, Model Checking, and Abstract Interpretation - 15th International Conference, VMCAI 2014, San Diego, CA, USA, January 19\u201321, 2014. Proceedings, Lecture Notes in Computer Science, vol.\u00a08318, pp.\u00a01\u201320. Springer, Berlin (2014). https:\/\/doi.org\/10.1007\/978-3-642-54013-4_1"},{"key":"754_CR10","unstructured":"Bohy, A.: Antichain based algorithms for the synthesis of reactive systems. PhD thesis, University of Mons (2014)"},{"key":"754_CR11","doi-asserted-by":"publisher","first-page":"652","DOI":"10.1007\/978-3-642-31424-7_45","volume-title":"CAV, LNCS","author":"A. Bohy","year":"2012","unstructured":"Bohy, A., Bruy\u00e8re, V., Filiot, E., et al.: Acacia+, a tool for LTL synthesis. In: Madhusudan, P., Seshia, S.A. (eds.) CAV, LNCS, vol.\u00a07358, pp.\u00a0652\u2013657. Springer, Berlin (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_45"},{"key":"754_CR12","series-title":"LIPIcs","doi-asserted-by":"publisher","first-page":"412","DOI":"10.4230\/LIPIcs.FSTTCS.2010.412","volume-title":"IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2010","author":"U. Boker","year":"2010","unstructured":"Boker, U., Kupferman, O., Steinitz, A.: Parityizing rabin and streett. In: Lodaya, K., Mahajan, M. (eds.) IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2010, Chennai, India, December 15-18, 2010, LIPIcs, vol.\u00a08, pp.\u00a0412\u2013423. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik (2010). https:\/\/doi.org\/10.4230\/LIPIcs.FSTTCS.2010.412"},{"key":"754_CR13","series-title":"Proceedings, Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1007\/978-3-030-30806-3_6","volume-title":"Reachability Problems \u2013 13th International Conference, RP 2019","author":"V. Bruy\u00e8re","year":"2019","unstructured":"Bruy\u00e8re, V., P\u00e9rez, G.A., Raskin, J., et al.: Partial solvers for generalized parity games. In: Filiot, E., Jungers, R.M., Potapov, I. (eds.) Reachability Problems \u2013 13th International Conference, RP 2019, Brussels, Belgium, September 11\u201313, 2019, Proceedings, Lecture Notes in Computer Science, vol.\u00a011674, pp.\u00a063\u201378. Springer, Berlin (2019). https:\/\/doi.org\/10.1007\/978-3-030-30806-3_6"},{"key":"754_CR14","series-title":"Proceedings, Part II, Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"192","DOI":"10.1007\/978-3-031-30820-8_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems \u2013 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023","author":"M. Cadilhac","year":"2023","unstructured":"Cadilhac, M., P\u00e9rez, G.A.: Acacia-bonsai: a modern implementation of downset-based LTL realizability. In: Tools and Algorithms for the Construction and Analysis of Systems \u2013 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023. Paris, France, April 22-27, 2023, Proceedings, Part II, Lecture Notes in Computer Science, vol.\u00a013994, pp.\u00a0192\u2013207. Springer, Berlin (2023)."},{"key":"754_CR15","first-page":"4683","volume-title":"IJCAI","author":"A. Camacho","year":"2018","unstructured":"Camacho, A., Muise, C.J., Baier, J.A., et al.: LTL realizability via safety and reachability games. In: IJCAI. ijcai.org pp.\u00a04683\u20134691 (2018)"},{"key":"754_CR16","series-title":"LIPIcs","doi-asserted-by":"publisher","first-page":"123:1","DOI":"10.4230\/LIPIcs.ICALP.2021.123","volume-title":"48th International Colloquium on Automata, Languages, and Programming, ICALP 2021","author":"A. Casares","year":"2021","unstructured":"Casares, A., Colcombet, T., Fijalkow, N.: Optimal transformations of games and automata using Muller conditions. In: Bansal, N., Merelli, E., Worrell, J. (eds.) 48th International Colloquium on Automata, Languages, and Programming, ICALP 2021, Glasgow, Scotland (Virtual Conference), July 12\u201316, 2021, LIPIcs, vol.\u00a0198, pp.\u00a0123:1\u2013123:14. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik (2021). https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2021.123"},{"key":"754_CR17","series-title":"Proceedings, Part II, Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-030-99527-0_6","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems \u2013 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022","author":"A. Casares","year":"2022","unstructured":"Casares, A., Duret-Lutz, A., Meyer, K.J., et al.: Practical applications of the alternating cycle decomposition. In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems \u2013 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\u20137, 2022. Proceedings, Part II, Lecture Notes in Computer Science, vol.\u00a013244, pp.\u00a099\u2013117. Springer, Berlin (2022). https:\/\/doi.org\/10.1007\/978-3-030-99527-0_6"},{"key":"754_CR18","series-title":"Proceedings, Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/978-3-540-71389-0_12","volume-title":"Foundations of Software Science and Computational Structures, 10th International Conference, FOSSACS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007","author":"K. Chatterjee","year":"2007","unstructured":"Chatterjee, K., Henzinger, T.A., Piterman, N.: Generalized parity games. In: Seidl, H. (ed.) Foundations of Software Science and Computational Structures, 10th International Conference, FOSSACS 2007, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2007, Braga, Portugal, March 24\u2013April 1, 2007. Proceedings, Lecture Notes in Computer Science, vol.\u00a04423, pp.\u00a0153\u2013167. Springer, Berlin (2007). https:\/\/doi.org\/10.1007\/978-3-540-71389-0_12"},{"key":"754_CR19","first-page":"3","volume-title":"Summaries of the Summer Institute of Symbolic Logic","author":"A. Church","year":"1957","unstructured":"Church, A.: Application of recursive arithmetic to the problem of circuit synthesis. In: Summaries of the Summer Institute of Symbolic Logic, vol.\u00a01, pp.\u00a03\u201350. Am. Math. Soc., Providence (1957)"},{"key":"754_CR20","doi-asserted-by":"crossref","unstructured":"Church, A.: Logic, arithmetic, and automata. J. Symb. Log. 29(4) (1964)","DOI":"10.2307\/2271624"},{"key":"754_CR21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8","volume-title":"Handbook of Model Checking","year":"2018","unstructured":"Clarke, E.M., Henzinger, T.A., Veith, H., et al. (eds.): Handbook of Model Checking Springer, Berlin (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8"},{"issue":"6","key":"754_CR22","doi-asserted-by":"publisher","first-page":"666","DOI":"10.1016\/j.ic.2009.05.007","volume":"208","author":"L. de Alfaro","year":"2010","unstructured":"de Alfaro, L., Roy, P.: Solving games via three-valued abstraction refinement. Inf. Comput. 208(6), 666\u2013676 (2010). https:\/\/doi.org\/10.1016\/j.ic.2009.05.007","journal-title":"Inf. Comput."},{"key":"754_CR23","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-77974-2","volume-title":"Computational Geometry: Algorithms and Applications","author":"M. De Berg","year":"2008","unstructured":"De Berg, M., Cheong, O., van Kreveld, M.J., et al.: Computational Geometry: Algorithms and Applications, 3rd edn. Springer, Berlin (2008). https:\/\/www.worldcat.org\/oclc\/227584184","edition":"3"},{"key":"754_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-319-46520-3_8","volume-title":"Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA\u201916)","author":"A. Duret-Lutz","year":"2016","unstructured":"Duret-Lutz, A., Lewkowicz, A., Fauchille, A., et al.: Spot 2.0 \u2014 a framework for LTL and $\\omega $-automata manipulation. In: Proceedings of the 14th International Symposium on Automated Technology for Verification and Analysis (ATVA\u201916). Lecture Notes in Computer Science, vol.\u00a09938, pp.\u00a0122\u2013129. Springer, Berlin (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_8"},{"key":"754_CR25","doi-asserted-by":"publisher","first-page":"365","DOI":"10.1007\/978-3-642-14295-6_33","volume-title":"International Conference on Computer Aided Verification","author":"R. Ehlers","year":"2010","unstructured":"Ehlers, R.: Symbolic bounded synthesis. In: International Conference on Computer Aided Verification, pp.\u00a0365\u2013379. Springer, Berlin (2010)"},{"key":"754_CR26","first-page":"272","volume-title":"International Conference on Tools and Algorithms for the Construction and Analysis of Systems","author":"R. Ehlers","year":"2011","unstructured":"Ehlers, R.: Unbeast: symbolic bounded synthesis. In: International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp.\u00a0272\u2013275. Springer, Berlin (2011)"},{"key":"754_CR27","doi-asserted-by":"publisher","first-page":"384","DOI":"10.1145\/3209108.3209161","volume-title":"Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS\u201918)","author":"J. Esparza","year":"2018","unstructured":"Esparza, J., K\u0159et\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\u201918), pp.\u00a0384\u2013393. ACM, New York (2018). https:\/\/doi.org\/10.1145\/3209108.3209161"},{"issue":"6","key":"754_CR28","doi-asserted-by":"publisher","first-page":"33:1","DOI":"10.1145\/3417995","volume":"67","author":"J. Esparza","year":"2020","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","journal-title":"J. ACM"},{"key":"754_CR29","series-title":"Proceedings, Part II, 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 \u2013 29th International Conference, CAV 2017","author":"P. Faymonville","year":"2017","unstructured":"Faymonville, P., Finkbeiner, B., Tentrup, L.: Bosy: an experimentation framework for bounded synthesis. In: Majumdar, R., Kuncak, V. (eds.) Computer Aided Verification \u2013 29th International Conference, CAV 2017, Heidelberg, Germany, July 24\u201328, 2017. Proceedings, Part II, Lecture Notes in Computer Science, vol.\u00a010427, pp.\u00a0325\u2013332. Springer, Berlin (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_17"},{"key":"754_CR30","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":"Proceedings, Part I","author":"B. Finkbeiner","year":"2016","unstructured":"Finkbeiner, B., Klein, F.: Bounded cycle synthesis. In: Chaudhuri, S., Farzan, A. (eds.) Proceedings, Part I, Computer Aided Verification \u2013 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17\u201323, 2016. Lecture Notes in Computer Science, vol.\u00a09779, pp.\u00a0118\u2013135. Springer, Berlin (2016). https:\/\/doi.org\/10.1007\/978-3-319-41528-4_7"},{"key":"754_CR31","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1145\/3331545.3342601","volume-title":"Proceedings of the 12th ACM SIGPLAN International Symposium on Haskell, Haskell@ICFP 2019","author":"B. Finkbeiner","year":"2019","unstructured":"Finkbeiner, B., Klein, F., Piskac, R., et al.: Synthesizing functional reactive programs. In: Eisenberg, R.A. (ed.) Proceedings of the 12th ACM SIGPLAN International Symposium on Haskell, Haskell@ICFP 2019, Berlin, Germany, August 18-23, 2019, pp.\u00a0162\u2013175. ACM, New York (2019). https:\/\/doi.org\/10.1145\/3331545.3342601"},{"key":"754_CR32","series-title":"Proceedings, Part I, Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"609","DOI":"10.1007\/978-3-030-25540-4_35","volume-title":"Computer Aided Verification \u2013 31st International Conference, CAV 2019","author":"B. Finkbeiner","year":"2019","unstructured":"Finkbeiner, B., Klein, F., Piskac, R., et al.: Temporal stream logic: synthesis beyond the bools. In: Dillig, I., Tasiran, S. (eds.) Computer Aided Verification \u2013 31st International Conference, CAV 2019, New York City, NY, USA, July 15\u201318, 2019. Proceedings, Part I, Lecture Notes in Computer Science, vol.\u00a011561, pp.\u00a0609\u2013629. Springer, Berlin (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_35"},{"key":"754_CR33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-76384-8_8","volume-title":"Proceedings for the 13th NASA Formal Methods Symposium (NFM\u201921)","author":"B. Finkbeiner","year":"2021","unstructured":"Finkbeiner, B., Geier, G., Passing, N.: Specification decomposition for reactive synthesis. In: Proceedings for the 13th NASA Formal Methods Symposium (NFM\u201921) (2021). https:\/\/doi.org\/10.1007\/978-3-030-76384-8_8"},{"key":"754_CR34","series-title":"Proceedings, Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"182","DOI":"10.1007\/978-3-642-04761-9_15","volume-title":"Automated Technology for Verification and Analysis, 7th International Symposium, ATVA 2009","author":"O. Friedmann","year":"2009","unstructured":"Friedmann, O., Lange, M.: Solving parity games in practice. In: Liu, Z., Ravn, A.P. (eds.) Automated Technology for Verification and Analysis, 7th International Symposium, ATVA 2009, Macao, China, October 14\u201316, 2009, Proceedings, Lecture Notes in Computer Science, vol.\u00a05799, pp.\u00a0182\u2013196. Springer, Berlin (2009). https:\/\/doi.org\/10.1007\/978-3-642-04761-9_15"},{"key":"754_CR35","doi-asserted-by":"publisher","first-page":"138","DOI":"10.23919\/FMCAD.2019.8894261","volume-title":"Formal Methods in Computer Aided Design, FMCAD 2019","author":"G. Geier","year":"2019","unstructured":"Geier, G., Heim, P., Klein, F., et al.: Syntroids: synthesizing a game for FPGAs using temporal logic specifications. In: Barrett, C.W., Yang, J. (eds.) Formal Methods in Computer Aided Design, FMCAD 2019, San Jose, CA, USA, October 22\u201325, 2019, pp.\u00a0138\u2013146. IEEE, Los Alamitos (2019). https:\/\/doi.org\/10.23919\/FMCAD.2019.8894261"},{"key":"754_CR36","unstructured":"Jacobs, S.: Extended AIGER format for synthesis. CoRR (2014). http:\/\/arxiv.org\/abs\/1405.5793. arXiv:1405.5793"},{"key":"754_CR37","doi-asserted-by":"publisher","unstructured":"Jacobs, S., Perez, G.A.: Data and scripts used for the SYNTCOMP report 2018\u20132021 (2023). https:\/\/doi.org\/10.5281\/zenodo.7588780","DOI":"10.5281\/zenodo.7588780"},{"key":"754_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"435","DOI":"10.1007\/978-3-030-81688-9_20","volume-title":"Computer Aided Verification \u2013 33rd International Conference, CAV 2021, Virtual Event, July 20\u201323, 2021, Proceedings, Part II","author":"S. Jacobs","year":"2021","unstructured":"Jacobs, S., Sakr, M.: AIGEN: random generation of symbolic transition systems. In: Silva, A., Leino, K.R.M. (eds.) Computer Aided Verification \u2013 33rd International Conference, CAV 2021, Virtual Event, July 20\u201323, 2021, Proceedings, Part II. Lecture Notes in Computer Science, vol.\u00a012760, pp.\u00a0435\u2013446. Springer, Berlin (2021). https:\/\/doi.org\/10.1007\/978-3-030-81688-9_20"},{"key":"754_CR39","doi-asserted-by":"publisher","first-page":"112","DOI":"10.4204\/EPTCS.229.10","volume-title":"Proceedings Fifth Workshop on Synthesis, SYNT@CAV 2016","author":"S. Jacobs","year":"2016","unstructured":"Jacobs, S., Klein, F., Schirmer, S.: A high-level LTL synthesis format: TLSF v1.1. In: Piskac, R., Dimitrova, R. (eds.) Proceedings Fifth Workshop on Synthesis, SYNT@CAV 2016, Toronto, Canada, July 17\u201318, 2016, pp.\u00a0112\u2013132 (2016). https:\/\/doi.org\/10.4204\/EPTCS.229.10"},{"key":"754_CR40","doi-asserted-by":"publisher","first-page":"116","DOI":"10.4204\/EPTCS.260.10","volume-title":"Proceedings Sixth Workshop on Synthesis, SYNT@CAV 2017","author":"S. Jacobs","year":"2017","unstructured":"Jacobs, S., Basset, N., Bloem, R., et al.: The 4th reactive synthesis competition (SYNTCOMP 2017): benchmarks, participants & results. In: Fisman, D., Jacobs, S. (eds.) Proceedings Sixth Workshop on Synthesis, SYNT@CAV 2017, Heidelberg, Germany, 22nd July 2017, pp.\u00a0116\u2013143 (2017). https:\/\/doi.org\/10.4204\/EPTCS.260.10"},{"issue":"3","key":"754_CR41","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/s10009-016-0416-3","volume":"19","author":"S. Jacobs","year":"2017","unstructured":"Jacobs, S., Bloem, R., Brenguier, R., et al.: The first reactive synthesis competition (SYNTCOMP 2014). Int. J. Softw. Tools Technol. Transf. 19(3), 367\u2013390 (2017) https:\/\/doi.org\/10.1007\/s10009-016-0416-3","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"754_CR42","series-title":"Proceedings, 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 \u2013 16th International Symposium, ATVA 2018","author":"J. Kret\u00ednsk\u00fd","year":"2018","unstructured":"Kret\u00ednsk\u00fd, J., Meggendorfer, T., Sickert, S.: Owl: a library for $\\omega $-words, automata, and LTL. In: Lahiri, S.K., Wang, C. (eds.) Automated Technology for Verification and Analysis \u2013 16th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7\u201310, 2018. Proceedings, Lecture Notes in Computer Science, vol.\u00a011138, pp.\u00a0543\u2013550. Springer, Berlin (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_34"},{"key":"754_CR43","doi-asserted-by":"publisher","first-page":"18","DOI":"10.4204\/EPTCS.326.2","volume-title":"Proceedings 11th International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2020","author":"O. Lijzenga","year":"2020","unstructured":"Lijzenga, O., van Dijk, T.: Symbolic parity game solvers that yield winning strategies. In: Raskin, J., Bresolin, D. (eds.) Proceedings 11th International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2020, Brussels, Belgium, September 21\u201322, 2020, pp.\u00a018\u201332 (2020). https:\/\/doi.org\/10.4204\/EPTCS.326.2"},{"key":"754_CR44","unstructured":"Luttenberger, M.: Strategy iteration using non-deterministic strategies for solving parity games. CoRR (2008). http:\/\/arxiv.org\/abs\/0806.2923. arXiv:0806.2923"},{"issue":"1\u20132","key":"754_CR45","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1007\/s00236-019-00349-3","volume":"57","author":"M. Luttenberger","year":"2020","unstructured":"Luttenberger, M., Meyer, P.J., Sickert, S.: Practical synthesis of reactive systems from LTL specifications via parity games. Acta Inform. 57(1\u20132), 3\u201336 (2020). https:\/\/doi.org\/10.1007\/s00236-019-00349-3","journal-title":"Acta Inform."},{"key":"754_CR46","unstructured":"Meyer, P.J., Sickert, S.: Modernising Strix. Presented at the 10th Workshop on Synthesis (2021)"},{"key":"754_CR47","series-title":"Proceedings, Part I, 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 - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018","author":"P.J. Meyer","year":"2018","unstructured":"Meyer, P.J., Sickert, S., Luttenberger, M.: Strix: explicit reactive synthesis strikes back! In: Chockler, H., Weissenbacher, G. (eds.) Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14\u201317, 2018. Proceedings, Part I, Lecture Notes in Computer Science, vol.\u00a010981, pp.\u00a0578\u2013586. Springer, Berlin (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_31"},{"key":"754_CR48","doi-asserted-by":"publisher","first-page":"180","DOI":"10.4204\/EPTCS.256.13","volume-title":"Proceedings of the Eighth International Symposium on Games, Automata, Logics and Formal Verification (GandALF\u201917)","author":"D. M\u00fcller","year":"2017","unstructured":"M\u00fcller, D., Sickert, S.: LTL to deterministic Emerson\u2013Lei automata. In: Bouyer, P., Orlandini, A., Pietro, P.S. (eds.) Proceedings of the Eighth International Symposium on Games, Automata, Logics and Formal Verification (GandALF\u201917), pp.\u00a0180\u2013194 (2017). https:\/\/doi.org\/10.4204\/EPTCS.256.13"},{"key":"754_CR49","unstructured":"P\u00e9rez, G.A.: The extended HOA format for synthesis. CoRR (2019). http:\/\/arxiv.org\/abs\/1912.05793. arXiv:1912.05793"},{"key":"754_CR50","doi-asserted-by":"publisher","unstructured":"Piterman, N.: From nondeterministic B\u00fcchi and Streett automata to deterministic parity automata. Log. Methods Comput. Sci. 3(3) (2007). https:\/\/doi.org\/10.2168\/LMCS-3(3:5)2007","DOI":"10.2168\/LMCS-3(3:5)2007"},{"key":"754_CR51","doi-asserted-by":"publisher","first-page":"46","DOI":"10.1109\/SFCS.1977.32","volume-title":"18th Annual Symposium on Foundations of Computer Science","author":"A. Pnueli","year":"1977","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, 31 October\u20131 November 1977, pp.\u00a046\u201357. IEEE Comput. Soc., Providence (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.32"},{"key":"754_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/978-3-030-59152-6_7","volume-title":"Proceedings of the 18th International Symposium on Automated Technology for Verification and Analysis (ATVA\u201920)","author":"F. Renkin","year":"2020","unstructured":"Renkin, F., Duret-Lutz, A., Pommellet, A.: Practical \u201cparitizing\u201d of Emerson\u2013Lei automata. In: Proceedings of the 18th International Symposium on Automated Technology for Verification and Analysis (ATVA\u201920). Lecture Notes in Computer Science, vol.\u00a012302, pp.\u00a0127\u2013143. Springer, Berlin (2020). https:\/\/doi.org\/10.1007\/978-3-030-59152-6_7"},{"key":"754_CR53","unstructured":"Renkin, F., Schlehuber, P., Duret-Lutz, A., et\u00a0al.: Improvements to ltlsynt. Presented at the 10th Workshop on Synthesis (2021) https:\/\/hal.archives-ouvertes.fr\/hal-03523385"},{"key":"754_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/978-3-031-08679-3_8","volume-title":"Proceedings of the 42nd International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE\u201922)","author":"F. Renkin","year":"2022","unstructured":"Renkin, F., Schlehuber-Caissier, P., Duret-Lutz, A., et al.: Effective reductions of Mealy machines. In: Proceedings of the 42nd International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE\u201922). Lecture Notes in Computer Science, vol.\u00a013273, pp.\u00a0114\u2013130. Springer, Berlin (2022)."},{"key":"754_CR55","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1109\/SFCS.1988.21948","volume-title":"29th Annual Symposium on Foundations of Computer Science, White Plains","author":"S. Safra","year":"1988","unstructured":"Safra, S.: On the complexity of omega-automata. In: 29th Annual Symposium on Foundations of Computer Science, White Plains, 24\u201326 October 1988, pp.\u00a0319\u2013327. IEEE Comput. Soc., New York (1988). https:\/\/doi.org\/10.1109\/SFCS.1988.21948"},{"key":"754_CR56","series-title":"European Design and Automation Association","doi-asserted-by":"publisher","first-page":"1","DOI":"10.7873\/DATE.2014.162","volume-title":"Design, Automation & Test in Europe Conference & Exhibition, DATE 2014","author":"M. Seidl","year":"2014","unstructured":"Seidl, M., K\u00f6nighofer, R.: Partial witnesses from preprocessed quantified Boolean formulas. In: Fettweis, G.P., Nebel, W. (eds.) Design, Automation & Test in Europe Conference & Exhibition, DATE 2014, Dresden, Germany, March 24\u201328, 2014. European Design and Automation Association, pp.\u00a01\u20136 (2014). https:\/\/doi.org\/10.7873\/DATE.2014.162"},{"key":"754_CR57","doi-asserted-by":"publisher","first-page":"831","DOI":"10.1145\/3373718.3394743","volume-title":"LICS \u201920: 35th Annual ACM\/IEEE Symposium on Logic in Computer Science","author":"S. Sickert","year":"2020","unstructured":"Sickert, S., Esparza, J.: An efficient normalisation procedure for linear temporal logic and very weak alternating automata. In: Hermanns, H., Zhang, L., Kobayashi, N., et al. (eds.) LICS \u201920: 35th Annual ACM\/IEEE Symposium on Logic in Computer Science, Saarbr\u00fccken, Germany, July 8\u201311, 2020, pp.\u00a0831\u2013844. ACM, New York (2020). https:\/\/doi.org\/10.1145\/3373718.3394743"},{"key":"754_CR58","unstructured":"Somenzi, F.: CUDD package, release 2.4.1 (2005). http:\/\/vlsi.colorado.edu\/~fabio\/CUDD\/"},{"key":"754_CR59","series-title":"Proceedings, Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1007\/978-3-319-08587-6_28","volume-title":"Automated Reasoning \u2013 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014","author":"A. Stump","year":"2014","unstructured":"Stump, A., Sutcliffe, G., Tinelli, C.: Starexec: a cross-community infrastructure for logic solving. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) Automated Reasoning \u2013 7th International Joint Conference, IJCAR 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 19\u201322, 2014. Proceedings, Lecture Notes in Computer Science, vol.\u00a08562, pp.\u00a0367\u2013373. Springer, Berlin (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_28"},{"key":"754_CR60","first-page":"388","volume-title":"SAT, Lecture Notes in Computer Science","author":"L. Tentrup","year":"2019","unstructured":"Tentrup, L., Rabe, M.N.: Clausal abstraction for DQBF. In: SAT, Lecture Notes in Computer Science, vol.\u00a011628, pp.\u00a0388\u2013405. Springer, Berlin (2019)"},{"key":"754_CR61","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-319-89960-2_16","volume-title":"Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201918)","author":"T. Van Dijk","year":"2018","unstructured":"Van Dijk, T.: Oink: an implementation and evaluation of modern parity game solvers. In: Proceedings of the 24th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS\u201918), pp.\u00a0291\u2013308. Springer, Berlin (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_16"},{"key":"754_CR62","doi-asserted-by":"publisher","first-page":"123","DOI":"10.4204\/EPTCS.305.9","volume-title":"Proceedings Tenth International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2019","author":"T. Van Dijk","year":"2019","unstructured":"Van Dijk, T., Rubbens, B.: Simple fixpoint iteration to solve parity games. In: Leroux, J., Raskin, J. (eds.) Proceedings Tenth International Symposium on Games, Automata, Logics, and Formal Verification, GandALF 2019, Bordeaux, France, 2\u20133 September 2019, pp.\u00a0123\u2013139 (2019). https:\/\/doi.org\/10.4204\/EPTCS.305.9"},{"issue":"6","key":"754_CR63","doi-asserted-by":"publisher","first-page":"675","DOI":"10.1007\/s10009-016-0433-2","volume":"19","author":"T. Van Dijk","year":"2017","unstructured":"Van Dijk, T., van de Pol, J.: Sylvan: multi-core framework for decision diagrams. Int. J. Softw. Tools Technol. Transf. 19(6), 675\u2013696 (2017). https:\/\/doi.org\/10.1007\/s10009-016-0433-2","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"754_CR64","doi-asserted-by":"publisher","first-page":"446","DOI":"10.1145\/800057.808711","volume-title":"Proceedings of the 16th Annual ACM Symposium on Theory of Computing","author":"M.Y. Vardi","year":"1984","unstructured":"Vardi, M.Y., Wolper, P.: Automata theoretic techniques for modal logics of programs (extended abstract). In: DeMillo, R.A. (ed.) Proceedings of the 16th Annual ACM Symposium on Theory of Computing, Washington, DC, USA, April 30\u2013May 2, 1984, pp.\u00a0446\u2013456. ACM, New York (1984). https:\/\/doi.org\/10.1145\/800057.808711"}],"container-title":["International Journal on Software Tools for Technology Transfer"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-024-00754-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10009-024-00754-1\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10009-024-00754-1.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,27]],"date-time":"2024-09-27T13:05:31Z","timestamp":1727442331000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10009-024-00754-1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,6,11]]},"references-count":64,"journal-issue":{"issue":"5","published-print":{"date-parts":[[2024,10]]}},"alternative-id":["754"],"URL":"https:\/\/doi.org\/10.1007\/s10009-024-00754-1","relation":{},"ISSN":["1433-2779","1433-2787"],"issn-type":[{"value":"1433-2779","type":"print"},{"value":"1433-2787","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,6,11]]},"assertion":[{"value":"17 May 2024","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 June 2024","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}