More Web Proxy on the site http://driver.im/

article

Free access

Bisimulation can't be traced

Authors:

Albert R. MeyerAuthors Info & Claims

Journal of the ACM (JACM), Volume 42, Issue 1

Pages 232 - 268

https://doi.org/10.1145/200836.200876

Published: 03 January 1995 Publication History

Abstract

In the concurrent language CCS, two programs are considered the same if they are bisimilar. Several years and many researchers have demonstrated that the theory of bisimulation is mathematically appealing and useful in practice. However, bisimulation makes too many distinctions between programs. We consider the problem of adding operations to CCS to make bisimulation fully abstract. We define the class of GSOS operations, generalizing the style and technical advantages of CCS operations. We characterize GSOS congruence in as a bisimulation-like relation called ready-simulation. Bisimulation is strictly finer than ready simulation, and hence not a congruence for any GSOS language.

References

[1]

~ABRAMSKY, S. 1987. Observation equivalence as a testing equivalence. Theoret. Cortlpttt. Sci. ~53, 2/3, 225-241.

[2]

~ABRAMSKY, S. 1989. Tutorial on concurrency. Slides of an invited lecture given at the 16th ~Annual ACM Symposium on Principles of Programming Languages, (Austin, Tex., Jan. 11-13).

[3]

~AaRAMSKY, S. 1991. A domain equation for bisimulation. Inf. Comput. 92, 161-218.

[4]

~ABRAMSKY, S., AND VICKERS, S. 1989. Observational logic and process semantics. In prepara- ~tion.

[5]

~AUSTRY, D., AND BOUDOL, O. 1984. Atg~bre de processus et synchronisation. Theoret. Comput. ~Sci. 30, 1, 91-131.

[6]

~BAETEN, J. C.M. 1990. Applications of process algebra. In Cambridge Tracts in Theoretical ~Computer Sctence, vol. 17. Cambridge University Press, New York, NY.

[7]

~BAETEN, J. C. M., AND VAN GLABBEEK, R. 1987. Another look at abstraction in process ~algebra. In Automata, Languages, and Programming: 14th International Colloqium, T. Ottmann, ~ed. Lecture Notes in Computer Science, vol. 267. Springer-Verlag, New York. July.

[8]

~BAETEN, J. C. M., AND WEIJLAND, W.P. 1990. Process Algebra. Cambridge Tracts in Theoreti- ~cal Computer Science 18. Cambridge University Press.

[9]

~BARENDREGT, H.P. 1981/1984. The Lambda Calculus: Its Syntax and Semantics. In Studies in ~Logtc, vol. 103. North-Holland, Amsterdam, The Netherlands.

[10]

~BERGSTRA, J. A. AND KLOP, J.W. 1984. Process algebra for synchronous communication. Inf. ~Comput. 60, 1-3, 109-137.

[11]

~BERGSTRA, J. A., AND KLOP, J.W. 1985. Algebra of communicating processes with abstraction. ~Theoret. Cornput. Scl. 37, 1, 77-121.

[12]

~BLOOM, B. 1987. Computational complexity of bisimulation in SCCS. Unpublished.

[13]

~BLOOM, B. 1988. Can LCF be topped?: Flat lattice models of the simply typed A-calculus. In ~Proceedings of the 3rd Annual Symposturn on Logtc m Computer Science. Computer Society Press, ~pp. 282-295.

[14]

~BLOOM, B. 1984. Ready simulation, bisimulation, and the semantics of CCS-like languages. ~Ph.D dissertation. Massachusetts Institute of Technology, Cambridge, Mass., Aug.

[15]

~BLOOM, B. 1993. Structural operational semantics for weak bisimulations. Technical Report ~TR 93-1373, Cornell Univ., Ithaca, N.Y. (Aug.) (Theoret. Comput. Sci., to appear).

[16]

~BLOOM, B., ISTRAIL, S., AND MEYER, A. R. 1988. Bisimulation can't be traced (preliminary ~report). In Conference Record of the 15th Annual ACM Symposium on Principles of Programming ~Languages (San Diego, Calif., Jan 13-15) ACM, New York, pp. 229-239. (Also appears as MIT ~Tech. Memo MIT/LCS/TM-345. MIT, Cambridge, Mass.)

[17]

~BLOOM, B., ISTRAIL, S., AND MEYER, A.R. 1990. Bisimulation can't be traced. Tech. Rep. TR ~90-1150. Cornell Univ., Ithaca, N.Y., (Aug.).

[18]

~BLOOM, B., AND MEYER, h.R. 1992. Experimenting with process equivalence. Theoret. Corn- ~put. Sci. 102, 1 (Nov.), 223-237.

[19]

~BLOOM, B., AND PAINE, R. 1992. Computing ready simulations efficiently. In Proceedings of the ~North American Process Algebra Workshop '92. Workshops in Computer Science, Springer-Verlag, ~New York, pp. 119-134.

[20]

~BROOKES, S. 1983. A semantics and proof system for communicating processes. Tech. Rep. ~CMU-CS-83-134. Carnegie-Mellon University, Pittsburgh, Pa.

[21]

~BROOKES, S. D., HOARE, C. A. R., AND ROSCOE, A. W. 1984. A theory of communicating ~sequential processes. J. ACM 31, 3 (July), 560-599.

[22]

~CASTELLANO, L., MICHELIS, G. D., AND POMELLO, L. 1987. Concurrency vs interleaving: An ~instructive example. Bull. Europ. Ass. Theoret. Cornput. Sci. 31 (Feb.) 12-15.

[23]

~DE NICOLA, R., AND HENNESSY, M. C.B. 1984. Testing equivalences for processes. Theoret. ~Comput. Sci. 34, 2/3, 83-133.

[24]

~DE SIMONE, R. 1985. Higher-level synchronising devices in MEIJE-SCCS. Theoret. Comput. Sci. ~37, 3, 245-267.

[25]

~GROOTE, J. F., AND VAANDRAGER, F. 1989. Structured operational semantics and bisimulation ~as a congruence (extended abstract). In Automata, Languages and Programming.' 16th Interna- ~tional Colloquium, G. Ausiello, M. Dezani-Ciancaglini, and S. R. D. Rocca, eds. Lecture Notes ~in Computer Science, vol. 372. Springer-Verlag, New York, pp. 423-438.

[26]

~HENNESSY, M. AND MILNER, R.1985. Algebraic laws for nondeterminism and concurrency. J. ~ACM 32, 1 (Jan.), 137-161.

[27]

~HOARE, C. A. R. 1978. Communicating sequential processes. Commun. ACM, 21, 8 (Aug.), ~666-677.

[28]

~HOARE, C. A. R. 1985. Communicating Sequential Processes. Series in Computer Science. ~Prentice-Hall.

[29]

~LARSEN, K., AND SKOU, h. 1988. Bisimulation through probabilistie testing (preliminary report). ~Tech. Rep. R 88-16. Institut for Elektroniske Systemer, Aalborg Universitetscenter, Aalborg, ~Denmark, June.

[30]

~LARSEN, K. G., AND SKOU, A. 1991. Bisimulation through probabilistic testing. Inf. Comput. 94, ~1 (Sept.), 1-28.

[31]

~MEYER, A.R. 1988. Semantical paradigms: Notes for an invited lecture, with two appendices ~by Stavros Cosmadakis. In Proceedings of the 3rd Annual Symposium on Logic in Computer ~Science, Computer Society Press, Washington, D.C., pp. 236-253.

[32]

~MmNER, R. A Calculus of Communicating Systems. In Lecture Notes in Computer Science, vol. 92. ~Springer-Verlag, New York.

[33]

~MmNER, 1981. A modal characterisation of observable machine-behaviour. In CAAP '81: Trees ~in Algebra and Programming, 6th Colloquium, E. Astesiano and C. B~3hm, eds. Lecture Notes in ~Computer Science, vol. 112. Springer-Verlag, New York, pp. 25-34.

[34]

~MmNER, R. 1983. Calculi for synchrony and asynchrony. Theoret. Comput. Sci., 25, 3, 267-310.

[35]

~MILNER, R. 1984. Lectures on a calculus for communicating systems. In Seminar on Concur- ~rency: CMU, Jtdy 9-11, 1984, S. D. Brookes, A. W. Roscoe, and G. Winskel, eds. Lecture Notes ~in Computer Science, vol. 197. Springer-Verlag, New York, pp. 197-220.

[36]

~MILNER, R. 1989. Communication and Concurrency. Prentice Hall International Series in ~Computer Science. Prentice Hall, New York.

[37]

~MILNER, R. 1990. Functions as processes. In Automata, Languages and Programming: 17th ~International Colloqium, M. Paterson, ed., Lecture Notes in Computer Science, vol. 443. ~Springer-Verlag, New York, pp. 167-180.

[38]

~MILNER, R., PARROW, J., AND WALKER, D. 1992. A calculus of mobile processes I and II. Inf. ~Comput. 100, 1-40 and 41-77.

[39]

~OLDEROG, E.-R., AND HOARE, C. A.R. 1986. Specification-oriented semantics for communicat- ~ing processes. Acta Inf. 23, 1, 9-66.

[40]

~PARROW, J. 1987. Verifying a CSMA/CD-protocol with CCS. Tech. Rep. ECS-LFCS-87-18, ~Laboratory for Foundations of Computer Science. University of Edinburgh, Scotland, Jan.

[41]

~PLOTKIN, G.D. 1977. LCF considered as a programming language. Theoret. Comput. Sci. 5, 3, ~223-255.

[42]

~PLOTK1N, G. 1981. A structural approach to operational semantics. Tech. Rep. DAIMI FN-19. ~Computer Science Department, Aarhus Univ., Denmark.

[43]

~PLOTKIN, G., AND PRATT, V. 1988. Teams can see pomsets. Manuscript available as pub/pp.tex ~by anonymous FTP from Boole. Stanford.EDU, Oct.

[44]

~PNUELI, A. 1985. Linear and branching structures in the semantics and logics of reactive ~systems. In Automata, Languages and Programming: 12th Colloquium, W. Brauer, ed. Lecture ~Notes in Computer Science, vol. 194. Springer-Verlag, New York, pp. 15-32.

[45]

~ULIDOWSKh I. 1992. Equwalences on observable processes. In Proceedings of the 7th Annual ~IEEE Symposium on Logic in Computer Science IEEE, New York, pp. 148-161.

[46]

~VAN GL,~BEEK, R. 1993. The linear time-branching time spectrum II: The semantics of ~sequential processes with silent moves. In Proceedings of CONCUR '93. E. Best, ed. Lecture ~Notes in Computer Science, vol. 715. Springer-Verlag, New York, pp. 66-81 (paper also ~available by anonymous ftp from Boole.stanford.edu.).

[47]

~WEBER, S., BLOOM, g., AND BROWN, G. 1992. Compiling joy to silicon: A verified silicon ~compilation scheme. In Proceedings of the Advanced Research in I/LSI and Parallel Systems ~Conference, T. Knight and J. Savage, eds. p. 79-98.

Cited By

Kori MWatanabe KRot JKatsumata SSobocinski PLago UEsparza J(2024)Composing Codensity BisimulationsProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662139(1-13)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662139
Castiglioni VLanotte RTini S(2024)Back to the format: A survey on SOS for probabilistic processesJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2023.100929137(100929)Online publication date: Feb-2024
https://doi.org/10.1016/j.jlamp.2023.100929
Voogd EJohnsen EKløvstad ÅRot JSilva A(2024)Correct and Complete Symbolic Execution for FreeIntegrated Formal Methods10.1007/978-3-031-76554-4_13(237-255)Online publication date: 13-Nov-2024
https://doi.org/10.1007/978-3-031-76554-4_13
Show More Cited By

Recommendations

Bisimulation Can''t Be Traced
Bisimulation on speed: a unified approach

Two process-algebraic approaches have been developed for comparing two bisimulation-equivalent processes with respect to speed: the one of Moller/Tofts equips actions with lower time bounds, while the other by Lüttgen/Vogler considers upper time bounds ...
Bisimulation on speed: worst-case efficiency

This paper introduces a novel (bi)simulation-based faster-than preorder which relates asynchronous processes, where the relative speeds of system components are indeterminate, with respect to their worst-case timing behavior. The study is conducted for ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Journal of the ACM

Journal of the ACM Volume 42, Issue 1

Jan. 1995

289 pages

ISSN:0004-5411

EISSN:1557-735X

DOI:10.1145/200836

Issue’s Table of Contents

Copyright © 1995 ACM.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 03 January 1995

Published in JACM Volume 42, Issue 1

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

268
Total Citations
View Citations
1,369
Total Downloads

Downloads (Last 12 months)121
Downloads (Last 6 weeks)20

Reflects downloads up to 21 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Kori MWatanabe KRot JKatsumata SSobocinski PLago UEsparza J(2024)Composing Codensity BisimulationsProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662139(1-13)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662139
Castiglioni VLanotte RTini S(2024)Back to the format: A survey on SOS for probabilistic processesJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2023.100929137(100929)Online publication date: Feb-2024
https://doi.org/10.1016/j.jlamp.2023.100929
Voogd EJohnsen EKløvstad ÅRot JSilva A(2024)Correct and Complete Symbolic Execution for FreeIntegrated Formal Methods10.1007/978-3-031-76554-4_13(237-255)Online publication date: 13-Nov-2024
https://doi.org/10.1007/978-3-031-76554-4_13
Aceto LCrescenzi PIngólfsdóttir AMousavi M(2023)The Way We Were: Structural Operational Semantics Research in PerspectiveElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.387.3387(26-40)Online publication date: 14-Sep-2023
https://doi.org/10.4204/EPTCS.387.3
Cimini M(2023)A Declarative Validator for GSOS LanguagesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.378.2378(14-25)Online publication date: 13-Apr-2023
https://doi.org/10.4204/EPTCS.378.2
Goncharov SMilius SSchröder LTsampas SUrbat H(2023)Towards a Higher-Order Mathematical Operational SemanticsProceedings of the ACM on Programming Languages10.1145/35712157:POPL(632-658)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571215
Urbat HTsampas SGoncharov SMilius SSchröder L(2023)Weak Similarity in Higher-Order Mathematical Operational Semantics2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1109/LICS56636.2023.10175706(1-13)Online publication date: 26-Jun-2023
https://doi.org/10.1109/LICS56636.2023.10175706
Ameur-Boulifa RHenrio LMadelaine E(2023)Compositional equivalences based on open pNetsJournal of Logical and Algebraic Methods in Programming10.1016/j.jlamp.2022.100842131(100842)Online publication date: Feb-2023
https://doi.org/10.1016/j.jlamp.2022.100842
Cimini M(2023)Testing Languages with a Languages-as-Databases ApproachTests and Proofs10.1007/978-3-031-38828-6_7(108-126)Online publication date: 18-Jul-2023
https://dl.acm.org/doi/10.1007/978-3-031-38828-6_7
Aceto LCastiglioni VFokkink WIngólfsdóttir ALuttik B(2022)Are Two Binary Operators Necessary to Obtain a Finite Axiomatisation of Parallel Composition?ACM Transactions on Computational Logic10.1145/352953523:4(1-56)Online publication date: 20-Oct-2022
https://dl.acm.org/doi/10.1145/3529535
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents