GETCO'00 to appear Occurrence Counting Analysis for the pi-calculus Jérôme Feret Laboratoire d'Informatique de l'École Normale Supérieure ENS-LIENS, 45, rue d'Ulm, 75230 PARIS cédex 5, FRANCE Abstract 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 ?-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. At last, dynamic partitioning allows us to detect some configurations by which no infinite computation sequences can pass. 1 Introduction We are interested in automatically proving non-trivial properties of mobile systems of processes. We focus on properties relying on a good description of the multiset of processes that occur inside computation sequences, such as mutual exclusion and non-exhaustion of resources, for instance. We propose an abstract interpretation-based analysis for the full pi-calculus [19,18].
- short computation
- counting occurrences
- detecting mutual
- channel
- computation
- complexity problems
- configurations such
- standard semantics