An expressiveness study of priority in process calculi

Priority is a frequently used feature of many computational systems. In this paper we study the expressiveness of two process algebras enriched with different priority mechanisms. In particular, we consider a finite (that is, recursion-free) fragment of asynchronous CCS with global priority (FAP, for short) and Phillips' CPG (CCS with local priority), and contrast their expressive power with that of two non-prioritised calculi, namely the π-calculus and its broadcast-based version, called bπ. We prove, by means of leader-election-based separation results, that, under certain conditions, there exists no encoding of FAP in π-Calculus or CPG. Moreover, we single out another problem in distributed computing, which we call the last man standing problem (LMS for short), that better reveals the gap between the two prioritised calculi above and the two non-prioritised ones, by proving that there exists no parallel-preserving encoding of the prioritised calculi in the non-prioritised calculi retaining any sincere (complete but partially correct, that is, admitting divergence or premature termination) semantics.

Download Full-text

Tutorial on separation results in process calculi via leader election problems

Theoretical Computer Science ◽

10.1016/j.tcs.2007.09.001 ◽

2007 ◽

Vol 388 (1-3) ◽

pp. 267-289 ◽

Cited By ~ 14

Author(s):

Maria Grazia Vigliotti ◽

Iain Phillips ◽

Catuscia Palamidessi

Keyword(s):

Leader Election ◽

Process Calculi ◽

Separation Results

Download Full-text

Breaking symmetries

Mathematical Structures in Computer Science ◽

10.1017/s0960129514000346 ◽

2014 ◽

Vol 26 (6) ◽

pp. 1054-1106 ◽

Cited By ~ 4

Author(s):

KIRSTIN PETERS ◽

UWE NESTMANN

Keyword(s):

Expressive Power ◽

Leader Election ◽

Problem Domain ◽

Underlying Principle ◽

Π Calculus ◽

The Difference ◽

Uniformity Criterion ◽

Symmetric Networks

A well-known result by Palamidessi tells us that πmix(the π-calculus with mixed choice) is more expressive than πsep(its subset with only separate choice). The proof of this result analyses their different expressive power concerning leader election in symmetric networks. Later on, Gorla offered an arguably simpler proof that, instead of leader election in symmetric networks, employed the reducibility of ‘incestual’ processes (mixed choices that include both enabled senders and receivers for the same channel) when running two copies in parallel. In both proofs, the role ofbreaking (initial) symmetriesis more or less apparent. In this paper, we shed more light on this role by re-proving the above result – based on a proper formalization of what it means to break symmetries – without referring to another problem domain like leader election.Both Palamidessi and Gorla rephrased their results by stating that there is no uniform and reasonable encoding from πmixinto πsep. We indicate how their proofs can be adapted and exhibit the consequences of varying notions of uniformity and reasonableness. In each case, the ability to break initial symmetries turns out to be essential. Moreover, by abandoning the uniformity criterion, we show that there indeed is a reasonable encoding. We emphasize its underlying principle, which highlights the difference between breaking symmetries locally instead of globally.

Download Full-text

On the Expressive Power of Global and Local Priority in Process Calculi

CONCUR 2007 – Concurrency Theory - Lecture Notes in Computer Science ◽

10.1007/978-3-540-74407-8_17 ◽

2007 ◽

pp. 241-255 ◽

Cited By ~ 6

Author(s):

Cristian Versari ◽

Nadia Busi ◽

Roberto Gorrieri

Keyword(s):

Expressive Power ◽

Process Calculi ◽

Global And Local

Download Full-text

Light logics and higher-order processes

Mathematical Structures in Computer Science ◽

10.1017/s0960129514000310 ◽

2014 ◽

Vol 26 (6) ◽

pp. 969-992 ◽

Cited By ~ 1

Author(s):

UGO DAL LAGO ◽

SIMONE MARTINI ◽

DAVIDE SANGIORGI

Keyword(s):

Polynomial Time ◽

Linear Logic ◽

Higher Order ◽

Resource Control ◽

Process Algebras ◽

Π Calculus ◽

Soft Processes

We show that the techniques for resource control that have been developed by the so-calledlight logicscan be fruitfully applied also to process algebras. In particular, we present a restriction of higher-order π-calculus inspired by soft linear logic. We prove that any soft process terminates in polynomial time. We argue that the class of soft processes may be naturally enlarged so that interesting processes are expressible, still maintaining the polynomial bound on executions.

Download Full-text

Towards a unified approach to encodability and separation results for process calculi

Information and Computation ◽

10.1016/j.ic.2010.05.002 ◽

2010 ◽

Vol 208 (9) ◽

pp. 1031-1053 ◽

Cited By ~ 58

Author(s):

Daniele Gorla

Keyword(s):

Unified Approach ◽

Process Calculi ◽

Separation Results

Download Full-text

New-HOPLA--A Higher-Order Process Language with Name Generation

BRICS Report Series ◽

10.7146/brics.v11i21.21846 ◽

2004 ◽

Vol 11 (21) ◽

Cited By ~ 1

Author(s):

Glynn Winskel ◽

Francesco Zappa Nardelli

Keyword(s):

Operational Semantics ◽

Expressive Power ◽

Higher Order ◽

Domain Theory ◽

Process Algebras ◽

Order Process ◽

Pi Calculus ◽

Mobile Ambients ◽

Congruence Properties

This paper introduces new-HOPLA, a concise but powerful language for higher-order nondeterministic processes with name generation. Its origins as a metalanguage for domain theory are sketched but for the most part the paper concentrates on its operational semantics. The language is typed, the type of a process describing the shape of the computation paths it can perform. Its transition semantics, bisimulation, congruence properties and expressive power are explored. Encodings are given of well-known process algebras, including pi-calculus, Higher-Order pi-calculus and Mobile Ambients.

Download Full-text

Simple Algorithms for Distributed Leader Election in Anonymous Synchronous Rings and Complete Networks Inspired by Neural Development in Fruit Flies

International Journal of Neural Systems ◽

10.1142/s0129065715500252 ◽

2015 ◽

Vol 25 (07) ◽

pp. 1550025 ◽

Cited By ~ 2

Author(s):

Lei Xu ◽

Peter Jeavons

Keyword(s):

Distributed Computing ◽

Neural Development ◽

Message Passing ◽

Practical Problem ◽

Fruit Fly ◽

Neural System ◽

Leader Election ◽

Good Time ◽

Message Complexity ◽

Complete Networks

Leader election in anonymous rings and complete networks is a very practical problem in distributed computing. Previous algorithms for this problem are generally designed for a classical message passing model where complex messages are exchanged. However, the need to send and receive complex messages makes such algorithms less practical for some real applications. We present some simple synchronous algorithms for distributed leader election in anonymous rings and complete networks that are inspired by the development of the neural system of the fruit fly. Our leader election algorithms all assume that only one-bit messages are broadcast by nodes in the network and processors are only able to distinguish between silence and the arrival of one or more messages. These restrictions allow implementations to use a simpler message-passing architecture. Even with these harsh restrictions our algorithms are shown to achieve good time and message complexity both analytically and experimentally.

Download Full-text