Concurrent Nets A Study of Prefixing in Process Calculi

26 pages

English

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

Concurrent Nets A Study of Prefixing in Process Calculi

mijec - Emmanuel Beffara

Découvre YouScribe en t'inscrivant gratuitement

Je m'inscris

Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus

26 pages

English

Obtenez un accès à la bibliothèque pour le consulter en ligne
En savoir plus

A propos
Informations
Extrait

Description

Niveau: Supérieur, Doctorat, Bac+8
Concurrent Nets A Study of Prefixing in Process Calculi Emmanuel Beffara François Maurel May 1, 2005 Abstract We introduce the calculus of concurrent nets as an extension of the fu- sion calculus in which usual prefixing is replaced by arbitrary monotonic guards. Then we use this formalism to describe the prefixing policy of standard calculi as a particular form of communication. By developing a graphical syntax, we sharpen the geometric intuition and finally we pro- vide an encoding of these guards as causality in the prefix-free fragment, in the spirit of the encoding of the fusion calculus into solos by Laneve and Victor, proving that communication by fusion is expressive enough to implement arbitrary monotonic guards. 1 Introduction The pi-calculus [1] has generated a wide range of calculi on the search for both a simplification of the syntax and a widening of the expressiveness. Fu's ?- calculus [2], Parrow and Victor's fusion calculus [3] and Gardner and Wischik's explicit fusions [4] are important examples where name substitution is replaced by unification, which makes the calculus simpler, more symmetric and yet more expressive. Most models for concurrent and mobile computation are geometric in nature, and even term calculi have a strong spatial intuition. Indeed, every process calculus comes with a handful of structural rules for commutation and scoping that define appropriate notions of locality. This geometric flavour of term calculi led to the proposal of several graphical syntaxes for existing cal- culi, like pi-nets [5] or solo diagrams [6], and to the introduction of new purely

monotonic scheduling

victor's fusion

fusion calculus into

process calculi

arbitrary mono- tonic

fusion calculus

implement arbitrary

calculus

rules

actions ?

Sujets

Maurel

Process calculus

Calculus

Informations

Publié par	mijec
Nombre de lectures	28
Langue	English

Extrait

Study

Concurrent Nets of Preﬁxing in Process Calculi

Emmanuel Beﬀara

François Maurel

May 1, 2005

Abstract

We introduce the calculus of concurrent nets as an extension of the fu-sion calculus in which usual preﬁxing is replaced by arbitrary monotonic guards. Then we use this formalism to describe the preﬁxing policy of standard calculi as a particular form of communication. By developing a graphical syntax, we sharpen the geometric intuition and ﬁnally we pro-vide an encoding of these guards as causality in the preﬁx-free fragment, in the spirit of the encoding of the fusion calculus into solos by Laneve and Victor, proving that communication by fusion is expressive enough to implement arbitrary monotonic guards.

1 Introduction

Theπwide range of calculi on the search for both-calculus [1] has generated a a simpliﬁcation of the syntax and a widening of the expressiveness. Fu’sχ-calculus [2], Parrow and Victor’s fusion calculus [3] and Gardner and Wischik’s explicit fusions [4] are important examples where name substitution is replaced by uniﬁcation, which makes the calculus simpler, more symmetric and yet more expressive. Most models for concurrent and mobile computation are geometric in nature, and even term calculi have a strong spatial intuition. Indeed, every process calculus comes with a handful of structural rules for commutation and scoping that deﬁne appropriate notions of locality. This geometric ﬂavour of term calculi led to the proposal of several graphical syntaxes for existing cal-culi, likeπ-nets [5] or solo diagrams [6], and to the introduction of new purely graphical calculi, like in Milner’s recent work on bigraphs [7]. In a sense, the evolution from name substitution inπ-calculus to fusion cor-responds to the evolution from syntactical communication to a more geometric one; however the sequentiality imposed by preﬁxing remains very syntactical, since it is directly inspired by CCS and synchronization trees. Motivated by the search for a more general form of preﬁxing, we introduce and study the calculus of concurrent nets as a similar evolution towards a geometrical formulation of sequentiality constraints. Actions in a process get associated with semaphores

that indicate when these actions have been performed, and subsequently pre-ﬁxing is replaced by the use of guards that are monotonic functions of those semaphores, resulting in a form of sequentiality constraints that is reminiscent of enabling in event structures. We deﬁne a graphical syntax for this calculus, in which guards appear as a new form of communication between actions. With the calculus of solos [8], Laneve and Victor simplify the fusion calculus by removing preﬁxing and they show by means of encodings that no expres-sive power is lost. The idea of using the expressiveness of fusion for expressing scheduling constraints can be generalized to our framework of arbitrary mono-tonic guards. The ﬁrst contribution of this paper is to show how concurrent nets extend existing calculi, and notably theπ The-calculus and the fusion calculus. charac-terisation of these sub-calculi yields a classiﬁcation of the forms of sequentiality in use in process calculi using natural geometric arguments. Our second contribution is showing the completeness of the expressive power of communication by fusion with respect to monotonic scheduling, by means of encodings of the arbitrary monotonic guards of concurrent nets into pure communications, using a new and more geometric approach suggested by our graphical syntax. In section 2, the syntax and semantics of the calculus of concurrent nets are introduced, both as a term calculus and as a graph reduction formalism. In section 3 we characterize various existing calculi as restrictions on guarding and scoping. In section 4, we develop two encodings of monotonic guards into communications. In section 5, we study how guards, considered as a form of communication, interact with replication and recursion.

Deﬁnitions

2.1 Introductory Examples

Informally, a concurrent net is a web of input and output actions related by channels. Each action has a principal port (the subject) and a set of auxiliary ¯ ports (the objects). For instance, the processa¯(cd)|a(xy).b(xy)inπ-calculus is represented as

c d

x y

Formally, the set of channels here isC={a, b, c, d, x, y}, but onlya, b, c, dare considered public, which is represented by the fact that they have dangling edges whilexandy Thehave none. actionsa¯(cd)on the left anda(xy)in the middle form a redex. The reduction of this redex will remove both actions and connect ¯ cwithxanddwithy arrow means that the third action. Theb(xy)is preﬁxed bya(xy), i.e. it will not be reduced as long asa(xy)is present. We generalise this preﬁxing in two ways. Consider the following examples:

Univers
Ebooks
Livres audio
Presse
Podcasts
BD
Documents

Concurrent Nets A Study of Prefixing in Process Calculi

Maurel

Process calculus

Calculus

YouScribe

Le catalogue

Le service

Les conditions