On the decidability of fragments of the asynchronous π-calculus

We study the decidability of a reachability problem for various fragments of the asynchronous π-calculus. We consider the combination of three main features: name generation, name mobility, and unbounded control. We show that the combination of name generation with either name mobility or unbounded control leads to an undecidable fragment. On the other hand, we prove that name generation without name mobility and with bounded control is decidable by reduction to the coverability problem for Petri Nets.