Is Timed Branching Bisimilarity a Congruence Indeed?

• Autorzy: Fokkink W. , Pang J. , Wijs A.
• Języki publikacji: EN

Abstrakty

EN

We show that timed branching bisimilarity as defined by Van der Zwaag [17] and Baeten and 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. Finally, we prove that a rooted version of timed branching bisimilarity is a congruence over a basic timed process algebra containing parallelism, successful termination and deadlock.

Słowa kluczowe

EN

branching bisimilarity

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2008
• Tom: Vol. 87, nr 3-4
• Strony: 287--311
• Opis fizyczny: bibliogr. 18 poz.

Twórcy

autor

Fokkink W.

autor

Pang J.

autor

Wijs A.

• Address for correspondence: Vrije Universiteit Amsterdam, Department of Computer Science, De Boelelaan 1081a, 1081 HV Amsterdam, The Netherlands,,

Bibliografia

• [1] Baeten, J., Bergstra, J.: Real time process algebra, Formal Aspects of Computing, 3(2), 1991, 142-188.
• [2] Baeten, J., Middelburg, C.: Process Algebra with Timing, EATCS Monograph, Springer, 2002.
• [3] Basten, T.: Branching bisimilarity is an equivalence indeed!, Information Processing Letters, 58(3), 1996, 141-147.
• [4] Bergstra, J., Klop, J.: Algebra of communicating processes with abstraction, Theoretical Computer Science, 37(1), 1985, 77-121.
• [5] Fokkink, W.: Rooted branching bisimulation as a congruence, Journal of Computer and System Sciences, 60(1), 2000, 13-37.
• [6] Fokkink, W., Pang, J., Wijs, A.: Is timed branching bisimilarity an equivalence indeed?, in: Proceedings of FORMATS 2005, vol. 3829 of Lecture Notes in Computer Science, Springer, 2005, 258-272.
• [7] Glabbeek, R. v.: What is branching time and why to use it?, The Concurrency Column, Bulletin of the EATCS, 53, 1994, 190-198.
• [8] Glabbeek, R. v.,Weijland, W.: Branching time and abstraction in bisimulation semantics, in: Proceedings of Information Processing 1989, Elsevier, 1989, 613-618.
• [9] Glabbeek, R. v., Weijland, W.: Branching time and abstraction in bisimulation semantics, Journal of the ACM, 43(3), 1996, 555-600.
• [10] Groote, J., Reniers,M.,Wamel, J. v., Zwaag,M. v. d.: Completeness of timed μCRL, Fundamenta Informaticae, 50(3,4), 2002, 361-402.
• [11] Klusener, A.: Abstraction in real time process algebra, in: Proceedings of Real-Time: Theory in Practice REX Workshop, vol. 600 of Lecture Notes in Computer Science, Springer, 1991, 325-352.
• [12] Klusener, A.: The silent step in time, in: Proceedings of CONCUR 1992, vol. 630 of Lecture Notes in Computer Science, Springer, 1992, 421-435.
• [13] Klusener, A.: Models and Axioms for a Fragment of Real Time Process Algebra, Ph.D. Thesis, Technical University of Eindhoven, 1993.
• [14] Milner, R.: Communication and Concurrency, Prentice-Hall, 1989.
• [15] Reniers, M., Weerdenburg,M. v.: Action abstraction in timed process algebra: the case for an untimed tilent step, in: Proceedings of FSEN 2007, vol. 4767 of Lecture Notes in Computer Science, Springer, 2007, 287-301.
• [16] Trčka, N.: Silent Steps in Transition Systems and Markov Chains, Ph.D. Thesis, Technical University of Eindhoven, 2007.
• [17] Zwaag, M. v. d.: The cones and foci proof technique for timed transition systems, Information Processing Letters, 80(1), 2001, 33-40.
• [18] Zwaag, M. v. d.: Models and Logics for Process Algebra, Ph.D. Thesis, University of Amsterdam, 2002