Affiliations: Department of Computer Science Vrije Universiteit,
Amsterdam & Department of Software Engineering, CWI, Amsterdam, The
Netherlands. wanf@cs.vu.nl | Faculté des Sciences, de la Technologie
et de la Communication Université du Luxembourg, France.
jun.pang@uni.lu | Faculté des Sciences Mirande INRIA /
VASY, Dijon, France. Anton.Wijs@inria.fr
Note: [] Address for correspondence: Vrije Universiteit Amsterdam,
Department of Computer Science, De Boelelaan 1081a, 1081 HV Amsterdam, The
Netherlands. wanf@cs.vu.nl
Abstract: 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.
