{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,4]],"date-time":"2024-09-04T13:04:09Z","timestamp":1725455049558},"publisher-location":"Berlin, Heidelberg","reference-count":17,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642386121"},{"type":"electronic","value":"9783642386138"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-38613-8_13","type":"book-chapter","created":{"date-parts":[[2013,5,13]],"date-time":"2013-05-13T02:45:19Z","timestamp":1368413119000},"page":"177-191","source":"Crossref","is-referenced-by-count":12,"title":["Solving Games Using Incremental Induction"],"prefix":"10.1007","author":[{"given":"Andreas","family":"Morgenstern","sequence":"first","affiliation":[]},{"given":"Manuel","family":"Gesell","sequence":"additional","affiliation":[]},{"given":"Klaus","family":"Schneider","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction of Analysis of Systems","author":"A. Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol.\u00a01579, pp. 193\u2013207. Springer, Heidelberg (1999)"},{"key":"13_CR2","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., K\u00f6nighofer, 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":"13_CR3","doi-asserted-by":"crossref","unstructured":"Bloem, R., Galler, S., Jobstmann, B., Piterman, N., Pnueli, A., Weiglhofer, M.: Specify, compile, run: Hardware from PSL. Electronic Notes in Theoretical Computer Science (ENTCS), vol.\u00a0190, pp. 3\u201316 (2007)","DOI":"10.1016\/j.entcs.2007.09.004"},{"key":"13_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"70","DOI":"10.1007\/978-3-642-18275-4_7","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"A.R. Bradley","year":"2011","unstructured":"Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol.\u00a06538, pp. 70\u201387. Springer, Heidelberg (2011)"},{"key":"13_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"4","DOI":"10.1007\/978-3-642-31424-7_4","volume-title":"Computer Aided Verification","author":"A.R. Bradley","year":"2012","unstructured":"Bradley, A.R.: IC3 and beyond: Incremental, inductive verification. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol.\u00a07358, pp. 4\u20134. Springer, Heidelberg (2012)"},{"key":"13_CR6","first-page":"125","volume-title":"Formal Methods in Computer-Aided Design (FMCAD)","author":"N. E\u00e9n","year":"2011","unstructured":"E\u00e9n, N., Mishchenko, A., Brayton, R.: Efficient implementation of property directed reachability. In: Bjesse, P., Slobodov\u00e1, A. (eds.) Formal Methods in Computer-Aided Design (FMCAD), pp. 125\u2013134. IEEE Computer Society, Austin (2011)"},{"key":"13_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-642-15643-4_10","volume-title":"Automated Technology for Verification and Analysis","author":"E. Filiot","year":"2010","unstructured":"Filiot, E., Jin, N., Raskin, J.-F.: Compositional algorithms for LTL synthesis. In: Bouajjani, A., Chin, W.-N. (eds.) ATVA 2010. LNCS, vol.\u00a06252, pp. 112\u2013127. Springer, Heidelberg (2010)"},{"key":"13_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"275","DOI":"10.1007\/978-3-540-30494-4_20","volume-title":"Formal Methods in Computer-Aided Design","author":"O. Grumberg","year":"2004","unstructured":"Grumberg, O., Schuster, A., Yadgar, A.: Memory efficient all-solutions SAT solver and its application for reachability analysis. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 275\u2013289. Springer, Heidelberg (2004)"},{"key":"13_CR9","series-title":"Lecture Notes in Computer Science","volume-title":"Automata, Logics, and Infinite Games","year":"2002","unstructured":"Gr\u00e4del, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games. LNCS, vol.\u00a02500. Springer, Heidelberg (2002)"},{"key":"13_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1007\/978-3-642-21581-0_19","volume-title":"Theory and Applications of Satisfiability Testing - SAT 2011","author":"M. Janota","year":"2011","unstructured":"Janota, M., Marques-Silva, J.: Abstraction-based algorithm for 2QBF. In: Sakallah, K.A., Simon, L. (eds.) SAT 2011. LNCS, vol.\u00a06695, pp. 230\u2013244. Springer, Heidelberg (2011)"},{"key":"13_CR11","doi-asserted-by":"crossref","unstructured":"Jobstmann, B.: Applications and Optimizations for LTL Synthesis. PhD thesis, IST \u2013 Institute for Software Technology, TU Graz, Graz, Austria (February 2007)","DOI":"10.1109\/FMCAD.2006.22"},{"key":"13_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-540-45069-6_1","volume-title":"Computer Aided Verification","author":"K.L. McMillan","year":"2003","unstructured":"McMillan, K.L.: Interpolation and SAT-based model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 1\u201313. Springer, Heidelberg (2003)"},{"key":"13_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1007\/978-3-540-30494-4_21","volume-title":"Formal Methods in Computer-Aided Design","author":"T. Nopper","year":"2004","unstructured":"Nopper, T., Scholl, C.: Approximate symbolic model checking for incomplete designs. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol.\u00a03312, pp. 290\u2013305. Springer, Heidelberg (2004)"},{"key":"13_CR14","unstructured":"Rosner, R.: Modular Synthesis of Reactive Systems. PhD thesis, The Weizmann Institute of Science, Israel, Rehovot, Israel (1992)"},{"key":"13_CR15","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":"13_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1007\/978-3-540-78163-9_26","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"S. Sohail","year":"2008","unstructured":"Sohail, S., Somenzi, F., Ravi, K.: A hybrid algorithm for LTL games. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol.\u00a04905, pp. 309\u2013323. Springer, Heidelberg (2008)"},{"key":"13_CR17","unstructured":"Somenzi, F.: Binary decision diagrams. In: Broy, M., Steinbr\u00fcggen, R. (eds.) Calculational System Design. NATO Science Series F: Computer and Systems Sciences, vol.\u00a0173, pp. 303\u2013366. IOS Press (1999)"}],"container-title":["Lecture Notes in Computer Science","Integrated Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-38613-8_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,13]],"date-time":"2019-05-13T00:56:20Z","timestamp":1557708980000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-38613-8_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642386121","9783642386138"],"references-count":17,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-38613-8_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}