ﻻ يوجد ملخص باللغة العربية
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.
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 G
We present a formalisation in Agda of the theory of concurrent transitions, residuation, and causal equivalence of traces for the pi-calculus. Our formalisation employs de Bruijn indices and dependently-typed syntax, and aligns the proved transitions
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 ra
Formalising the pi-calculus is an illuminating test of the expressiveness of logical frameworks and mechanised metatheory systems, because of the presence of name binding, labelled transitions with name extrusion, bisimulation, and structural congrue
We present a type system to guarantee termination of pi-calculus processes that exploits input/output capabilities and subtyping, as originally introduced by Pierce and Sangiorgi, in order to analyse the usage of channels. We show that our system imp