Precise Analysis of pi-Calculus in Cubic Time

It is known that a static analysis of pi-calculus can be done rather simply and also efficiently, i.e. in cubic time. Clearly, a static analysis should be as precise as possible. We show that it is not only desirable, but also possible to improve the precision of the analysis without worsening its asymptotic complexity. We illustrate the main principles of this efficient algorithm, we prove that it is indeed cubic and we also show that it is correct. The technique introduced here appears to be useful also for other applications, in particular, for the static analysis of languages that extend the pi-calculus.