{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,1]],"date-time":"2026-01-01T03:09:54Z","timestamp":1767236994001},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"11","license":[{"start":{"date-parts":[[2017,7,12]],"date-time":"2017-07-12T00:00:00Z","timestamp":1499817600000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Sci. China Inf. Sci."],"published-print":{"date-parts":[[2017,11]]},"DOI":"10.1007\/s11432-016-9026-x","type":"journal-article","created":{"date-parts":[[2017,7,12]],"date-time":"2017-07-12T11:46:33Z","timestamp":1499859993000},"update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["On the complexity of \u03c9-pushdown automata"],"prefix":"10.1007","volume":"60","author":[{"given":"Yusi","family":"Lei","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Fu","family":"Song","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Wanwei","family":"Liu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Min","family":"Zhang","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,7,12]]},"reference":[{"key":"9026_CR1","doi-asserted-by":"crossref","first-page":"425","DOI":"10.1007\/978-1-4613-8928-6_23","volume-title":"The Collected Works of J. Richard B\u00fcchi","author":"J R B\u00fcchi","year":"1990","unstructured":"B\u00fcchi J R. On a decision method in restricted second order arithmetic. In: The Collected Works of J. Richard B\u00fcchi. New York: Springer-Verlag, 1990. 425\u2013435"},{"key":"9026_CR2","first-page":"3","volume-title":"Proceedings of the 4th Annual Symposium on Switching Circuit Theory and Logical Design","author":"D E Muller","year":"1963","unstructured":"Muller D E. Infinite sequences and finite machines. In: Proceedings of the 4th Annual Symposium on Switching Circuit Theory and Logical Design. New York: IEEE, 1963. 3\u201316"},{"key":"9026_CR3","doi-asserted-by":"crossref","first-page":"521","DOI":"10.1016\/S0019-9958(66)80013-X","volume":"9","author":"R McNaughton","year":"1966","unstructured":"McNaughton R. Testing and generating infinite sequences by a finite automaton. Inf Contr, 1966, 9: 521\u2013530","journal-title":"Inf Contr"},{"key":"9026_CR4","first-page":"1","volume":"141","author":"M O Rabin","year":"1969","unstructured":"Rabin M O. Decidability of second-order theories and automata on infinite trees. Trans Amer Math Soc, 1969, 141: 1\u201335","journal-title":"Trans Amer Math Soc"},{"key":"9026_CR5","doi-asserted-by":"crossref","first-page":"121","DOI":"10.1016\/S0019-9958(82)91258-X","volume":"54","author":"R S Streett","year":"1982","unstructured":"Streett R S. Propositional dynamic logic of looping and converse is elementary decidable. Inf Contr, 1982, 54: 121\u2013141","journal-title":"Inf Contr"},{"key":"9026_CR6","first-page":"157","volume-title":"Proceedings of the 5th Symposium on Computation Theory","author":"A W Mostowski","year":"1984","unstructured":"Mostowski A W. Regular expressions for infinite trees and a standard form of automata. In: Proceedings of the 5th Symposium on Computation Theory. Berlin: Springer-Verlag, 1984. 157\u2013168"},{"key":"9026_CR7","first-page":"84","volume-title":"Proceedings of the 12th ACM Symposium on Principles of Programming Languages","author":"E A Emerson","year":"1985","unstructured":"Emerson E A, Lei C. Modalities for model checking: branching time strikes back. In: Proceedings of the 12th ACM Symposium on Principles of Programming Languages. New York: ACM, 1985. 84\u201396"},{"key":"9026_CR8","first-page":"133","volume-title":"Handbook of Theoretical Computer Science, Volume B","author":"W Thomas","year":"1990","unstructured":"Thomas W. Automata on infinite objects. In: Handbook of Theoretical Computer Science, Volume B. Cambridge: MIT Press, 1990. 133\u2013192"},{"key":"9026_CR9","doi-asserted-by":"crossref","first-page":"79","DOI":"10.1016\/0168-0072(91)90066-U","volume":"51","author":"M Y Vardi","year":"1991","unstructured":"Vardi M Y. Verification of concurrent programs: the automata-theoretic framework. Ann Pure Appl Logic, 1991, 51: 79\u201398","journal-title":"Ann Pure Appl Logic"},{"key":"9026_CR10","doi-asserted-by":"crossref","first-page":"183","DOI":"10.1016\/0022-0000(86)90026-7","volume":"32","author":"M Y Vardi","year":"1986","unstructured":"Vardi M Y, Wolper P. Automata-theoretic techniques for modal logics of programs. J Comput Syst Sci, 1986, 32: 183\u2013221","journal-title":"J Comput Syst Sci"},{"key":"9026_CR11","first-page":"46","volume-title":"Proceedings of the 18th Annual Symposium on Foundations of Computer Science","author":"A Pnueli","year":"1977","unstructured":"Pnueli A. The temporal logic of programs. In: Proceedings of the 18th Annual Symposium on Foundations of Computer Science. New York: IEEE, 1977. 46\u201357"},{"key":"9026_CR12","volume-title":"Dissertation for Ph.D. Degree","author":"C L\u00f6ding","year":"1998","unstructured":"L\u00f6ding C. Methods for the transformation of \u03c9-automata: complexity and connection to second order logic. Dissertation for Ph.D. Degree. Kiel: Christian-Albrechts-University of Kiel, 1998"},{"key":"9026_CR13","doi-asserted-by":"crossref","first-page":"97","DOI":"10.1007\/3-540-46691-6_8","volume-title":"Proceedings of the 19th Conference on Foundations of Software Technology and Theoretical Computer Science","author":"C L\u00f6ding","year":"1999","unstructured":"L\u00f6ding C. Optimal bounds for transformations of omega-automata. In: Proceedings of the 19th Conference on Foundations of Software Technology and Theoretical Computer Science. Berlin: Springer-Verlag, 1999. 97\u2013109"},{"key":"9026_CR14","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-3(3:5)2007","volume":"3","author":"N Piterman","year":"2007","unstructured":"Piterman N. From nondeterministic B\u00fcchi and Streett automata to deterministic parity automata. Log Meth Comput Sci, 2007, 3: 1\u201321","journal-title":"Log Meth Comput Sci"},{"key":"9026_CR15","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1007\/s10703-006-4341-z","volume":"28","author":"R Bloem","year":"2006","unstructured":"Bloem R, Gabow H N, Somenzi F. An algorithm for strongly connected component analysis in n log n symbolic steps. Form Meth Syst Des, 2006, 28: 37\u201356","journal-title":"Form Meth Syst Des"},{"key":"9026_CR16","first-page":"16","volume-title":"Proceedings of the 5th Scandinavian Workshop on Algorithm Theory","author":"M R Henzinger","year":"1996","unstructured":"Henzinger M R, Telle J A. Faster algorithms for the nonemptiness of Streett automata and for communication protocol pruning. In: Proceedings of the 5th Scandinavian Workshop on Algorithm Theory. Berlin: Springer-Verlag, 1996. 16\u201327"},{"key":"9026_CR17","doi-asserted-by":"crossref","first-page":"276","DOI":"10.1007\/3-540-45315-6_18","volume-title":"Proceedings of the 17th International Conference on Foundations of Software Science and Computation Structures","author":"V King","year":"2001","unstructured":"King V, Kupferman O, Vardi M Y. On the complexity of parity word automata. In: Proceedings of the 17th International Conference on Foundations of Software Science and Computation Structures. Berlin: Springer-Verlag, 2001. 276\u2013286"},{"key":"9026_CR18","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1016\/S0022-0000(77)80004-4","volume":"15","author":"R S Cohen","year":"1977","unstructured":"Cohen R S, Gold A Y. Theory of omega-languages I: characterizations of omega-context-free languages. J Comput Syst Sci, 1977, 15: 169\u2013184","journal-title":"J Comput Syst Sci"},{"key":"9026_CR19","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1016\/S0022-0000(77)80005-6","volume":"15","author":"R S Cohen","year":"1977","unstructured":"Cohen R S, Gold A Y. Theory of omega-languages II: a study of various models of omega-type generation and recognition. J Comput Syst Sci, 1977, 15: 185\u2013208","journal-title":"J Comput Syst Sci"},{"key":"9026_CR20","doi-asserted-by":"crossref","first-page":"275","DOI":"10.1016\/0022-0000(78)90019-3","volume":"16","author":"R S Cohen","year":"1978","unstructured":"Cohen R S, Gold A Y. Omega-computations on deterministic pushdown machines. J Comput Syst Sci, 1978, 16: 275\u2013300","journal-title":"J Comput Syst Sci"},{"key":"9026_CR21","doi-asserted-by":"crossref","first-page":"272","DOI":"10.1016\/S0019-9958(76)90415-0","volume":"31","author":"M Linna","year":"1976","unstructured":"Linna M. On omega-sets associated with context-free languages. Inf Contr, 1976, 31: 272\u2013293","journal-title":"Inf Contr"},{"key":"9026_CR22","doi-asserted-by":"crossref","first-page":"83","DOI":"10.1016\/0304-3975(77)90058-5","volume":"4","author":"M Linna","year":"1977","unstructured":"Linna M. A decidability result for deterministic \u03c9-context-free languages. Theor Comput Sci, 1977, 4: 83\u201398","journal-title":"Theor Comput Sci"},{"key":"9026_CR23","first-page":"135","volume-title":"Proceedings of the 8th International Conference on Concurrency Theory","author":"A Bouajjani","year":"1997","unstructured":"Bouajjani A, Esparza J, Maler O. Reachability analysis of pushdown automata: application to model checking. In: Proceedings of the 8th International Conference on Concurrency Theory. Berlin: Springer-Verlag, 1997. 135\u2013150"},{"key":"9026_CR24","doi-asserted-by":"crossref","first-page":"232","DOI":"10.1007\/10722167_20","volume-title":"Proceedings of the 12th International Conference Computer Aided Verification","author":"J Esparza","year":"2000","unstructured":"Esparza J, Hansel D, Rossmanith P, et al. Efficient algorithm for model checking pushdown systems. In: Proceedings of the 12th International Conference Computer Aided Verification. Berlin: Springer-Verlag, 2000. 232\u2013247"},{"key":"9026_CR25","doi-asserted-by":"crossref","first-page":"324","DOI":"10.1007\/3-540-44585-4_30","volume-title":"Proceedings of the 13th International Conference Computer Aided Verification","author":"J Esparza","year":"2001","unstructured":"Esparza J, Schwoon S. A BDD-based model checker for recursive programs. In: Proceedings of the 13th International Conference Computer Aided Verification. Berlin: Springer-Verlag, 2001. 324\u2013336"},{"key":"9026_CR26","doi-asserted-by":"crossref","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. Electr Notes Theor Comput Sci, 1997, 9: 27\u201337","journal-title":"Electr Notes Theor Comput Sci"},{"key":"9026_CR27","first-page":"62","volume":"164","author":"I Walukiewicz","year":"1996","unstructured":"Walukiewicz I. Pushdown processes: games and model checking. Inf Comput, 1996, 164: 62\u201374","journal-title":"Inf Comput"},{"key":"9026_CR28","first-page":"384","volume-title":"Proceedings of the 20th International Conference on Concurrency Theory","author":"M Hague","year":"2009","unstructured":"Hague M, Ong C L. Winning regions of pushdown parity games: a saturation method. In: Proceedings of the 20th International Conference on Concurrency Theory. Berlin: Springer-Verlag, 2009. 384\u2013398"},{"key":"9026_CR29","doi-asserted-by":"crossref","first-page":"799","DOI":"10.1016\/j.ic.2010.12.004","volume":"209","author":"M Hague","year":"2011","unstructured":"Hague M, Ong C L. A saturation method for the modal \u00b5-calculus over pushdown systems. Inf Comput, 2011, 209: 799\u2013821","journal-title":"Inf Comput"},{"key":"9026_CR30","doi-asserted-by":"crossref","first-page":"262","DOI":"10.1007\/3-540-36078-6_18","volume-title":"Proceedings of the 9th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning","author":"O Kupferman","year":"2002","unstructured":"Kupferman O, Piterman N, Vardi M Y. Pushdown specifications. In: Proceedings of the 9th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning. Berlin: Springer-Verlag, 2002. 262\u2013277"},{"key":"9026_CR31","first-page":"434","volume-title":"Proceedings of the 8th International Conference on Concurrency Theory","author":"F Song","year":"2011","unstructured":"Song F, Touili T. Efficient CTL model-checking for pushdown systems. In: Proceedings of the 8th International Conference on Concurrency Theory. Berlin: Springer-Verlag, 2011. 434\u2013449"},{"key":"9026_CR32","doi-asserted-by":"crossref","first-page":"127","DOI":"10.1016\/j.tcs.2014.07.001","volume":"549","author":"F Song","year":"2014","unstructured":"Song F, Touili T. Efficient CTL model-checking for pushdown systems. Theor Comput Sci, 2014, 549: 127\u2013145","journal-title":"Theor Comput Sci"},{"key":"9026_CR33","doi-asserted-by":"crossref","first-page":"346","DOI":"10.1145\/2351676.2351743","volume-title":"Proceedings of the 27th IEEE\/ACM International Conference on Automated Software Engineering","author":"F Song","year":"2012","unstructured":"Song F, Touili T. PoMuC: a CTL model-checker for sequential programs. In: Proceedings of the 27th IEEE\/ACM International Conference on Automated Software Engineering. New York: ACM, 2012. 346\u2013349"},{"key":"9026_CR34","doi-asserted-by":"crossref","first-page":"701","DOI":"10.1016\/S0950-5849(98)00093-7","volume":"40","author":"T W Reps","year":"1998","unstructured":"Reps T W. Program analysis via graph reachability. Inf Softw Tech, 1998, 40: 701\u2013726","journal-title":"Inf Softw Tech"},{"key":"9026_CR35","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier C, Katoen J. Principles of Model Checking. London: MIT Press, 2008"},{"key":"9026_CR36","doi-asserted-by":"crossref","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, 2003, 186: 355\u2013376","journal-title":"Inf Comput"},{"key":"9026_CR37","doi-asserted-by":"crossref","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, 2007, 379: 286\u2013297","journal-title":"Theor Comput Sci"},{"key":"9026_CR38","doi-asserted-by":"crossref","first-page":"704","DOI":"10.1007\/3-540-45465-9_60","volume-title":"Proceedings of the 29th International Colloquium on Automata, Languages and Programming","author":"T Cachat","year":"2002","unstructured":"Cachat T. Symbolic strategy synthesis for games on pushdown graphs. In: Proceedings of the 29th International Colloquium on Automata, Languages and Programming. Berlin: Springer-Verlag, 2002. 704\u2013715"},{"key":"9026_CR39","doi-asserted-by":"crossref","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, 2003, 85: 285\u2013291","journal-title":"Inf Process Lett"}],"container-title":["Science China Information Sciences"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11432-016-9026-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s11432-016-9026-x\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s11432-016-9026-x.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,30]],"date-time":"2022-07-30T20:52:58Z","timestamp":1659214378000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s11432-016-9026-x"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,7,12]]},"references-count":39,"journal-issue":{"issue":"11","published-print":{"date-parts":[[2017,11]]}},"alternative-id":["9026"],"URL":"https:\/\/doi.org\/10.1007\/s11432-016-9026-x","relation":{},"ISSN":["1674-733X","1869-1919"],"issn-type":[{"value":"1674-733X","type":"print"},{"value":"1869-1919","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,7,12]]},"article-number":"112102"}}