{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,25]],"date-time":"2025-03-25T20:43:01Z","timestamp":1742935381063,"version":"3.40.3"},"publisher-location":"Berlin, Heidelberg","reference-count":23,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642401831"},{"type":"electronic","value":"9783642401848"}],"license":[{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2013,1,1]],"date-time":"2013-01-01T00:00:00Z","timestamp":1356998400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2013]]},"DOI":"10.1007\/978-3-642-40184-8_10","type":"book-chapter","created":{"date-parts":[[2013,7,23]],"date-time":"2013-07-23T01:50:56Z","timestamp":1374544256000},"page":"121-136","source":"Crossref","is-referenced-by-count":13,"title":["Well-Structured Pushdown Systems"],"prefix":"10.1007","author":[{"given":"Xiaojuan","family":"Cai","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mizuhito","family":"Ogawa","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"1-2","key":"10_CR1","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1006\/inco.1999.2843","volume":"160","author":"P. Abdulla","year":"2000","unstructured":"Abdulla, P., Cerans, K., Jonsson, C., Yih-Kuen, T.: Algorithmic analysis of programs with well quasi-ordered domains. Information and Computation\u00a0160(1-2), 109\u2013127 (2000)","journal-title":"Information and Computation"},{"key":"10_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/978-3-642-00768-2_11","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"M.F. Atig","year":"2009","unstructured":"Atig, M.F., Bouajjani, A., Qadeer, S.: Context-bounded analysis for concurrent pro-grams with dynamic creation of threads. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol.\u00a05505, pp. 107\u2013123. Springer, Heidelberg (2009)"},{"key":"10_CR3","doi-asserted-by":"crossref","unstructured":"Bouajjani, A., Emmi, M.: Analysis of recursively parallel programs. In: Principles of Programming Languages (POPL 2012), pp. 203\u2013214. ACM (2012)","DOI":"10.1145\/2103621.2103681"},{"key":"10_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/3-540-63141-0_10","volume-title":"CONCUR\u201997: Concurrency Theory","author":"A. Bouajjani","year":"1997","unstructured":"Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model-checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol.\u00a01243, pp. 135\u2013150. Springer, Heidelberg (1997)"},{"key":"10_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"136","DOI":"10.1007\/978-3-540-74407-8_10","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"R. Chadha","year":"2007","unstructured":"Chadha, R., Viswanathan, M.: Decidability results for well-structured transition systems with auxiliary storage. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol.\u00a04703, pp. 136\u2013150. Springer, Heidelberg (2007)"},{"issue":"1","key":"10_CR6","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1016\/j.jcss.2012.04.002","volume":"79","author":"S. Demri","year":"2012","unstructured":"Demri, S., Jurdzi\u0144ski, M., Lachish, O., Lazic, R.: The covering and boundedness problems for branching vector addition systems. Journal of Computer and System Sciences\u00a079(1), 23\u201338 (2012)","journal-title":"Journal of Computer and System Sciences"},{"key":"10_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/10722167_20","volume-title":"Computer Aided Verification","author":"J. Esparza","year":"2000","unstructured":"Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithms for model checking pushdown systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 232\u2013247. Springer, Heidelberg (2000)"},{"key":"10_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"499","DOI":"10.1007\/3-540-18088-5_43","volume-title":"Automata, Languages and Programming","author":"A. Finkel","year":"1987","unstructured":"Finkel, A.: A generalization of the procedure of Karp and Miller to well structured transition systems. In: Ottmann, T. (ed.) ICALP 1987. LNCS, vol.\u00a0267, pp. 499\u2013508. Springer, Heidelberg (1987)"},{"key":"10_CR9","doi-asserted-by":"publisher","first-page":"27","DOI":"10.1016\/S1571-0661(05)80426-8","volume":"9","author":"A. Finkel","year":"1997","unstructured":"Finkel, A., Willems, B., Wolper, P.: A direct symbolic approach to model checking pushdown systems. Electronic Notes Theoretical Computer Science\u00a09, 27\u201337 (1997)","journal-title":"Electronic Notes Theoretical Computer Science"},{"issue":"1-2","key":"10_CR10","doi-asserted-by":"publisher","first-page":"63","DOI":"10.1016\/S0304-3975(00)00102-X","volume":"256","author":"A. Finkel","year":"2001","unstructured":"Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theoretical Computer Science\u00a0256(1-2), 63\u201392 (2001)","journal-title":"Theoretical Computer Science"},{"key":"10_CR11","doi-asserted-by":"crossref","unstructured":"Finkel, A., Goubault-Larrecq, J.: Forward analysis for WSTS, Part I: Completions. In: STACS 2009, pp. 433\u2013444 (2009), \n                      http:\/\/www.stacs-conf.org","DOI":"10.1007\/978-3-642-02930-1_16"},{"key":"10_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"188","DOI":"10.1007\/978-3-642-02930-1_16","volume-title":"Automata, Languages and Programming","author":"A. Finkel","year":"2009","unstructured":"Finkel, A., Goubault-Larrecq, J.: Forward analysis for WSTS, Part II: Complete WSTS. In: Albers, S., Marchetti-Spaccamela, A., Matias, Y., Nikoletseas, S., Thomas, W. (eds.) ICALP 2009, Part II. LNCS, vol.\u00a05556, pp. 188\u2013199. Springer, Heidelberg (2009)"},{"key":"10_CR13","doi-asserted-by":"crossref","unstructured":"Jhala, R., Majumdar, R.: Interprocedural analysis of asynchronous programs. In: Principles of Programming Languages (POPL 2007), pp. 339\u2013350. ACM (2007)","DOI":"10.1145\/1190215.1190266"},{"key":"10_CR14","unstructured":"Lazi\u0107, R.: The reachability problem for vector addition systems with a stack is not elementary (2012), \n                      http:\/\/rp12.labri.fr\n                     (manuscript)"},{"key":"10_CR15","doi-asserted-by":"crossref","unstructured":"Leroux, J.: Vector addition system reachability problem. In: Principles of Programming Languages (POPL 2011), pp. 307\u2013316. ACM (2011)","DOI":"10.1145\/1925844.1926421"},{"issue":"3","key":"10_CR16","doi-asserted-by":"publisher","first-page":"441","DOI":"10.1137\/0213029","volume":"13","author":"E. Mayr","year":"1984","unstructured":"Mayr, E.: An algorithm for the general Petri net reachability problem. SIAM Journal Computing\u00a013(3), 441\u2013460 (1984)","journal-title":"SIAM Journal Computing"},{"key":"10_CR17","doi-asserted-by":"publisher","first-page":"264","DOI":"10.1006\/inco.1999.2826","volume":"156","author":"R. Mayr","year":"1999","unstructured":"Mayr, R.: Process rewrite systems. Information and Computation\u00a0156, 264\u2013286 (1999)","journal-title":"Information and Computation"},{"key":"10_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-540-31980-1_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Qadeer","year":"2005","unstructured":"Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol.\u00a03440, pp. 93\u2013107. Springer, Heidelberg (2005)"},{"issue":"2","key":"10_CR19","doi-asserted-by":"publisher","first-page":"416","DOI":"10.1145\/349214.349241","volume":"22","author":"G. Ramalingam","year":"2000","unstructured":"Ramalingam, G.: Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans. Programming Languages and Systems\u00a022(2), 416\u2013430 (2000)","journal-title":"ACM Trans. Programming Languages and Systems"},{"key":"10_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/11817963_29","volume-title":"Computer Aided Verification","author":"K. Sen","year":"2006","unstructured":"Sen, K., Viswanathan, M.: Model checking multithreaded programs with asynchronous atomic methods. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 300\u2013314. Springer, Heidelberg (2006)"},{"issue":"1","key":"10_CR21","first-page":"217","volume":"7","author":"K. Verma","year":"2005","unstructured":"Verma, K., Goubault-Larrecq, J.: Karp-Miller trees for a branching extension of VASS. Discrete Mathematics & Theoretical Computer Science\u00a07(1), 217\u2013230 (2005)","journal-title":"Discrete Mathematics & Theoretical Computer Science"},{"key":"10_CR22","doi-asserted-by":"publisher","first-page":"463","DOI":"10.1006\/jsco.1994.1059","volume":"18","author":"A. Weiermann","year":"1994","unstructured":"Weiermann, A.: Complexity bounds for some finite form of Kruskal\u2019s theorem. Journal of Symbolic Computation\u00a018, 463\u2013488 (1994)","journal-title":"Journal of Symbolic Computation"},{"key":"10_CR23","unstructured":"Xiaojuan, C., Ogawa, M.: Well-structured pushdown system, Part 1: Decidable classes for coverability. JAIST Research Report IS-RR-2013-001 (2013), \n                      http:\/\/hdl.handle.net\/10119\/11347"}],"container-title":["Lecture Notes in Computer Science","CONCUR 2013 \u2013 Concurrency Theory"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-40184-8_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,2,19]],"date-time":"2023-02-19T15:17:10Z","timestamp":1676819830000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-642-40184-8_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013]]},"ISBN":["9783642401831","9783642401848"],"references-count":23,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-40184-8_10","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2013]]}}}