{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,15]],"date-time":"2024-09-15T14:33:24Z","timestamp":1726410804143},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783662491218"},{"type":"electronic","value":"9783662491225"}],"license":[{"start":{"date-parts":[[2015,12,25]],"date-time":"2015-12-25T00:00:00Z","timestamp":1451001600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-662-49122-5_24","type":"book-chapter","created":{"date-parts":[[2015,12,24]],"date-time":"2015-12-24T05:01:36Z","timestamp":1450933296000},"page":"495-513","source":"Crossref","is-referenced-by-count":0,"title":["A General Modular Synthesis Problem for Pushdown Systems"],"prefix":"10.1007","author":[{"given":"Ilaria","family":"De Crescenzo","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Salvatore","family":"La Torre","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2015,12,25]]},"reference":[{"issue":"4","key":"24_CR1","doi-asserted-by":"publisher","first-page":"786","DOI":"10.1145\/1075382.1075387","volume":"27","author":"R Alur","year":"2005","unstructured":"Alur, R., Benedikt, M., Etessami, K., Godefroid, P., Reps, T.W., Yannakakis, M.: Analysis of recursive state machines. ACM Trans. Program. Lang. Syst. 27(4), 786\u2013818 (2005)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"24_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"467","DOI":"10.1007\/978-3-540-24730-2_35","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Alur","year":"2004","unstructured":"Alur, R., Etessami, K., Madhusudan, P.: A temporal logic of nested calls and returns. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 467\u2013481. Springer, Heidelberg (2004)"},{"key":"24_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1007\/978-3-540-45069-6_6","volume-title":"Computer Aided Verification","author":"R Alur","year":"2003","unstructured":"Alur, R., La Torre, S., Madhusudan, P.: Modular strategies for infinite games on recursive graphs. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 67\u201379. Springer, Heidelberg (2003)"},{"key":"24_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/3-540-36577-X_26","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"R Alur","year":"2003","unstructured":"Alur, R., La Torre, S., Madhusudan, P.: Modular strategies for recursive game graphs. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 363\u2013378. Springer, Heidelberg (2003)"},{"issue":"2","key":"24_CR5","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1016\/j.tcs.2005.11.017","volume":"354","author":"R Alur","year":"2006","unstructured":"Alur, R., La Torre, S., Madhusudan, P.: Modular strategies for recursive game graphs. Theor. Comput. Sci. 354(2), 230\u2013249 (2006)","journal-title":"Theor. Comput. Sci."},{"issue":"3","key":"24_CR6","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1516512.1516518","volume":"56","author":"R Alur","year":"2009","unstructured":"Alur, R., Madhusudan, P.: Adding nesting structure to words. J. ACM 56(3), 1\u201343 (2009)","journal-title":"J. ACM"},{"key":"24_CR7","doi-asserted-by":"publisher","first-page":"56","DOI":"10.1016\/j.scico.2013.07.001","volume":"83","author":"B Aminof","year":"2014","unstructured":"Aminof, B., Mogavero, F., Murano, A.: Synthesis of hierarchical systems. Sci. Comput. Program. 83, 56\u201379 (2014)","journal-title":"Sci. Comput. Program."},{"key":"24_CR8","unstructured":"De Crescenzo, I., La Torre, S.: Winning CaRet games with modular strategies. In: CILC. CEUR Workshop Proceedings, vol. 810, pp. 327\u2013331. CEUR-WS.org (2011)"},{"key":"24_CR9","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"96","DOI":"10.1007\/978-3-642-41036-9_10","volume-title":"Reachability Problems","author":"I Crescenzo De","year":"2013","unstructured":"De Crescenzo, I., La Torre, S.: Modular synthesis with open components. In: Abdulla, P.A., Potapov, I. (eds.) RP 2013. LNCS, vol. 8169, pp. 96\u2013108. Springer, Heidelberg (2013)"},{"key":"24_CR10","doi-asserted-by":"crossref","unstructured":"De Crescenzo, I., La Torre, S., Velner, Y.: Visibly pushdown modular games. GandALF. EPTCS, vol. 161, pp. 260\u2013274 (2014)","DOI":"10.4204\/EPTCS.161.22"},{"key":"24_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"581","DOI":"10.1007\/978-3-642-31424-7_41","volume-title":"Computer Aided Verification","author":"WR Harris","year":"2012","unstructured":"Harris, W.R., Jha, S., Reps, T.: Secure programming via visibly pushdown safety games. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 581\u2013598. Springer, Heidelberg (2012)"},{"key":"24_CR12","doi-asserted-by":"crossref","unstructured":"Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: Oracle-guided component-based program synthesis. In: ICSE, pp. 215\u2013224. ACM (2010)","DOI":"10.1145\/1806799.1806833"},{"key":"24_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/11513988_23","volume-title":"Computer Aided Verification","author":"B Jobstmann","year":"2005","unstructured":"Jobstmann, B., Griesmayer, A., Bloem, R.: Program repair as a game. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 226\u2013238. Springer, Heidelberg (2005)"},{"issue":"2","key":"24_CR14","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. J. Comput. Syst. Sci. 78(2), 441\u2013460 (2012)","journal-title":"J. Comput. Syst. Sci."},{"issue":"9\u201310","key":"24_CR15","doi-asserted-by":"publisher","first-page":"1161","DOI":"10.1016\/j.ic.2008.03.017","volume":"206","author":"S Torre La","year":"2008","unstructured":"La Torre, S., Napoli, M., Parente, M., Parlato, G.: Verification of scope-dependent hierarchical state machines. Inf. Comput. 206(9\u201310), 1161\u20131177 (2008)","journal-title":"Inf. Comput."},{"key":"24_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"937","DOI":"10.1007\/978-3-540-73420-8_80","volume-title":"Automata, Languages and Programming","author":"S Torre La","year":"2007","unstructured":"La Torre, S., Parlato, G.: On the complexity of Ltl model-checking of recursive state machines. In: Arge, L., Cachin, C., Jurdzi\u0144ski, T., Tarlecki, A. (eds.) ICALP 2007. LNCS, vol. 4596, pp. 937\u2013948. Springer, Heidelberg (2007)"},{"key":"24_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1007\/978-3-540-30538-5_34","volume-title":"FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science","author":"C L\u00f6ding","year":"2004","unstructured":"L\u00f6ding, C., Madhusudan, P., Serre, O.: Visibly pushdown games. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol. 3328, pp. 408\u2013420. Springer, Heidelberg (2004)"},{"key":"24_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"395","DOI":"10.1007\/978-3-642-00596-1_28","volume-title":"Foundations of Software Science and Computational Structures","author":"Y Lustig","year":"2009","unstructured":"Lustig, Y., Vardi, M.Y.: Synthesis from component libraries. In: de Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol. 5504, pp. 395\u2013409. Springer, Heidelberg (2009)"},{"key":"24_CR19","doi-asserted-by":"crossref","first-page":"1","DOI":"10.4204\/EPTCS.54.1","volume":"54","author":"Yoad Lustig","year":"2011","unstructured":"Lustig, Y., Vardi, M.Y.: Synthesis from recursive-components libraries. In: GandALF. EPTCS vol. 54, pp. 1\u201316 (2011)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"24_CR20","unstructured":"Madhusudan, P.: Synthesizing reactive programs. In: CSL. LIPIcs, vol. 12, pp. 428\u2013442 (2011)"},{"key":"24_CR21","unstructured":"Salvati, S., Walukiewicz, I.: Evaluation is MSOL-compatible. In: FSTTCS. LIPIcs, vol. 24, pp. 103\u2013114 (2013)"},{"key":"24_CR22","first-page":"133","volume-title":"Formal Models and Semantics","author":"Wolfgang THOMAS","year":"1990","unstructured":"Thomas, W.: Automata on infinite objects. In: Handbook of Theoretical Computer Science, Volume B: Formal Models and Sematics (B), pp. 133\u2013192 (1990)"},{"key":"24_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"58","DOI":"10.1007\/3-540-45657-0_5","volume-title":"Computer Aided Verification","author":"W Thomas","year":"2002","unstructured":"Thomas, W.: Infinite games and verification (Extended abstract of a tutorial). In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 58\u201364. Springer, Heidelberg (2002)"},{"key":"24_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-00596-1_1","volume-title":"Foundations of Software Science and Computational Structures","author":"W Thomas","year":"2009","unstructured":"Thomas, W.: Facets of synthesis: revisiting church\u2019s problem. In: de Alfaro, L. (ed.) FOSSACS 2009. LNCS, vol. 5504, pp. 1\u201314. Springer, Heidelberg (2009)"},{"issue":"2","key":"24_CR25","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1006\/inco.2000.2894","volume":"164","author":"I Walukiewicz","year":"2001","unstructured":"Walukiewicz, I.: Pushdown processes: Games and model-checking. Inf. Comput. 164(2), 234\u2013263 (2001)","journal-title":"Inf. Comput."}],"container-title":["Lecture Notes in Computer Science","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-662-49122-5_24","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,1]],"date-time":"2019-06-01T04:34:38Z","timestamp":1559363678000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-662-49122-5_24"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,12,25]]},"ISBN":["9783662491218","9783662491225"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-662-49122-5_24","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2015,12,25]]}}}