Structured coalgebras and minimal HD-automata for the -calculus

The coalgebraic framework developed for the classical process algebras, and in particular its advantages concerning minimal realizations, does not fully apply to the π-calculus, due to the constraints on the freshly generated names that appear in the bisimulation.In this paper we propose to model the transition system of the π-calculus as a coalgebra on a category of name permutation algebras and to define its abstract semantics as the final coalgebra of such a category. We show that permutations are sufficient to represent in an explicit way fresh name generation, thus allowing for the definition of minimal realizations.We also link the coalgebraic semantics with a slightly improved version of history dependent (HD) automata, a model developed for verification purposes, where states have local names and transitions are decorated with names and name relations. HD-automata associated with agents with a bounded number of threads in their derivatives are finite and can be actually minimized. We show that the bisimulation relation in the coalgebraic context corresponds to the minimal HD-automaton.     

A CPS Encoding of Name-Passing in Higher-Order Mobile Embedded Resources

We present an encoding of the synchronous π-calculus in the calculus of Higher-Order Mobile Embedded Resources (Homer), a pure higher-order calculus with mobile processes in nested locations, defined as a simple, conservative extension of the core process-passing subset of Thomsen's Plain CHOCS. We prove that our encoding is fully abstract with respect to barbed bisimulation and sound with respect to barbed congruence. Our encoding demonstrates that higher-order process-passing together with mobile resources in (local) named locations are sufficient to express π-calculus name-passing. The encoding uses a novel continuation passing style to facilitate the encoding of synchronous communication.     

A Partition Refinement Algorithm for the π-Calculus

The partition refinement algorithm is the basis for most of the tools for checking bisimulation equivalences and for computing minimal realisations of CCS-like finite state processes. In this paper, we present a partition refinement algorithm for the π-calculus, a development of CCS where channel names can be communicated. It can be used to check bisimilarity and to compute minimal realisations of finite control processes—the π-calculus counterpart of CCS finite state processes. The algorithm is developed for strong open bisimulation and can be adapted to late and early bisimulations, as well as to weak bisimulations. To arrive at the algorithm, a few laws, proof techniques, and four characterizations of open bisimulation are proved.     

A Proof Search Specification of the π-Calculus

We present a meta-logic that contains a new quantifier (for encoding “generic judgments”) and inference rules for reasoning within fixed points of a given specification. We then specify the operational semantics and bisimulation relations for the finite π-calculus within this meta-logic. Since we restrict to the finite case, the ability of the meta-logic to reason within fixed points becomes a powerful and complete tool since simple proof search can compute this one fixed point. The quantifier helps with the delicate issues surrounding the scope of variables within π-calculus expressions and their executions (proofs). We shall illustrate several merits of the logical specifications we write: they are natural and declarative; they contain no side conditions concerning names of variables while maintaining a completely formal treatment of such variables; differences between late and open bisimulation relations are easy to see declaratively; and proof search involving the application of inference rules, unification, and backtracking can provide complete proof systems for both one-step transitions and for bisimulation.     

Open Bisimulation, Revisited

In the context of the π-calculus, open bisimulation is prominent and popular due to its congruence properties and its easy implementability. Motivated by the attempt to generalise it to the spi-calculus, we offer a new, more refined definition and show in how far it coincides with the original one.     

Linearity and bisimulation

Exploiting linear type structure, we introduce a new theory of weak bisimilarity for the π-calculus in which we abstract away not only τ-actions but also non-τ actions which do not affect well-typed observers. This gives a congruence far larger than the standard bisimilarity while retaining semantic soundness. The framework is smoothly extendible to other settings involving nondeterminism and state. As an application we develop a behavioural theory of secrecy in the π-calculus which ensures secure information flow for a strictly greater set of processes than the type-based approach, while still offering compositional verification techniques.     

Models for name-passing processes: interleaving and causal

We study syntax-free models for name-passing processes. For interleaving semantics, we identify the indexing structure required of an early labelled transition system to support the usual π-calculus operations, defining Indexed Labelled Transition Systems. For non-interleaving causal semantics we define Indexed Labelled Asynchronous Transition Systems, smoothly generalizing both our interleaving model and the standard Asynchronous Transition Systems model for CCS-like calculi. In each case we relate a denotational semantics to an operational view, for bisimulation and causal bisimulation respectively. We establish completeness properties of, and adjunctions between, categories of the two models. Alternative indexing structures and possible applications are also discussed. These are first steps towards a uniform understanding of the semantics and operations of name-passing calculi.     

Algebraic Theories for Name-Passing Calculi

In a theory of processes the names are atomic data items which can be exchanged and tested for identify. A well-known example of a calculus for name-passing is the π-calculus, where names are additionally used as communication ports. We provide complete axiomatisations of late and early bisimulation equivalences in such calculi. Since neither of the equivalences is a congruence we also axiomatise the corresponding largest congruences. We consider a few variations of the signature of the language; among these, a calculus of deterministic processes which is reminiscent of sequential functional programs with a conditional construct. Most of our axioms are shown to be independent. The axiom systems differ only by a few simple axioms and reveal the similarities and the symmetries of the calculi and the equivalences.     

Congruence of Bisimulation in a Non-Deterministic Call-By-Need Lambda Calculus

We present a call-by-need λ-calculus λ_ND with an erratic non-deterministic operator pick and a non-recursive let. A definition of a bisimulation is given, which has to be based on a further calculus named λ_≈, since the naïve bisimulation definition is useless. The main result is that bisimulation in λ_≈ is a congruence and coincides with the contextual equivalence. The proof is a non-trivial extension of Howe's method. This might be a step towards defining useful bisimulation relations and proving them to be congruences in calculi that extend the λ_ND-calculus.     

On the Expressive Power of Polyadic Synchronisation in π-calculus

We extend the π-calculus with polyadic synchronisation, a generalisation of the communication mechanism which allows channel names to be composite. We show that this operator embeds nicely in the theory of π-calculus, and makes it possible to derive divergence-free encodings of distributed calculi. We give a separation result between the π-calculus with polyadic synchronisation (^eπ) and the original calculus, in the style of an analogous result given by Palamidessi for mixed choice. We encode Local Area π showing how to control the local use of resources in ^eπ.     

Computing Bisimulations for Finite-Controlπ-Calculus

Symbolic bisimulation avoids the infinite branching problem caused by instantiating input names with all names in the standard definition of bisimulation in π-calculus.However,it does not automatically lead to an efficient algorithm,because symbolic bisimulation is indexed by conditions on names,and directly manipulating such conditions can be computationally costly.In this paper a new notion of bisimulation is introduced,in which the manipulation of maximally consistent conditions is replaced with a systematic employment of schematic names.It is shown that the new notion captures symbolic bisimulation in a precise sense.Based on the new definition an efficient algorithm,which instantiates input names “on-the -fly“,is presented to check bisimulations for finite-control π-calculus.     

π-calculus with noisy channels

It is assumed in the π-calculus that communication channels are always noiseless. But it is usually not the case in the mobile systems that developers are faced with in the real life. In this paper, we introduce an extension of π, called π_N, in which noisy channels may be present. A probabilistic transitional semantics of π_N is given. The notions of approximate (strong) bisimilarity and equivalence between agents in π_N are proposed, and various algebraic laws for them are established. In particular, we introduce the notion of stratified bisimulation which is suited to describe behavior equivalence between infinite probabilistic processes. Some useful techniques for reasoning about approximate bisimilarity and equivalence are developed. We also introduce a notion of reliability in order to compare different behaviors of an agent in π and π_N. It is shown that reliability is preserved by the basic combinators in π. A link between reliability and bisimulation is given. This provides us with a uniform framework in which we can reason about both correctness properties and reliability of mobile systems. Also, a potential way of combing value-passing process algebras and Shannon’s information theory is pointed out.     

Graphical Verification of a Spatial Logic for the π-calculus

The paper introduces a novel approach to the verification of spatial properties for finite π-calculus specifications. The mechanism is based on a recently proposed graphical encoding for mobile calculi: Each process is mapped into a (ranked) graph, such that the denotation is fully abstract with respect to the usual structural congruence (i.e., two processes are equivalent exactly when the corresponding encodings yield the same graph). Spatial properties for reasoning about the behavior and the structure of π-calculus processes are then expressed in a logic introduced by Caires, and they are verified on the graphical encoding of a process, rather than on its textual representation. More precisely, the graphical presentation allows for providing a simple and easy to implement verification algorithm based on the graphical encoding (returning true if and only if a given process verifies a given spatial formula).     

Bigraphical Semantics of Higher-Order Mobile Embedded Resources with Local Names

Bigraphs have been introduced with the aim to provide a topographical meta-model for mobile, distributed agents that can manipulate their own linkages and nested locations, generalising both characteristics of the π-calculus and the Mobile Ambients calculus. We give the first bigraphical presentation of a non-linear, higher-order process calculus with nested locations, non-linear active process mobility, and local names, the calculus of Higher-Order Mobile Embedded Resources (Homer). The presentation is based on Milner's recent presentation of the λ-calculus in local bigraphs. The combination of non-linear active process mobility and local names requires a new definition of parametric reaction rules and a representation of the location of names. We suggest localised bigraphs as a generalisation of local bigraphs in which links can be further localised.     

Linearity, Persistence and Testing Semantics in the Asynchronous Pi-Calculus

In [C. Palamidessi, V. Saraswat, F. Valencia and B. Victor. On the Expressiveness of Linearity vs Persistence in the Asynchronous Pi Calculus. LICS 2006:59–68, 2006] the authors studied the expressiveness of persistence in the asynchronous π-calculus (Aπ) wrt weak barbed congruence. The study is incomplete because it ignores the issue of divergence. In this paper, we present an expressiveness study of persistence in the asynchronous π-calculus (Aπ) wrt De Nicola and Hennessy's testing scenario which is sensitive to divergence. Following [C. Palamidessi, V. Saraswat, F. Valencia and B. Victor. On the Expressiveness of Linearity vs Persistence in the Asynchronous Pi Calculus. LICS 2006:59–68, 2006], we consider Aπ and three sub-languages of it, each capturing one source of persistence: the persistent-input calculus (PIAπ), the persistent-output calculus (POAπ) and persistent calculus (PAπ). In [C. Palamidessi, V. Saraswat, F. Valencia and B. Victor. On the Expressiveness of Linearity vs Persistence in the Asynchronous Pi Calculus. LICS 2006:59–68, 2006] the authors showed encodings from Aπ into the semi-persistent calculi (i.e., POAπ and PIAπ) correct wrt weak barbed congruence. In this paper we prove that, under some general conditions, there cannot be an encoding from Aπ into a (semi)-persistent calculus preserving the must testing semantics.     

Parametric synchronizations in mobile nominal calculi

We present and compare P-PRISMA and F-PRISMA, two parametric calculi that can be instantiated with different interaction policies, defined as synchronization algebras with mobility of names (SAMs). In particular, P-PRISMA is based on name transmission (P-SAM), like π-calculus, and thus exploits directional (input–output) communication only, while F-PRISMA is based on name fusion (F-SAM), like Fusion calculus, and thus exploits a more symmetric form of communication. However, P-PRISMA and F-PRISMA can easily accommodate many other high-level synchronization mechanisms than the basic ones available in π-calculus and Fusion, hence allowing for the development of a general meta-theory of mobile calculi. We define for both the labeled operational semantics and a form of strong bisimilarity, showing that the latter is compositional for any SAM. We also discuss reduction semantics and weak bisimilarity. We give several examples based on heterogeneous SAMs, we investigate the case studies of π-calculus and Fusion calculus giving correspondence theorems, and we show how P-PRISMA can be encoded in F-PRISMA. Finally, we show that basic categorical tools can help to relate and to compose SAMs and PRISMA processes in an elegant way.     

A fully abstract semantics for causality in the \pi-calculus

We examine the meaning of causality in calculi for mobile processes like the -calculus, and we investigate the relationship between interleaving and causal semantics for such calculi. We separate two forms of causal dependencies on actions of -calculus processes, called subject and object dependencies: The former originate from the nesting of prefixes and are propagated through interactions among processes (they are the only form of causal dependencies present in CCS-like languages); the latter originate from the binding mechanisms on names. We propose a notion of causal bisimulation which distinguishes processes which differ for the subject or for the object dependencies. We show that this causal equivalence can be reconducted to, or implemented into, the ordinary interleaving observation equivalence. We prove that our encoding is fully abstract w.r.t. the two behavioural equivalences. This allows us to exploit the simpler theory of the interleaving semantics to reason about the causal one. In [San94b] a similar programme is carried out for location bisimulation [BCHK91], a non-interleaving spatial-sensitive (as opposed to causal-sensitive) behavioural equivalence. The comparison between the encodings of causal bisimulation in this paper, and of location bisimulation in [San94b], evidences the similarities and the differences between these two equivalences. Received 11 December 1995 / 16 June 1997     

Types and full abstraction for polyadic π-calculus

A type system for terms of the monadic π-calculus is introduced and used to obtain a full-abstraction result for the translation of the polyadic π-calculus into the monadic calculus: well-sorted terms of the polyadic calculus are barbed congruent iff their translations are typed barbed congruent.     

Encoding Distributed Areas and Local Communication into the π-Calculus

We show how the π-calculus can express local communications within a distributed system, through an encoding of the local area π-calculus, an enriched system that explicitly represents names which are known universally but always refer to local information. Our translation replaces point-to-point communication with a system of shared local ethers; we prove that this preserves and reflects process behaviour. We give an example based on an internet service dæmon, and investigate some limitations of the encoding.     

Barbs and Congruences for Safe Mobile Ambients

The Ambient Calculus offers many ways in which processes can interact and be observed. In the context of Levi and Sangiorgi's Safe Mobile Ambients (SA), the extra co-capabilities required for interaction complicate the fundamental observations. We show that different formulations of barbs lead to the same barbed congruence. We prove this by following Honda and Yoshida's approach for the π-calculus by defining the insensitive terms of SA.