Decidability of bisimulation equivalence for process generating context-free languages

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Decidability of bisimulation equivalence for process generating context-free languages

Full text

Pdf (1.71 MB)

Source

Journal of the ACM (JACM) archive
Volume 40 , Issue 3 (July 1993) table of contents

Pages: 653 - 682

Year of Publication: 1993

ISSN:0004-5411

Authors

J. C. M. Baeten	Univ. of Amsterdam, Amsterdam, The Netherlands
J. A. Bergstra	Univ. of Amsterdam, Amsterdam, The Netherlands; and State Univ. of Utrecht, Utrecht, The Netherlands
J. W. Klop	CWI, Amsterdam, The Netherlands; and Free Univ., Amsterdam, The Netherlands

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 1, Downloads (12 Months): 45, Citation Count: 22

Additional Information:

references cited by index terms review collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/174130.174141 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	J. C. M. Baeten , J. A. Bergstra, Global renaming operators in concrete process algebra, Information and Computation, v.78 n.3, p.205-245, Sept. 1988 [doi>10.1016/0890-5401(88)90027-2]
	2	J. C. M. Baeten , J. A. Bergstra , J. W. Klop, On the consistency of Koomen's fair abstraction rule, Theoretical Computer Science, v.51 n.1-2, p.129-176, March 31, 1987 [doi>10.1016/0304-3975(87)90052-1]
	3	J C M Baeten , J A Bergstra , J W Klop, Decidability of bisimulation equivalence for processes generating context-free languages, Volume II: Parallel Languages on PARLE: Parallel Architectures and Languages Europe, p.94-111, March 1987, Eindhoven, The Netherlands
	4	J. C. M. Baeten , W. P. Weijland, Process algebra, Cambridge University Press, New York, NY, 1991
	5	~BERGSTRA, J. m., AND KLOP. J. W. Process algebra for synchronous communication. ~Inform. Cont. 60 (1984), 109-137.
	6	~BERGSTRA, J. m., AND KLOP, J.W. Algebra of communicating processes. In Proceedhzgs of ~tile CW1 Symposium on Mathematics and Computer Science J. W. de Bakker, M. Hazewinkel, ~and J. K. Lenstra, eds. CWI Monographs 1. North-Holland, Amsterdam, The Netherlands, ~1986, pp. 89-138.
	7	Jan A. Bergstra , Jan Willem Klop, The Algebra of Recursively Defined Processes and the Algebra of Regular Processes, Proceedings of the 11th Colloquium on Automata, Languages and Programming, p.82-94, July 16-20, 1984
	8	J. A. Bergstra , J. W. Klop , E.-R. Olderrog, Readies and failures in the algebra of communicating processes, SIAM Journal on Computing, v.17 n.6, p.1134-1177, Dec. 1988 [doi>10.1137/0217073]
	9	S. D. Brookes , C. A. R. Hoare , A. W. Roscoe, A Theory of Communicating Sequential Processes, Journal of the ACM (JACM), v.31 n.3, p.560-599, July 1984 [doi>10.1145/828.833]
	10	~CAUCAL, D. Graphes canoniques de graphes alg6briques. Rapport de Recherche 872. ~INRIA, 1988.
	11	~CAUCAL, D. Graphes canoniques de graphes alg~briques, hlformatique thdorique et Applica- ~tions (RAIRO) 24, 4 (1990), 339-352.
	12	~CAUCAL, D. Les graphs h motifs. Rapport de Recherche 958. INRIA, 1988.
	12a	Søren Christensen , Hans Hüttel , Colin Stirling, Bisimulation Equivalence is Decidable for all Context-Free Processes, Proceedings of the Third International Conference on Concurrency Theory, p.138-147, August 24-27, 1992
	13	J. W. de Bakker , Jan A. Bergstra , Jan Willem Klop , John-Jules Ch. Meyer, Linear Time and Branching Time Semantics for Recursion with Merge, Proceedings of the 10th Colloquium on Automata, Languages and Programming, p.39-51, July 18-22, 1983
	14	J W de Bakker , J J Meyer , E R Olderog , J I Zucker, Transition systems, infinitary languages and the semantics of uniform concurrency, Proceedings of the seventeenth annual ACM symposium on Theory of computing, p.252-262, May 06-08, 1985, Providence, Rhode Island, United States [doi>10.1145/22145.22174]
	15	Jan Friso Groote, A short proof of the decidability of bisimulation for normed BPA-processes, Information Processing Letters, v.42 n.3, p.167-171, May 25, 1992 [doi>10.1016/0020-0190(92)90142-I]
	16	Jan Friso Groote , Hans Hüttel, Undecidable equivalences for basic process algebra, Information and Computation, v.115 n.2, p.354-371, Dec. 1994 [doi>10.1006/inco.1994.1101]
	17	M.A. A. Harrison , M. A. Harrison, Introduction to Formal Language Theory, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1978
	18	~HOARE, C. A.R. A model for communicating sequentml processes. In O~z the Construction ~of Programs R. M. McKeag and A. M. McNaughton, eds. Cambridge Univ. Press, ~London/New York, 1980, pp. 229-243.
	19	C. A. R. Hoare, Communicating sequential processes, Prentice-Hall, Inc., Upper Saddle River, NJ, 1985
	20	John E. Hopcroft , Jeffrey D. Ullman, Introduction To Automata Theory, Languages, And Computation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
	21	Hans Hüttel, Silence is Golden: Branching Bisimilarity is Decidable for Context-Free Processes, Proceedings of the 3rd International Workshop on Computer Aided Verification, p.2-12, July 01-04, 1991
	22	~ HOTrEL, H., AND STIRLING, C. Actions speak louder than words: Proving bisimilarity for ~context-free processes. In Proceedings of 6th Annual IEEE Symposzum LICS 91. IEEE ~Computer Society Press, New York, 1991, pp. 376-385.
	23	~ HUYN{4, D. T., AND T~AN, L. On deciding readiness and failure equivalences for processes. ~Tech. Rep. UTDCS-31-90. Univ. Texas at Dallas, Dallas, Tex., Sept. 1990.
	24	Paris C. Kanellakis , Scott A. Smolka, CCS expressions, finite state processes, and three problems of equivalence, Proceedings of the second annual ACM symposium on Principles of distributed computing, p.228-240, August 17-19, 1983, Montreal, Quebec, Canada [doi>10.1145/800221.806724]
	25	~KORENJAK, A. J., AND HOPCROFT, J.E. Simple deterministic languages. In Proceedings of ~ the 7th Annual Symposium on Switching and Automata Theory (Berkeley, Calif.). 1966, pp. ~ 36-46.
	26	~MEYER, J.-J. CH. Programming calculi based on fixed point transformation: Semantics and ~applications. Ph.D. dissertation, Free University, Amsterdam, The Netherlands, 1985.
	27	R. Milner, A Calculus of Communicating Systems, Springer-Verlag New York, Inc., Secaucus, NJ, 1982
	28	~MILNER, R. A complete inference system for a class of regular behaviours. J. Comput. Syst. ~Sct. 28 (1984), 439-466.
	29	R. Milner, Communication and concurrency, Prentice-Hall, Inc., Upper Saddle River, NJ, 1989
	30	David Park, Concurrency and Automata on Infinite Sequences, Proceedings of the 5th GI-Conference on Theoretical Computer Science, p.167-183, March 23-25, 1981
	31	Arto Salomaa, Computation and automata, Cambridge University Press, New York, NY, 1985
	32	Arto Salomaa, Formal languages, Academic Press Professional, Inc., San Diego, CA, 1987
	33	Scott Allen Smolka, Analysis of communicating finite-state processes, 1984

CITED BY 22

	Jan A. Bergstra , Alban Ponse, Register-machine based processes, Journal of the ACM (JACM), v.48 n.6, p.1207-1241, November 2001
	Colin Stirling, Bisimulation and language equivalence, Logic for concurrency and synchronisation, Kluwer Academic Publishers, Norwell, MA, 2003
	Rance Cleaveland , Scott A. Smolka, Strategic directions in concurrency research, ACM Computing Surveys (CSUR), v.28 n.4, p.607-625, Dec. 1996
	Antonín Kuča , Richard Mayr, Weak bisimilarity between finite-state systems and BPA or normed BPP is decidable in polynomial time, Theoretical Computer Science, v.270 n.1-2, p.677-700, January
	Jiří Srba, Basic process algebra with deadlocking states, Theoretical Computer Science, v.266 n.1-2, p.605-630, 09/06/2001
	Irina A. Lomazova, Modeling dynamic objects in distributed systems with nested Petri nets, Fundamenta Informaticae, v.51 n.1, p.121-133, June 2002
	Faron Moller , Scott A. Smolka, On the computational complexity of bisimulation, redux, Proceedings of the Paris C. Kanellakis memorial workshop on Principles of computing & knowledge: Paris C. Kanellakis memorial workshop on the occasion of his 50th birthday, p.55-59, June 08-08, 2003, San Diego, California, USA
	Antonín Kučera, The complexity of bisimilarity-checking for one-counter processes, Theoretical Computer Science, v.304 n.1-3, p.157-183, 28 July 2003
	Luca Aceto , Wan Fokkink , Anna Ingólfsdóttir, A note on an expressiveness hierarchy for multi-exit iteration, Information Processing Letters, v.87 n.1, p.17-23, 16 July 2003
	Faron Moller , Scott Smolka , Jiří Srba, On the computational complexity of bisimulation, redux, Information and Computation, v.194 n.2, p.129-143, November 1, 2004
	Luca Aceto , Wan Fokkink , Rob van Glabbeek , Anna Ingólfsdóttir, Nested semantics over finite trees are equationally hard, Information and Computation, v.191 n.2, p.203-232, 15 June 2004
	Denis Lugiez , Philippe Schnoebelen, Decidable first-order transition logics for PA-processes, Information and Computation, v.203 n.1, p.75-113, November 25, 2005
	Haiyan Chen, Decidability of Weak Bisimilarity for a Subset of BPA, Electronic Notes in Theoretical Computer Science (ENTCS), 212, p.241-255, April, 2008
	Colin Stirling, Model-Checking Games for Typed λ-Calculi, Electronic Notes in Theoretical Computer Science (ENTCS), 172, p.589-609, April, 2007
	Antonín Kučera , Philippe Schnoebelen, A general approach to comparing infinite-state systems with their finite-state specifications, Theoretical Computer Science, v.358 n.2, p.315-333, 7 August 2006
	Luca Aceto , Wan Fokkink , Anna Ingolfsdottir , Sumit Nain, Bisimilarity is not finitely based over BPA with interrupt, Theoretical Computer Science, v.366 n.1, p.60-81, 16 November 2006
	J. C. M. Baeten , F. Corradini , C. A. Grabmayer, A characterization of regular expressions under bisimulation, Journal of the ACM (JACM), v.54 n.2, p.6-es, April 2007
	Erzsébet Csuhaj-Varjú , Alexandru Mateescu, On a Connection Between Cooperating Distributed Grammar Systems and Basic Process Algebra, Fundamenta Informaticae, v.73 n.1,2, p.37-50, April 2006
	Antonín Kučera , Petr Jančar, Equivalence-checking on infinite-state systems: Techniques and results, Theory and Practice of Logic Programming, v.6 n.3, p.227-264, May 2006
	Luca Aceto , Wan Fokkink , Anna Ingólfsdóttir, A menagerie of non-finitely based process semantics over BPA* - from ready simulation to completed traces, Mathematical Structures in Computer Science, v.8 n.3, p.193-230, June 1998
	Dorel Lucanu , Grigore Roşu , Gheorghe Grigoraş, Regular Strategies as Proof Tactics for CIRC, Electronic Notes in Theoretical Computer Science (ENTCS), 204, p.83-98, April, 2008
	Petr Jančar , Jivří Srba, Undecidability of bisimilarity by defender's forcing, Journal of the ACM (JACM), v.55 n.1, p.1-26, February 2008

INDEX TERMS

Primary Classification:
F. Theory of Computation
F.3 LOGICS AND MEANINGS OF PROGRAMS
F.3.2 Semantics of Programming Languages
Subjects: Algebraic approaches to semantics

Additional Classification:
F. Theory of Computation
F.1 COMPUTATION BY ABSTRACT DEVICES
F.1.1 Models of Computation
Subjects: Automata (e.g., finite, push-down, resource-bounded)
F.4 MATHEMATICAL LOGIC AND FORMAL LANGUAGES
F.4.3 Formal Languages
Subjects: Decision problems

General Terms:
Languages, Theory

Keywords:
bisimulation semantics, context-free grammars, process algebra, simple context-free languages

REVIEW

"Paul Cull : Reviewer"

A system of recursion equations specifies a process. This process consists of some atomic actions and two operators, + meaning “or” and .meaning “followed by.” Both operations are assumed to be more...

Collaborative Colleagues:

J. C. M. Baeten: colleagues

J. A. Bergstra: colleagues

J. W. Klop: colleagues

Adobe Acrobat

QuickTime

Windows Media Player

Real Player