On Cool Congruence Formats for Weak Bisimulations

  • Rob Jan van Glabbeek
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3722)


In TCS 146, Bard Bloom presented rule formats for four main notions of bisimulation with silent moves. He proved that weak bisimulation equivalence is a congruence for any process algebra defined by WB cool rules, and established similar results for rooted weak bisimulation (Milner’s “observational congruence”), branching bisimulation and rooted branching bisimulation. This study reformulates Bloom’s results in a more accessible form and contributes analogues for (rooted) η-bisimulation and (rooted) delay bisimulation. Moreover, finite equational axiomatisations of rooted weak bisimulation equivalence are provided that are sound and complete for finite processes in any RWB cool process algebra. These require the introduction of auxiliary operators with lookahead. Finally, a challenge is presented for which Bloom’s formats fall short and further improvement is called for.


Transition Rule Active Argument Closed Term Auxiliary Operator Structural Operational Semantic 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Aceto, L., Bloom, B., Vaandrager, F.W.: Turning SOS rules into equations. Information and Computation 111(1), 1–52 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  2. 2.
    Basten, T.: Branching bisimulation is an equivalence indeed! Information Processing Letters 58(3), 141–147 (1996)zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    Bergstra, J.A., Klop, J.W.: Algebra of communicating processes with abstraction. Theoretical Computer Science 37(1), 77–121 (1985)zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    Bloom, B.: Structural operational semantics for weak bisimulations. Theoretical Computer Science 146, 25–68 (1995)zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    Bloom, B., Istrail, S., Meyer, A.R.: Bisimulation can’t be traced. Journal of the ACM 42(1), 232–268 (1995)zbMATHCrossRefMathSciNetGoogle Scholar
  6. 6.
    Fokkink, W.J.: Rooted branching bisimulation as a congruence. Journal of Computer and System Sciences 60(1), 13–37 (2000)zbMATHCrossRefMathSciNetGoogle Scholar
  7. 7.
    van Glabbeek, R.J., Weijland, W.P.: Branching time and abstraction in bisimulation semantics. Journal of the ACM 43(3), 555–600 (1996)CrossRefMathSciNetzbMATHGoogle Scholar
  8. 8.
    Milner, R.: Operational and algebraic semantics of concurrent processes. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, ch. 19, pp. 1201–1242. Elsevier Science Publishers B.V, North-Holland (1990) Alternatively see Communication and Concurrency, Prentice-Hall International, Englewood Cliffs (1989), or A Calculus of Communication Systems. LNCS, vol. 92. Springer, Heidelberg (1980)Google Scholar
  9. 9.
    Moller, F.: The nonexistence of finite axiomatisations for CCS congruences. In: Proceedings 5th Annual Symposium on Logic in Computer Science, Philadelphia, USA, pp. 142–153. IEEE Computer Society Press, Los Alamitos (1990)CrossRefGoogle Scholar
  10. 10.
    Plotkin, G.D.: A structural approach to operational semantics. The Journal of Logic and Algebraic Programming 60–61, 17–139 (2004) First appeared in 1981CrossRefMathSciNetGoogle Scholar
  11. 11.
    de Simone, R.: Higher-level synchronising devices in Meije-SCCS. Theoretical Computer Science 37, 245–267 (1985)zbMATHCrossRefMathSciNetGoogle Scholar
  12. 12.
    Ulidowski, I.: Equivalences on observable processes. In: Proceedings 7th Annual Symposium on Logic in Computer Science, Santa Cruz, California, pp. 148–159. IEEE Computer Society Press, Los Alamitos (1992)CrossRefGoogle Scholar
  13. 13.
    Ulidowski, I., Phillips, I.: Ordered SOS rules and process languages for branching and eager bisimulations. Information & Computation 178, 180–213 (2002)zbMATHMathSciNetGoogle Scholar
  14. 14.
    Ulidowski, I., Yuen, S.: Process languages for rooted eager bisimulation. In: Palamidessi, C. (ed.) CONCUR 2000. LNCS, vol. 1877, pp. 275–289. Springer, Heidelberg (2000)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Rob Jan van Glabbeek
    • 1
  1. 1.National ICT Australia and School of Computer Science and EngineeringThe University of New South Wales 

Personalised recommendations