BISIMULATION FOR HIGHER-ORDER PROCESS CALCULI

A higher-order process calculus is a calculus for communicating system s which contains higher-order constructs like communication of terms. We analyse the notion of bisimulation in these calculi. We argue that both the standard definition of bisimulation (i.e., the one for CCS an d related calculi), as well as higher-order bisimulation [E. Astesiano , A. Giovini, and G. Reggio, in ''STACS '88,'' Lecture Notes in Comput er Science, Vol. 294, pp. 207-226, Springer-Verlag, Berlin/New York, 1 988; G. Boudol, in ''TAPSOFT '89,'' Lecture Notes in Computer Science, Vol. 351, pp. 149-161, Springer-Verlag, Berlin/New York, 1989; B. Tho msen, Ph.D. thesis, Dept. of Computing, Imperial College, 1990] are in general unsatisfactory, because of their over-discrimination. We prop ose and study a new form of bisimulation for such calculi, called cont ext bisimulation, which yields a more satisfactory discriminanting pow er. A drawback of context bisimulation is the heavy use of universal q uantification in its definition, which is hard to handle in practice. To resolve this difficulty we introduce triggered bisimulation and nor mal bisimulation, and we prove that they both coincide with context bi simulation. In the proof, we exploit the factorisation theorem: When c omparing the behaviour of two processes, it allows us to ''isolate'' s ubcomponents which might give differences, so that the analysis can be concentrated on them. (C) 1996 Academic Press.