We propose an abstract interpretation-based analysis for automatically proving non-trivial properties of mobile systems of processes. We focus on properties relying on the number of occurrences of processes during computation sequences, such as mutual exclusion and non-exhaustion of resources. We design a non-standard semantics for the pi-calculus in order to explicitly trace the origin of channels and to solve efficiently problems set by alpha-conversion and non-deterministic choices. We abstract this semantics into an approximate one. The use of a relational domain for counting the occurrences of processes allows us to prove quickly and efficiently properties such as mutual exclusion and non-exhaustion of resources. The results obtained are to the best of our knowledge much more precise than those obtained with other published analyses for mobile systems. At last, dynamic partitioning allows us to detect some configurations by which no infinite computation sequences can pass.