A short proof of the decidability of bisimulation for normed BPA- processes. (English) Zbl 0779.68029

Summary: The decidability of bisimulation for normed processes was first proven by J. C. M. Baeten, J. A. Bergstra and J. W. Klop [Lect. Notes Comput. Sci. 259, 94-111 (1987; Zbl 0635.68014)] and subsequently, using other proof techniques, by D. Caucal [RAIRO, Inf. Theor. Appl. 24, No. 4, 339-352 (1990; Zbl 0701.68082)] and H. Hüttel and C. Stirling [Actions speak louder than works: Proving bisimilarity for context-free processes, in: Proc. 6th Ann. Symp. on Logic in Computer Science, Amsterdam, The Netherlands (IEEE Computer Society Press, Silver Spring, MD), 376-386 (1991)]. We provide a short and straightforward proof.


68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
68Q55 Semantics in the theory of computing
Full Text: DOI


[1] Baeten, J.C.M.; Bergstra, J.A.; Klop, J.W., Decidability of bisimulation equivalence for processes generating context-free languages, (), 94-113, Eindhoven, Lecture Notes in Computer Science · Zbl 0635.68014
[2] Caucal, D., Graphes canoniques de graphes algébriques, Theoret. inform. and appl., 24, 4, 339-352, (1990) · Zbl 0701.68082
[3] Hüttel, H.; Stirling, C., Actions speak louder than words: proving bisimilarity for context-free processes, (), 376-386, Amsterdam, The Netherlands · Zbl 0904.68129
[4] Huynh, D.T.; Tian, L., Deciding bisimilarity of normed context-free processes is in ∑^{p}2, () · Zbl 0801.68058
[5] Park, D.M.R., Concurrency and automata on infinite sequences, (), 167-183, Lecture Notes in Computer Science
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.