ON THE DECIDABILITY OF PROCESS EQUIVALENCES FOR THE PI-CALCULUS

We present general results for showing process equivalences applied to the finite control fragment of the pi-calculus decidable. Firstly, a Finite Reachability Theorem states that up to finite name spaces and u p to a static normalisation procedure, the set of reachable agent expr essions is finite. Secondly, a Boundedness Lemma shows that no potenti al computations are missed when name spaces are chosen large enough, b ut finite. We show how these results lead to decidability for a number of pi-calculus equivalences such as strong or weak, late or early bis mulation equivalence. Furthermore, for strong late equivalence we show how our techniques can be used to adapt the well-known Paige-Tarjan a lgorithm. Strikingly, this results in a single exponential running tim e not much worse than the running time for the case of for instance CC S. Our results considerably strengthens previous results on decidable equivalences for parameter-passing process calculi.