Logo: to the web site of Uppsala University

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.

Applied process calculi include advanced programming constructs such as type systems, communication with pattern matching, encryption primitives, concurrent constraints, nondeterminism, process creation, and dynamic connection topologies. Several such formalisms, e.g. the applied pi calculus, are extensions of the the pi-calculus; a growing number is geared towards particular applications or computational paradigms.

Our goal is a unified framework to represent different process calculi and notions of computation. To this end, we extend our previous work on psi-calculi with novel abstract patterns and pattern matching, and add sorts to the data term language, giving sufficient criteria for subject reduction to hold. Our framework can directly represent several existing process calculi; the resulting transition systems are isomorphic to the originals up to strong bisimulation. We also demonstrate different notions of computation on data terms, including cryptographic primitives and a lambda-calculus with erratic choice. Finally, we prove standard congruence and structural properties of bisimulation; the proof has been machine-checked using Nominal Isabelle in the case of a single name sort.

Psi-calculi is a parametric framework for process calculi similar to popular pi-calculus extensions such as the explicit fusion calculus, the applied pi-calculus and the spi calculus. Remarkably, machine-checked proofs of standard algebraic and congruence properties of bisimilarity apply to all calculi within the framework. Bisimulation up-to techniques are methods for reducing the size of relations needed in bisimulation proofs. In this paper, we show how these bisimulation proof methods can be adapted to psi-calculi. We formalise all our definitions and theorems in Nominal Isabelle, and show examples where the use of up to-techniques yields drastically simplified proofs of known results. We also prove new structural laws about the replication operator.

This paper presents a mechanisation of psi-calculi, a parametric framework for modelling various dialects of process calculi including (but not limited to) the pi-calculus, the applied pi-calculus, and the spi calculus. psi-calculi are significantly more expressive, yet their semantics is as simple in structure as the semantics of the original pi-calculus. Proofs of meta-theoretic properties for psi-calculi are more involved, however, not least because psi-calculi (unlike simpler calculi) utilise binders that bind multiple names at once. The mechanisation is carried out in the Nominal Isabelle framework, an interactive proof assistant designed to facilitate formal reasoning about calculi with binders. Our main contributions are twofold. First, we have developed techniques that allow efficient reasoning about calculi that bind multiple names in Nominal Isabelle. Second, we have adopted these techniques to mechanise substantial results from the meta-theory of psi-calculi, including congruence properties of bisimilarity and the laws of structural congruence. To our knowledge, this is the most extensive formalisation of process calculi mechanised in a proof assistant to date.

Psi-calculi is a parametric framework for extensions of the pi-calculus, with arbitrary data structures and logical assertions for facts about data. In this paper we add primitives for broadcast communication in order to model wireless protocols. The additions preserve the purity of the psi-calculi semantics, and we formally prove the standard congruence and structural properties of bisimilarity. We demonstrate the expressive power of broadcast psi-calculi by modelling the wireless ad-hoc routing protocol LUNAR and verifying a basic reachability property.