Dependency analysis of mobile systems

Abstract

We propose an Abstract Interpretation-based static analysis for automatically detecting the dependencies between the names linkedto the agents of a mobile system. We focus our study on the mobile systems written in the π-calculus. We first refine the standard semanticsin order to restore the relation between the names and the agents thathave declared them. We then abstract the dependency relations that arealways satisfied by the names of the agents of a mobile system. That is tosay we will detect which names are always pair-wisely equal, and which names have necessarily been declared by the same recursive instance of an agent.