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.     

Interaction in Time and Space

Distributed π-calculus and ambient calculus are extended with timers which may trigger timeout recovery processes. Timers provide a useful notion of relative time with respect to the interaction in a distributed system. The rather flat notion of space in timed distributed π-calculus is improved by considering a hierarchical representation of space in timed mobile ambients. Some basic results are proven, making sound both formal approaches. An easily understood example is used for both extensions, showing how it is possible to describe a non-monotonic behaviour and use a decentralized control to coordinate the interacting components in time and space.     

Assigning Types to Processes

In wide area distributed systems it is now common for higher-order code to be transferred from one domain to another; the receiving host may initialise parameters and then execute the code in its local environment. In this paper we propose a fine-grained typing system for a higher-order π-calculus which can be used to control the effect of such migrating code on local environments. Processes may be assigned different types depending on their intended use. This is in contrast to most of the previous work on typing processes where all processes are typed by a unique constant type, indicating essentially that they are well typed relative to a particular environment. Our fine-grained typing facilitates the management of access rights and provides host protection from potentially malicious behaviour. Our process type takes the form of an interface limiting the resources to which it has access and the types at which they may be used. Allowing resource names to appear both in process types and process terms, as interaction ports, complicates the typing system considerably. For the development of a coherent typing system, we use a kinding technique, similar to that used by the subtyping of the system F, and order-theoretic properties of our subtyping relation. Various examples of this paper illustrate the usage of our fine-grained process types in distributed systems.     

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

Lexically scoped distribution: what you see is what you get

We define a lexically scoped, asynchronous and distributed π-calculus, with local communication and process migration. This calculus adopts the network-awareness principle for distributed programming and follows a simple model of distribution for mobile calculi: a lexical scope discipline combines static scoping with dynamic linking, associating channels to a fixed site throughout computation. This discipline provides for both remote invocation and process migration. A simple type system is a straightforward extension of that of the π-calculus, adapted to take into account the lexical scope of channels. An equivalence law captures the essence of this model: a process behavior depends on the channels it uses, not on where it runs.     

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.     

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.     

On the Expressiveness of Chi, Update, and Fusion calculi

Chi and Update calculi [9,17] have been independently introduced in order to model mobile systems. The two calculi are very close to each other and represent an evolution of π-calculus [15]. More recently a (non-straightforward) polyadic version of the Update calculus, the Fusion calculus, has been proposed [18].In the paper we give a fully abstract encoding from an asynchronous variant of Chi and Update calculi to asynchronous π-calculus [11,4]. This proves that, at least for their asynchronous variants, Chi and Update calculi are not more expressive than π-calculus. A similar result can be proved for the Fusion calculus.     

Relating state-based and process-based concurrency through linear logic (full-version)

This paper has the purpose of reviewing some of the established relationships between logic and concurrency, and of exploring new ones.Concurrent and distributed systems are notoriously hard to get right. Therefore, following an approach that has proved highly beneficial for sequential programs, much effort has been invested in tracing the foundations of concurrency in logic. The starting points of such investigations have been various idealized languages of concurrent and distributed programming, in particular the well established state-transformation model inspired by Petri nets and multiset rewriting, and the prolific process-based models such as the π-calculus and other process algebras. In nearly all cases, the target of these investigations has been linear logic, a formal language that supports a view of formulas as consumable resources. In the first part of this paper, we review some of these interpretations of concurrent languages into linear logic and observe that, possibly modulo duality, they invariably target a small semantic fragment of linear logic that we call LV^obs.In the second part of the paper, we propose a new approach to understanding concurrent and distributed programming as a manifestation of logic, which yields a language that merges those two main paradigms of concurrency. Specifically, we present a new semantics for multiset rewriting founded on an alternative view of linear logic and specifically LV^obs. The resulting interpretation is extended with a majority of linear connectives into the language of ω-multisets. This interpretation drops the distinction between multiset elements and rewrite rules, and considerably enriches the expressive power of standard multiset rewriting with embedded rules, choice, replication, and more. Derivations are now primarily viewed as open objects, and are closed only to examine intermediate rewriting states. The resulting language can also be interpreted as a process algebra. For example, a simple translation maps process constructors of the asynchronous π-calculus to rewrite operators. The language of ω-multisets forms the basis for the security protocol specification language MSR 3. With relations to both multiset rewriting and process algebra, it supports specifications that are process-based, state-based, or of a mixed nature, with the potential of combining verification techniques from both worlds. Additionally, its logical underpinning makes it an ideal common ground for systematically comparing protocol specification languages.     

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.     

A Rewriting Calculus for Cyclic Higher-order Term Graphs

Introduced at the end of the nineties, the Rewriting Calculus (ρ-calculus, for short) is a simple calculus that fully integrates term-rewriting and λ-calculus. The rewrite rules, acting as elaborated abstractions, their application and the obtained structured results are first class objects of the calculus. The evaluation mechanism, generalizing beta-reduction, strongly relies on term matching in various theories.In this paper we propose an extension of the ρ-calculus, handling graph like structures rather than simple terms. The transformations are performed by explicit application of rewrite rules as first class entities. The possibility of expressing sharing and cycles allows one to represent and compute over regular infinite entities.The calculus over terms is naturally generalized by using unification constraints in addition to the standard ρ-calculus matching constraints. This therefore provides us with the basics for a natural extension of an explicit substitution calculus to term graphs. Several examples illustrating the introduced concepts are given.     

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.     

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.     

De Bruijn''s syntax and reductional behaviour of λ-terms: the typed case

In this paper, we consider the typed versions of the λ-calculus written in a notation which helps describe canonical forms more elegantly than the classical notation, and enables to divide terms into classes according to their reductional behaviour. In this notation, β-reduction can be generalised from a relation on terms to one on equivalence classes. This class reduction covers many known notions of generalised reduction. We extend the Barendregt cube with our class reduction and show that the subject reduction property fails but that this is not unique to our class reduction. We show that other generalisations of reduction (such as the σ-reduction of Regnier) also behave badly in typed versions of the λ-calculus. Nevertheless, solution is at hand for these generalised reductions by adopting the useful addition of definitions in the contexts of type derivations. We show that adding such definitions enables the extensions of type systems with class reduction and σ-reduction to satisfy all the desirable properties of type systems, including subject reduction and strong normalisation. Our proposed typing relation ^c is the most general relation in the literature that satisfies all the desirable properties of type systems. We show that classes contain all the desirable information related to a term with respect to typing, strong normalisation, subject reduction, etc.     

A Simple Calculus for Proteins and Cells

The use of process calculi to represent biological systems has led to the design of different calculi such as brane calculi [Luca Cardelli. Brane calculi. In CMSB, pages 257–278, 2004] and κ-calculus [Vincent Danos and Cosimo Laneve. Formal molecular biology. Theoritical Computer Science, 325(1):69–110, 2004]. Both have proved to be useful to model different types of biological systems.As an attempt to unify the two directions, we introduce the bioκ-calculus, a simple calculus for describing proteins and cells, in which bonds are represented by means of shared names and interactions are modelled at the domain level. Protein-protein interactions have to be at most binary and cell interactions have to fit with sort constraints.We define the semantics of bioκ-calculus, analyse its properties, and discuss its expressiveness by modelling two significant examples: a signalling pathway and a virus infection.     

A Symmetric Lambda Calculus for Classical Program Extraction

We introduce aλ-calculus with symmetric reduction rules and “classical” types, i.e., types corresponding to formulas of classical propositional logic. The strong normalization property is proved to hold for such a calculus, as well as for its extension to a system equivalent to Peano arithmetic. A theorem on the shape of terms in normal form is also proved, making it possible to get recursive functions out of proofs ofΠ⁰₂formulas, i.e., those corresponding to program specifications.