zbMATH — the first resource for mathematics

Bisimulation for higher-order process calculi. (English) Zbl 0876.68042
Summary: A higher-order process calculus is a calculus for communicating systems 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 and related calculi), as well as higher-order bisimulation [E. Astesiano, A. Giovini and G. Reggio, in Lect. Notes Comput. Sci. 294, 207-226 (1988; Zbl 0674.68050), G. Boudol, in “TAPSOFT ’89”, Lect. Notes Comput. Sci. 351, 149-161 (1989), B. Thomsen, Ph.D. thesis, Dept. of Computing, Imperial College (1989)] are in general unsatisfactory, because of their over-discrimination. We propose and study a new form of bisimulation for such calculi, called context bisimulation, which yields a more satisfactory discriminanting power. A drawback of context bisimulation is the heavy use of universal quantification in its definition, which is hard to handle in practice. To resolve this difficulty we introduce triggered bisimulation and normal bisimulation, and we prove that they both coincide with context bisimulation. In the proof, we exploit the factorization theorem: When comparing the behaviour of two processes, it allows us to “isolate” subcomponents which might give differences, so that the analysis can be concentrated on them.

68Q10 Modes of computation (nondeterministic, parallel, interactive, probabilistic, etc.)
Full Text: DOI