Psi-calculi: a framework for mobile process calculi : Cook your own correct process calculus - just add data and logic

A psi-calculus is an extension of the pi-calculus with nominal data types for data structures, logical assertions, and conditions. These can be transmitted between processes and their names can be statically scoped as in the standard pi-calculus. Expressiveness and therefore modelling convenience significantly exceed those of other formalisms: psi-calculi can capture the same phenomena as other extensions of the pi-calculus, and can be more general, e.g. by allowing structured channels, higher-order formalisms such as the lambda calculus for data structures, and predicate logic for assertions. Ample comparisons to related calculi are provided and a few significant applications are discussed. The labelled operational semantics and definition of bisimulation is straightforward, without a structural congruence. Minimal requirements on the nominal data and logic are established in order to prove general algebraic properties of psi-calculi. The purity of the semantics is on par with the pi-calculus. The theory of weak bisimulation is established, where the tau actions are unobservable. The notion of barb is defined as the output label of a communication action, and weak barbed equivalence is bisimilarity for tau actions and preservation of weak barbs in all static contexts. It is proved that weak barbed equivalence coincides with weak bisimulation equivalence. A symbolic transition system and bisimulation equivalence is presented, and shown fully abstract with respect to bisimulation congruence in the non-symbolic semantics. The symbolic semantics is necessary for an efficient implementation of the calculus in automated tools exploring state spaces, and the full abstraction property means processes are bisimilar in the symbolic setting if they are bisimilar in the original semantics. Psi-calculi remove the necessity of proving general properties every time a new mobile process calculus is defined. By properly instantiating the framework the properties are guaranteed to hold, thus removing the need to do tedious and error-prone proofs.UPMAR