{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T14:30:03Z","timestamp":1725460203936},"publisher-location":"Berlin, Heidelberg","reference-count":24,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642341878"},{"type":"electronic","value":"9783642341885"}],"license":[{"start":{"date-parts":[[2012,1,1]],"date-time":"2012-01-01T00:00:00Z","timestamp":1325376000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-34188-5_6","type":"book-chapter","created":{"date-parts":[[2012,10,11]],"date-time":"2012-10-11T10:04:33Z","timestamp":1349949873000},"page":"20-34","source":"Crossref","is-referenced-by-count":4,"title":["Generalized Reactivity(1) Synthesis without a Monolithic Strategy"],"prefix":"10.1007","author":[{"given":"Matthias","family":"Schlaipfer","sequence":"first","affiliation":[]},{"given":"Georg","family":"Hofferek","sequence":"additional","affiliation":[]},{"given":"Roderick","family":"Bloem","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"Baneres, D., Cortadella, J., Kishinevsky, M.: A recursive paradigm to solve Boolean relations. In: Design Automation Conference, pp. 416\u2013421 (2004)","DOI":"10.1145\/996566.996687"},{"key":"6_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"410","DOI":"10.1007\/978-3-642-14295-6_36","volume-title":"Computer Aided Verification","author":"R. Bloem","year":"2010","unstructured":"Bloem, R., Chatterjee, K., Greimel, K., Henzinger, T., Jobstmann, B.: Robustness in the Presence of Liveness. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 410\u2013424. Springer, Heidelberg (2010)"},{"key":"6_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"140","DOI":"10.1007\/978-3-642-02658-4_14","volume-title":"Computer Aided Verification","author":"R. Bloem","year":"2009","unstructured":"Bloem, R., Chatterjee, K., Henzinger, T., Jobstmann, B.: Better Quality in Synthesis through Quantitative Objectives. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 140\u2013156. Springer, Heidelberg (2009)"},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"425","DOI":"10.1007\/978-3-642-14295-6_37","volume-title":"Computer Aided Verification","author":"R. Bloem","year":"2010","unstructured":"Bloem, R., Cimatti, A., Greimel, K., Hofferek, G., Koenighofer, R., Roveri, M., Schuppan, V., Seeber, R.: RATSY \u2013 A New Requirements Analysis Tool with Synthesis. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol.\u00a06174, pp. 425\u2013429. Springer, Heidelberg (2010)"},{"key":"6_CR5","doi-asserted-by":"crossref","unstructured":"Bloem, R., Galler, S., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Automatic hardware synthesis from specifications: A case study. In: Proceedings of the Design, Automation and Test in Europe, pp. 1188\u20131193 (2007)","DOI":"10.1109\/DATE.2007.364456"},{"key":"6_CR6","doi-asserted-by":"crossref","unstructured":"Bloem, R., Galler, S., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Specify, compile, run: Hardware form PSL. In: 6th International Workshop on Compiler Optimization Meets Compiler Verification (2007)","DOI":"10.1016\/j.entcs.2007.09.004"},{"key":"6_CR7","unstructured":"Church, A.: Logic, arithmetic and automata. In: Proceedings International Mathematical Congress (1962)"},{"key":"6_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"263","DOI":"10.1007\/978-3-642-02658-4_22","volume-title":"Computer Aided Verification","author":"E. Filiot","year":"2009","unstructured":"Filiot, E., Jin, N., Raskin, J.F.: An Antichain Algorithm for LTL Realizability. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol.\u00a05643, pp. 263\u2013277. Springer, Heidelberg (2009)"},{"key":"6_CR9","doi-asserted-by":"publisher","first-page":"779","DOI":"10.1145\/1687399.1687544","volume-title":"Proceedings of the 2009 International Conference on Computer-Aided Design, ICCAD 2009","author":"J.H.R. Jiang","year":"2009","unstructured":"Jiang, J.H.R., Lin, H.P., Hung, W.L.: Interpolating functions from large Boolean relations. In: Proceedings of the 2009 International Conference on Computer-Aided Design, ICCAD 2009, pp. 779\u2013784. ACM, New York (2009)"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"Jobstmann, B., Bloem, R.: Optimizations for LTL synthesis. In: 6th Conference on Formal Methods in Computer Aided Design (FMCAD 2006), pp. 117\u2013124 (2006)","DOI":"10.1109\/FMCAD.2006.22"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"258","DOI":"10.1007\/978-3-540-73368-3_29","volume-title":"Computer Aided Verification","author":"B. Jobstmann","year":"2007","unstructured":"Jobstmann, B., Galler, S., Weiglhofer, M., Bloem, R.: Anzu: A Tool for Property Synthesis. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol.\u00a04590, pp. 258\u2013262. Springer, Heidelberg (2007)"},{"issue":"2","key":"6_CR12","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1016\/j.jcss.2011.05.005","volume":"78","author":"B. Jobstmann","year":"2012","unstructured":"Jobstmann, B., Staber, S., Griesmayer, A., Bloem, R.: Finding and fixing faults. Journal of Computer and System Sciences\u00a078(2), 441\u2013460 (2012)","journal-title":"Journal of Computer and System Sciences"},{"key":"6_CR13","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional \u03bc-calculus. Theoretical Computer Science\u00a027, 333\u2013354 (1983)","journal-title":"Theoretical Computer Science"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Complete functional synthesis. In: Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2010 (2010)","DOI":"10.1145\/1806596.1806632"},{"key":"6_CR15","doi-asserted-by":"crossref","unstructured":"Morgenstern, A., Schneider, K.: Exploiting the temporal logic hierarchy and the non-confluence property for efficient LTL synthesis. In: Montanari, A., Napoli, M., Parente, M. (eds.) Games, Automata, Logics, and Formal Verification (GandALF). Electronic Proceedings in Theoretical Computer Science (EPTCS), Minori, Italy, vol.\u00a025, pp. 89\u2013102 (2010)","DOI":"10.4204\/EPTCS.25.11"},{"key":"6_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"364","DOI":"10.1007\/11609773_24","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"N. Piterman","year":"2005","unstructured":"Piterman, N., Pnueli, A., Sa\u2019ar, Y.: Synthesis of Reactive(1) Designs. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 364\u2013380. Springer, Heidelberg (2005)"},{"key":"6_CR17","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proc. Symposium on Principles of Programming Languages (POPL 1989), pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"key":"6_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"474","DOI":"10.1007\/978-3-540-75596-8_33","volume-title":"Automated Technology for Verification and Analysis","author":"S. Schewe","year":"2007","unstructured":"Schewe, S., Finkbeiner, B.: Bounded Synthesis. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol.\u00a04762, pp. 474\u2013488. Springer, Heidelberg (2007)"},{"key":"6_CR19","doi-asserted-by":"crossref","unstructured":"Sohail, S., Somenzi, F.: Safety first: A two-stage algorithm for LTL games. In: 9th Int. Conf. on Formal Methods in Computer Aided Design, pp. 77\u201384 (2009)","DOI":"10.1109\/FMCAD.2009.5351138"},{"key":"6_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/978-3-642-10672-9_3","volume-title":"Programming Languages and Systems","author":"A. Solar-Lezama","year":"2009","unstructured":"Solar-Lezama, A.: The Sketching Approach to Program Synthesis. In: Hu, Z. (ed.) APLAS 2009. LNCS, vol.\u00a05904, pp. 4\u201313. Springer, Heidelberg (2009)"},{"key":"6_CR21","unstructured":"Somenzi, F.: CUDD: CU Decision Diagram Package. University of Colorado at Boulder, \n                    \n                      ftp:\/\/vlsi.colorado.edu\/pub\/"},{"key":"6_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1007\/11560548_6","volume-title":"Correct Hardware Design and Verification Methods","author":"S. Staber","year":"2005","unstructured":"Staber, S., Jobstmann, B., Bloem, R.: Finding and Fixing Faults. In: Borrione, D., Paul, W. (eds.) CHARME 2005. LNCS, vol.\u00a03725, pp. 35\u201349. Springer, Heidelberg (2005)"},{"key":"6_CR23","doi-asserted-by":"crossref","unstructured":"Vechev, M., Yahav, E., Yorsh, G.: Abstraction-guided synthesis of synchronization. In: Proc. Principles of Programming Languages, pp. 327\u2013338. ACM (2010)","DOI":"10.1145\/1707801.1706338"},{"issue":"10","key":"6_CR24","doi-asserted-by":"publisher","first-page":"1458","DOI":"10.1109\/43.256920","volume":"12","author":"Y. Watanabe","year":"1993","unstructured":"Watanabe, Y., Brayton, R.: Heuristic minimization of multiple-valued relations. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems\u00a012(10), 1458\u20131472 (1993)","journal-title":"IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems"}],"container-title":["Lecture Notes in Computer Science","Hardware and Software: Verification and Testing"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-34188-5_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,19]],"date-time":"2019-05-19T21:08:13Z","timestamp":1558300093000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-34188-5_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642341878","9783642341885"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-34188-5_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}