Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userThe Buffered pi-Calculus: A Model for Concurrent Languages
148
0
0.0
(
0
)
Added by
Xiaojie Deng
Publication date
2012
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
Message-passing based concurrent languages are widely used in developing large distributed and coordination systems. This paper presents the buffered $pi$-calculus --- a variant of the $pi$-calculus where channel names are classified into buffered and unbuffered: communication along buffered channels is asynchronous, and remains synchronous along unbuffered channels. We show that the buffered $pi$-calculus can be fully simulated in the polyadic $pi$-calculus with respect to strong bisimulation. In contrast to the $pi$-calculus which is hard to use in practice, the new language enables easy and clear modeling of practical concurrent languages. We encode two real-world concurrent languages in the buffered $pi$-calculus: the (core) Go language and the (Core) Erlang. Both encodings are fully abstract with respect to weak bisimulations.
rate research
Read More
188 -
Martin Lange (School of Electrical Engineering
, Computer Science
, n University of Kassel
2012
The higher-dimensional modal mu-calculus is an extension of the mu-calculus in which formulas are interpreted in tuples of states of a labeled transition system. Every property that can be expressed in this logic can be checked in polynomial time, and conversely every polynomial-time decidable problem that has a bisimulation-invariant encoding into labeled transition systems can also be defined in the higher-dimensional modal mu-calculus. We exemplify the latter connection by giving several examples of decision problems which reduce to model checking of the higher-dimensional modal mu-calculus for some fixed formulas. This way generic model checking algorithms for the logic can then be used via partial evaluation in order to obtain algorithms for theses problems which may benefit from improvements that are well-established in the field of program verification, namely on-the-fly and symbolic techniques. The aim of this work is to extend such techniques to other fields as well, here exemplarily done for process equivalences, automata theory, parsing, string problems, and games.
We define a semantics for Milners pi-calculus, with three main novelties. First, it provides a fully-abstract model for fair testing equivalence, whereas previous semantics covered variants of bisimilarity and the may and must testing equivalences. Second, it is based on reduction semantics, whereas previous semantics were based on labelled transition systems. Finally, it has a strong game semantical flavor in the sense of Hyland-Ong and Nickau. Indeed, our model may both be viewed as an innocent presheaf semantics and as a concurrent game semantics.
A (fragment of a) process algebra satisfies unique parallel decomposition if the definable behaviours admit a unique decomposition into indecomposable parallel components. In this paper we prove that finite processes of the pi-calculus, i.e. processes that perform no infinite executions, satisfy this property modulo strong bisimilarity and weak bisimilarity. Our results are obtained by an application of a general technique for establishing unique parallel decomposition using decomposition orders.
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.
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 congruence. Formalisations have been undertaken in a variety of systems, primarily focusing on well-studied (and challenging) properties such as the theory of process bisimulation. We present a formalisation in Agda that instead explores the theory of concurrent transitions, residuation, and causal equivalence of traces, which has not previously been formalised for the pi-calculus. Our formalisation employs de Bruijn indices and dependently-typed syntax, and aligns the proved transitions proposed by Boudol and Castellani in the context of CCS with the proof terms naturally present in Agdas representation of the labelled transition relation. Our main contributions are proofs of the diamond lemma for residuation of concurrent transitions and a formal definition of equivalence of traces up to permutation of transitions.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
