Research in Theory for Concurrent Systems

We study and develop mathematical and logical theories and models for concurrent systems, including tools and applications.

• Johannes Borgström, Associate Professor
• Lars-Henrik Eriksson, Associate Professor
• Joachim Parrow, Professor
• Anke Stüber, PhD Student
• Björn Victor, Professor
• Tjark Weber, Associate Professor

Nominal Modal Logics

We define a general notion of transition system where states and action labels can be from arbitrary nominal sets, actions may bind names, and state predicates from an arbitrary logic define properties of states. A Hennessy-Milner logic for these systems is introduced, and proved adequate and expressively complete for bisimulation equivalence. A main technical novelty is the use of finitely supported infinite conjunctions. We show how to treat different bisimulation variants such as early, late, open and weak in a systematic way, explore the folklore theorem that state predicates can be replaced by actions, and make substantial comparisons with related work. The main definitions and theorems have been formalised in Nominal Isabelle. Hear about it here: [1]

Applied Calculi

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.

Interactive Theorem Proving

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.

A video playlist explaining our results on nominal modal logic.

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.

Our research is partly funded by

• 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.

Basic Calculi

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.

Projects

The Uppsala Programming for Multicore Architectures Research Center (UPMARC), was supported by a 10-year Linnaeus grant from the Swedish Research Council.

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.

• Michael Baldamus
• Jesper Bengtson
• Volkan Cambazoglu
• Sofia Cassel
• Arve Gengelbach
• Ramunas Gutkovas
• Magnus Johansson
• Amin Khorsandi
• Sophia Knight
• David Koll, visiting researcher (U Göttingen)
• Jan Kudlicka
• Edith Ngai
• 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