{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,31]],"date-time":"2026-03-31T23:41:43Z","timestamp":1775000503960,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":101,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783642137532","type":"print"},{"value":"9783642137549","type":"electronic"}],"license":[{"start":{"date-parts":[[2010,1,1]],"date-time":"2010-01-01T00:00:00Z","timestamp":1262304000000},"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":[[2010]]},"DOI":"10.1007\/978-3-642-13754-9_11","type":"book-chapter","created":{"date-parts":[[2010,6,30]],"date-time":"2010-06-30T11:05:52Z","timestamp":1277895952000},"page":"202-259","source":"Crossref","is-referenced-by-count":12,"title":["An Automata-Theoretic Approach to Infinite-State Systems"],"prefix":"10.1007","author":[{"given":"Orna","family":"Kupferman","sequence":"first","affiliation":[]},{"given":"Nir","family":"Piterman","sequence":"additional","affiliation":[]},{"given":"Moshe Y.","family":"Vardi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"11_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/11817963_31","volume-title":"Computer Aided Verification","author":"R. Alur","year":"2006","unstructured":"Alur, R., Chaudhuri, S., Madhusudan, P.: Languages of nested trees. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 329\u2013342. Springer, Heidelberg (2006)"},{"key":"11_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"67","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.\u00a02988, pp. 67\u201379. Springer, Heidelberg (2004)"},{"key":"11_CR3","doi-asserted-by":"crossref","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. In: Proc. 38th IEEE Symp. on Foundations of Computer Science, pp. 100\u2013109 (1997)","DOI":"10.1109\/SFCS.1997.646098"},{"key":"11_CR4","doi-asserted-by":"crossref","unstructured":"Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Proc. 36th ACM Symp. on Theory of Computing. ACM press, New York (2004)","DOI":"10.1145\/1007352.1007390"},{"key":"11_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/11779148_1","volume-title":"Developments in Language Theory","author":"R. Alur","year":"2006","unstructured":"Alur, R., Madhusudan, P.: Adding nesting structure to words. In: Ibarra, O.H., Dang, Z. (eds.) DLT 2006. LNCS, vol.\u00a04036, pp. 1\u201313. Springer, Heidelberg (2006)"},{"key":"11_CR6","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 game graphs. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol.\u00a02725, pp. 67\u201379. Springer, Heidelberg (2003)"},{"key":"11_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-540-27836-8_23","volume-title":"Automata, Languages and Programming","author":"M. Bojanczyk","year":"2004","unstructured":"Bojanczyk, M., Colcombet, T.: Tree-walking automata cannot be determinized. In: D\u00edaz, J., Karhum\u00e4ki, J., Lepist\u00f6, A., Sannella, D. (eds.) ICALP 2004. LNCS, vol.\u00a03142, pp. 246\u2013256. Springer, Heidelberg (2004)"},{"key":"11_CR8","volume-title":"Proc. 37th ACM Symp. on Theory of Computing","author":"M. Bojanczyk","year":"2005","unstructured":"Bojanczyk, M., Colcombet, T.: Tree-walking automata do not recognize all regular languages. In: Proc. 37th ACM Symp. on Theory of Computing. ACM press, New York (2005)"},{"key":"11_CR9","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":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"454","DOI":"10.1007\/3-540-44585-4_44","volume-title":"Computer Aided Verification","author":"P. Biesse","year":"2001","unstructured":"Biesse, P., Leonard, T., Mokkedem, A.: Finding bugs in an alpha microprocessor using satisfiability solvers. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 454\u2013464. Springer, Heidelberg (2001)"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"420","DOI":"10.1007\/11672142_34","volume-title":"STACS 2006","author":"V. B\u00e1r\u00e1ny","year":"2006","unstructured":"B\u00e1r\u00e1ny, V., L\u00f6ding, C., Serre, O.: Regularity problem for visibly pushdown languages. In: Durand, B., Thomas, W. (eds.) STACS 2006. LNCS, vol.\u00a03884, pp. 420\u2013431. Springer, Heidelberg (2006)"},{"key":"11_CR12","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)"},{"key":"11_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"65","DOI":"10.1007\/11609773_5","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"L. Bozzelli","year":"2005","unstructured":"Bozzelli, L.: Complexity results on branching-time pushdown model checking. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 65\u201379. Springer, Heidelberg (2005)"},{"key":"11_CR14","series-title":"ENTCS","first-page":"15","volume-title":"Proc. 1st Int. workshop on verification of infinite states systems","author":"O. Burkart","year":"1996","unstructured":"Burkart, O., Quemener, Y.-M.: Model checking of infinite graphs defined by graph grammars. In: Proc. 1st Int. workshop on verification of infinite states systems. ENTCS, p. 15. Elsevier, Amsterdam (1996)"},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1007\/10722468_7","volume-title":"SPIN Model Checking and Software Verification","author":"T. Ball","year":"2000","unstructured":"Ball, T., Rajamani, S.: Bebop: A symbolic model checker for boolean programs. In: Havelund, K., Penix, J., Visser, W. (eds.) SPIN 2000. LNCS, vol.\u00a01885, pp. 113\u2013130. Springer, Heidelberg (2000)"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"260","DOI":"10.1007\/3-540-44585-4_25","volume-title":"Computer Aided Verification","author":"T. Ball","year":"2001","unstructured":"Ball, T., Rajamani, S.: The SLAM toolkit. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 260\u2013264. Springer, Heidelberg (2001)"},{"key":"11_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"123","DOI":"10.1007\/BFb0084787","volume-title":"CONCUR \u201992","author":"O. Burkart","year":"1992","unstructured":"Burkart, O., Steffen, B.: Model checking for context-free processes. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol.\u00a0630, pp. 123\u2013137. Springer, Heidelberg (1992)"},{"key":"11_CR18","first-page":"89","volume":"2","author":"O. Burkart","year":"1995","unstructured":"Burkart, O., Steffen, B.: Composition, decomposition and model checking of pushdown processes. Nordic J. Comut.\u00a02, 89\u2013125 (1995)","journal-title":"Nordic J. Comut."},{"key":"11_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/978-3-540-24597-1_8","volume-title":"FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science","author":"A.-J. Bouquet","year":"2003","unstructured":"Bouquet, A.-J., Serre, O., Walukiewicz, I.: Pushdown games with unboundedness and regular conditions. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol.\u00a02914, pp. 88\u201399. Springer, Heidelberg (2003)"},{"key":"11_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"412","DOI":"10.1007\/11609773_27","volume-title":"Verification, Model Checking, and Abstract Interpretation","author":"L. Bozzelli","year":"2005","unstructured":"Bozzelli, L., La Torre, S., Peron, A.: Verification of well-formed communicating recursive state machines. In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol.\u00a03855, pp. 412\u2013426. Springer, Heidelberg (2005)"},{"key":"11_CR21","first-page":"1","volume-title":"Proc. Int. Congress on Logic, Method, and Philosophy of Science","author":"J.R. B\u00fcchi","year":"1960","unstructured":"B\u00fcchi, J.R.: On a decision method in restricted second order arithmetic. In: Proc. Int. Congress on Logic, Method, and Philosophy of Science, pp. 1\u201312. Stanford University Press, Stanford (1960)"},{"key":"11_CR22","doi-asserted-by":"crossref","unstructured":"Burkart, O.: Model checking rationally restricted right closures of recognizable graphs. In: Moller, F. (ed.) Proc. 2nd Int. workshop on verification of infinite states systems (1997)","DOI":"10.1016\/S1571-0661(05)80424-4"},{"key":"11_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"556","DOI":"10.1007\/3-540-45061-0_45","volume-title":"Automata, Languages and Programming","author":"T. Cachat","year":"2003","unstructured":"Cachat, T.: Higher order pushdown automata, the caucal hierarchy of graphs and parity games. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol.\u00a02719, pp. 556\u2013569. Springer, Heidelberg (2003)"},{"key":"11_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1007\/3-540-61440-0_128","volume-title":"Automata, Languages and Programming","author":"D. Caucal","year":"1996","unstructured":"Caucal, D.: On infinite transition graphs having a decidable monadic theory. In: Meyer auf der Heide, F., Monien, B. (eds.) ICALP 1996. LNCS, vol.\u00a01099, pp. 194\u2013205. Springer, Heidelberg (1996)"},{"issue":"1","key":"11_CR25","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/S0304-3975(01)00089-5","volume":"290","author":"D. Caucal","year":"2003","unstructured":"Caucal, D.: On infinite transition graphs having a decidable monadic theory. Theoretical Computer Science\u00a0290(1), 79\u2013115 (2003)","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"11_CR26","doi-asserted-by":"publisher","first-page":"244","DOI":"10.1145\/5397.5399","volume":"8","author":"E.M. Clarke","year":"1986","unstructured":"Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languagues and Systems\u00a08(2), 244\u2013263 (1986)","journal-title":"ACM Transactions on Programming Languagues and Systems"},{"key":"11_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"436","DOI":"10.1007\/3-540-44585-4_43","volume-title":"Computer Aided Verification","author":"F. Copty","year":"2001","unstructured":"Copty, F., Fix, L., Fraer, R., Giunchiglia, E., Kamhi, G., Tacchella, A., Vardi, M.Y.: Benefits of bounded model checking at an industrial setting. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol.\u00a02102, pp. 436\u2013453. Springer, Heidelberg (2001)"},{"key":"11_CR28","volume-title":"Model Checking","author":"E.M. Clarke","year":"1999","unstructured":"Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)"},{"issue":"1","key":"11_CR29","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1145\/322234.322243","volume":"28","author":"A.K. Chandra","year":"1981","unstructured":"Chandra, A.K., Kozen, D.C., Stockmeyer, L.J.: Alternation. Journal of the Association for Computing Machinery\u00a028(1), 114\u2013133 (1981)","journal-title":"Journal of the Association for Computing Machinery"},{"key":"11_CR30","doi-asserted-by":"crossref","first-page":"235","DOI":"10.1145\/586110.586142","volume-title":"Proc. 9th ACM conference on Computer and Communications Security","author":"H. Chen","year":"2002","unstructured":"Chen, H., Wagner, D.: Mops: an infrastructure for examining security properties of software. In: Proc. 9th ACM conference on Computer and Communications Security, pp. 235\u2013244. ACM, New York (2002)"},{"key":"11_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"112","DOI":"10.1007\/978-3-540-24597-1_10","volume-title":"FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science","author":"A. Carayol","year":"2003","unstructured":"Carayol, A., W\u00f6hrle, S.: The caucal hierarchy of infinite graphs in terms of logic and higher-order pushdown automata. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol.\u00a02914, pp. 112\u2013123. Springer, Heidelberg (2003)"},{"key":"11_CR32","first-page":"279","volume-title":"Proc. 16th IEEE Symp. on Logic in Computer Science","author":"L. Alfaro de","year":"2001","unstructured":"de Alfaro, L., Henzinger, T.A., Majumdar, R.: From verification to control: dynamic programs for omega-regular objectives. In: Proc. 16th IEEE Symp. on Logic in Computer Science, pp. 279\u2013290. IEEE Computer Society Press, Los Alamitos (2001)"},{"key":"11_CR33","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/0304-3975(94)90269-0","volume":"126","author":"M. Dam","year":"1994","unstructured":"Dam, M.: CTL\u2009\u22c6\u2009 and ECTL\u2009\u22c6\u2009 as fragments of the modal \u03bc-calculus. Theoretical Computer Science\u00a0126, 77\u201396 (1994)","journal-title":"Theoretical Computer Science"},{"key":"11_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/3-540-48523-6_25","volume-title":"Automata, Languages and Programming","author":"M. Dickhfer","year":"1999","unstructured":"Dickhfer, M., Wilke, T.: Timed alternating tree automata: the automata-theoretic solution to the TCTL model checking problem. In: Wiedermann, J., Van Emde Boas, P., Nielsen, M. (eds.) ICALP 1999. LNCS, vol.\u00a01644, pp. 281\u2013290. Springer, Heidelberg (1999)"},{"key":"11_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"16","DOI":"10.1007\/978-3-540-30538-5_2","volume-title":"FSTTCS 2004: Foundations of Software Technology and Theoretical Computer Science","author":"J. Esparza","year":"2004","unstructured":"Esparza, J., Etessami, K.: Verifying probabilistic procedural programs. In: Lodaya, K., Mahajan, M. (eds.) FSTTCS 2004. LNCS, vol.\u00a03328, pp. 16\u201331. Springer, Heidelberg (2004)"},{"key":"11_CR36","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":"11_CR37","first-page":"51","volume":"14","author":"J. Engelfriet","year":"1999","unstructured":"Engelfriet, J., Hoggeboom, H.J., van Best, J.-P.: Trips on trees. Acta Cybernetica\u00a014, 51\u201364 (1999)","journal-title":"Acta Cybernetica"},{"key":"11_CR38","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Jutla, C.: The complexity of tree automata and logics of programs. In: Proc. 29th IEEE Symp. on Foundations of Computer Science, pp. 328\u2013337 (1988)","DOI":"10.1109\/SFCS.1988.21949"},{"key":"11_CR39","doi-asserted-by":"crossref","unstructured":"Emerson, E.A., Jutla, C.: Tree automata, \u03bc-calculus and determinacy. In: Proc. 32nd IEEE Symp. on Foundations of Computer Science, pp. 368\u2013377 (1991)","DOI":"10.1109\/SFCS.1991.185392"},{"key":"11_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"385","DOI":"10.1007\/3-540-56922-7_32","volume-title":"Proc 5th Int. Conf. on Computer Aided Verification","author":"E.A. Emerson","year":"1993","unstructured":"Emerson, E.A., Jutla, C., Sistla, A.P.: On model-checking for fragments of \u03bc-calculus. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol.\u00a0697, pp. 385\u2013396. Springer, Heidelberg (1993)"},{"key":"11_CR41","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., Kucera, A., Schwoon, S.: Model-checking LTL with regular valuations for pushdown systems. In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS, vol.\u00a02215, pp. 316\u2013339. Springer, Heidelberg (2001)"},{"key":"11_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"489","DOI":"10.1007\/11691372_35","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"J. Esparza","year":"2006","unstructured":"Esparza, J., Kiefer, S., Schwoon, S.: Abstraction refinement with craig interpolation and symbolic pushdown systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, pp. 489\u2013503. Springer, Heidelberg (2006)"},{"key":"11_CR43","unstructured":"Emerson, E.A., Lei, C.-L.: Efficient model checking in fragments of the propositional \u03bc-calculus. In: Proc. 1st IEEE Symp. on Logic in Computer Science, pp. 267\u2013278 (1986)"},{"key":"11_CR44","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1007\/3-540-15648-8_7","volume-title":"Logics of Programs","author":"E.A. Emerson","year":"1985","unstructured":"Emerson, E.A.: Automata, tableaux, and temporal logics. In: Parikh, R. (ed.) Logic of Programs 1985. LNCS, vol.\u00a0193, pp. 79\u201387. Springer, Heidelberg (1985)"},{"key":"11_CR45","doi-asserted-by":"crossref","first-page":"185","DOI":"10.1090\/dimacs\/031\/06","volume-title":"Descriptive Complexity and Finite Models","author":"E.A. Emerson","year":"1997","unstructured":"Emerson, E.A.: Model checking and the \u03bc-calculus. In: Immerman, N., Kolaitis, P.G. (eds.) Descriptive Complexity and Finite Models, pp. 185\u2013214. American Mathematical Society, Providence (1997)"},{"key":"11_CR46","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, pp. 324\u2013336. Springer, Heidelberg (2001)"},{"key":"11_CR47","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"M.J. Fischer","year":"1979","unstructured":"Fischer, M.J., Ladner, R.E.: Propositional dynamic logic of regular programs. Journal of Computer and Systems Science\u00a018, 194\u2013211 (1979)","journal-title":"Journal of Computer and Systems Science"},{"key":"11_CR48","unstructured":"Gimbert, H.: Explosion and parity games over context-free graphs. Technical Report 2003-015, Liafa, CNRS, Paris University 7 (2003)"},{"key":"11_CR49","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"439","DOI":"10.1007\/978-3-540-45138-9_38","volume-title":"Mathematical Foundations of Computer Science 2003","author":"P. Gastin","year":"2003","unstructured":"Gastin, P., Oddoux, D.: Ltl with past and two-way very-weak alternating automata. In: Rovan, B., Vojt\u00e1\u0161, P. (eds.) MFCS 2003. LNCS, vol.\u00a02747, pp. 439\u2013448. Springer, Heidelberg (2003)"},{"key":"11_CR50","first-page":"3","volume-title":"Protocol Specification, Testing, and Verification","author":"R. Gerth","year":"1995","unstructured":"Gerth, R., Peled, D., Vardi, M.Y., Wolper, P.: Simple on-the-fly automatic verification of linear temporal logic. In: Dembiski, P., Sredniawa, M. (eds.) Protocol Specification, Testing, and Verification, pp. 3\u201318. Chapman & Hall, Boca Raton (1995)"},{"issue":"2","key":"11_CR51","doi-asserted-by":"publisher","first-page":"305","DOI":"10.1006\/inco.1994.1035","volume":"110","author":"P. Godefroid","year":"1994","unstructured":"Godefroid, P., Wolper, P.: A partial approach to model checking. Information and Computation\u00a0110(2), 305\u2013326 (1994)","journal-title":"Information and Computation"},{"key":"11_CR52","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/3-540-61474-5_94","volume-title":"Computer Aided Verification","author":"R.H. Hardin","year":"1996","unstructured":"Hardin, R.H., Har\u2019el, Z., Kurshan, R.P.: COSPAN. In: Alur, R., Henzinger, T.A. (eds.) CAV 1996. LNCS, vol.\u00a01102, pp. 423\u2013427. Springer, Heidelberg (1996)"},{"key":"11_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/3-540-60630-0_3","volume-title":"Proc. 1st Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems","author":"T.A. Henzinger","year":"1995","unstructured":"Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: A user guide to hytech. In: TACAS 1995. LNCS, vol.\u00a01019, pp. 41\u201371. Springer, Heidelberg (1995)"},{"key":"11_CR54","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"514","DOI":"10.1007\/3-540-61604-7_73","volume-title":"CONCUR \u201996: Concurrency Theory","author":"T.A. Henzinger","year":"1996","unstructured":"Henzinger, T.A., Kupferman, O., Vardi, M.Y.: A space-efficient on-the-fly algorithm for real-time model checking. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol.\u00a01119, pp. 514\u2013529. Springer, Heidelberg (1996)"},{"issue":"5","key":"11_CR55","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1109\/32.588521","volume":"23","author":"G.J. Holzmann","year":"1997","unstructured":"Holzmann, G.J.: The model checker SPIN. IEEE Transactions on Software Engineering\u00a023(5), 279\u2013295 (1997)","journal-title":"IEEE Transactions on Software Engineering"},{"key":"11_CR56","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"126","DOI":"10.1007\/11691372_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"S. Jha","year":"2006","unstructured":"Jha, S., Schwoon, S., Wang, H., Reps, T.: Weighted pushdown systems and trust-management systems. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol.\u00a03920, p. 126. Springer, Heidelberg (2006)"},{"key":"11_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"552","DOI":"10.1007\/3-540-60246-1_160","volume-title":"Mathematical Foundations of Computer Science 1995","author":"D. Janin","year":"1995","unstructured":"Janin, D., Walukiewicz, I.: Automata for the modal \u03bc-calculus and related results. In: H\u00e1jek, P., Wiedermann, J. (eds.) MFCS 1995. LNCS, vol.\u00a0969, pp. 552\u2013562. Springer, Heidelberg (1995)"},{"key":"11_CR58","first-page":"101","volume-title":"Proc. 21st IEEE Symp. on Logic in Computer Science","author":"V. Kahlon","year":"2006","unstructured":"Kahlon, V., Gupta, A.: An automata theoretic approach for model checking threads for ltl properties. In: Proc. 21st IEEE Symp. on Logic in Computer Science, pp. 101\u2013110. IEEE press, Los Alamitos (2006)"},{"key":"11_CR59","doi-asserted-by":"crossref","unstructured":"Kahlon, V., Gupta, A.: On the analysis of interacting pushdown systems. In: Proc. 34th ACM Symp. on Principles of Programming Languages (2007)","DOI":"10.1145\/1190216.1190262"},{"key":"11_CR60","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/11817963_28","volume-title":"Computer Aided Verification","author":"V. Kahlon","year":"2006","unstructured":"Kahlon, V., Gupta, A., Sinha, N.: Symbolic model checking of concurrent programs using partial orders and on-the-fly transactions. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol.\u00a04144, pp. 286\u2013299. Springer, Heidelberg (2006)"},{"key":"11_CR61","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"505","DOI":"10.1007\/11513988_49","volume-title":"Computer Aided Verification","author":"V. Kahlon","year":"2005","unstructured":"Kahlon, V., Ivan\u0109i\u0107, F., Gupta, A.: Reasoning about threads communicating via locks. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol.\u00a03576, pp. 505\u2013518. Springer, Heidelberg (2005)"},{"key":"11_CR62","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1450","DOI":"10.1007\/11523468_117","volume-title":"Automata, Languages and Programming","author":"T. Knapik","year":"2005","unstructured":"Knapik, T., Niwinski, D., Urzczyn, P., Walukiewicz, I.: Unsafe grammars and panic automata. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol.\u00a03580, pp. 1450\u20131461. Springer, Heidelberg (2005)"},{"key":"11_CR63","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D. Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional \u03bc-calculus. Theoretical Computer Science\u00a027, 333\u2013354 (1983)","journal-title":"Theoretical Computer Science"},{"key":"11_CR64","unstructured":"Kupferman, O., Pnueli, A.: Once and for all. In: Proc. 10th IEEE Symp. on Logic in Computer Science, pp. 25\u201335 (1995)"},{"key":"11_CR65","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1007\/3-540-45657-0_31","volume-title":"Computer Aided Verification","author":"O. Kupferman","year":"2002","unstructured":"Kupferman, O., Piterman, N., Vardi, M.Y.: Model checking linear properties of prefix-recognizable systems. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol.\u00a02404, pp. 371\u2013385. Springer, Heidelberg (2002)"},{"key":"11_CR66","volume-title":"Computer Aided Verification of Coordinating Processes","author":"R.P. Kurshan","year":"1994","unstructured":"Kurshan, R.P.: Computer Aided Verification of Coordinating Processes. Princeton Univ. Press, Princeton (1994)"},{"key":"11_CR67","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1007\/3-540-49213-5_14","volume-title":"Compositionality: The Significant Difference","author":"O. Kupferman","year":"1998","unstructured":"Kupferman, O., Vardi, M.Y.: Modular model checking. In: de Roever, W.-P., Langmaack, H., Pnueli, A. (eds.) COMPOS 1997. LNCS, vol.\u00a01536, pp. 381\u2013401. Springer, Heidelberg (1998)"},{"key":"11_CR68","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"383","DOI":"10.1007\/3-540-48320-9_27","volume-title":"CONCUR\u201999. Concurrency Theory","author":"O. Kupferman","year":"1999","unstructured":"Kupferman, O., Vardi, M.Y.: Robust satisfaction. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol.\u00a01664, pp. 383\u2013398. Springer, Heidelberg (1999)"},{"key":"11_CR69","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":"11_CR70","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/978-94-015-9586-5_6","volume-title":"Advances in Temporal Logic","author":"O. Kupferman","year":"2000","unstructured":"Kupferman, O., Vardi, M.Y.: Synthesis with incomplete information. In: Advances in Temporal Logic, pp. 109\u2013127. Kluwer Academic Publishers, Dordrecht (2000)"},{"key":"11_CR71","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"24","DOI":"10.1007\/3-540-45653-8_2","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"O. Kupferman","year":"2001","unstructured":"Kupferman, O., Vardi, M.Y.: On bounded specifications. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol.\u00a02250, pp. 24\u201338. Springer, Heidelberg (2001)"},{"issue":"2","key":"11_CR72","doi-asserted-by":"publisher","first-page":"312","DOI":"10.1145\/333979.333987","volume":"47","author":"O. Kupferman","year":"2000","unstructured":"Kupferman, O., Vardi, M.Y., Wolper, P.: An automata-theoretic approach to branching-time model checking. Journal of the ACM\u00a047(2), 312\u2013360 (2000)","journal-title":"Journal of the ACM"},{"key":"11_CR73","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.\u00a03328, pp. 408\u2013420. Springer, Heidelberg (2004)"},{"key":"11_CR74","doi-asserted-by":"crossref","unstructured":"Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: Proc. 12th ACM Symp. on Principles of Programming Languages, pp. 97\u2013107 (1985)","DOI":"10.1145\/318593.318622"},{"key":"11_CR75","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"456","DOI":"10.1007\/3-540-63166-6_47","volume-title":"Computer Aided Verification","author":"K.G. Larsen","year":"1997","unstructured":"Larsen, K.G., Petterson, P., Yi, W.: Uppaal: Status & developments. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol.\u00a01254, pp. 456\u2013459. Springer, Heidelberg (1997)"},{"key":"11_CR76","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"196","DOI":"10.1007\/3-540-15648-8_16","volume-title":"Logics of Programs","author":"O. Lichtenstein","year":"1985","unstructured":"Lichtenstein, O., Pnueli, A., Zuck, L.: The glory of the past. In: Parikh, R. (ed.) Logic of Programs 1985. LNCS, vol.\u00a0193, pp. 196\u2013218. Springer, Heidelberg (1985)"},{"key":"11_CR77","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1016\/0304-3975(85)90087-8","volume":"37","author":"D.E. Muller","year":"1985","unstructured":"Muller, D.E., Schupp, P.E.: The theory of ends, pushdown automata, and second-order logic. Theoretical Computer Science\u00a037, 51\u201375 (1985)","journal-title":"Theoretical Computer Science"},{"key":"11_CR78","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1016\/0304-3975(87)90133-2","volume":"54","author":"D.E. Muller","year":"1987","unstructured":"Muller, D.E., Schupp, P.E.: Alternating automata on infinite trees. Theoretical Computer Science\u00a054, 267\u2013276 (1987)","journal-title":"Theoretical Computer Science"},{"key":"11_CR79","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"2","DOI":"10.1007\/3-540-45793-3_2","volume-title":"Computer Science Logic","author":"F. Neven","year":"2002","unstructured":"Neven, F.: Automata, logic, and XML. In: Bradfield, J.C. (ed.) CSL 2002 and EACSL 2002. LNCS, vol.\u00a02471, pp. 2\u201326. Springer, Heidelberg (2002)"},{"key":"11_CR80","first-page":"81","volume-title":"Proc. 21st IEEE Symp. on Logic in Computer Science","author":"L. Ong","year":"2006","unstructured":"Ong, L.: On model-checking trees generated by higher-order recursion schemes. In: Proc. 21st IEEE Symp. on Logic in Computer Science, pp. 81\u201390. IEEE Computer Society Press, Los Alamitos (2006)"},{"key":"11_CR81","unstructured":"Piterman, N.: Verification of Infinite-State Systems. PhD thesis, Weizmann Institute of Science (2004)"},{"key":"11_CR82","doi-asserted-by":"crossref","unstructured":"Pnueli, A.: The temporal logic of programs. In: Proc. 18th IEEE Symp. on Foundations of Computer Science, pp. 46\u201357 (1977)","DOI":"10.1109\/SFCS.1977.32"},{"key":"11_CR83","doi-asserted-by":"crossref","unstructured":"Pnueli, A., Rosner, R.: On the synthesis of a reactive module. In: Proc. 16th ACM Symp. on Principles of Programming Languages, pp. 179\u2013190 (1989)","DOI":"10.1145\/75277.75293"},{"issue":"1-3","key":"11_CR84","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1016\/S0304-3975(02)00410-3","volume":"295","author":"N. Piterman","year":"2003","unstructured":"Piterman, N., Vardi, M.Y.: From bidirectionality to alternation. Theoretical Computer Science\u00a0295(1-3), 295\u2013321 (2003)","journal-title":"Theoretical Computer Science"},{"key":"11_CR85","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.: 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":"11_CR86","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"337","DOI":"10.1007\/3-540-11494-7_22","volume-title":"Proc. 8th ACM Symp. on Principles of Programming Languages","author":"J.P. Queille","year":"1982","unstructured":"Queille, J.P., Sifakis, J.: Specification and verification of concurrent systems in Cesar. In: Proc. 8th ACM Symp. on Principles of Programming Languages. LNCS, vol.\u00a0137, pp. 337\u2013351. Springer, Heidelberg (1982)"},{"key":"11_CR87","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. Transaction of the AMS\u00a0141, 1\u201335 (1969)","journal-title":"Transaction of the AMS"},{"key":"11_CR88","unstructured":"Schwoon, S.: Model-checking pushdown systems. PhD thesis, Technische Universit\u00e4t M\u00fcnchen (2002)"},{"key":"11_CR89","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/11690634_23","volume-title":"Foundations of Software Science and Computation Structures","author":"O. Serre","year":"2006","unstructured":"Serre, O.: Parity games played on transition graphs of one-counter processes. In: Aceto, L., Ing\u00f3lfsd\u00f3ttir, A. (eds.) FOSSACS 2006. LNCS, vol.\u00a03921, pp. 337\u2013351. Springer, Heidelberg (2006)"},{"key":"11_CR90","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":"11_CR91","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"628","DOI":"10.1007\/BFb0055090","volume-title":"Automata, Languages and Programming","author":"M.Y. Vardi","year":"1998","unstructured":"Vardi, M.Y.: Reasoning about the past with two-way automata. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol.\u00a01443, pp. 628\u2013641. Springer, Heidelberg (1998)"},{"issue":"4","key":"11_CR92","doi-asserted-by":"publisher","first-page":"350","DOI":"10.1007\/s100090050042","volume":"2","author":"W. Visser","year":"2000","unstructured":"Visser, W., Barringer, H.: Practical CTL\u2009\u22c6\u2009 model checking: Should SPIN be extended? Software Tools for Technology Transfer\u00a02(4), 350\u2013365 (2000)","journal-title":"Software Tools for Technology Transfer"},{"key":"11_CR93","unstructured":"Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification. In: Proc. 1st IEEE Symp. on Logic in Computer Science, pp. 332\u2013344 (1986)"},{"issue":"2","key":"11_CR94","doi-asserted-by":"publisher","first-page":"182","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. Journal of Computer and Systems Science\u00a032(2), 182\u2013221 (1986)","journal-title":"Journal of Computer and Systems Science"},{"issue":"1","key":"11_CR95","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1006\/inco.1994.1092","volume":"115","author":"M.Y. Vardi","year":"1994","unstructured":"Vardi, M.Y., Wolper, P.: Reasoning about infinite computations. Information and Computation\u00a0115(1), 1\u201337 (1994)","journal-title":"Information and Computation"},{"key":"11_CR96","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":"11_CR97","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)"},{"issue":"1-2","key":"11_CR98","doi-asserted-by":"publisher","first-page":"311","DOI":"10.1016\/S0304-3975(01)00185-2","volume":"275","author":"I. Walukiewicz","year":"2002","unstructured":"Walukiewicz, I.: Monadic second-order logic on tree-like structures. Theoretical Computer Science\u00a0275(1-2), 311\u2013346 (2002)","journal-title":"Theoretical Computer Science"},{"key":"11_CR99","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1007\/3-540-46691-6_9","volume-title":"Foundations of Software Technology and Theoretical Computer Science","author":"T. Wilke","year":"1999","unstructured":"Wilke, T.: CTL\u2009+\u2009 is exponentially more succinct than CTL. In: Pandu Rangan, C., Raman, V., Sarukkai, S. (eds.) FST TCS 1999. LNCS, vol.\u00a01738, pp. 110\u2013121. Springer, Heidelberg (1999)"},{"key":"11_CR100","doi-asserted-by":"crossref","unstructured":"Wolper, P., Vardi, M.Y., Sistla, A.P.: Reasoning about infinite computation paths. In: Proc. 24th IEEE Symp. on Foundations of Computer Science, pp. 185\u2013194 (1983)","DOI":"10.1109\/SFCS.1983.51"},{"key":"11_CR101","doi-asserted-by":"crossref","unstructured":"Willems, B., Wolper, P.: Partial-order methods for model checking: From linear time to branching time. In: Proc. 11th IEEE Symp. on Logic in Computer Science, pp. 294\u2013303 (1996)","DOI":"10.1109\/LICS.1996.561357"}],"container-title":["Lecture Notes in Computer Science","Time for Verification"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-13754-9_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,10,30]],"date-time":"2021-10-30T11:09:11Z","timestamp":1635592151000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-13754-9_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642137532","9783642137549"],"references-count":101,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-13754-9_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2010]]}}}