Abstract
Deciding strong and weak bisimilarity of BPP 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. In this paper, we present a tableau method to decide weak bisimilarity of totally normed BPP. Compared with Hirshfeld’s bisimulation tree method, our method is more intuitive and more direct. Moreover from the decidability proof we can derive a complete axiomatisation for the weak bisimulation of totally normed BPP.
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)
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.: Forthcoming Ph.D. thesis. University of Edinburgh
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)
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)
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)
R., Milner: A Calculus of Communicating 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: Prodeedings of REX Workshop, pp. 50–122. The Netherlands, Amsterdam (1988)
Caucal, D.: Graphes canoniques de graphes algébriques. Informatique théorique et Applications(RAIRO) 90-24(4), 339–352 (1990)
Dixon, L.E.: Finiteness of the odd perfct and primitive abundant numbers with distinct factors. American Journal of Mathematics 35, 413–422 (1913)
Christensen, S., Hirshfield, Y., Moller, F.: Decomposability, Decidability and Axiomatisability for Bisimulation Equivalence on Basic Parallel Processes. In: LICS 1993. Proceedings of the Eighth Annual Symposium on Logic in Computer Science, Montreal, Canada, pp. 386–396 (1993)
Jan\(\check{c}\)ar, P.: Strong bisimilarity on basic parallel processes is PSPACE-complete. In: LICS 2003. Proceedings of the 18th Annual IEEE Symposium on Logic in Computer Science, Ottawa, Canada, pp. 218-227 (2003)
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)
Srba, J.: Roadmap of Infinite Results. Bulletin of the European Association for Theoretical Computer Science 78, 163–175 (2002), columns:Concurrency
Mayr, R.: On the Complexity of Bisimulation Problems for Basic Parallel Processes. In: Welzl, E., Montanari, U., Rolim, J.D.P. (eds.) ICALP 2000. LNCS, vol. 1853, pp. 329–341. Springer, Heidelberg (2000)
Mayr, R.: Weak Bisimulation and Model Checking for Basic Parallel Processes. In: Chandru, V., Vinay, V. (eds.) FSTTCS 1996. LNCS, vol. 1180, pp. 88–99. Springer, Heidelberg (1996)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Chen, H. (2008). More on Weak Bisimilarity of Normed Basic Parallel Processes. In: Agrawal, M., Du, D., Duan, Z., Li, A. (eds) Theory and Applications of Models of Computation. TAMC 2008. Lecture Notes in Computer Science, vol 4978. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-79228-4_17
Download citation
DOI: https://doi.org/10.1007/978-3-540-79228-4_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-79227-7
Online ISBN: 978-3-540-79228-4
eBook Packages: Computer ScienceComputer Science (R0)