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

January 01, 2018

Fair Dynamic Spectrum Management for QRD-Based Precoding with User Encoding Ordering in Downstream G.fast Transmission

In next generation DSL networks such as G.fast, employing discrete multi-tone transmission in high frequencies up to 212 MHz, the crosstalk among lines reaches very high levels. To precompensate the crosstalk in downstream transmission, QRD-based precoding has been proposed as a near-optimal dynamic spectrum management (DSM) technique. However, the performance ...

January 01, 2018

Practical Mitigation of Passive Intermodulation in Microstrip Circuits

This paper presents new experimental evidence and a novel practical approach for mitigation of passive intermodulation (PIM) in microstrip circuits fabricated on commercial printed circuit board laminates. The mechanisms of distributed PIM in microstrip circuits are reviewed and a phenomenology of PIM generation due to locally enhanced electromagnetic fields at ...

January 01, 2018

Efficient Cooperative HARQ for Multi-Source Multi-Relay Wireless Networks

In this paper, we compare the performance of three different cooperative Hybrid Automatic Repeat reQuest (HARQ) protocols for slow-fading half-duplex orthogonal multiple access multiple relay channel. Channel State Information (CSI) is available at the receiving side of each link only. Time Division Multiplexing is assumed, where each orthogonal transmission occurs ...