Bounds on Mobility

摘要

We study natural semantic fragments of the π-calculus: depth-bounded processes (there is a bound on the longest communication path), breadth-bounded processes (there is a bound on the number of parallel processes sharing a name), and name-bounded processes (there is a bound on the number of shared names). We give a complete characterization of the decidability frontier for checking if a π-calculus process in one subclass belongs to another. Our main construction is a general acceleration scheme for π-calculus processes. Based on this acceleration, we define a Karp and Miller (KM) tree construction for the depth-bounded π-calculus. The KM tree can be used to decide if a depth-bounded process is name-bounded, if a depth-bounded process is breadth-bounded by a constant κ, and if a name-bounded process is additionally breadth-bounded. Moreover, we give a procedure that decides whether an arbitrary process is bounded in depth by a given κ. We complement our positive results with undecidability results for the remaining cases. While depth- and name-boundedness are known to be Σ_1-complete, we show that breadth-boundedness is Σ_2-complete, and checking if a process has a breadth bound at most κ is Π_1-complete, even when the input process is promised to be breadth-bounded.