Replacement freeness: A criterion for separating process calculi

We introduce a new criterion to discern the relative expressiveness of process calculi. Intuitively, a calculus is replacement free if replacing a sub-process that cannot perform any visible action by an arbitrary one never affects the capability of the resulting process to perform a visible action. By relying on two slightly different formulations of our criterion we partition the set of process calculi into three classes. Then, we prove that no suitable encodings between any two of such classes exist; hence calculi belonging to different classes have different relative expressiveness. Finally, we classify many well-known variants of the mainstream calculi CCS and the π-calculus, thus demonstrating their expressiveness gaps.