Applied Calculi

Motivation

When modelling real world problems in pure process algebra one soon discovers that the model becomes big and hard to understand due to a lack of more complex datatypes and constructs. To address this a few richer process algebras have emerged, e.g. the spi-calculus and the applied pi-calculus. The spi-calculus is basically a pure process algebra spiced up with security primitives, and the applied pi-calculus can be seen as a generalisation of the spi-calculus where you allow arbitrary data signatures. There are a few more calculi which all extend the pi-calculus with new primitives. In an attempt to unify these extensions and to get simpler semantics we have developed a framework in which these extensions can be formulated.

Results

We have developed Psi-calculi, a framework for defining applied calculi. By instantiating three data types and four operators that must respect a handful of requirements we show that you get a process calculus that is compositional and respects the usual structural rules. The data types are terms (used for both communication channels and data), conditions (used for tests), and assertions (used for statements about data). The operators are channel equivalence (saying which terms are deemed to be equal channels), composition (saying how to compose assertions), unit (an assertion being the unit element of the composition operator), and entailment (saying which conditions can be entailed from which assertions). In brief, the requirements on these parameters of the framework are: The channel equivalence operator must be symmetric and transitive, the composition operator must preserve logical equivalence between assertions, and the equivalence classes of assertions form an abelian monoid.

The Psi-calculi are in themselves unsuitable for some kinds of automated reasoning, and because of this we have developed a symbolic semantics for Psi-calculi. This will lead to efficient tools that can be used to do bisimulation checking. As usual with symbolic semantics we are not interested in the concrete values a process comes into contact with. Instead we have symbolic placeholders (see the nice illustration to the right where K is a placeholder). The main idea is to equip the processes with constraints on the symbolic placeholders. These constraints are accumulated as the process evolves and tests are being made on the symbolic values.

Ongoing Work

The equivalence given for Psi-calculi is of the strong kind, i.e. it does not abstract from internal actions. We are currently working on a weak variant of Psi-calculi where certain internal actions are ignored, and thus we get a coarser equivalence. It turns out that in the presence of assertions, this is not as straightforward as one would think. Therefore we are concurrently looking at barbed equivalence for weak Psi-calculi in order to get a verification that we have found the right weak equivalence.

Future work will include looking at type systems for the semantics and finish an implementation of a bimsimulation checker. When successfull we will have an efficient tool that's applicable to a potentially wide range of applications.

Publications