Research in Theory for Concurrent Systems
We study and develop mathematical and logical theories and models for concurrent systems, including tools and applications.
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
In the probabilistic programming approach to machine learning, users specify a probabilistic model as a program in a language with probabilistic primitives. The compiler and run-time of that language do not merely execute the program as written, but instead perform generic probabilistic inference for that model. Our work is in the area of probabilistic languages with a mix of discrete and continuous distributions, and treats expressiveness, semantics, and the creation of domain-specific languages for specific classes of models or inference methods.
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.
- Evidence-based Model Composition in Probabilistic Programming, supported by the Swedish Research Council.
- Trustworthy Scalable Floating-Point Reasoning, supported by the Swedish Research Council.
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 an 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
- Sofia Cassel
- Ramunas Gutkovas
- Magnus Johansson
- Amin Khorsandi
- Sophia Knight
- 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
- Johannes Åman Pohjola