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 plethora of 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.
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.
Semantics and Bisimulation
Typically the semantics of an applied calculus is quite complicated, involving different levels and quoutients on so called structural congruences. We have developed an operational semantics in a single inductive definition. It is accompanied by definitions of strong and weak bisimulation, with proofs that the operators preserve the equivalences where expected. We have also developed a theory of so called up-to techniques for proving bisimilarity. Up-to techniques minimize the proof effort by allowing basic bisimulation proofs to be combined in a rigorous way.
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.
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.
Extensions and Expressiveness
Extensions of our framework include variants with
- Multi-sorted terms and generalised pattern matching. These make it easier to directly capture existing applied calculi in our framework.
- Broadcasts, where the communication paradigm is extended to one-to-many communications. With this we model an example based on the LUNAR wireless ad-hoc network protocol.
- Priorities, where the fact that certain actions are given priority over other actions and thus inhibit them, can be explicitly represented. These can be used e.g. to encode clocks and the passing of time.
- Higher-order, where processes can be transmitted as objects in a communication.
We also study general expressiveness problems and provide criteria for when a certain dialect can express another.
We have developed Hennessy-Milner style modal logics for general nominal transition systems (of which the Psi-calculi form an example), and showed adequacy for both strong and weak bisimulation. A particular aspect is that the logics are infinitary in the sense that they admit arbitrary conjunction of infinite sets of formulas. We treat this formally and avoid paradoxes by restricting the cardinality of the sets and requiring them to be finitely supported. In this way we get a completely formal development of very expressive logics where quantifiers and fixpoints are derived constructs. We show how this subsumes many existing modal logics.
Many key results have been formally proved in the interactive theorem prover Isabelle, using the nominal data type package to represent binding constructs. The proofs scripts exceed 100K lines and represent one of the largest efforts of their kind. This ties into our related research effort on interactive theorem provers.