Bisimulation for higher-order process calculi

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 %, if static binding is assumed, both the standard definition of bisimulation (i.e., the one for CCS and related calculi), as well as higher-order bisimulation \cite{AsGi88,Bou89,Tho90} are in general unsatisfactory, because over-discriminating. 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. A major goal of the paper is to find characterisations which make bisimilarities easier to verify. An important role in our theory is played by the factorisation theorem: When comparing the behaviour of two processes, it allows us to «isolate» subcomponents which might cause differences, so that the analysis can be concentrated on them.