Uncovering Symmetries in Irregular Process Networks

  • Namjoshi K.
  • Trefler R.

Distributed protocols are often designed to run on arbitrary networks. The verification of such protocols is a challenge, as symmetry reduction arguments do not apply to irregular networks. On the other hand, the protocols often have correctness proofs which treat all nodes similarly, glossing over structural differences. In this work, we set up an abstraction framework which helps to formalize a lack of distinguishability between nodes. Specifically, we show that abstracting the neighborhood of a process helps to uncover local symmetries in a process network. This turns an irregular, concrete process network into a regular, abstract process network. Using these ideas, we show how to obtain a simple, compositional invariance proof for the Dining philosophers protocol, which applies to any network. As the proof works in the same manner for all networks, it actually results in a parameterized proof of correctness, one which holds for networks of arbitrary size and topology.

View Original Article

Recent Publications

August 09, 2017

A Cloud Native Approach to 5G Network Slicing

  • Francini A.
  • Miller R.
  • Sharma S.

5G networks will have to support a set of very diverse and often extreme requirements. Network slicing offers an effective way to unlock the full potential of 5G networks and meet those requirements on a shared network infrastructure. This paper presents a cloud native approach to network slicing. The cloud ...

August 01, 2017

Modeling and simulation of RSOA with a dual-electrode configuration

  • De Valicourt G.
  • Liu Z.
  • Violas M.
  • Wang H.
  • Wu Q.

Based on the physical model of a bulk reflective semiconductor optical amplifier (RSOA) used as a modulator in radio over fiber (RoF) links, the distributions of carrier density, signal photon density, and amplified spontaneous emission photon density are demonstrated. One of limits in the use of RSOA is the lower ...

July 12, 2017

PrivApprox: Privacy-Preserving Stream Analytics

  • Chen R.
  • Christof Fetzer
  • Le D.
  • Martin Beck
  • Pramod Bhatotia
  • Thorsten Strufe

How to preserve users' privacy while supporting high-utility analytics for low-latency stream processing? To answer this question: we describe the design, implementation and evaluation of PRIVAPPROX, a data analytics system for privacy-preserving stream processing. PRIVAPPROX provides three properties: (i) Privacy: zero-knowledge privacy (ezk) guarantees for users, a privacy bound tighter ...