Abstract
We prove undecidability of the problem whether a given pair of pushdown processes is weakly bisimilar. We also show that this undecidability result extends to a subclass of pushdown processes satisfying the normedness condition.
The author is supported in part by the GACR, grant No. 201/00/0400.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
O. Burkart, D. Caucal, F. Moller, and B. Steffen. Verification on infinite structures. In J. Bergstra, A. Ponse, and S. Smolka, editors, Handbook of Process Algebra, chapter 9, pages 545–623. Elsevier Science, 2001.
S. Christensen, Y. Hirshfeld, and F. Moller. Bisimulation is decidable for basic parallel processes. In Proc. of CONCUR’93, volume 715 of LNCS, pages 143–157. Springer-Verlag, 1993.
S. Christensen, H. Hüttel, and C. Stirling. Bisimulation equivalence is decidable for all context-free processes. Information and Computation, 121:143–148, 1995.
J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon. Efficient algorithms for model checkingpus hdown systems. In Proc. of CAV’00, volume 1855 of LNCS, pages 232–247. Springer-Verlag, 2000.
J. F. Groote and H. Hüttel. Undecidable equivalences for basic process algebra. Information and Computation, 115(2):353–371, 1994.
Y. Hirshfeld. Bisimulation trees and the decidability of weak bisimulations. In Proc. of INFINITY’96, volume 5 of ENTCS. Springer-Verlag, 1996.
Y. Hirshfeld, M. Jerrum, and F. Moller. A polynomial algorithm for decidingb isimilarity of normed context-free processes. Theoretical Computer Science, 158(1–2):143–159, 1996.
Y. Hirshfeld, M. Jerrum, and F. Moller. A polynomial-time algorithm for decidingbi simulation equivalence of normed basic parallel processes. Mathematical Structures in Computer Science, 6(3):251–259, 1996.
H. Hüttel. Undecidable equivalences for basic parallel processes. In Proc. of TACS’94, volume 789 of LNCS, pages 454–464. Springer-Verlag, 1994.
P. Jančar. High undecidability of weak bisimilarity for Petri nets. In Proc. of CAAP’95, volume 915 of LNCS, pages 349–363. Springer-Verlag, 1995.
P. Jančar and J. Esparza. Deciding finiteness of Petri nets up to bisimulation. In Proc. of ICALP’96, volume 1099 of LNCS, pages 478–489. Springer-Verlag, 1996.
P. Jančar and F. Moller. Checkingre gular properties of Petri nets. In Proc. of CONCUR’95, volume 962 of LNCS, pages 348–362. Springer-Verlag, 1995.
A. Kučera and R. Mayr. On the complexity of semantic equivalences for pushdown automata and BPA. In Proc. of MFCS’02, LNCS. Springer-Verlag, 2002. To appear.
R. Mayr. On the complexity of bisimulation problems for pushdown automata. In Proc. of IFIP TCS’00, volume 1872 of LNCS. Springer-Verlag, 2000.
R. Milner. Communication and Concurrency. Prentice-Hall, 1989.
M. L. Minsky. Computation: Finite and Infinite Machines. Prentice-Hall, 1967.
D. M. R. Park. Concurrency and automata on infinite sequences. In Proc. of 5th GI Conference, volume 104 of LNCS, pages 167–183. Springer-Verlag, 1981.
G. Sénizergues. The equivalence problem for deterministic pushdown automata is decidable. In Proc. of ICALP’97, volume 1256 of LNCS, pages 671–681. Springer-Verlag, 1997.
G. Sénizergues. Decidability of bisimulation equivalence for equational graphs of finite out-degree. In Proc. of FOCS’98, pages 120–129. IEEE Computer Society, 1998.
J. Srba. Strong bisimilarity and regularity of basic process algebra is PSPACEhard. In Proc. of ICALP’02, LNCS. Springer-Verlag, 2002. To appear.
C. Stirling. Local model checking games. In Proc. of CONCUR’95, volume 962 of LNCS, pages 1–11. Springer-Verlag, 1995.
C. Stirling. Decidability of bisimulation equivalence for normed pushdown processes. Theoretical Computer Science, 195(2):113–131, 1998.
C. Stirling. Decidability of weak bisimilarity for a subset of basic parallel processes. In Proc. of FOSSACS’01, volume 2030 of LNCS, pages 379–393. Springer-Verlag, 2001.
W. Thomas. On the Ehrenfeucht-Fraïssé game in theoretical computer science (extended abstract). In Proc. of TAPSOFT’93, volume 668 of LNCS, pages 559–568. Springer-Verlag, 1993.
R. J. van Glabbeek. Comparative Concurrency Semantics and Refinement of Actions. PhD thesis, CWI/Vrije Universiteit, 1990.
R. J. van Glabbeek. The linear time—anchingt ime spectrum. In Proc. of CONCUR⫗, volume 458 of LNCS, pages 278–297. Springer-Verlag, 1990.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2002 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Srba, J. (2002). Undecidability of Weak Bisimilarity for Pushdown Processes. In: Brim, L., Křetínský, M., Kučera, A., Jančar, P. (eds) CONCUR 2002 — Concurrency Theory. CONCUR 2002. Lecture Notes in Computer Science, vol 2421. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45694-5_38
Download citation
DOI: https://doi.org/10.1007/3-540-45694-5_38
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-44043-7
Online ISBN: 978-3-540-45694-0
eBook Packages: Springer Book Archive