{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:16:45Z","timestamp":1740097005146,"version":"3.37.3"},"publisher-location":"Berlin, Heidelberg","reference-count":30,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642548291"},{"type":"electronic","value":"9783642548307"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-642-54830-7_1","type":"book-chapter","created":{"date-parts":[[2014,3,21]],"date-time":"2014-03-21T09:30:31Z","timestamp":1395394231000},"page":"1-28","source":"Crossref","is-referenced-by-count":6,"title":["Equivalences of Pushdown Systems Are Hard"],"prefix":"10.1007","author":[{"given":"Petr","family":"Jan\u010dar","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"1_CR1","doi-asserted-by":"crossref","unstructured":"Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Proc. STOC 2004, pp. 202\u2013211. ACM (2004)","DOI":"10.1145\/1007352.1007390"},{"key":"1_CR2","doi-asserted-by":"crossref","unstructured":"Benedikt, M., G\u00f6ller, S., Kiefer, S., Murawski, A.S.: Bisimilarity of pushdown automata is nonelementary. In: Proc. LICS 2013, pp. 488\u2013498. IEEE Computer Society (2013)","DOI":"10.1109\/LICS.2013.55"},{"key":"1_CR3","doi-asserted-by":"crossref","unstructured":"B\u00f6hm, S., G\u00f6ller, S., Jan\u010dar, P.: Equivalence of deterministic one-counter automata is NL-complete. In: Proc. STOC 2013, pp. 131\u2013140. ACM (2013)","DOI":"10.1145\/2488608.2488626"},{"key":"1_CR4","doi-asserted-by":"publisher","first-page":"720","DOI":"10.1016\/j.jcss.2013.11.003","volume":"80","author":"S. B\u00f6hm","year":"2014","unstructured":"B\u00f6hm, S., G\u00f6ller, S., Jan\u010dar, P.: Bisimulation equivalence and regularity for real-time one-counter automata. J. Comput. Syst. Sci.\u00a080, 720\u2013743 (2014), \n                  \n                    http:\/\/dx.doi.org\/10.1016\/j.jcss.2013.11.003","journal-title":"J. Comput. Syst. Sci."},{"key":"1_CR5","unstructured":"Broadbent, C.H., G\u00f6ller, S.: On bisimilarity of higher-order pushdown automata: Undecidability at order two. In: FSTTCS 2012. LIPIcs, vol.\u00a018, pp. 160\u2013172. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2012)"},{"key":"1_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/3-540-60246-1_148","volume-title":"Mathematical Foundations of Computer Science 1995","author":"O. Burkart","year":"1995","unstructured":"Burkart, O., Caucal, D., Steffen, B.: An elementary bisimulation decision procedure for arbitrary context-free processes. In: H\u00e1jek, P., Wiedermann, J. (eds.) MFCS 1995. LNCS, vol.\u00a0969, pp. 423\u2013433. Springer, Heidelberg (1995)"},{"key":"1_CR7","doi-asserted-by":"crossref","unstructured":"Courcelle, B.: Recursive applicative program schemes. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol.\u00a0B, pp. 459\u2013492. Elsevier, MIT Press (1990)","DOI":"10.1016\/B978-0-444-88074-1.50014-7"},{"key":"1_CR8","unstructured":"Czerwinski, W., Lasota, S.: Fast equivalence-checking for normed context-free processes. In: Proc. of FSTTCS 2010. LIPIcs, vol.\u00a08, pp. 260\u2013271. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2010)"},{"key":"1_CR9","doi-asserted-by":"crossref","unstructured":"Figueira, D., Figueira, S., Schmitz, S., Schnoebelen, P.: Ackermannian and primitive-recursive bounds with Dickson\u2019s lemma. In: Proc. LICS 2011, pp. 269\u2013278. IEEE Computer Society (2011)","DOI":"10.1109\/LICS.2011.39"},{"issue":"4","key":"1_CR10","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1016\/0304-3975(76)90074-8","volume":"1","author":"E.P. Friedman","year":"1976","unstructured":"Friedman, E.P.: The inclusion problem for simple languages. Theor. Comput. Sci.\u00a01(4), 297\u2013316 (1976)","journal-title":"Theor. Comput. Sci."},{"key":"1_CR11","unstructured":"G\u00f6ller, S., Lohrey, M.: The First-Order Theory of Ground Tree Rewrite Graphs. Logical Methods in Computer Science\u00a010(1) (2014), \n                  \n                    http:\/\/dx.doi.org\/10.2168\/LMCS-101:72014"},{"key":"1_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"169","DOI":"10.1007\/978-3-642-39274-0_16","volume-title":"CIAA 2013","author":"P. Henry","year":"2013","unstructured":"Henry, P., S\u00e9nizergues, G.: LALBLC A program testing the equivalence of dpda\u2019s. In: Konstantinidis, S. (ed.) CIAA 2013. LNCS, vol.\u00a07982, pp. 169\u2013180. Springer, Heidelberg (2013)"},{"issue":"1&2","key":"1_CR13","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1016\/0304-3975(95)00064-X","volume":"158","author":"Y. Hirshfeld","year":"1996","unstructured":"Hirshfeld, Y., Jerrum, M., Moller, F.: A polynomial algorithm for deciding bisimilarity of normed context-free processes. Theor. Comput. Sci.\u00a0158(1&2), 143\u2013159 (1996)","journal-title":"Theor. Comput. Sci."},{"key":"1_CR14","doi-asserted-by":"crossref","unstructured":"Jan\u010dar, P., Srba, J.: Undecidability of bisimilarity by Defender\u2019s forcing. J. ACM 55(1) (2008)","DOI":"10.1145\/1326554.1326559"},{"key":"1_CR15","doi-asserted-by":"crossref","unstructured":"Jan\u010dar, P.: Decidability of DPDA language equivalence via first-order grammars. In: Proc. LICS 2012, pp. 415\u2013424. IEEE Computer Society (2012)","DOI":"10.1109\/LICS.2012.51"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Jan\u010dar, P.: Bisimilarity on basic process algebra is in 2-ExpTime (an explicit proof). Logical Methods in Computer Science 9(1) (2013)","DOI":"10.2168\/LMCS-9(1:10)2013"},{"issue":"4","key":"1_CR17","doi-asserted-by":"publisher","first-page":"101","DOI":"10.1016\/j.ipl.2012.12.004","volume":"113","author":"S. Kiefer","year":"2013","unstructured":"Kiefer, S.: BPA bisimilarity is EXPTIME-hard. Inf. Process. Lett.\u00a0113(4), 101\u2013106 (2013)","journal-title":"Inf. Process. Lett."},{"issue":"7","key":"1_CR18","doi-asserted-by":"publisher","first-page":"772","DOI":"10.1016\/j.ic.2010.01.003","volume":"208","author":"A. Ku\u010dera","year":"2010","unstructured":"Ku\u010dera, A., Mayr, R.: On the complexity of checking semantic equivalences between pushdown processes and finite-state processes. Inf. Comput.\u00a0208(7), 772\u2013796 (2010)","journal-title":"Inf. Comput."},{"key":"1_CR19","unstructured":"Schmitz, S.: Complexity hierarchies beyond elementary. CoRR abs\/1312.5686 (2013)"},{"key":"1_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"616","DOI":"10.1007\/978-3-642-15155-2_54","volume-title":"Mathematical Foundations of Computer Science 2010","author":"P. Schnoebelen","year":"2010","unstructured":"Schnoebelen, P.: Revisiting Ackermann-hardness for lossy counter machines and reset Petri nets. In: Hlin\u011bn\u00fd, P., Ku\u010dera, A. (eds.) MFCS 2010. LNCS, vol.\u00a06281, pp. 616\u2013628. Springer, Heidelberg (2010)"},{"key":"#cr-split#-1_CR21.1","doi-asserted-by":"crossref","unstructured":"S\u00e9nizergues, G.: L(A)=L(B)? Decidability results from complete formal systems. Theoretical Computer Science 251(1-2), 1-166 (2001)","DOI":"10.1016\/S0304-3975(00)00285-1"},{"key":"#cr-split#-1_CR21.2","unstructured":"a preliminary version appeared at Degano, P., Gorrieri, R., Marchetti-Spaccamela, A. (eds.): ICALP 1997. LNCS, vol.\u00a01256. Springer, Heidelberg (1997)"},{"key":"1_CR22","unstructured":"S\u00e9nizergues, G.: The bisimulation problem for equational graphs of finite out-degree. SIAM J. Comput. 34(5), 1025\u20131106 (2005) (a preliminary version appeared at FOCS 1998)"},{"key":"1_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"478","DOI":"10.1007\/3-540-45061-0_39","volume-title":"Automata, Languages and Programming","author":"G. S\u00e9nizergues","year":"2003","unstructured":"S\u00e9nizergues, G.: The equivalence problem for t-turn DPDA is co-NP. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol.\u00a02719, pp. 478\u2013489. Springer, Heidelberg (2003)"},{"key":"1_CR24","doi-asserted-by":"crossref","unstructured":"Srba, J.: Roadmap of infinite results. in: Current Trends In Theoretical Computer Science, The Challenge of the New Century, vol.\u00a02, pp. 337\u2013350. World Scientific Publishing Co. (2004), updated version at \n                  \n                    http:\/\/users-cs.au.dk\/srba\/roadmap\/","DOI":"10.1142\/9789812562494_0054"},{"key":"1_CR25","doi-asserted-by":"crossref","unstructured":"Srba, J.: Beyond language equivalence on visibly pushdown automata. Logical Methods in Computer Science 5(1) (2009)","DOI":"10.2168\/LMCS-5(1:2)2009"},{"key":"1_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"821","DOI":"10.1007\/3-540-45465-9_70","volume-title":"Automata, Languages and Programming","author":"C. Stirling","year":"2002","unstructured":"Stirling, C.: Deciding DPDA equivalence is primitive recursive. In: Widmayer, P., Triguero, F., Morales, R., Hennessy, M., Eidenbenz, S., Conejo, R. (eds.) ICALP 2002. LNCS, vol.\u00a02380, pp. 821\u2013832. Springer, Heidelberg (2002)"},{"key":"1_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"509","DOI":"10.1007\/11817949_34","volume-title":"CONCUR 2006 \u2013 Concurrency Theory","author":"C. Stirling","year":"2006","unstructured":"Stirling, C.: Second-order simple grammars. In: Baier, C., Hermanns, H. (eds.) CONCUR 2006. LNCS, vol.\u00a04137, pp. 509\u2013523. Springer, Heidelberg (2006)"},{"issue":"4","key":"1_CR28","doi-asserted-by":"publisher","first-page":"1774","DOI":"10.2307\/2586811","volume":"64","author":"A. Urquhart","year":"1999","unstructured":"Urquhart, A.: The complexity of decision procedures in relevance logic II. J. Symb. Log.\u00a064(4), 1774\u20131802 (1999)","journal-title":"J. Symb. Log."},{"issue":"2","key":"1_CR29","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1006\/inco.2000.2894","volume":"164","author":"I. Walukiewicz","year":"2001","unstructured":"Walukiewicz, I.: Pushdown processes: Games and model-checking. Inf. Comput.\u00a0164(2), 234\u2013263 (2001)","journal-title":"Inf. Comput."}],"container-title":["Lecture Notes in Computer Science","Foundations of Software Science and Computation Structures"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-54830-7_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T08:17:32Z","timestamp":1558858652000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-54830-7_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783642548291","9783642548307"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-54830-7_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}