Is Timed Branching Bisimilarity an Equivalence Indeed?

  • Wan Fokkink
  • Jun Pang
  • Anton Wijs
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3829)


We show that timed branching bisimilarity as defined by van der Zwaag [14] and Baeten & Middelburg [2] is not an equivalence relation, in case of a dense time domain. We propose an adaptation based on van der Zwaag’s definition, and prove that the resulting timed branching bisimilarity is an equivalence indeed. Furthermore, we prove that in case of a discrete time domain, van der Zwaag’s definition and our adaptation coincide.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Baeten, J.C.M., Bergstra, J.A.: Real time process algebra. Formal Aspects of Computing 3(2), 142–188 (1991)CrossRefMathSciNetGoogle Scholar
  2. 2.
    Baeten, J.C.M., Middelburg, C.A.: Process Algebra with Timing. EATCS Monograph. Springer, Heidelberg (2002)Google Scholar
  3. 3.
    Basten, T.: Branching bisimilarity is an equivalence indeed! Information Processing Letters 58(3), 141–147 (1996)zbMATHCrossRefMathSciNetGoogle Scholar
  4. 4.
    van Glabbeek, R.J.: The linear time – branching time spectrum II: The semantics of sequential systems with silent moves. In: Best, E. (ed.) CONCUR 1993. LNCS, vol. 715, pp. 66–81. Springer, Heidelberg (1993)Google Scholar
  5. 5.
    van Glabbeek, R.J.: What is branching time and why to use it? In: Nielsen, M. (ed.) The Concurrency Column. Bulletin of the EATCS, vol. 53, pp. 190–198 (1994)Google Scholar
  6. 6.
    van Glabbeek, R.J., Weijland, W.P.: Branching time and abstraction in bisimulation semantics. In: Ritter, G. (ed.) Proceedings of the IFIP 11th World Computer Congress (Information Processing 1989), San Francisco, pp. 613–618 (1989)Google 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.
    Groote, J.F., Reniers, M.A., van Wamel, J.J., van der Zwaag, M.B.: Completeness of timed μCRL. Fundamenta Informaticae 50(3/4), 361–402 (2002)zbMATHMathSciNetGoogle Scholar
  9. 9.
    Groote, J.F., Springintveld, J.G.: Focus points and convergent process operators. A proof strategy for protocol verification. Journal of Logic and Algebraic Programming 49(1/2), 31–60 (2001)zbMATHCrossRefMathSciNetGoogle Scholar
  10. 10.
    Fokkink, W.J., Pang, J.: Formal verification of timed systems using cones and foci. In: Ulidowski, I. (ed.) Proceedings of the 6th Workshop on Real-Time Systems (ARTS 2004), Stirling. ENTCS (2005) (to appear)Google Scholar
  11. 11.
    Klusener, A.S.: Abstraction in real time process algebra. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1991. LNCS, vol. 600, pp. 325–352. Springer, Heidelberg (1992)CrossRefGoogle Scholar
  12. 12.
    Klusener, A.S.: The silent step in time. In: Cleaveland, W.R. (ed.) CONCUR 1992. LNCS, vol. 630, pp. 421–435. Springer, Heidelberg (1992)CrossRefGoogle Scholar
  13. 13.
    Klusener, A.S.: Models and Axioms for a Fragment of Real Time Process Algebra. PhD thesis, Eindhoven University of Technology (1993)Google Scholar
  14. 14.
    van der Zwaag, M.B.: The cones and foci proof technique for timed transition systems. Information Processing Letters 80(1), 33–40 (2001)zbMATHCrossRefMathSciNetGoogle Scholar
  15. 15.
    van der Zwaag, M.B.: Models and Logics for Process Algebra. PhD thesis, University of Amsterdam (2002)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Wan Fokkink
    • 1
    • 3
  • Jun Pang
    • 2
  • Anton Wijs
    • 3
  1. 1.Department of Theoretical Computer ScienceVrije Universiteit AmsterdamAmsterdamThe Netherlands
  2. 2.INRIA Futurs and LIX, École PolytechniquePalaiseauFrance
  3. 3.Department of Software EngineeringCWIAmsterdamThe Netherlands

Personalised recommendations