{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,11]],"date-time":"2025-10-11T01:37:17Z","timestamp":1760146637492,"version":"3.32.0"},"publisher-location":"Boston","reference-count":43,"publisher":"Kluwer Academic Publishers","isbn-type":[{"type":"print","value":"1402081405"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/1-4020-8141-3_31","type":"book-chapter","created":{"date-parts":[[2006,2,21]],"date-time":"2006-02-21T15:15:11Z","timestamp":1140534911000},"page":"395-408","source":"Crossref","is-referenced-by-count":5,"title":["A Generic Framework for Checking Semantic Equivalences Between Pushdown Automata and Finite-State Automata"],"prefix":"10.1007","author":[{"given":"Antonin","family":"Ku\u010dera","sequence":"first","affiliation":[]},{"given":"Richard","family":"Mayr","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"31_CR1","doi-asserted-by":"crossref","unstructured":"R. Alur, K. Etessami, and P. Madhusudan. A temporal logic of nested calls and returns. In Proceedings of TACAS 2004, vol. 2988 of Lecture Notes in Computer Science, pp. 467\u2013481. Springer, 2004.","DOI":"10.1007\/978-3-540-24730-2_35"},{"key":"31_CR2","doi-asserted-by":"crossref","unstructured":"R. Alur, K. Etessami, and M. Yannakakis. Analysis of recursive state machines. In Proceedings of CAV 2001, vol. 2102 of Lecture Notes in Computer Science, pp. 207\u2013220. Springer, 2001.","DOI":"10.1007\/3-540-44585-4_18"},{"key":"31_CR3","doi-asserted-by":"crossref","first-page":"653","DOI":"10.1145\/174130.174141","volume":"40","author":"J.C.M. Baeten","year":"1993","unstructured":"J.C.M. Baeten, J.A. Bergstra, and J.W. Klop. Decidability of bisimulation equivalence for processes generating context-free languages. Journal of the Association for Computing Machinery, 40:653\u2013682, 1993.","journal-title":"Journal of the Association for Computing Machinery"},{"key":"31_CR4","doi-asserted-by":"crossref","unstructured":"J.C.M. Baeten and W.P. Weijland. Process Algebra. No. 18 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1990.","DOI":"10.1017\/CBO9780511624193"},{"key":"31_CR5","doi-asserted-by":"crossref","unstructured":"A. Bouajjani. Languages, rewriting systems, and verification of infinite-state systems. In Proceedings of ICALP 2001, vol. 2076 of Lecture Notes in Computer Science, pp. 24\u201339. Springer, 2001.","DOI":"10.1007\/3-540-48224-5_3"},{"key":"31_CR6","doi-asserted-by":"crossref","unstructured":"A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: application to model checking. In Proceedings of CONCUR\u201997, vol. 1243 of Lecture Notes in Computer Science, pp. 135\u2013150. Springer, 1997.","DOI":"10.1007\/3-540-63141-0_10"},{"key":"31_CR7","doi-asserted-by":"crossref","unstructured":"O. Burkart, D. Caucal, F. Moller, and B. Steffen. Verification on infinite structures. In J.A. Bergstra, A. Ponse, and S.A. Smolka, editors, Handbook of Process Algebra, pp. 545\u2013623. Elsevier, 2001.","DOI":"10.1016\/B978-044482830-9\/50027-8"},{"key":"31_CR8","doi-asserted-by":"crossref","unstructured":"O. Burkart, D. Caucal, and B. Steffen. An elementary decision procedure for arbitrary context-free processes. In Proceedings of MFCS\u201995, vol. 969 of Lecture Notes in Computer Science, pp. 423\u2013433. Springer, 1995.","DOI":"10.1007\/3-540-60246-1_148"},{"issue":"4","key":"31_CR9","first-page":"339","volume":"24","author":"D. Caucal","year":"1990","unstructured":"D. Caucal. Graphes canoniques des graphes alg\u00e9briques. Informatique Th\u00e9orique et Applications (RAIRO), 24(4):339\u2013352, 1990.","journal-title":"Informatique Th\u00e9orique et Applications (RAIRO)"},{"key":"31_CR10","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1006\/inco.1995.1129","volume":"121","author":"S. Christensen","year":"1995","unstructured":"S. Christensen, H. H\u00fcttel, and C. Stirling. Bisimulation equivalence is decidable for all context-free processes. Information and Computation, 121:143\u2013148, 1995.","journal-title":"Information and Computation"},{"key":"31_CR11","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/s002360050074","volume":"34","author":"J. Esparza","year":"1997","unstructured":"J. Esparza. Decidability of model checking for infinite-state concurrent systems. Acta Informatica, 34:85\u2013107, 1997.","journal-title":"Acta Informatica"},{"key":"31_CR12","doi-asserted-by":"crossref","unstructured":"J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon. Efficient algorithms for model checking pushdown systems. In Proceedings of CAV 2000, vol. 1855 of Lecture Notes in Computer Science, pp. 232\u2013247. Springer, 2000.","DOI":"10.1007\/10722167_20"},{"key":"31_CR13","doi-asserted-by":"crossref","unstructured":"J. Esparza and J. Knoop. An automata-theoretic approach to interprocedural data-flow analysis. In Proceedings of FoSSaCS\u201999, vol. 1578 of Lecture Notes in Computer Science, pp. 14\u201330. Springer, 1999.","DOI":"10.1007\/3-540-49019-1_2"},{"issue":"2","key":"31_CR14","doi-asserted-by":"publisher","first-page":"355","DOI":"10.1016\/S0890-5401(03)00139-1","volume":"186","author":"J. Esparza","year":"2003","unstructured":"J. Esparza, A. Ku\u010dera, and S. Schwoon. Model-checking LTL with regular valuations for pushdown systems. Information and Computation, 186(2):355\u2013376, 2003.","journal-title":"Information and Computation"},{"key":"31_CR15","doi-asserted-by":"crossref","unstructured":"J. Esparza and S. Schwoon. A BDD-based model checker for recursive programs. In Proceedings of CAV 2001, vol. 2102 of Lecture Notes in Computer Science, pp. 324\u2013336. Springer, 2001.","DOI":"10.1007\/3-540-44585-4_30"},{"issue":"4","key":"31_CR16","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/0304-3975(76)90074-8","volume":"1","author":"E.P. Friedman","year":"1976","unstructured":"E.P. Friedman. The inclusion problem for simple languages. Theoretical Computer Science, 1(4):297\u2013316, 1976.","journal-title":"Theoretical Computer Science"},{"key":"31_CR17","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1016\/0020-0190(92)90142-I","volume":"42","author":"J.F. Groote","year":"1992","unstructured":"J.F. Groote. A short proof of the decidability of bisimulation for normed BPA processes. Information Processing Letters, 42:167\u2013171, 1992.","journal-title":"Information Processing Letters"},{"key":"31_CR18","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1016\/0304-3975(95)00064-X","volume":"158","author":"Y. Hirshfeld","year":"1996","unstructured":"Y. Hirshfeld, M. Jerrum, and F. Moller. A polynomial algorithm for deciding bisimilarity of normed context-free processes. Theoretical Computer Science, 158:143\u2013159, 1996.","journal-title":"Theoretical Computer Science"},{"issue":"4","key":"31_CR19","doi-asserted-by":"crossref","first-page":"485","DOI":"10.1093\/logcom\/8.4.485","volume":"8","author":"H. H\u00fcttel","year":"1998","unstructured":"H. H\u00fcttel and C. Stirling. Actions speak louder than words: Proving bisimilarity for context-free processes. Journal of Logic and Computation, 8(4):485\u2013509, 1998.","journal-title":"Journal of Logic and Computation"},{"key":"31_CR20","doi-asserted-by":"crossref","unstructured":"P. Jan\u010dar and F. Moller. Techniques for decidability and undecidability of bisimilarity. In Proceedings of CONCUR\u201999, vol. 1664 of Lecture Notes in Computer Science, pp. 30\u201345. Springer, 1999.","DOI":"10.1007\/3-540-48320-9_5"},{"issue":"1","key":"31_CR21","doi-asserted-by":"crossref","first-page":"23","DOI":"10.1016\/S0020-0190(99)00029-0","volume":"70","author":"A. Ku\u010dera","year":"1999","unstructured":"A. Ku\u010dera. On finite representations of infinite-state behaviours. Information Processing Letters, 70(1):23\u201330, 1999.","journal-title":"Information Processing Letters"},{"issue":"6","key":"31_CR22","doi-asserted-by":"crossref","first-page":"863","DOI":"10.1093\/logcom\/13.6.863","volume":"13","author":"A. Ku\u010dera","year":"2003","unstructured":"A. Ku\u010dera and J. Esparza. A logical viewpoint on process-algebraic quotients. Journal of Logic and Computation, 13(6):863\u2013880, 2003.","journal-title":"Journal of Logic and Computation"},{"key":"31_CR23","doi-asserted-by":"crossref","unstructured":"A. Ku\u010dera and P. Jan\u010dar. Equivalence-checking with infinite-state systems: Techniques and results. In Proceedings of SOFSEM\u20192002, vol. 2540 of Lecture Notes in Computer Science. Springer, 2002.","DOI":"10.1007\/3-540-36137-5_3"},{"key":"31_CR24","doi-asserted-by":"crossref","unstructured":"A. Ku\u010dera and R. Mayr. On the complexity of semantic equivalences for pushdown automata and BPA. In Proceedings of MFCS 2002, vol. 2420 of Lecture Notes in Computer Science, pp. 433\u2013445. Springer, 2002.","DOI":"10.1007\/3-540-45687-2_36"},{"issue":"1\u20132","key":"31_CR25","doi-asserted-by":"crossref","first-page":"677","DOI":"10.1016\/S0304-3975(01)00094-9","volume":"270","author":"A. Ku\u010dera","year":"2002","unstructured":"A. Ku\u010dera and R. Mayr. Weak bisimilarity between finite-state systems and BPA or normed BPP is decidable in polynomial time. Theoretical Computer Science, 270(1\u20132):677\u2013700, 2002.","journal-title":"Theoretical Computer Science"},{"key":"31_CR26","unstructured":"A. Ku\u010dera and R. Mayr. A generic framework for checking semantic equivalences between pushdown automata and finite-state automata. Technical report FIMU-RS-2004-01, Faculty of Informatics, Masaryk University, 2004."},{"issue":"1","key":"31_CR27","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0890-5401(91)90030-6","volume":"94","author":"K. Larsen","year":"1991","unstructured":"K. Larsen and A. Skou. Bisimulation through probabilistic testing. Information and Computation, 94(1):1\u201328, 1991.","journal-title":"Information and Computation"},{"key":"31_CR28","doi-asserted-by":"crossref","unstructured":"R. Mayr. Undecidability of weak bisimulation equivalence for 1-counter processes. In Proceedings of ICALP 2003, vol. 2719 of Lecture Notes in Computer Science, pp. 570\u2013583. Springer, 2003.","DOI":"10.1007\/3-540-45061-0_46"},{"key":"31_CR29","unstructured":"R. Milner. Communication and Concurrency. Prentice-Hall, 1989."},{"key":"31_CR30","doi-asserted-by":"crossref","unstructured":"F. Moller. Infinite results. In Proceedings of CONCUR\u201996, vol. 1119 of Lecture Notes in Computer Science, pp. 195\u2013216. Springer, 1996.","DOI":"10.1007\/3-540-61604-7_56"},{"key":"31_CR31","doi-asserted-by":"crossref","unstructured":"D.M.R. Park. Concurrency and automata on infinite sequences. In Proceedings 5 th GI Conference, vol. 104 of Lecture Notes in Computer Science, pp. 167\u2013183. Springer, 1981.","DOI":"10.1007\/BFb0017309"},{"key":"31_CR32","doi-asserted-by":"crossref","unstructured":"G. S\u00e9nizergues. Decidability of bisimulation equivalence for equational graphs of finite out-degree. In Proceedings of FOCS\u201998, pp. 120\u2013129. IEEE Computer Society Press, 1998.","DOI":"10.1109\/SFCS.1998.743435"},{"key":"31_CR33","unstructured":"J. Srba. Roadmap of infinite results. EATCS Bulletin, (78): 163\u2013175, 2002."},{"key":"31_CR34","doi-asserted-by":"crossref","unstructured":"J. Srba. Strong bisimilarity and regularity of basic process algebra is PSPACE-hard. In Proceedings of ICALP 2002, vol. 2380 of Lecture Notes in Computer Science, pp. 716\u2013727. Springer, 2002.","DOI":"10.1007\/3-540-45465-9_61"},{"key":"31_CR35","doi-asserted-by":"crossref","unstructured":"J. Srba. Undecidability of weak bisimilarity for pushdown processes. In Proceedings of CONCUR 2002, vol. 2421 of Lecture Notes in Computer Science, pp. 579\u2013593. Springer, 2002.","DOI":"10.1007\/3-540-45694-5_38"},{"key":"31_CR36","doi-asserted-by":"publisher","first-page":"113","DOI":"10.1016\/S0304-3975(97)00216-8","volume":"195","author":"C. Stirling","year":"1998","unstructured":"C. Stirling. Decidability of bisimulation equivalence for normed pushdown processes. Theoretical Computer Science, 195:113\u2013131, 1998.","journal-title":"Theoretical Computer Science"},{"key":"31_CR37","doi-asserted-by":"crossref","unstructured":"C. Stirling. The joys of bisimulation. In Proceedings of MFCS\u201998, vol. 1450 of Lecture Notes in Computer Science, pp. 142\u2013151. Springer, 1998.","DOI":"10.1007\/BFb0055763"},{"key":"31_CR38","doi-asserted-by":"crossref","unstructured":"W. Thomas. On the Ehrenfeucht-Fra\u00efss\u00e9 game in theoretical computer science. In Proceedings of TAPSOFT\u201993, vol. 668 of Lecture Notes in Computer Science, pp. 559\u2013568. Springer, 1993.","DOI":"10.1007\/3-540-56610-4_89"},{"key":"31_CR39","unstructured":"R. van Glabbeek. What is branching time semantics and why to use it? EATCS Bulletin, (53):191\u2013198, 1994."},{"key":"31_CR40","unstructured":"R. van Glabbeek. The linear time\u2014branching time spectrum. Handbook of Process Algebra, pp. 3\u201399, 1999."},{"key":"31_CR41","doi-asserted-by":"crossref","unstructured":"R. van Glabbeek, A. Smolka, B. Steffen, and C. Tofts. Reactive, generative, and stratified models for probabilistic processes. In Proceedings of LICS\u201990, pp. 130\u2013141. IEEE Computer Society Press, 1990.","DOI":"10.1109\/LICS.1990.113740"},{"key":"31_CR42","doi-asserted-by":"crossref","unstructured":"R.J. van Glabbeek. The linear time\u2014branching time spectrum II: The semantics of sequential systems with silent moves. In Proceedings of CONCUR\u201993, vol. 715 of Lecture Notes in Computer Science, pp. 66\u201381. Springer, 1993.","DOI":"10.1007\/3-540-57208-2_6"},{"issue":"3","key":"31_CR43","doi-asserted-by":"crossref","first-page":"555","DOI":"10.1145\/233551.233556","volume":"43","author":"R.J. Glabbeek van","year":"1996","unstructured":"R.J. van Glabbeek and W.P. Weijland. Branching time and abstraction in bisimulation semantics. Journal of the Association for Computing Machinery, 43(3):555\u2013600, 1996.","journal-title":"Journal of the Association for Computing Machinery"}],"container-title":["IFIP International Federation for Information Processing","Exploring New Frontiers of Theoretical Informatics"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/1-4020-8141-3_31.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T20:45:32Z","timestamp":1736282732000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/1-4020-8141-3_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["1402081405"],"references-count":43,"URL":"https:\/\/doi.org\/10.1007\/1-4020-8141-3_31","relation":{},"subject":[]}}