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
- 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.
Concurrent systems often exhibit subtle behavior, and reasoning about their correctness can require long and intricate arguments. Interactive theorem proving allows to develop fully formal, machine-checked proofs through human-computer collaboration. The theorem prover keeps track of every detail and allows no gaps in reasoning. As a result, we obtain theorems about the theory and behavior of concurrent systems that are extremely trustworthy.
We currently use the interactive 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 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
- Volkan Cambazoglu, PhD Student
- 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