Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userOn the Validity of Encodings of the Synchronous in the Asynchronous $pi$-calculus
87
0
0.0
(
0
)
Added by
Rob van Glabbeek
Publication date
2018
fields
Informatics Engineering
and research's language is
English
Authors
Rob van Glabbeek
Ask ChatGPT about the research
No Arabic abstract
Process calculi may be compared in their expressive power by means of encodings between them. A widely accepted definition of what constitutes a valid encoding for (dis)proving relative expressiveness results between process calculi was proposed by Gorla. Prior to this work, diverse encodability and separation results were generally obtained using distinct, and often incompatible, quality criteria on encodings. Textbook examples of valid encoding are the encodings proposed by Boudol and by Honda & Tokoro of the synchronous choice-free $pi$-calculus into its asynchronous fragment, illustrating that the latter is no less expressive than the former. Here I formally establish that these encodings indeed satisfy Gorlas criteria.
rate research
Read More
We study the relation between process calculi that differ in their either synchronous or asynchronous interaction mechanism. Concretely, we are interested in the conditions under which synchronous interaction can be implemented using just asynchronous interactions in the pi-calculus. We assume a number of minimal conditions referring to the work of Gorla: a good encoding must be compositional and preserve and reflect computations, deadlocks, divergence, and success. Under these conditions, we show that it is not possible to encode synchronous interactions without introducing additional causal dependencies in the translation.
We study whether, in the pi-calculus, the match prefix-a conditional operator testing two names for (syntactic) equality-is expressible via the other operators. Previously, Carbone and Maffeis proved that matching is not expressible this way under rather strong requirements (preservation and reflection of observables). Later on, Gorla developed a by now widely-tested set of criteria for encodings that allows much more freedom (e.g. instead of direct translations of observables it allows comparison of calculi with respect to reachability of successful states). In this paper, we offer a considerably stronger separation result on the non-expressibility of matching using only Gorlas relaxed requirements.
When considering distributed systems, it is a central issue how to deal with interactions between components. In this paper, we investigate the paradigms of synchronous and asynchronous interaction in the context of distributed systems. We investigate to what extent or under which conditions synchronous interaction is a valid concept for specification and implementation of such systems. We choose Petri nets as our system model and consider different notions of distribution by associating locations to elements of nets. First, we investigate the concept of simultaneity which is inherent in the semantics of Petri nets when transitions have multiple input places. We assume that tokens may only be taken instantaneously by transitions on the same location. We exhibit a hierarchy of `asynchronous Petri net classes by different assumptions on possible distributions. Alternatively, we assume that the synchronisations specified in a Petri net are crucial system properties. Hence transitions and their preplaces may no longer placed on separate locations. We then answer the question which systems may be implemented in a distributed way without restricting concurrency, assuming that locations are inherently sequential. It turns out that in both settings we find semi-structural properties of Petri nets describing exactly the problematic situations for interactions in distributed systems.
The $pi$ -calculus is used as a model for programminglanguages. Its contexts exhibit arbitrary concurrency, makingthem very discriminating. This may prevent validating desir-able behavioural equivalences in cases when more disciplinedcontexts are expected.In this paper we focus on two such common disciplines:sequentiality, meaning that at any time there is a single threadof computation, and well-bracketing, meaning that calls toexternal services obey a stack-like discipline. We formalise thedisciplines by means of type systems. The main focus of thepaper is on studying the consequence of the disciplines onbehavioural equivalence. We define and study labelled bisim-ilarities for sequentiality and well-bracketing. These relationsare coarser than ordinary bisimilarity. We prove that they aresound for the respective (contextual) barbed equivalence, andalso complete under a certain technical condition.We show the usefulness of our techniques on a number ofexamples, that have mainly to do with the representation offunctions and store.
In the logic programming paradigm, it is difficult to develop an elegant solution for generating distinguishing formulae that witness the failure of open-bisimilarity between two pi-calculus processes; this was unexpected because the semantics of the pi-calculus and open bisimulation have already been elegantly specified in higher-order logic programming systems. Our solution using Haskell defines the formulae generation as a tree transformation from the forest of all nondeterministic bisimulation steps to a pair of distinguishing formulae. Thanks to laziness in Haskell, only the necessary paths demanded by the tree transformation function are generated. Our work demonstrates that Haskell and its libraries provide an attractive platform for symbolically analyzing equivalence properties of labeled transition systems in an environment sensitive setting.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
