On modelling mobility

AbstractWe present a model of distributed computation which is based on a fragment of the π-calculus relying on asynchronous point-to-point communication. We enrich the model with the following features: the explicit distribution of processes to locations, the routing of messages, the mobility of processes, and the failure of locations and their detection. Our contributions are two folds. At the specification level, we give a synthetic and flexible formalization of the features mentioned above. At the verification level, we provide original methods to reason about the bisimilarity of processes