{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:31:52Z","timestamp":1759638712339},"publisher-location":"Berlin, Heidelberg","reference-count":9,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783540414131"},{"type":"electronic","value":"9783540444503"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2000]]},"DOI":"10.1007\/3-540-44450-5_10","type":"book-chapter","created":{"date-parts":[[2007,8,16]],"date-time":"2007-08-16T08:26:08Z","timestamp":1187252768000},"page":"127-138","source":"Crossref","is-referenced-by-count":36,"title":["Model Checking CTL Properties of Pushdown Systems"],"prefix":"10.1007","author":[{"given":"Igor","family":"Walukiewicz","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2000,11,24]]},"reference":[{"key":"10_CR1","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"135","DOI":"10.1007\/3-540-63141-0_10","volume-title":"CONCUR\u201997","author":"A. Bouajjani","year":"1997","unstructured":"A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Applications to model checking. In CONCUR\u201997, volume 1243 of LNCS, pages 135\u2013150, 1997."},{"key":"10_CR2","series-title":"Lect Notes Comput Sci","volume-title":"ICALP\u201996","author":"D. Caucal","year":"1996","unstructured":"D. Caucal. On infinite transition graphs a having decidable monadic theory. In ICALP\u201996, LNCS, 1996."},{"issue":"1","key":"10_CR3","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1145\/322234.322243","volume":"28","author":"A. K. Chandra","year":"1981","unstructured":"A. K. Chandra, D. C.& Kozen, and L. J. Stockmeyer. Alternation. Journal of the ACM, 28(1):114\u2013133, 1981.","journal-title":"Journal of the ACM"},{"key":"10_CR4","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"52","DOI":"10.1007\/BFb0025774","volume-title":"Design and synthesis of synchronization skeletons using branching time temporal logic","author":"E. Clarke","year":"1982","unstructured":"E. Clarke and E. Emerson. Design and synthesis of synchronization skeletons using branching time temporal logic. In Workshop on Logics of Programs, volume 131 of LNCS, pages 52\u201371. Springer-Verlag, 1981."},{"key":"10_CR5","doi-asserted-by":"crossref","unstructured":"E. A. Emerson. Temporal and modal logic. In J. Leeuven, editor, Handbook of Theoretical Computer Science Vol.B, pages 995\u20131072. Elsevier, 1990.","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"10_CR6","unstructured":"J. Esparza. Private communication."},{"key":"10_CR7","series-title":"Lect Notes Comput Sci","volume-title":"CAV\u2019 00","author":"J. Esparza","year":"2000","unstructured":"J. Esparza, D. Hansel, and P. Rossmanith. efficient algorithms for model checking pushdown systems. In CAV\u2019 00, LNCS, 2000. to appear."},{"key":"10_CR8","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/0304-3975(85)90087-8","volume":"37","author":"D. Muller","year":"1985","unstructured":"D. Muller and P. Schupp. The theory of ends,tipushdown automata and second-order logic. Theoretical Computer Science, 37:51\u201375, 1985.","journal-title":"Theoretical Computer Science"},{"key":"10_CR9","series-title":"Lect Notes Comput Sci","doi-asserted-by":"crossref","first-page":"62","DOI":"10.1007\/3-540-61474-5_58","volume-title":"Pushdown processes: Games and model checking","author":"I. Walukiewicz","year":"1996","unstructured":"I. Walukiewicz. Pushdown processes: Games and model checking. InCAV\u201996, volume 1102 of LNCS, pages 62\u201374, 1996. To appear in Information and Computation."}],"container-title":["Lecture Notes in Computer Science","FST TCS 2000: Foundations of Software Technology and Theoretical Computer Science"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-44450-5_10","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,2]],"date-time":"2019-05-02T04:17:19Z","timestamp":1556770639000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-44450-5_10"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000]]},"ISBN":["9783540414131","9783540444503"],"references-count":9,"URL":"https:\/\/doi.org\/10.1007\/3-540-44450-5_10","relation":{},"ISSN":["0302-9743"],"issn-type":[{"type":"print","value":"0302-9743"}],"subject":[],"published":{"date-parts":[[2000]]}}}