26 April 2004A Paper on Power Bisimulation
I recently read the paper Power simulation and its relation to traces and failures refinement by Paul Gardiner that appears in Theoretical Computer Science Volume 309, Issues 1-3, 2 December 2003, Pages 157-176. The aim of this paper is to propose a bridge between bisimulation equivalence and failures equivalence by recasting trace and failures equivalence in the form of a bisimulation relation. This is achieved by the author by defining notions of (bi)simulation (which he calls power (bi)simulations) between sets of states in a labelled transition system that, in a precise technical sense, are bounded by a predicate transformer. In the case of trace equivalence, the predicate transformer is just requiring that one set of processes is empty iff so is the other. On the other hand, for failures equivalence, the predicate transformer requires the existence of a Smyth-ordering (see Smyth, M. B. Power domains. J. Comput. System Sci. 16 (1978), no. 1, 23--36) between the sets of initial actions afforded by the states that are included in the sets that are being related by the relation. The coincidence between failures equivalence and the corresponding largest bounded power bisimulation is proven for divergence free processes.
Apart from the formulation of these results in the language of predicate transformers, I believe that the general ideas underlying them were already present in the paper by Rocco De Nicola entitled Extensional equivalences for transition systems. Acta Inform. 24 (1987), no. 2, 211--237, where the must testing preorder of De Nicola and Hennessy was presented as a form of bisimulation for divergence free processes. (It is well known that failures equivalence coincides with this testing equivalence over divergence free processes.) These results were then extended to deal with possibly divergent processes in the paper by Rance Cleaveland and Matthew Hennessy entitled Testing Equivalence as a Bisimulation Equivalence, Formal Aspects of Computing 5(1)(1993): 1--20.
I find it very surprising that the author does not refer to any of those papers, and does not compare his contribution to those offered ibidem. Moreover, to my mind, it is totally inappropriate for a paper dealing with the notion of bisimulation not to cite the original paper by David Park, viz. Concurrency and Automata on Infinite Sequences, pp. 167-183 in Peter Deussen (Ed.): Theoretical Computer Science, 5th GI-Conference, Karlsruhe, Germany, March 23--25, 1981, Proceedings. Lecture Notes in Computer Science 104, Springer 1981, ISBN 3-540-10576-X.
Overall, I enjoyed reading this well-written paper, but I believe that the novelty of its contribution is not high. To my mind, it is also somewhat surprising that none of the referees for the paper pointed out the existence of closely related literature that the author does not cite. Moreover the author does not seem to be aware of the presence of other schools of process algebra apart from the CCS and CSP ones. Whatever lesson there is to be learned from this, I leave to any readers I may have to judge.
Last modified: Monday, 26-Apr-2004 13:51:54 CEST.