Department of Information Technology

Research in Theory for Concurrent Systems

Objective

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

Research Directions

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 Provers

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.

Probabilistic Programming for Machine Learning

To be updated

Resources

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.

Projects

To be updated.

  • We participate in UPMARC, a 10-year project funded by the Swedish Research Council.
  • A Framework for Parallel Programming Specifications, 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

Here are some examples of previous work by group members.

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.

Descriptions of Mobile Ad-hoc Networks

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.

Alumni

Previous members of our group include

Projects

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.

Updated  2016-08-19 10:07:01 by Joachim Parrow.