Abstract
We present an elementary algorithm for deciding bisimulation between arbitrary context-free processes. This improves on the state of the art algorithm of Christensen, Hüttel and Stirling consisting of two semi-decision procedures running in parallel, which prohibits any complexity estimation. The point of our algorithm is the effective construction of a finite relation characterizing all bisimulation equivalence classes, whose mere existence was exploited for the above mentioned decidability result.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
J.C.M. Baeten, J.A. Bergstra, and J.W. Klop. Decidability of Bisimulation Equivalence for Processes Generating Context-Free Languages. In PARLE '87, LNCS 259, pages 94–113. Springer, 1987. Full version appeared as: Technical Report CS-R8632, CWI, Sep. 1987.
O. Burkart, D. Caucal, and S. Steffen. An Elementary Bisimulation Decision Procedure for Arbitrary Context-Free Processes. Technical Report AIB-94-28, RWTH Aachen, 1994.
J.C.M. Baeten and W.P. Weijland. Process Algebra, volume 18 of Cambridge Tracts in TCS. Cambridge University Press, 1990.
D. Caucal. A Fast Algorithm to Decide on Simple Grammars Equivalence. In Int. Symposium on Optimal Algorithms, LNCS 401, pages 66–85. Springer, 1989.
D. Caucal. Graphes Canoniques de Graphes Algébriques. RAIRO, 24(4):339–352, 1990. A preliminary, version appeared as: Rapport de Recherche 872, INRIA, July 1988.
S. Christensen, H. Hüttel, and C. Stirling. Bisimulation Equivalence is Decidable for all Context-Free Processes. In CONCUR '92, LNCS 630, pages 138–147. Springer, 1992.
R.J. van Glabbeek. The Linear Time — Branching Time Spectrum. In CONCUR 90, LNCS 458, pages 278–297. Springer, 1990.
J.F. Groote. A Short Proof of the Decidability of Bisimulation for Normed BPA-Processes. Technical Report CS-R9151, CWI, Dec 1991.
Y. Hirshfeld, M. Jerrum, and F. Moller. A Polynomial Algorithm for Deciding Bisimilarity of Normed Context-Free Processes. Technical Report ECS-LFCS-94-286, LFCS, Edinburgh, March 1994. To be presented at FOCS '94.
Y. Hirshfeld and F. Moller. A Fast Algorithm for Deciding Bisimilarity of Normed Context-Free Processes. In CONCUR '94, LNCS 836, pages 48–63, 1994.
C.A.R. Hoare. Communicating Sequential Processes. Prentice-Hall, 1985.
H. Hüttel and C. Stirling. Actions Speak Louder than Words: Proving Bisimilarity for Context-Free Processes. In LICS '91, pages 376–386. IEEE Computer Society Press, 1991.
D.T. Huynh and L. Tian. Deciding Bisimilarity of Normed Context-Free Processes is in Deciding Bisimilarity of Normed Context-Free Processes is in σ p2 . Theoretical Computer Science, 123:183–197, 1994.
R. Milner. Communication and Concurrency. Prentice-Hall, 1989.
D. Park. Concurrency and Automata on Infinite Sequences. In 5th GI Conference, LNCS 104, pages 167–183. Springer, 1981.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Burkart, O., Caucal, D., Steffen, B. (1995). An elementary bisimulation decision procedure for arbitrary context-free processes. In: Wiedermann, J., Hájek, P. (eds) Mathematical Foundations of Computer Science 1995. MFCS 1995. Lecture Notes in Computer Science, vol 969. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60246-1_148
Download citation
DOI: https://doi.org/10.1007/3-540-60246-1_148
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60246-0
Online ISBN: 978-3-540-44768-9
eBook Packages: Springer Book Archive