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

## Tool

We have developed a tool, Psi Calculi Workbench, for implementing and analysing Psi-calculi. It implements the symbolic semantics and provides a symbolic simulator and a weak bisimulation generator.

## Publications

In Journal of Logic and Algebraic Programming, volume 81, number 3, pp 162-180, Elsevier, 2012. (DOI).
In Logical Methods in Computer Science, volume 7, number 1, p 11, 2011. (DOI).
Johannes Borgström, Shuqin Huang, Magnus Johansson, Palle Raabjerg, Björn Victor, Johannes Åman Pohjola, and Joachim Parrow. In Software Engineering and Formal Methods: SEFM 2011, volume 7041 of Lecture Notes in Computer Science, pp 74-89, Springer Berlin/Heidelberg, Berlin, 2011. (DOI, fulltext).
In Proc. 25th Symposium on Logic in Computer Science: LICS 2010, pp 322-331, IEEE, Piscataway, NJ, 2010. (DOI).
In Proc. 6th Workshop on Structural Operational Semantics: SOS 2009, volume 18 of Electronic Proceedings in Theoretical Computer Science, pp 17-31, 2010. (DOI).
In Theorem Proving in Higher Order Logics: Proceedings of TPHOLs 2009, volume 5674 of Lecture Notes in Computer Science, pp 99-114, Springer-Verlag, Berlin, 2009. (DOI).
In Proc. 24th Annual IEEE Symposium on Logic in Computer Science, pp 39-48, IEEE, Piscataway, NJ, 2009. (DOI).

x

## Search result appears here...

Notable workshops:

• BEAT 2, the 2nd International Workshop on Behavioural Types.
• EXPRESS/SOS 2013, Combined 20th International Workshop on Expressiveness in Concurrency and 10th Workshop on Structural Operational Semantics.

PhD theses: