Skip to Main content Skip to Navigation
Conference papers

Occurrence counting analysis for the pi-calculus

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 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.
Document type :
Conference papers
Complete list of metadata
Contributor : Jérôme Feret Connect in order to contact the contributor
Submitted on : Wednesday, October 20, 2010 - 4:11:26 PM
Last modification on : Thursday, March 17, 2022 - 10:08:35 AM

Links full text




Jérôme Feret. Occurrence counting analysis for the pi-calculus. GEometry and Topology in COncurrency theory (Satellite Workshop from CONCUR 2000), Eric Goubault, Aug 2000, University Park, United States. pp.1--18, ⟨10.1016/S1571-0661(05)01155-2⟩. ⟨inria-00527933⟩



Record views