arXiv subjects

Uwe Nestmann

Publications and source records attributed to Uwe Nestmann.

21 records · Page 2Linked to original sources

arXiv2011

Synchrony vs Causality in the Asynchronous Pi-Calculus

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.

cs.LO↗

arXiv2010

Breaking Symmetries

A well-known result by Palamidessi tells us that \pimix (the π-calculus with mixed choice) is more expressive than \pisep (its subset with only separate choice). The proof of this result argues with 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 of breaking (initial) symmetries is 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 layer of the distinguishing problem domain of leader election. Both Palamidessi and Gorla rephrased their results by stating that there is no uniform and reasonable encoding from \pimix into \pisep. We indicate how the respective 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.

cs.LO↗

arXiv2010

Breaking Symmetries

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 argues with their different expressive power concerning leader election in symmetric networks. Later on, Gorla of- fered 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 of breaking (ini- tial) symmetries is 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 layer of the distinguishing problem domain of leader election. Both Palamidessi and Gorla rephrased their results by stating that there is no uniform and reason- able encoding from πmix into πsep . We indicate how the respective 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.

cs.LO↗