{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T06:15:47Z","timestamp":1725603347949},"publisher-location":"Berlin, Heidelberg","reference-count":25,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642232169"},{"type":"electronic","value":"9783642232176"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-23217-6_29","type":"book-chapter","created":{"date-parts":[[2011,8,25]],"date-time":"2011-08-25T13:14:02Z","timestamp":1314278042000},"page":"434-449","source":"Crossref","is-referenced-by-count":11,"title":["Efficient CTL Model-Checking for Pushdown Systems"],"prefix":"10.1007","author":[{"given":"Fu","family":"Song","sequence":"first","affiliation":[]},{"given":"Tayssir","family":"Touili","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"29_CR1","doi-asserted-by":"crossref","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)","DOI":"10.1007\/3-540-63141-0_10"},{"issue":"1-2","key":"29_CR2","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1016\/j.tcs.2007.03.049","volume":"379","author":"L. Bozzelli","year":"2007","unstructured":"Bozzelli, L.: Complexity results on branching-time pushdown model checking. Theor. Comput. Sci.\u00a0379(1-2), 286\u2013297 (2007)","journal-title":"Theor. Comput. Sci."},{"key":"29_CR3","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"504","DOI":"10.1007\/11591191_35","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"L. Bozzelli","year":"2005","unstructured":"Bozzelli, L., Murano, A., Peron, A.: Pushdown module checking. In: Sutcliffe, G., Voronkov, A. (eds.) LPAR 2005. LNCS (LNAI), vol.\u00a03835, pp. 504\u2013518. Springer, Heidelberg (2005)"},{"issue":"1","key":"29_CR4","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/s10703-010-0093-x","volume":"36","author":"L. Bozzelli","year":"2010","unstructured":"Bozzelli, L., Murano, A., Peron, A.: Pushdown module checking. Formal Methods in System Design\u00a036(1), 65\u201395 (2010)","journal-title":"Formal Methods in System Design"},{"issue":"2","key":"29_CR5","first-page":"89","volume":"2","author":"O. Burkart","year":"1995","unstructured":"Burkart, O., Steffen, B.: Composition, decomposition and model checking of pushdown processes. Nord. J. Comput.\u00a02(2), 89\u2013125 (1995)","journal-title":"Nord. J. Comput."},{"key":"29_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"419","DOI":"10.1007\/3-540-63165-8_198","volume-title":"Automata, Languages and Programming","author":"O. Burkart","year":"1997","unstructured":"Burkart, O., Steffen, B.: Model checking the full modal mu-calculus for infinite sequential processes. In: Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.) ICALP 1997. LNCS, vol.\u00a01256, pp. 419\u2013429. Springer, Heidelberg (1997)"},{"key":"29_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"704","DOI":"10.1007\/3-540-45465-9_60","volume-title":"Automata, Languages and Programming","author":"T. Cachat","year":"2002","unstructured":"Cachat, T.: Symbolic strategy synthesis for games on pushdown graphs. In: Widmayer, P., Triguero, F., Morales, R., Hennessy, M., Eidenbenz, S., Conejo, R. (eds.) ICALP 2002. LNCS, vol.\u00a02380, pp. 704\u2013715. Springer, Heidelberg (2002)"},{"key":"29_CR8","doi-asserted-by":"crossref","unstructured":"Cachat, T.: Uniform solution of parity games on prefix-recognizable graphs. Electr. Notes Theor. Comput. Sci.\u00a068(6) (2002)","DOI":"10.1016\/S1571-0661(04)80534-6"},{"key":"29_CR9","doi-asserted-by":"crossref","unstructured":"Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithm for model checking pushdown systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, 232\u2013247. Springer, Heidelberg (2000)","DOI":"10.1007\/10722167_20"},{"key":"29_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1007\/3-540-49019-1_2","volume-title":"Foundations of Software Science and Computation Structures","author":"J. Esparza","year":"1999","unstructured":"Esparza, J., Knoop, J.: An automata-theoretic approach to interprocedural data-flow analysis. In: Thomas, W. (ed.) FOSSACS 1999. LNCS, vol.\u00a01578, pp. 14\u201330. Springer, Heidelberg (1999)"},{"key":"29_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1007\/3-540-45500-0_16","volume-title":"Theoretical Aspects of Computer Software","author":"J. Esparza","year":"2001","unstructured":"Esparza, J., Ku\u010dera, A., Schwoon, S.: Model-checking LTL with regular valuations for pushdown systems. In: Kobayashi, N., Babu, C. S. (eds.) TACS 2001. LNCS, vol.\u00a02215, pp. 316\u2013339. Springer, Heidelberg (2001)"},{"issue":"2","key":"29_CR12","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1016\/S0890-5401(03)00139-1","volume":"186","author":"J. Esparza","year":"2003","unstructured":"Esparza, J., Kucera, A., Schwoon, S.: Model checking ltl with regular valuations for pushdown systems. Inf. Comput.\u00a0186(2), 355\u2013376 (2003)","journal-title":"Inf. Comput."},{"key":"29_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"324","DOI":"10.1007\/3-540-44585-4_30","volume-title":"Computer Aided Verification","author":"J. Esparza","year":"2001","unstructured":"Esparza, J., Schwoon, S.: A BDD-based model checker for recursive programs. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, p. 324. Springer, Heidelberg (2001)"},{"key":"29_CR14","series-title":"ENTCS","volume-title":"Infinity 1997","author":"A. Finkel","year":"1997","unstructured":"Finkel, A., Willems, B., Wolper, P.: A Direct Symbolic Approach to Model Checking Pushdown Systems. In: Infinity 1997. ENTCS, vol.\u00a09. Elsevier Sci. Pub., Amsterdam (1997)"},{"issue":"2","key":"29_CR15","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1006\/inco.1994.1073","volume":"113","author":"D. Harel","year":"1994","unstructured":"Harel, D., Raz, D.: Deciding emptiness for stack automata on infinite trees. Inf. Comput.\u00a0113(2), 278\u2013299 (1994)","journal-title":"Inf. Comput."},{"key":"29_CR16","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"262","DOI":"10.1007\/3-540-36078-6_18","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"O. Kupferman","year":"2002","unstructured":"Kupferman, O., Piterman, N., Vardi, M.Y.: Pushdown specifications. In: Baaz, M., Voronkov, A. (eds.) LPAR 2002. LNCS (LNAI), vol.\u00a02514, pp. 262\u2013277. Springer, Heidelberg (2002)"},{"key":"29_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"202","DOI":"10.1007\/978-3-642-13754-9_11","volume-title":"Time for Verification","author":"O. Kupferman","year":"2010","unstructured":"Kupferman, O., Piterman, N., Vardi, M.Y.: An automata-theoretic approach to infinite-state systems. In: Manna, Z., Peled, D.A. (eds.) Time for Verification. LNCS, vol.\u00a06200, pp. 202\u2013259. Springer, Heidelberg (2010)"},{"key":"29_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"36","DOI":"10.1007\/10722167_7","volume-title":"Computer Aided Verification","author":"O. Kupferman","year":"2000","unstructured":"Kupferman, O., Vardi, M.Y.: An automata-theoretic approach to reasoning about infinite-state systems. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol.\u00a01855, pp. 36\u201352. Springer, Heidelberg (2000)"},{"key":"29_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"387","DOI":"10.1007\/978-3-540-27813-9_30","volume-title":"Computer Aided Verification","author":"N. Piterman","year":"2004","unstructured":"Piterman, N., Vardi, M.Y.: Global model-checking of infinite-state systems. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol.\u00a03114, pp. 387\u2013400. Springer, Heidelberg (2004)"},{"key":"29_CR20","doi-asserted-by":"crossref","unstructured":"Qadeer, S., Wu, D.: Kiss: Keep it simple and sequential. In: PLDI 2004: Programming Language Design and Implementation, pp. 14\u201324 (2004)","DOI":"10.1145\/996841.996845"},{"key":"29_CR21","unstructured":"Schwoon, S.: Model-Checking Pushdown Systems. PhD thesis, Technische Universit\u00e4t M\u00fcnchen (2002)"},{"issue":"6","key":"29_CR22","doi-asserted-by":"publisher","first-page":"285","DOI":"10.1016\/S0020-0190(02)00445-3","volume":"85","author":"O. Serre","year":"2003","unstructured":"Serre, O.: Note on winning positions on pushdown games with [omega]-regular conditions. Inf. Process. Lett.\u00a085(6), 285\u2013291 (2003)","journal-title":"Inf. Process. Lett."},{"key":"29_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/11901914_13","volume-title":"Automated Technology for Verification and Analysis","author":"D. Suwimonteerabuth","year":"2006","unstructured":"Suwimonteerabuth, D., Schwoon, S., Esparza, J.: Efficient algorithms for alternating pushdown systems with an application to the computation of certificate chains. In: Graf, S., Zhang, W. (eds.) ATVA 2006. LNCS, vol.\u00a04218, pp. 141\u2013153. Springer, Heidelberg (2006)"},{"key":"29_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/3-540-61474-5_58","volume-title":"Computer Aided Verification","author":"I. Walukiewicz","year":"1996","unstructured":"Walukiewicz, I.: Pushdown processes: Games and model checking. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 62\u201374. Springer, Heidelberg (1996)"},{"key":"29_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"127","DOI":"10.1007\/3-540-44450-5_10","volume-title":"FST TCS 2000: Foundations of Software Technology and Theoretical Science","author":"I. Walukiewicz","year":"2000","unstructured":"Walukiewicz, I.: Model checking CTL properties of pushdown systems. In: Kapoor, S., Prasad, S. (eds.) FST TCS 2000. LNCS, vol.\u00a01974, pp. 127\u2013138. Springer, Heidelberg (2000)"}],"container-title":["Lecture Notes in Computer Science","CONCUR 2011 \u2013 Concurrency Theory"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-23217-6_29","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,14]],"date-time":"2019-06-14T11:45:01Z","timestamp":1560512701000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-23217-6_29"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642232169","9783642232176"],"references-count":25,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-23217-6_29","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}