Search

In this position paper, we would like to offer and defend a template to study equivalences between programs---in the particular framework of process algebras for concurrent computation.We believe that our layered model of development will clarify the distinction that is too often left implicit between the tasks and duties of the programmer and of the tester.It will also enlighten pre-existing issues that have been running across process algebras such as the calculus of communicating systems, the \(\pi\)-calculus---also in its distributed version---or mobile ambients.Our distinction starts by subdividing the notion of process in three conceptually separated entities, that we call \emph{process terms}, (completed) \emph{processes} and \emph{tests}, and by stressing the importance of formalizing the \emph{completion} of process terms and the \emph{instrumentation} that results from placing a (completed) processes into a test.While the role of what can be observed and the subtleties in the definitions of congruences have been intensively studied, the fact that \emph{not every term can be tested}, and that \emph{the tester should have access to a different set of tools than the programmer} is curiously left out, or at least not often formally discussed--in this respect, the theory of monitor is a counter-examples that we discuss and compare to our approach.We argue that this blind spot comes from the under-specification of contexts---environments in which comparisons occur---that play multiple distinct roles but are generally---at least, on the surface of it---given only one definition that fails to capture all of their aspects.

International audience; In this position paper, we would like to offer and defend a new template to study equivalences between programs---in the particular framework of process algebras for concurrent computation.We believe that our layered model of development will clarify the distinction that is too often left implicit between the tasks and duties of the programmer and of the tester. It will also enlighten pre-existing issues that have been running across process algebras as diverse as the calculus of communicating systems, the \(\pi\)-calculus---also in its distributed version---or mobile ambients.Our distinction starts by subdividing the notion of process itself in three conceptually separated entities, that we call \emph{Processes}, \emph{Systems} and \emph{Tests}.While the role of what can be observed and the subtleties in the definitions of congruences have been intensively studied, the fact that \emph{not every process can be tested}, and that \emph{the tester should have access to a different set of tools than the programmer} is curiously left out, or at least not often formally discussed.We argue that this blind spot comes from the under-specification of contexts---environments in which comparisons takes place---that play multiple distinct roles but supposedly always \enquote{stay the same}.We illustrate our statement with a simple Java example, the \enquote{usual} concurrent languages, but also back it up with \(\lambda\)-calculus and existing implementations of concurrent languages as well.

In this position paper, we would like to offer a new template to study process algebras for concurrent computation. We believe our template will clarify the distinction that is too often left implicit between user and programmer, and that it enlightens pre-existing issues that have been running across process algebras as diverse as the calculus of communicating systems (CCS), the π-calculus-also in its distributed version-or mobile ambients. Our distinction starts by subdividing the notion of process itself in three conceptually separated entities, and shapes future improvements-both technically and organizationally-as well as it captures recent and diverse progresses in process algebras. While the role of what can be observed and the subtleties in the definitions of congruences have been intensively studied, the fact that not all the comparisons serve the same purpose and should not be made in the same context is curiously left over, or at least not formally discussed. We argue that this blind spot comes from the under-specification of contexts-environments in which the comparison takes place-that supposedly 'stay the same' no matter the nature of the process, who is testing it, or for what. We illustrate our statement with the 'usual' concurrent languages, but also back it up with λ-calculus and existing implementations of concurrent languages as well.

Message-passing is a key ingredient of concurrent programming. The purpose of this paper is to describe the equivalence between the proof theory, the categorical semantics, and term calculus of message-passing. In order to achieve this we introduce the categorical notion of a linear actegory and the related polycategorical notion of a poly-actegory. Not surprisingly the notation used for the term calculus borrows heavily from the (synchronous) π-calculus. The cut-elimination procedure for the system provides an operational semantics.

A term calculus for the proofs in multiplicative-additive linear logic is introduced and motivated as a programming language for channel based concurrency. The term calculus is proved complete for a semantics in linearly distributive categories with additives. It is also shown that proof equivalence is decidable by showing that the cut elimination rewrites supply a confluent rewriting system modulo equations., 16 pages without appendices, 30 with appendices

Structured occurrence nets consist of multiple occurrence nets -- each recording causality and concurrency in an execution of a component of a concurrent system. These occurrence nets are linked together by means of various types of relationships, aimed at representing dependencies between communicating and evolving sub-systems. In this paper, we investigate causality in the basic class of communication structured occurrence nets (cso-nets). We start by introducing the corresponding system-level model of communication structured Place Transition Nets (cspt-nets) which extend Place Transition Nets with an explicit structuring into communicating sub-systems and process interaction based on a combination of synchronous and asynchronous communication. After that we develop a cso-net based process semantics for cspt-nets showing that causality in cso-nets is underpinned by stratified order structures extending causal partial orders with weak causality.

This paper is concerned with defining causality semantics for infinite executions of Petri nets with inhibitor arcs. We first show how one can deal with infinite step sequences and the corresponding occurrence nets (processes) and causal structures. We then discuss how to improve the succinctness of both finite and infinite processes generated from step sequences. In the latter case, the proposed constructions avoid infinite branching in the case of bounded nets.

Dynamic nets are an extension of Petri nets where the net topology may change dynamically. This is achieved by allowing (i) tokens to be coloured with place names (carried on as data), (ii) transitions to designate places where to spawn new tokens on the basis of the colours in the fetched tokens, and (iii) firings to add fresh places and transitions to the net. Dynamic nets have been given step or interleaving semantics but, to the best of our knowledge, their non-sequential truly concurrent semantics has not been addressed in the literature. To fill this gap, we extend the ordinary notions of processes and unfolding to dynamic nets, providing two different constructions: (i) a specific process and unfolding for a particular initial marking, and (ii) processes and unfolding patterns that abstract away from the colours of the token initially available.

A causality semantics for weighted Place/Transition nets with weighted inhibitor arcs (PTI-nets) is proposed, by extending the standard approach based on the process semantics given through net unfolding and occurrence nets. It is demonstrated how processes corresponding to step sequences of PTI-nets can be constructed, and a nonalgorithmic (axiomatic) characterisation is given of the processes that can be obtained in this way. Moreover, a framework is established allowing to separately consider behaviours, processes and causality, in order to facilitate the discussion of their mutual consistency for different Petri net classes.

Localities and a/sync places are two recent extensions to the Petri net model. Whereas localities have been introduced as a modelling tool for membrane systems and more general GALS (globally asynchronous locally synchronous) systems, a/sync places make it possible to model synchronous communication between transitions. We investigate the interaction between locally synchronous execution and synchronous communication. Our focus is in particular on the causalities in the concurrent runs of a new Petri net model combining these features.