Abstract
Deciding strong and weak bisimilarity of context-free proce-sses are challenging because of the infinite nature of the state space of such processes. Deciding weak bisimilarity is harder since the usual decomposition property which holds for strong bisimilarity fails. Hirshfeld proposed the notion of bisimulation tree to prove that weak bisimulation is decidable for totally normed BPA and BPP processes. Suggested by his idea of decomposition, in this paper we present a tableau method for deciding weak bisimilarity of totally normed context-free processes. Compared with Hirshfeld’s bisimulation tree method, our method is more intuitive and more direct.
Supported by the National Natural Science Foundation of China under Grant Nos. 60673045, 60496321.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Moller, F.: Infinite results. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 195–216. Springer, Heidelberg (1996)
Esparza, J.: Decidability of model checking for infinite-state concurrent systems. Acta Informatica 97(34), 85–107 (1997)
burkart, O., Esparza, J.: More infinite results. Electronic Notes in Theoretical computer Science 5 (1997)
Baeten, J.C.M., Bergstra, J.A., Klop, J.W.: Decidability of bisimulation equivalence for processes generating context-free languages. Journal of the Association for Computing Machinery 93(40), 653–682 (1993)
Christensen, S., Hüttel, H., Stirling, C.: Bisimulation equivalence is decidable for all context-free processes. Information and Computation 95(121), 143–148 (1995)
Burkart, O., Caucal, D., Steffen, B.: An elementary bisimulation decision procedure for arbitrary context-free processes. In: Hájek, P., Wiedermann, J. (eds.) MFCS 1995. LNCS, vol. 969, pp. 423–433. Springer, Heidelberg (1995)
Srba, J.: Roadmap of Infinite Results. In: Current Trends in Theoretical Computer Science, The Challenge of the New Century. Formal Models and Semantics, vol. 2, pp. 337–350. World Scientific Publishing Co., Singapore (2004)
Esparza, J.: Petri nets,commutative context-free grammars, and basic parallel processes. In: Reichel, H. (ed.) FCT 1995. LNCS, vol. 965, pp. 221–232. Springer, Heidelberg (1995)
Hirshfeld, Y.: Bisimulation trees and the decidability of weak bisimulations. In: INFINITY 1996. Proceedings of the 1st International Workshop on Verification of Infinite State Systems, Germany, vol. 5 (1996)
Stirling, C.: Decidability of bisimulation equivalence for normed pushdown processes. In: Sassone, V., Montanari, U. (eds.) CONCUR 1996. LNCS, vol. 1119, pp. 217–232. Springer, Heidelberg (1996)
Hüttel, H., Stirling, C.: Actions speak louder than words. Proving bisimilarity for context-free processes. In: LICS 1991. Proceedings of 6th Annual symposium on Logic in Computer Science, Amsterdam, pp. 376–386 (1991)
Hans, H.: Silence is golden: Branching bisimilarity is decidable for context-free processes. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 2–12. Springer, Heidelberg (1992)
Mayr, R.: Weak bisimulation and regularity of BPA is EXPTIME-hard. In: EXPRESS’03. Proceedings of the 10th International Workshop on Expressiveness in Concurrency, France, pp. 143–160 (2003)
Milner, R.: A Calculus of Communication Systems. LNCS, vol. 92. Springer, Heidelberg (1980)
Milner, R.: Communication and Concurrency. Prentice-Hall International, Englewood Cliffs (1989)
Bergstra, J.A., Klop, J.W.: Process theory based on bisimulation semantics. In: Proceedings of REX Workshop, Amsterdam, The Netherlands, pp. 50–122 (1988)
Caucal, D.: Graphes canoniques de graphes algébriques. Informatique théorique et Applications (RAIRO) 90-24(4), 339–352 (1990)
Hirshfeld, Y., Jerrum, M., Moller, F.: Bisimulation equivalence is decidable for normed process algebra. In: Wiedermann, J., van Emde Boas, P., Nielsen, M. (eds.) ICALP 1999. LNCS, vol. 1644, pp. 412–421. Springer, Heidelberg (1999)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Liu, X., Chen, H. (2007). Deciding Weak Bisimilarity of Normed Context-Free Processes Using Tableau. In: Jones, C.B., Liu, Z., Woodcock, J. (eds) Theoretical Aspects of Computing – ICTAC 2007. ICTAC 2007. Lecture Notes in Computer Science, vol 4711. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-75292-9_23
Download citation
DOI: https://doi.org/10.1007/978-3-540-75292-9_23
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-75290-5
Online ISBN: 978-3-540-75292-9
eBook Packages: Computer ScienceComputer Science (R0)