{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T08:43:33Z","timestamp":1770281013547,"version":"3.49.0"},"reference-count":40,"publisher":"Springer Science and Business Media LLC","issue":"1-2","license":[{"start":{"date-parts":[[2019,11,21]],"date-time":"2019-11-21T00:00:00Z","timestamp":1574294400000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2019,11,21]],"date-time":"2019-11-21T00:00:00Z","timestamp":1574294400000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["253384115"],"award-info":[{"award-number":["253384115"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["253384115"],"award-info":[{"award-number":["253384115"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["317422601"],"award-info":[{"award-number":["317422601"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"crossref","award":["253384115"],"award-info":[{"award-number":["253384115"]}],"id":[{"id":"10.13039\/501100001659","id-type":"DOI","asserted-by":"crossref"}]},{"name":"European Research Council","award":["787367"],"award-info":[{"award-number":["787367"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Acta Informatica"],"published-print":{"date-parts":[[2020,4]]},"DOI":"10.1007\/s00236-019-00349-3","type":"journal-article","created":{"date-parts":[[2019,11,21]],"date-time":"2019-11-21T11:03:08Z","timestamp":1574334188000},"page":"3-36","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":36,"title":["Practical synthesis of reactive systems from LTL specifications via parity games"],"prefix":"10.1007","volume":"57","author":[{"given":"Michael","family":"Luttenberger","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1334-9079","authenticated-orcid":false,"given":"Philipp J.","family":"Meyer","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0280-8981","authenticated-orcid":false,"given":"Salomon","family":"Sickert","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,11,21]]},"reference":[{"key":"349_CR1","doi-asserted-by":"publisher","unstructured":"Abel, A., Reineke, J.: MeMin: SAT-based exact minimization of incompletely specified Mealy machines. In: Proceedings of the IEEE\/ACM International Conference on Computer-Aided Design, ICCAD 2015, Austin, TX, USA, November 2\u20136, 2015, pp. 94\u2013101 (2015). https:\/\/doi.org\/10.1109\/ICCAD.2015.7372555","DOI":"10.1109\/ICCAD.2015.7372555"},{"key":"349_CR2","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/978-3-319-21690-4_31","volume-title":"Computer Aided Verification","author":"Tom\u00e1\u0161 Babiak","year":"2015","unstructured":"Babiak, T., Blahoudek, F., Duret-Lutz, A., Klein, J., Kret\u00ednsk\u00fd, J., M\u00fcller, D., Parker, D., Strejcek, J.: The Hanoi omega-automata format. In: Computer Aided Verification\u201427th International Conference, CAV 2015, San Francisco, CA, USA, July 18\u201324, 2015, Proceedings, Part I, pp. 479\u2013486 (2015). https:\/\/doi.org\/10.1007\/978-3-319-21690-4_31"},{"key":"349_CR3","doi-asserted-by":"publisher","first-page":"921","DOI":"10.1007\/978-3-319-10575-8_27","volume-title":"Handbook of Model Checking","author":"R Bloem","year":"2018","unstructured":"Bloem, R., Chatterjee, K., Jobstmann, B.: Graph games and reactive synthesis. In: Clarke, E.M., Henzinger, T.A., Veith, H., Bloem, R. (eds.) Handbook of Model Checking, pp. 921\u2013962. Springer, Berlin (2018). https:\/\/doi.org\/10.1007\/978-3-319-10575-8_27"},{"key":"349_CR4","doi-asserted-by":"publisher","first-page":"68","DOI":"10.4204\/EPTCS.157.9","volume":"157","author":"Roderick Bloem","year":"2014","unstructured":"Bloem, R., Jacobs, S., Khalimov, A.: Parameterized synthesis case study: AMBA AHB. In: Proceedings 3rd Workshop on Synthesis, SYNT 2014, Vienna, Austria, July 23\u201324, 2014., pp. 68\u201383 (2014). https:\/\/doi.org\/10.4204\/EPTCS.157.9","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"349_CR5","doi-asserted-by":"publisher","first-page":"652","DOI":"10.1007\/978-3-642-31424-7_45","volume-title":"Computer Aided Verification","author":"Aaron Bohy","year":"2012","unstructured":"Bohy, A., Bruy\u00e8re, V., Filiot, E., Jin, N., Raskin, J.: Acacia+, a tool for LTL synthesis. In: Computer Aided Verification\u201424th International Conference, CAV 2012, Berkeley, CA, USA, July 7\u201313, 2012 Proceedings, pp. 652\u2013657 (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_45"},{"key":"349_CR6","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-642-14295-6_5","volume-title":"Computer Aided Verification","author":"Robert Brayton","year":"2010","unstructured":"Brayton, R.K., Mishchenko, A.: ABC: an academic industrial-strength verification tool. In: Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings, pp. 24\u201340 (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_5"},{"key":"349_CR7","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/978-3-319-08867-9_22","volume-title":"Computer Aided Verification","author":"Roberto Cavada","year":"2014","unstructured":"Cavada, R., Cimatti, A., Dorigatti, M., Griggio, A., Mariotti, A., Micheli, A., Mover, S., Roveri, M., Tonetta, S.: The nuXmv symbolic model checker. In: Computer Aided Verification\u201426th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18\u201322, 2014. Proceedings, pp. 334\u2013342 (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_22"},{"key":"349_CR8","doi-asserted-by":"publisher","first-page":"122","DOI":"10.1007\/978-3-319-46520-3_8","volume-title":"Automated Technology for Verification and Analysis","author":"Alexandre Duret-Lutz","year":"2016","unstructured":"Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, E., Xu, L.: Spot 2.0\u2014a framework for LTL and $$\\omega $$-automata manipulation. In: Automated Technology for Verification and Analysis\u201414th International Symposium, ATVA 2016, Chiba, Japan, October 17\u201320, 2016, Proceedings, pp. 122\u2013129 (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_8"},{"key":"349_CR9","doi-asserted-by":"publisher","first-page":"272","DOI":"10.1007\/978-3-642-19835-9_25","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R\u00fcdiger Ehlers","year":"2011","unstructured":"Ehlers, R.: Unbeast: symbolic bounded synthesis. In: Tools and Algorithms for the Construction and Analysis of Systems\u201417th International Conference, TACAS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbr\u00fccken, Germany, March 26-April 3, 2011. Proceedings, pp. 272\u2013275 (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_25"},{"issue":"2","key":"349_CR10","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/s10703-011-0137-x","volume":"40","author":"R Ehlers","year":"2012","unstructured":"Ehlers, R.: Symbolic bounded synthesis. Form. Methods Syst. Des. 40(2), 232\u2013262 (2012). https:\/\/doi.org\/10.1007\/s10703-011-0137-x","journal-title":"Form. Methods Syst. Des."},{"key":"349_CR11","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/978-3-030-31784-3_23","volume-title":"Automated Technology for Verification and Analysis","author":"R\u00fcdiger Ehlers","year":"2019","unstructured":"Ehlers, R., Adabala, K.: Reactive synthesis of graphical user interface glue code. In: Y.\u00a0Chen, C.\u00a0Cheng, J.\u00a0Esparza (eds.) Automated Technology for Verification and Analysis\u201417th International Symposium, ATVA 2019, Taipei, Taiwan, October 28\u201331, 2019, Proceedings, Lecture Notes in Computer Science, vol. 11781, pp. 387\u2013403. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-31784-3_23"},{"key":"349_CR12","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":"Javier Esparza","year":"2017","unstructured":"Esparza, J., Kret\u00ednsk\u00fd, J., Raskin, J., Sickert, S.: From LTL and limit-deterministic B\u00fcchi automata to deterministic parity automata. In: Tools and Algorithms for the Construction and Analysis of Systems\u201423rd International Conference, TACAS 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22\u201329, 2017, Proceedings, Part I, pp. 426\u2013442 (2017). https:\/\/doi.org\/10.1007\/978-3-662-54577-5_25"},{"key":"349_CR13","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: Proceedings of the 33rd Annual ACM\/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09\u201312, 2018, pp. 384\u2013393 (2018). https:\/\/doi.org\/10.1145\/3209108.3209161","DOI":"10.1145\/3209108.3209161"},{"key":"349_CR14","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-319-63390-9_17","volume-title":"Computer Aided Verification","author":"Peter Faymonville","year":"2017","unstructured":"Faymonville, P., Finkbeiner, B., Tentrup, L.: BoSy: An experimentation framework for bounded synthesis. In: Computer Aided Verification - 29th International Conference, CAV 2017, Heidelberg, Germany, July 24-28, 2017, Proceedings, Part II, pp. 325\u2013332 (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_17"},{"issue":"3","key":"349_CR15","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. Form. Methods Syst. Des. 39(3), 261\u2013296 (2011). https:\/\/doi.org\/10.1007\/s10703-011-0115-3","journal-title":"Form. Methods Syst. Des."},{"key":"349_CR16","doi-asserted-by":"publisher","unstructured":"Finkbeiner, B., Klein, F., Piskac, R., Santolucito, M.: 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\u201323, 2019, pp. 162\u2013175. ACM (2019). https:\/\/doi.org\/10.1145\/3331545.3342601","DOI":"10.1145\/3331545.3342601"},{"issue":"3","key":"349_CR17","doi-asserted-by":"publisher","first-page":"669","DOI":"10.1142\/S0129054112400333","volume":"23","author":"O Friedmann","year":"2012","unstructured":"Friedmann, O., Lange, M.: Two local strategy iteration schemes for parity game solving. Int. J. Found. Comput. Sci. 23(3), 669\u2013685 (2012). https:\/\/doi.org\/10.1142\/S0129054112400333","journal-title":"Int. J. Found. Comput. Sci."},{"key":"349_CR18","doi-asserted-by":"crossref","unstructured":"Geier, G., Heim, P., Klein, F., Finkbeiner, B.: Synthroids: Synthesizing a game for fpgas using temporal logic specifications. In: FMCAD, pp. 1\u20135. IEEE (2019)","DOI":"10.23919\/FMCAD.2019.8894261"},{"key":"349_CR19","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1007\/978-3-030-01090-4_26","volume-title":"Automated Technology for Verification and Analysis","author":"Carsten Gerstacker","year":"2018","unstructured":"Gerstacker, C., Klein, F., Finkbeiner, B.: Bounded synthesis of reactive programs. In: Automated Technology for Verification and Analysis\u201416th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7\u201310, 2018, Proceedings, pp. 441\u2013457 (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_26"},{"key":"349_CR20","doi-asserted-by":"publisher","first-page":"308","DOI":"10.1007\/3-540-36135-9_20","volume-title":"Formal Techniques for Networked and Distributed Sytems \u2014 FORTE 2002","author":"Dimitra Giannakopoulou","year":"2002","unstructured":"Giannakopoulou, D., Lerda, F.: From states to transitions: Improving translation of LTL formulae to B\u00fcchi automata. In: Formal Techniques for Networked and Distributed Systems\u2014FORTE 2002, 22nd IFIP WG 6.1 International Conference Houston, Texas, USA, November 11\u201314, 2002, Proceedings, pp. 308\u2013326 (2002). https:\/\/doi.org\/10.1007\/3-540-36135-9_20"},{"issue":"5\u20136","key":"349_CR21","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/s10009-011-0207-9","volume":"15","author":"Y Godhal","year":"2013","unstructured":"Godhal, Y., Chatterjee, K., Henzinger, T.A.: Synthesis of AMBA AHB from formal specification: a case study. STTT (Int. J. Softw. Tools. Technol. Trans.) 15(5\u20136), 585\u2013601 (2013). https:\/\/doi.org\/10.1007\/s10009-011-0207-9","journal-title":"STTT (Int. J. Softw. Tools. Technol. Trans.)"},{"key":"349_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36387-4","volume-title":"Automata Logics, and Infinite Games","year":"2002","unstructured":"Gr\u00e4del, E., Thomas, W., Wilke, T.: Automata, Logics, and Infinite Games: A Guide to Current Research, Lecture Notes in Computer Science, vol. 2500. Springer (2002). https:\/\/doi.org\/10.1007\/3-540-36387-4"},{"key":"349_CR23","unstructured":"Jacobs, S., Basset, N., Bloem, R., Brenguier, R., Colange, M., Faymonville, P., Finkbeiner, B., Khalimov, A., Klein, F., Michaud, T., P\u00e9rez, G.A., Raskin, J., Sankur, O., Tentrup, L.: The 4th reactive synthesis competition (SYNTCOMP 2017): Benchmarks, participants & results (2017). arxiv:1711.11439"},{"key":"349_CR24","unstructured":"Jacobs, S., Bloem, R., Brenguier, R., Khalimov, A., Klein, F., K\u00f6nighofer, R., Kreber, J., Legg, A., Narodytska, N., P\u00e9rez, G.A., Raskin, J., Ryzhyk, L., Sankur, O., Seidl, M., Tentrup, L., Walker, A.: The 3rd reactive synthesis competition (SYNTCOMP 2016): Benchmarks, participants & results (2016). arxiv:1609.00507"},{"key":"349_CR25","unstructured":"Jacobs, S., Bloem, R., Colange, M., Faymonville, P., Finkbeiner, B., Khalimov, A., Klein, F., Luttenberger, M., Meyer, P.J., Michaud, T., Sakr, M., Sickert, S., Tentrup, L., Walker, A.: The 5th reactive synthesis competition (SYNTCOMP 2018): Benchmarks, participants & results (2019). arxiv:1904.07736"},{"key":"349_CR26","doi-asserted-by":"crossref","unstructured":"Jobstmann, B.: Applications and optimizations for LTL synthesis. Ph.D. thesis, Graz University of Technology (2007)","DOI":"10.1109\/FMCAD.2006.22"},{"key":"349_CR27","doi-asserted-by":"publisher","first-page":"928","DOI":"10.1007\/978-3-642-39799-8_66","volume-title":"Computer Aided Verification","author":"Ayrat Khalimov","year":"2013","unstructured":"Khalimov, A., Jacobs, S., Bloem, R.: PARTY parameterized synthesis of token rings. In: Computer Aided Verification\u201425th International Conference, CAV 2013, Saint Petersburg, Russia, July 13\u201319, 2013. Proceedings, pp. 928\u2013933 (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_66"},{"key":"349_CR28","doi-asserted-by":"publisher","first-page":"543","DOI":"10.1007\/978-3-030-01090-4_34","volume-title":"Automated Technology for Verification and Analysis","author":"Jan K\u0159et\u00ednsk\u00fd","year":"2018","unstructured":"Kret\u00ednsk\u00fd, J., Meggendorfer, T., Sickert, S.: Owl: A library for $$\\omega $$-words, automata, and LTL. In: Automated Technology for Verification and Analysis\u201416th International Symposium, ATVA 2018, Los Angeles, CA, USA, October 7\u201310, 2018, Proceedings, pp. 543\u2013550 (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_34"},{"key":"349_CR29","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-642-27660-6_8","volume-title":"SOFSEM 2012: Theory and Practice of Computer Science","author":"Orna Kupferman","year":"2012","unstructured":"Kupferman, O.: Recent challenges and ideas in temporal synthesis. In: SOFSEM 2012: Theory and Practice of Computer Science - 38th Conference on Current Trends in Theory and Practice of Computer Science, \u0160pindler\u016fv Ml\u00fdn, Czech Republic, January 21\u201327, 2012. Proceedings, pp. 88\u201398 (2012). https:\/\/doi.org\/10.1007\/978-3-642-27660-6_8"},{"key":"349_CR30","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/11817963_6","volume-title":"Computer Aided Verification","author":"Orna Kupferman","year":"2006","unstructured":"Kupferman, O., Piterman, N., Vardi, M.Y.: Safraless compositional synthesis. In: Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17\u201320, 2006, Proceedings, pp. 31\u201344 (2006). https:\/\/doi.org\/10.1007\/11817963_6"},{"key":"349_CR31","unstructured":"Luttenberger, M.: Strategy iteration using non-deterministic strategies for solving parity games (2008). arxiv:0806.2923"},{"key":"349_CR32","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/978-3-319-46520-3_17","volume-title":"Automated Technology for Verification and Analysis","author":"Philipp J. Meyer","year":"2016","unstructured":"Meyer, P.J., Luttenberger, M.: Solving mean-payoff games on the GPU. In: Automated Technology for Verification and Analysis\u201414th International Symposium, ATVA 2016, Chiba, Japan, October 17\u201320, 2016, Proceedings, pp. 262\u2013267 (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_17"},{"key":"349_CR33","doi-asserted-by":"publisher","first-page":"578","DOI":"10.1007\/978-3-319-96145-3_31","volume-title":"Computer Aided Verification","author":"Philipp J. Meyer","year":"2018","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\u201317, 2018, Proceedings, Part I, pp. 578\u2013586 (2018). https:\/\/doi.org\/10.1007\/978-3-319-96145-3_31"},{"key":"349_CR34","doi-asserted-by":"publisher","first-page":"89","DOI":"10.4204\/EPTCS.25.11","volume":"25","author":"Andreas Morgenstern","year":"2010","unstructured":"Morgenstern, A., Schneider, K.: Exploiting the temporal logic hierarchy and the non-confluence property for efficient LTL synthesis. In: Proceedings First Symposium on Games, Automata, Logic, and Formal Verification, GANDALF 2010, Minori (Amalfi Coast), Italy, 17\u201318th June 2010., pp. 89\u2013102 (2010). https:\/\/doi.org\/10.4204\/EPTCS.25.11","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"349_CR35","doi-asserted-by":"publisher","first-page":"180","DOI":"10.4204\/EPTCS.256.13","volume":"256","author":"David M\u00fcller","year":"2017","unstructured":"M\u00fcller, D., Sickert, S.: LTL to deterministic Emerson-Lei automata. In: Proceedings Eighth International Symposium on Games, Automata, Logics and Formal Verification, GandALF 2017, Roma, Italy, 20\u201322 September 2017., pp. 180\u2013194 (2017). https:\/\/doi.org\/10.4204\/EPTCS.256.13","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"349_CR36","doi-asserted-by":"publisher","unstructured":"Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science, Providence, Rhode Island, USA, 31 October\u20131 November 1977, pp. 46\u201357 (1977). https:\/\/doi.org\/10.1109\/SFCS.1977.32","DOI":"10.1109\/SFCS.1977.32"},{"key":"349_CR37","doi-asserted-by":"publisher","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL \u201989, pp. 179\u2013190. ACM, New York, NY, USA (1989). https:\/\/doi.org\/10.1145\/75277.75293","DOI":"10.1145\/75277.75293"},{"key":"349_CR38","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1007\/978-3-319-41540-6_17","volume-title":"Computer Aided Verification","author":"Salomon Sickert","year":"2016","unstructured":"Sickert, S., Esparza, J., Jaax, S., Kret\u00ednsk\u00fd, J.: Limit-deterministic B\u00fcchi automata for linear temporal logic. In: Computer Aided Verification\u201428th International Conference, CAV 2016, Toronto, ON, Canada, July 17\u201323, 2016, Proceedings, Part II, pp. 312\u2013332 (2016). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_17"},{"issue":"5\u20136","key":"349_CR39","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/s10009-012-0224-3","volume":"15","author":"S Sohail","year":"2013","unstructured":"Sohail, S., Somenzi, F.: Safety first: a two-stage algorithm for the synthesis of reactive systems. STTT (Int. J. Softw. Tools Technol. Trans.) 15(5\u20136), 433\u2013454 (2013). https:\/\/doi.org\/10.1007\/s10009-012-0224-3","journal-title":"STTT (Int. J. Softw. Tools Technol. Trans.)"},{"key":"349_CR40","unstructured":"Somenzi, F.: CUDD: CU decision diagram package release 3.0.0 (2015)"}],"container-title":["Acta Informatica"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-019-00349-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00236-019-00349-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00236-019-00349-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,20]],"date-time":"2020-11-20T01:28:58Z","timestamp":1605835738000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00236-019-00349-3"}},"subtitle":["You can teach an old dog new tricks: making a classic approach structured, forward-explorative, and incremental"],"short-title":[],"issued":{"date-parts":[[2019,11,21]]},"references-count":40,"journal-issue":{"issue":"1-2","published-print":{"date-parts":[[2020,4]]}},"alternative-id":["349"],"URL":"https:\/\/doi.org\/10.1007\/s00236-019-00349-3","relation":{},"ISSN":["0001-5903","1432-0525"],"issn-type":[{"value":"0001-5903","type":"print"},{"value":"1432-0525","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,11,21]]},"assertion":[{"value":"16 January 2019","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"2 November 2019","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 November 2019","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}