Abstract
We investigate normed commutative context-free processes (Basic Parallel Processes). We show that branching bisimilarity admits the small response property: in the Bisimulation Game, Duplicator always has a response leading to a process of size linearly bounded with respect to the Spoiler’s process. The linear bound is effective, which leads to decidability of branching bisimilarity. For weak bisimilarity, we are able merely to show existence of some linear bound, which is not sufficient for decidability. We conjecture however that the same effective bound holds for weak bisimilarity as well. We believe that further elaboration of novel techniques developed in this paper may be sufficient to demonstrate decidability.
The first author acknowledges a partial support by the Polish MNiSW grant N N206 568640. The remaining two authors acknowledge a partial support by the Polish MNiSW grant N N206 567840.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Christensen, S.: Decidability and Decomposition in process algebras. PhD thesis, Dept. of Computer Science, University of Edinburgh, UK (1993)
Christensen, S., Hirshfeld, Y., Moller, F.: Bisimulation equivalence is decidable for Basic Parallel Processes. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 143–157. Springer, Heidelberg (1993)
Esparza, J.: Petri nets, commutative context-free grammars, and Basic Parallel Processes. Fundam. Inform. 31(1), 13–25 (1997)
Fröschle, S., Lasota, S.: Normed processes, unique decomposition, and complexity of bisimulation equivalences. Electr. Notes Theor. Comp. Sci. 239, 17–42 (2009)
Hirshfeld, Y.: Congruences in commutative semigroups. Technical report, University of Edinburgh, LFCS report ECS-LFCS-94-291 (1994)
Hirshfeld, Y., Jerrum, M., Moller, F.: A polynomial-time algorithm for deciding bisimulation equivalence of normed Basic Parallel Processes. Mathematical Structures in Computer Science 6(3), 251–259 (1996)
Jancar, P.: Decidability questions for bismilarity of Petri nets and some related problems. In: Enjalbert, P., Mayr, E.W., Wagner, K.W. (eds.) STACS 1994. LNCS, vol. 775, pp. 581–592. Springer, Heidelberg (1994)
Jancar, P.: Strong bisimilarity on Basic Parallel Processes is PSPACE-complete. In: LICS, pp. 218–227 (2003)
Lasota, S.: Decidability of performance equivalence for Basic Parallel Processes. Theoretical Computer Science 360, 172–192 (2006)
Milner, R.: Communication and Concurrency. Prentice Hall, Englewood Cliffs (1995)
Srba, J.: Strong Bisimilarity and Regularity of Basic Parallel Processes Is PSPACE-Hard. In: Alt, H., Ferreira, A. (eds.) STACS 2002. LNCS, vol. 2285, pp. 535–546. Springer, Heidelberg (2002)
Srba, J.: Roadmap of Infinite results. Formal Models and Semantics, vol. 2. World Scientific Publishing Co., Singapore (2004)
Stirling, C.: The joys of bisimulation. In: Brim, L., Gruska, J., Zlatuška, J. (eds.) MFCS 1998. LNCS, vol. 1450, pp. 142–151. Springer, Heidelberg (1998)
Stirling, C.: Decidability of Weak Bisimilarity for a Subset of Basic Parallel Processes. In: Honsell, F., Miculan, M. (eds.) FOSSACS 2001. LNCS, vol. 2030, pp. 379–393. Springer, Heidelberg (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Czerwiński, W., Hofman, P., Lasota, S. (2011). Decidability of Branching Bisimulation on Normed Commutative Context-Free Processes. In: Katoen, JP., König, B. (eds) CONCUR 2011 – Concurrency Theory. CONCUR 2011. Lecture Notes in Computer Science, vol 6901. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-23217-6_35
Download citation
DOI: https://doi.org/10.1007/978-3-642-23217-6_35
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-23216-9
Online ISBN: 978-3-642-23217-6
eBook Packages: Computer ScienceComputer Science (R0)