{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:36:35Z","timestamp":1750307795281,"version":"3.41.0"},"reference-count":42,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2008,2,1]],"date-time":"2008-02-01T00:00:00Z","timestamp":1201824000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001823","name":"Ministry of Education, Youth and Sports","doi-asserted-by":"publisher","award":["1M0567MSM0021622419"],"award-info":[{"award-number":["1M0567MSM0021622419"]}],"id":[{"id":"10.13039\/501100001823","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2008,2]]},"abstract":"<jats:p>\n            Stirling [1996, 1998] proved the decidability of bisimilarity on so-called normed pushdown processes. This result was substantially extended by S\u00e9nizergues [1998, 2005] who showed the decidability of bisimilarity for regular (or equational) graphs of finite out-degree; this essentially coincides with weak bisimilarity of processes generated by (unnormed) pushdown automata where the\n            <jats:italic>\u03b5<\/jats:italic>\n            -transitions can only deterministically pop the stack. The question of decidability of bisimilarity for the more general class of so called Type -1 systems, which is equivalent to weak bisimilarity on unrestricted\n            <jats:italic>\u03b5<\/jats:italic>\n            -popping pushdown processes, was left open. This was repeatedly indicated by both Stirling and S\u00e9nizergues. Here we answer the question negatively, that is, we show the undecidability of bisimilarity on Type -1 systems, even in the normed case.\n          <\/jats:p>\n          <jats:p>\n            We achieve the result by applying a technique we call Defender's Forcing, referring to the bisimulation games. The idea is simple, yet powerful. We demonstrate its versatility by deriving further results in a uniform way. First, we classify several versions of the undecidable problems for prefix rewrite systems (or pushdown automata) as \u03a0\n            <jats:sup>0<\/jats:sup>\n            <jats:sub>1<\/jats:sub>\n            -complete or \u03a3\n            <jats:sup>1<\/jats:sup>\n            <jats:sub>1<\/jats:sub>\n            -complete. Second, we solve the decidability question for weak bisimilarity on PA (Process Algebra) processes, showing that the problem is undecidable and even \u03a3\n            <jats:sup>1<\/jats:sup>\n            <jats:sub>1<\/jats:sub>\n            -complete. Third, we show \u03a3\n            <jats:sup>1<\/jats:sup>\n            <jats:sub>1<\/jats:sub>\n            -completeness of weak bisimilarity for so-called parallel pushdown (or multiset) automata, a subclass of (labeled, place\/transition) Petri nets.\n          <\/jats:p>","DOI":"10.1145\/1326554.1326559","type":"journal-article","created":{"date-parts":[[2008,2,28]],"date-time":"2008-02-28T14:02:33Z","timestamp":1204207353000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":18,"title":["Undecidability of bisimilarity by defender's forcing"],"prefix":"10.1145","volume":"55","author":[{"given":"Petr","family":"Jan\u010dar","sequence":"first","affiliation":[{"name":"Technical University of Ostrava, Ostrava -- Poruba, Czech Republic"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jiv\u0159\u00ed","family":"Srba","sequence":"additional","affiliation":[{"name":"Aalborg University, Aalborg East, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2008,2,22]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/174130.174141"},{"key":"e_1_2_1_2_1","doi-asserted-by":"crossref","unstructured":"Baeten J. and Weijland W. 1990. Process Algebra. Number 18 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press.   Baeten J. and Weijland W. 1990. Process Algebra. Number 18 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press.","DOI":"10.1017\/CBO9780511624193"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF03180566"},{"key":"e_1_2_1_4_1","volume-title":"Proceedings of the 8th International Conference on Concurrency Theory (CONCUR'97)","volume":"1243","author":"Bouajjani A.","unstructured":"Bouajjani , A. , Esparza , J. , and Maler , O . 1997. Reachability analysis of pushdown automata: Application to model-checking . In Proceedings of the 8th International Conference on Concurrency Theory (CONCUR'97) . Lecture Notes in Computer Science , vol. 1243 . Springer-Verlag, New York, 135--150. Bouajjani, A., Esparza, J., and Maler, O. 1997. Reachability analysis of pushdown automata: Application to model-checking. In Proceedings of the 8th International Conference on Concurrency Theory (CONCUR'97). Lecture Notes in Computer Science, vol. 1243. Springer-Verlag, New York, 135--150."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01969548"},{"key":"e_1_2_1_6_1","first-page":"545","article-title":"Verification on infinite structures. In Handbook of Process Algebra, J. Bergstra, A. Ponse, and S. Smolka, Eds. Elsevier Science, Amsterdam, The Netherlands","volume":"9","author":"Burkart O.","year":"2001","unstructured":"Burkart , O. , Caucal , D. , Moller , F. , and Steffen , B. 2001 . Verification on infinite structures. In Handbook of Process Algebra, J. Bergstra, A. Ponse, and S. Smolka, Eds. Elsevier Science, Amsterdam, The Netherlands , Chapter 9 , 545 -- 623 . Burkart, O., Caucal, D., Moller, F., and Steffen, B. 2001. Verification on infinite structures. In Handbook of Process Algebra, J. Bergstra, A. Ponse, and S. Smolka, Eds. Elsevier Science, Amsterdam, The Netherlands, Chapter 9, 545--623.","journal-title":"Chapter"},{"key":"e_1_2_1_7_1","volume-title":"Proceedings of the 20th International Symposium on Mathematical Foundations of Computer Science (MFCS'95)","volume":"969","author":"Burkart O.","unstructured":"Burkart , O. , Caucal , D. , and Steffen , B . 1995. An elementary decision procedure for arbitrary context-free processes . In Proceedings of the 20th International Symposium on Mathematical Foundations of Computer Science (MFCS'95) . Lecture Notes in Computer Science , vol. 969 . Springer-Verlag, New York, 423--433. Burkart, O., Caucal, D., and Steffen, B. 1995. An elementary decision procedure for arbitrary context-free processes. In Proceedings of the 20th International Symposium on Mathematical Foundations of Computer Science (MFCS'95). Lecture Notes in Computer Science, vol. 969. Springer-Verlag, New York, 423--433."},{"key":"e_1_2_1_8_1","first-page":"138","article-title":"More infinite results","volume":"62","author":"Burkart O.","year":"1997","unstructured":"Burkart , O. , and Esparza , J. 1997 . More infinite results . Bull. Europ. Assoc. Theor. Comput. Sci. 62 , 138 -- 159 . Columns: Concurrency. Burkart, O., and Esparza, J. 1997. More infinite results. Bull. Europ. Assoc. Theor. Comput. Sci. 62, 138--159. Columns: Concurrency.","journal-title":"Bull. Europ. Assoc. Theor. Comput. Sci."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80534-6"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90278-N"},{"volume-title":"Modal Logic and Process Algebra. CSLI Lectures Notes","author":"Caucal D.","key":"e_1_2_1_11_1","unstructured":"Caucal , D. 1995. Bisimulation of context-free grammars and of pushdown automata . In Modal Logic and Process Algebra. CSLI Lectures Notes , vol. 53 . University of Chicago Press , 85--106. Caucal, D. 1995. Bisimulation of context-free grammars and of pushdown automata. In Modal Logic and Process Algebra. CSLI Lectures Notes, vol. 53. University of Chicago Press, 85--106."},{"key":"e_1_2_1_12_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 23th International Colloquium on Automata, Languages and Programming (ICALP'96)","author":"Caucal D.","unstructured":"Caucal , D. 1996. On infinite transition graphs having a decidable monadic theory . In Proceedings of the 23th International Colloquium on Automata, Languages and Programming (ICALP'96) . Lecture Notes in Computer Science , Vol. 1099 . Springer-Verlag , New York , 194--205. Caucal, D. 1996. On infinite transition graphs having a decidable monadic theory. In Proceedings of the 23th International Colloquium on Automata, Languages and Programming (ICALP'96). Lecture Notes in Computer Science, Vol. 1099. Springer-Verlag, New York, 194--205."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1995.1129"},{"key":"e_1_2_1_14_1","volume-title":"Proceedings of the 12th International Conference on Computer Aided Verification (CAV'00)","volume":"1855","author":"Esparza J.","unstructured":"Esparza , J. , Hansel , D. , Rossmanith , P. , and Schwoon , S . 2000. Efficient algorithms for model checking pushdown systems . In Proceedings of the 12th International Conference on Computer Aided Verification (CAV'00) . Lecture Notes in Computer Science , vol. 1855 . Springer-Verlag, New York, 232--247. Esparza, J., Hansel, D., Rossmanith, P., and Schwoon, S. 2000. Efficient algorithms for model checking pushdown systems. In Proceedings of the 12th International Conference on Computer Aided Verification (CAV'00). Lecture Notes in Computer Science, vol. 1855. Springer-Verlag, New York, 232--247."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/4904.4993"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/2455.2460"},{"key":"e_1_2_1_17_1","volume-title":"Proceedings of 26th International Colloquium on Automata, Languages and Programming (ICALP'99)","volume":"1644","author":"Hirshfeld Y.","unstructured":"Hirshfeld , Y. , and Jerrum , M . 1999. Bisimulation equivalence is decidable for normed process algebra . In Proceedings of 26th International Colloquium on Automata, Languages and Programming (ICALP'99) . Lecture Notes in Computer Science , vol. 1644 . Springer-Verlag, New York, 412--421. Hirshfeld, Y., and Jerrum, M. 1999. Bisimulation equivalence is decidable for normed process algebra. In Proceedings of 26th International Colloquium on Automata, Languages and Programming (ICALP'99). Lecture Notes in Computer Science, vol. 1644. Springer-Verlag, New York, 412--421."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00064-X"},{"key":"e_1_2_1_19_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of Colloquium on Trees in Algebra and Programming (CAAP'95)","author":"Jan\u010dar P.","unstructured":"Jan\u010dar , P. 1995a. High undecidability of weak bisimilarity for Petri nets . In Proceedings of Colloquium on Trees in Algebra and Programming (CAAP'95) . Lecture Notes in Computer Science , vol. 915 . Springer-Verlag , New York , 349--363. Jan\u010dar, P. 1995a. High undecidability of weak bisimilarity for Petri nets. In Proceedings of Colloquium on Trees in Algebra and Programming (CAAP'95). Lecture Notes in Computer Science, vol. 915. Springer-Verlag, New York, 349--363."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00037-W"},{"key":"e_1_2_1_21_1","series-title":"BRICS Research Series.","volume-title":"Tech. Rep. RS-06-7","author":"Jan\u010dar P.","year":"2006","unstructured":"Jan\u010dar , P. , and Srba , J . 2006 . Undecidability results for bisimilarity on prefix rewrite systems. Tech. Rep. RS-06-7 , BRICS Research Series. Jan\u010dar, P., and Srba, J. 2006. Undecidability results for bisimilarity on prefix rewrite systems. Tech. Rep. RS-06-7, BRICS Research Series."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(90)90025-D"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068406002651"},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the 27th International Symposium on Mathematical Foundations of Computer Science (MFCS'02)","volume":"2420","author":"Ku\u010dera A.","unstructured":"Ku\u010dera , A. , and Mayr , R . 2002. On the complexity of semantic equivalences for pushdown automata and BPA . In Proceedings of the 27th International Symposium on Mathematical Foundations of Computer Science (MFCS'02) . Lecture Notes in Computer Science , vol. 2420 . Springer-Verlag, New York, 433--445. Ku\u010dera, A., and Mayr, R. 2002. On the complexity of semantic equivalences for pushdown automata and BPA. In Proceedings of the 27th International Symposium on Mathematical Foundations of Computer Science (MFCS'02). Lecture Notes in Computer Science, vol. 2420. Springer-Verlag, New York, 433--445."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2826"},{"volume-title":"Communication and Concurrency","author":"Milner R.","key":"e_1_2_1_26_1","unstructured":"Milner , R. 1989. Communication and Concurrency . Prentice-Hall , Englewood Cliffs, NJ . Milner, R. 1989. Communication and Concurrency. Prentice-Hall, Englewood Cliffs, NJ."},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/646731.703702"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1137\/0216062"},{"key":"e_1_2_1_29_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 5th GI Conference","author":"Park D.","unstructured":"Park , D. 1981. Concurrency and automata on infinite sequences . In Proceedings of the 5th GI Conference . Lecture Notes in Computer Science , vol. 104 . Springer-Verlag , New York , 167-- 183. Park, D. 1981. Concurrency and automata on infinite sequences. In Proceedings of the 5th GI Conference. Lecture Notes in Computer Science, vol. 104. Springer-Verlag, New York, 167-- 183."},{"key":"e_1_2_1_31_1","first-page":"579","article-title":"Reversible machines and Post's correspondence problem for biprefix morphisms","volume":"21","author":"Ruohonen K.","year":"1985","unstructured":"Ruohonen , K. 1985 . Reversible machines and Post's correspondence problem for biprefix morphisms . Elektronische Informationsverarbeitung und Kybernetik 21 , 12, 579 -- 595 . Ruohonen, K. 1985. Reversible machines and Post's correspondence problem for biprefix morphisms. Elektronische Informationsverarbeitung und Kybernetik 21, 12, 579--595.","journal-title":"Elektronische Informationsverarbeitung und Kybernetik"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.5555\/795664.796448"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00285-1"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539700377256"},{"key":"e_1_2_1_35_1","volume-title":"Introduction to the Theory of Computation","author":"Sipser M.","unstructured":"Sipser , M. 2005. Introduction to the Theory of Computation , 2 nd ed. Course Technology . Sipser, M. 2005. Introduction to the Theory of Computation, 2nd ed. Course Technology.","edition":"2"},{"key":"e_1_2_1_36_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of the 29th International Colloquium on Automata, Languages and Programming (ICALP'02)","author":"Srba J.","unstructured":"Srba , J. 2002. Strong bisimilarity and regularity of basic process algebra is PSPACE-hard . In Proceedings of the 29th International Colloquium on Automata, Languages and Programming (ICALP'02) . Lecture Notes in Computer Science , vol. 2380 . Springer-Verlag , New York , 716-- 727. Srba, J. 2002. Strong bisimilarity and regularity of basic process algebra is PSPACE-hard. In Proceedings of the 29th International Colloquium on Automata, Languages and Programming (ICALP'02). Lecture Notes in Computer Science, vol. 2380. Springer-Verlag, New York, 716-- 727."},{"volume-title":"Formal Models and Semantics","author":"Srba J.","key":"e_1_2_1_37_1","unstructured":"Srba , J. 2004. Roadmap of Infinite results . Vol. 2 : Formal Models and Semantics . World Scientific Publishing Co. (Updated version can be downloaded from the author's home-page). Srba, J. 2004. Roadmap of Infinite results. Vol. 2: Formal Models and Semantics. World Scientific Publishing Co. (Updated version can be downloaded from the author's home-page)."},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.5555\/646730.759541"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.5555\/646731.703701"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(97)00216-8"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00389-3"},{"volume-title":"Logic for Concurrency and Synchronisation. Trends in Logic","author":"Stirling C.","key":"e_1_2_1_43_1","unstructured":"Stirling , C. 2003. Bisimulation and language equivalence . In Logic for Concurrency and Synchronisation. Trends in Logic , vol. 18 . Kluwer Academic Publishers , 269--284. Stirling, C. 2003. Bisimulation and language equivalence. In Logic for Concurrency and Synchronisation. Trends in Logic, vol. 18. Kluwer Academic Publishers, 269--284."},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.5555\/646618.697382"}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1326554.1326559","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1326554.1326559","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T13:56:25Z","timestamp":1750254985000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1326554.1326559"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,2]]},"references-count":42,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2008,2]]}},"alternative-id":["10.1145\/1326554.1326559"],"URL":"https:\/\/doi.org\/10.1145\/1326554.1326559","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"type":"print","value":"0004-5411"},{"type":"electronic","value":"1557-735X"}],"subject":[],"published":{"date-parts":[[2008,2]]},"assertion":[{"value":"2006-12-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2007-11-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2008-02-22","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}