Psi-calculi: a framework for mobile processes with nominal data and logic

Abstract

The framework of psi-calculi extends the pi-calculus with nominal datatypes for data structures and for logical assertions and conditions. These can be transmitted between processes and their names can be statically scoped as in the standard pi-calculus. Psi-calculi can capture the same phenomena as other proposed extensions of the pi-calculus such as the applied pi-calculus, the spi-calculus, the fusion calculus, the concurrent constraint pi-calculus, and calculi with polyadic communication channels or pattern matching. Psi-calculi can be even more general, for example by allowing structured channels, higher-order formalisms such as the lambda calculus for data structures, and predicate logic for assertions. We provide ample comparisons to related calculi and discuss a few significant applications. Our labelled operational semantics and definition of bisimulation is straightforward, without a structural congruence. We establish minimal requirements on the nominal data and logic in order to prove general algebraic properties of psi-calculi, all of which have been checked in the interactive theorem prover Isabelle. Expressiveness of psi-calculi significantly exceeds that of other formalisms, while the purity of the semantics is on par with the original pi-calculus.

44 pages

References in corpus (3)

• Relating two standard notions of secrecy
• Formalising the pi-calculus using nominal logic
• A Fully Abstract Symbolic Semantics for Psi-Calculi

Cited by in corpus (23)

• A survey of symbolic methods for establishing equivalence-based properties in cryptographic protocols
• A Concurrent Pattern Calculus
• The Applied Pi Calculus: Mobile Values, New Names, and Secure Communication
• Ensuring Liveness Properties of Distributed Systems: Open Problems
• On the Expressiveness of Intensional Communication
• A Bisimilarity Congruence for the Applied pi-Calculus Sufficiently Coarse to Verify Privacy Properties
• An Intensional Concurrent Faithful Encoding of Turing Machines
• On the Expressiveness of Joining
• Ensuring Liveness Properties of Distributed Systems (A Research Agenda)
• A Characterisation of Open Bisimilarity using an Intuitionistic Modal Logic
• A Parametric Framework for Reversible Pi-Calculi
• A Formal Approach to the Engineering of Domain-Specific Distributed Systems
• Modal Logics for Nominal Transition Systems
• Expressiveness via Intensionality and Concurrency
• Priorities Without Priorities: Representing Preemption in Psi-Calculi
• A Sorted Semantic Framework for Applied Process Calculi
• Context-Free Session Types for Applied Pi-Calculus
• Encodability and Separation for a Reflective Higher-Order Calculus
• Actor Network Procedures as Psi-calculi for Security Ceremonies
• Reactive Turing Machines with Infinite Alphabets
• Concurrency Models with Causality and Events as Psi-calculi
• A Generic Type System for Higher-Order $\Psi$-calculi
• Psi-Calculi Revisited: Connectivity and Compositionality