Timers for Distributed Systems

We deal with temporal aspects of distributed systems, introducing and studying a new model called timed distributed π-calculus. This model extends distributed π-calculus with timers, transforming the communication channels into temporary resources. Distributed π-calculus describes located interactions between processes with restricted access to resources. We introduce time constraints by considering timeout timers for channels. Combining these timers with types and locations, we provide a formal framework able to describe complex systems with constraints on time and on resource access. Its typing system and operational semantics are presented. It is proved that the passage of time does not interfere with the typing system. The new model is proved to be sound by using a method based on subject reduction.     

On the representation of McCarthy's in the -calculus

We study the encoding of , the call-by-name λ-calculus enriched with McCarthy's amb operator, into the π-calculus. Semantically, amb is a challenging operator, for the fairness constraints that it expresses. We prove that, under a certain interpretation of divergence in the λ-calculus (weak divergence), a faithful encoding is impossible. However, with a different interpretation of divergence (strong divergence), the encoding is possible, and for this case we derive results and coinductive proof methods to reason about that are similar to those for the encoding of pure λ-calculi. We then use these methods to derive the most important laws concerning amb. We take bisimilarity as behavioural equivalence on the π-calculus, which sheds some light on the relationship between fairness and bisimilarity.     

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.     

Probabilistic π-Calculus and Event Structures

This paper proposes two semantics of a probabilistic variant of the π-calculus: an interleaving semantics in terms of Segala automata and a true concurrent semantics, in terms of probabilistic event structures. The key technical point is a use of types to identify a good class of non-deterministic probabilistic behaviours which can preserve a compositionality of the parallel operator in the event structures and the calculus. We show an operational correspondence between the two semantics. This allows us to prove a “probabilistic confluence” result, which generalises the confluence of the linearly typed π-calculus.     

Coordination by Timers for Channel-Based Anonymous Communications

In this paper we present a new model for timed coordination of communicating distributed processes. The proposed model is an extension of the π-calculus with locations, types, and timers. Types are used to express restricted access to distributed resources. Timers define timeouts for both communication channels and resources. We define the syntax of the model and its operational semantics and provide a few results regarding the typing system and the timers. A timed barbed bisimulation relation is defined to compare the processes. Coordination is given in two stages: by strategically assigning values to timers, and then by employing a set of additional coordination rules. The timed coordination aspects are given through a coordinator pair. It consists of a timers assigning function which can be changed dynamically, and a set of coordination rules. As an illustrating example, we relate our model with the channels of the Reo coordination model.     

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π.     

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.     

Secrecy and group creation

We add an operation of group creation to the typed π-calculus, where a group is a type for channels. Creation of fresh groups has the effect of statically preventing certain communications, and can block the accidental or malicious leakage of secrets. Intuitively, no channel belonging to a fresh group can be received by processes outside the initial scope of the group, even if those processes are untyped. We formalize this intuition by adapting a notion of secrecy introduced by Abadi, and proving a preservation of secrecy property.     

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.     

A Model in κ for DNA Addition

DNA computing is a hot research topic in recent years. Formalization and verification using theories(π-calculus, bioambients, κ-calculus and etc.) in Computer Science attract attention because it can help prove and predict to a certian degree various kinds of biological processes. Combining these two aspects, formal methods can be used to verify algorithms in DNA computing, including basic arithmetic operations if they are to be included in a DNA chip. In this paper, we first introduce a newly-designed algorithm for solving binary addition with DNA, which contributes to a unit in DNA computer processor, and then formalize the algorithm in κ-calculus(a formal method well suited for describing protein interactions) to show the correctness of it in a sense, and a sensible example is provided. Finally, some discussion on the described model is made, in addition to a few possible future improvement directions.     

Biological Transactions for Quantitative Models

In this work an extension of stochastic π-calculus with biological transactions is presented. This permits to model multi-reactant multi-product reactions as atomic actions when quantitative information are given. First, the syntax and the semantics are defined, then some transaction properties are discussed. Finally, some examples are described.     

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.     

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.     

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.     

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.     

Interaction Nets vs. the ρ-calculus: Introducing Bigraphical Nets

The ρ-calculus generalises both term rewriting and the λ-calculus in a uniform framework. Interaction nets are a form of graph rewriting which proved most successful in understanding the dynamics of the λ-calculus, the prime example being the implementation of optimal β-reduction. It is thus natural to study interaction net encodings of the ρ-calculus as a first step towards the definition of efficient reduction strategies. We give two interaction net encodings which bring a new understanding to the operational semantics of the ρ-calculus; however, these encodings have some drawbacks and to overcome them we introduce bigraphical nets—a new paradigm of computation inspired by Lafont's interactions nets and Milner's bigraphs.     

What is a “Good” Encoding of Guarded Choice?

The π-calculus with synchronous output and mixed-guarded choices is strictly more expressive than the π-calculus with asynchronous output and no choice. This result was recently proved by C. Palamidessi and, as a corollary, she showed that there is no fully compositional encoding from the former into the latter that preserves divergence-freedom and symmetries. This paper argues that there are nevertheless “good” encodings between these calculi. In detail, we present a series of encodings for languages with (1) input-guarded choice, (2) both input- and output-guarded choice, and (3) mixed-guarded choice, and investigate them with respect to compositionality and divergence-freedom. The first and second encoding satisfy all of the above criteria, but various “good” candidates for the third encoding—inspired by an existing distributed implementation—invalidate one or the other criterion. While essentially confirming Palamidessi's result, our study suggests that the combination of strong compositionality and divergence-freedom is too strong for more practical purposes.