On Hierarchical Communication Topologies in the pi-calculus

In this talk, I will present recent work on automatic analysis of

concurrent message-passing systems, modelled by pi-calculus terms. In

this kind of systems the number of processes and names is unbounded

and the communication topology changes dynamically. We are interested

in the shape invariants satisfied by the communication topology, and

the automatic inference of these invariants.  We introduce the concept

of "hierarchical" system, a pi-term where the communication topology

is shaped according to a finite forest T specifying hierarchical

relationships between names. I will illustrate the design of a static

analysis to prove a term hierarchical by means of a novel type system

that enjoys decidable inference. The soundness proof of the type

system employs a non-standard view of pi calculus reactions. By also

showing that the coverability problem for hierarchical terms is

decidable, we obtain an expressive static fragment of the pi-calculus

with decidable safety verification problems.