Concurrent Nets A Study of Prefixing in Process Calculi
26
pages
English
Documents
Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus
Découvre YouScribe en t'inscrivant gratuitement
Découvre YouScribe en t'inscrivant gratuitement
26
pages
English
Ebook
Obtenez un accès à la bibliothèque pour le consulter en ligne En savoir plus
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
Voir
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 ?
A
Study
Concurrent Nets 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πwide range of calculi on the search for both-calculus [1] has generated a 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π-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 prefixing remains very syntactical, since it is directly inspired by CCS and synchronization trees. Motivated by the search for a more general form of prefixing, 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
1
that indicate when these actions have been performed, and subsequently pre-fixing 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 define 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 prefixing 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 first 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 classification 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.
2
Definitions
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
a
x y
b
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 prefixed bya(xy), i.e. it will not be reduced as long asa(xy)is present. We generalise this prefixing in two ways. Consider the following examples:
2
