{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,13]],"date-time":"2026-03-13T15:42:53Z","timestamp":1773416573142,"version":"3.50.1"},"publisher-location":"Cham","reference-count":23,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319961446","type":"print"},{"value":"9783319961453","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-96145-3_31","type":"book-chapter","created":{"date-parts":[[2018,7,20]],"date-time":"2018-07-20T18:25:55Z","timestamp":1532111155000},"page":"578-586","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":75,"title":["Strix: Explicit Reactive Synthesis Strikes Back!"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1334-9079","authenticated-orcid":false,"given":"Philipp J.","family":"Meyer","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0280-8981","authenticated-orcid":false,"given":"Salomon","family":"Sickert","sequence":"additional","affiliation":[]},{"given":"Michael","family":"Luttenberger","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2018,7,18]]},"reference":[{"key":"31_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, 2\u20136 November 2015, pp. 94\u2013101 (2015). https:\/\/doi.org\/10.1109\/ICCAD.2015.7372555","DOI":"10.1109\/ICCAD.2015.7372555"},{"issue":"4","key":"31_CR2","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/j.entcs.2007.09.004","volume":"190","author":"R Bloem","year":"2007","unstructured":"Bloem, R., Galler, S.J., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Specify, compile, run: hardware from PSL. Electr. Notes Theor. Comput. Sci. 190(4), 3\u201316 (2007). https:\/\/doi.org\/10.1016\/j.entcs.2007.09.004","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"31_CR3","doi-asserted-by":"publisher","unstructured":"Bloem, R., Jacobs, S., Khalimov, A.: Parameterized synthesis case study: AMBA AHB. In: Proceedings of the 3rd Workshop on Synthesis, SYNT 2014, Vienna, Austria, 23\u201324 July 2014, pp. 68\u201383 (2014). https:\/\/doi.org\/10.4204\/EPTCS.157.9","DOI":"10.4204\/EPTCS.157.9"},{"issue":"3","key":"31_CR4","doi-asserted-by":"publisher","first-page":"911","DOI":"10.1016\/j.jcss.2011.08.007","volume":"78","author":"R Bloem","year":"2012","unstructured":"Bloem, R., Jobstmann, B., Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of reactive(1) designs. J. Comput. Syst. Sci. 78(3), 911\u2013938 (2012). https:\/\/doi.org\/10.1016\/j.jcss.2011.08.007","journal-title":"J. Comput. Syst. Sci."},{"key":"31_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"652","DOI":"10.1007\/978-3-642-31424-7_45","volume-title":"Computer Aided Verification","author":"A Bohy","year":"2012","unstructured":"Bohy, A., Bruy\u00e8re, V., Filiot, E., Jin, N., Raskin, J.-F.: Acacia+, a tool for LTL synthesis. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 652\u2013657. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31424-7_45"},{"key":"31_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/978-3-642-14295-6_5","volume-title":"Computer Aided Verification","author":"R Brayton","year":"2010","unstructured":"Brayton, R., Mishchenko, A.: ABC: an academic industrial-strength verification tool. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 24\u201340. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_5"},{"key":"31_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"334","DOI":"10.1007\/978-3-319-08867-9_22","volume-title":"Computer Aided Verification","author":"R Cavada","year":"2014","unstructured":"Cavada, R., et al.: The nuXmv symbolic model checker. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 334\u2013342. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_22"},{"key":"31_CR8","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":"Automated Technology for Verification and Analysis","author":"A Duret-Lutz","year":"2016","unstructured":"Duret-Lutz, A., Lewkowicz, A., Fauchille, A., Michaud, T., Renault, \u00c9., Xu, L.: Spot 2.0 \u2014 a framework for LTL and $$\\omega $$\u03c9-automata manipulation. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 122\u2013129. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_8"},{"key":"31_CR9","series-title":"Lecture Notes in Computer Science","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 Ehlers","year":"2011","unstructured":"Ehlers, R.: Unbeast: symbolic bounded synthesis. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 272\u2013275. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-19835-9_25"},{"key":"31_CR10","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":"31_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-319-63390-9_17","volume-title":"Computer Aided Verification","author":"P Faymonville","year":"2017","unstructured":"Faymonville, P., Finkbeiner, B., Tentrup, L.: BoSy: an experimentation framework for bounded synthesis. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 325\u2013332. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63390-9_17"},{"issue":"5\u20136","key":"31_CR12","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 15(5\u20136), 585\u2013601 (2013). https:\/\/doi.org\/10.1007\/s10009-011-0207-9","journal-title":"STTT"},{"key":"31_CR13","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: A Guide to Current Research","year":"2002","unstructured":"Gr\u00e4del, E., Thomas, W., Wilke, T. (eds.): Automata Logics, and Infinite Games: A Guide to Current Research. LNCS, vol. 2500. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-36387-4"},{"key":"31_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"455","DOI":"10.1007\/978-3-319-02444-8_34","volume-title":"Automated Technology for Verification and Analysis","author":"P Hoffmann","year":"2013","unstructured":"Hoffmann, P., Luttenberger, M.: Solving parity games on the GPU. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 455\u2013459. Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-319-02444-8_34"},{"key":"31_CR15","doi-asserted-by":"crossref","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 and results. arXiv:1711.11439 [cs.LO] (2017)","DOI":"10.4204\/EPTCS.260.10"},{"key":"31_CR16","doi-asserted-by":"publisher","unstructured":"Jacobs, S., Klein, F., Schirmer, S.: A high-level LTL synthesis format: TLSF v1.1. In: Proceedings of the Fifth Workshop on Synthesis, SYNT@CAV 2016, Toronto, Canada, 17\u201318 July 2016, pp. 112\u2013132 (2016). https:\/\/doi.org\/10.4204\/EPTCS.229.10","DOI":"10.4204\/EPTCS.229.10"},{"key":"31_CR17","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":"31_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"928","DOI":"10.1007\/978-3-642-39799-8_66","volume-title":"Computer Aided Verification","author":"A Khalimov","year":"2013","unstructured":"Khalimov, A., Jacobs, S., Bloem, R.: PARTY parameterized synthesis of token rings. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 928\u2013933. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_66"},{"key":"31_CR19","unstructured":"Luttenberger, M.: Strategy iteration using non-deterministic strategies for solving parity games. arXiv:0806.2923 [cs.GT] (2008)"},{"key":"31_CR20","series-title":"Lecture Notes in Computer Science","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":"PJ Meyer","year":"2016","unstructured":"Meyer, P.J., Luttenberger, M.: Solving mean-payoff games on the GPU. In: Artho, C., Legay, A., Peled, D. (eds.) ATVA 2016. LNCS, vol. 9938, pp. 262\u2013267. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-46520-3_17"},{"key":"31_CR21","doi-asserted-by":"publisher","unstructured":"Morgenstern, A., Schneider, K.: Exploiting the temporal logic hierarchy and the non-confluence property for efficient LTL synthesis. In: Proceedings of the First Symposium on Games, Automata, Logic, and Formal Verification, GANDALF 2010, Minori (Amalfi Coast), Italy, 17\u201318 June 2010, pp. 89\u2013102 (2010). https:\/\/doi.org\/10.4204\/EPTCS.25.11","DOI":"10.4204\/EPTCS.25.11"},{"key":"31_CR22","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 1989, pp. 179\u2013190. ACM, New York (1989). https:\/\/doi.org\/10.1145\/75277.75293","DOI":"10.1145\/75277.75293"},{"key":"31_CR23","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","Computer Aided Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-96145-3_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,20]],"date-time":"2019-10-20T23:33:17Z","timestamp":1571614397000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-96145-3_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319961446","9783319961453"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-96145-3_31","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}