Research in Theory for Concurrent Systems
We study and develop mathematical and logical theories and models for concurrent systems, including tools and applications.
- Joachim Parrow, Professor, group leader
- Johannes Borgström, Associate Professor
- Volkan Cambazoglu, PhD Student
- Sofia Cassel, Researcher
- Lars-Henrik Eriksson, Associate Professor
- Arve Gengelbach, PhD Student
- Ramunas Gutkovas, PhD Student
- Sophia Knight, Postdoc
- Jan Kudlicka, PhD Student
- Edith Ngai, Associate Professor
- Anke Stüber, PhD Student
- Björn Victor, Professor
- Tjark Weber, Associate Professor
- Johannes Åman Pohjola, PhD Student
Process calculi are idealized languages for programming and description of concurrent systems. Basic calculi such as CCS and the pi-calculus isolate a few single constructs such as parallelism, scope localization, and parametric dependence. They form a basis for theory and tool developments but since they are very parsimonious they are hard to directly apply in realistic scenarios. Applied calculi remedy this by including more primitives specific for certain application areas. 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 the framework of Psi-calculi 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. Or main kind of results are:
- A simple structural operational semantics.
- Strong and weak bisimulation equivalences, with powerful uo-to techniques.
- A symbolic semantics (more complicated but better suited for implementation).
- An analysis tool, Psi Calculi Workbench, with a symbolic simulator and bisimulation generator.
- General expressiveness results and representations of other applied calculi.
- A Hennessy-Milner style modal logic.
- Extensions to multi-sorted, broadcast, priorioties, and higher-order versions.
- Applications in wireless networks.
- An archive of formal proofs of the fundamental properties, using Isabelle and its nominal package.
Correctness arguments for both basic and applied calculi can be long and error-prone. But the proofs often have a well-understood structure, and similar proofs in application-specific calculi often follow the same pattern. Therefore interactive theorem proving, which allows to track small details and identify relevant changes in definitions automatically, is a beneficial approach to prove theorems about process calculi with great confidence.
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 process calculi ever inside a theorem prover, fully covering basic aspects of strong and weak bisimulation equivalences for pi- and Psi-calculi.
Probabilistic Programming for Machine Learning
To be updated
A tool for Psi-calculi called Psi-Calculi Workbench.
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.
Our verification tool for graph grammars, the Graph Backwards Tool, can be found here.
Here are some publications by group members, in roughly chronological order. For more complete publication lists, see our individual home pages.
Our research is partly funded by
- the Uppsala Programming for Multicore Architectures Research Center (UPMARC), which is supported by a 10-year Linnaeus grant from the Swedish Research Council.
- A Framework for Parallel Programming Specifications, supported by the Swedish Research Council.
- To be updated.
Here are some examples of previous work by group members.
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.
ProFUN, was 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.
Previous members of our group include
- Michael Baldamus
- Jesper Bengtson
- Magnus Johansson
- Amin Khorsandi
- David Koll, visiting researcher (U Göttingen)
- Kirstin Peters
- Palle Raabjerg
- Ioana Rodhe
- Nadine Rohde, visiting student (TU Berlin)
- Egil Salomonsson, thesis student
- Zuowen Tan, visiting researcher
- Frank Valencia
- Christoph Wagner, visiting researcher (TU Berlin)
- Oskar Wibling
- Kidane Yemane