Research in Theory for Mobile Processes

Objective

We study and develop mathematical and logical theories and models for mobile processes, including tools for analysing and manipulating mobile systems.

Group members

Previous members of our group include

Research Directions

Our ongoing research directions include theories and tools for applied calculi, in particular a framework for applied calculi, Psi calculi. We are also working intimately with the theorem prover Isabelle, and have formalised most proofs for the meta theory of Psi calculi.

There are many extensions of the pi-calculus where higher-level data structures and operations on them are given as primitive. These primitives make it easier to do modelling, but the drawback is that the theory of the formalisms becomes difficult and error-prone. We have developed a framework with a lean and symmetric semantics, where a wide range of applied calculi can be formulated. The instances of the framework will then get desired results for the meta theory, such as compositionality, for free. The instances only need to fulfill a handful of criteria, like symmetry for channel equivalence. We have also developed a symbolic semantics for the framework, so any instance of it will get a symbolic semantics for free. Most of the proofs have been formalised in the theorem prover Isabelle. We have developed a tool, Psi Calculi Workbench, for implementing and analysing Psi-calculi. It implements the symbolic semantics and provides a symbolic simulator and a weak bisimulation generator.

The correctness arguments involving both basic and applied calculi are long and error-prone. But the proofs often have a well understood structure, and similar proofs in application specific calculi often follow a pattern. Therefore automated support for theorem proving is a viable approach. We currently use the theorem prover Isabelle, establishing a framework based on its nominal datatype package. Our results so far include the most extensive treatment of the pi-calculus ever inside a theorem prover, fully covering basic aspects of strong and weak bisimulation equivalences.

Resources

A tool for Psi-calculi called Psi Calculi Workbench.

A web site with introductory material, bibliographies, links to researchers and groups in the field, related calculi and tools, can be found at http://lampwww.epfl.ch/mobility/.

We run the Models for Mobility mailing list for researchers in mobile calculi.

Our verification tool for pi-calculus, the Mobility Workbench, can be found here.

There is a searchable bibliography on calculi for mobile processes on the net co-maintained by us, containing over 500 references.

Our verification tool for graph grammars, the Graph Backwards Tool, can be found here.

Projects

We participate in UPMARC, a 10-year project funded by the Swedish Research Council, and ProFUN, a 5-year project funded by the Strategic Research Foundation.

PROFUNDIS was a EU-sponsored FET-Global Computing project where we collaborated with Lisbon, INRIA Sophia-Antipolis, and Pisa.

CONFER (1992-1995), LOMAPS (1993-1997), EXPRESS (1994-1997), and CONFER-2 (1996-2000) are some relevant earlier European projects where group members participated.

We also have projects supported by the Swedish Research Council.

Publications

Here we list some publications of our group members, in roughly chronological order. For more complete publication lists, see our individual home pages.

Previous work

Much of the effort of the group has been in the area of the pi-calculus. We developed the fusion calculus, which is a simplification of the pi-calculus with significantly extended expressiveness. We are also developing the Mobility Workbench (MWB), an automated tool for describing and analysing mobile processes. It handles equivalence checking, deadlock search, interactive simulation, sort inference, and model checking for the pi-calculus, and equivalence checking for the fusion calculus. Other investigations have used categorical models and History-Dependent automata.

Working from a more applied perspective we have analysed mobile ad-hoc networks. This was a collaborative effort with the computer networks research group at the department, and we compared the protocols developed in house with other approaches. Results involved analysis in the UPPAAL tool to derive timing properties and a method to avoid severe state space explosions through application specific abstractions.