Towards an Analysis of Dynamic Gossip in Netkat

Malvin Gattinger, Jana Wagemaker

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

1 Citation (Scopus)

Abstract

In this paper we analyse the dynamic gossip problem using the algebraic network programming language Netkat.

Netkat is a language based on Kleene algebra with tests and describes packets travelling through networks. It has a sound and complete axiomatisation and an efficient coalgebraic decision procedure. Dynamic gossip studies how information spreads through a peer-to-peer network in which links are added dynamically.

In this paper we embed dynamic gossip into Netkat. We show that a reinterpretation of Netkat in which we keep track of the state of switches allows us to model Learn New Secrets, a well-studied protocol for dynamic gossip. We axiomatise this reinterpretation of Netkat and show that it is sound and complete with respect to the packet-processing model, via a translation back to standard Netkat.

Our main result is that many common decision problems about gossip graphs can be reduced to checks of Netkat equivalences. We also implemented the reduction.
Original languageEnglish
Title of host publicationRelational and Algebraic Methods in Computer Science
Subtitle of host publication17th International Conference, RAMiCS 2018, Groningen, The Netherlands, October 29 – November 1, 2018, Proceedings
EditorsJules Desharnais, Walter Guttmann, Stef Joosten
PublisherSpringer International Publishing, Cham, Switzerland
Chapter17
Pages280-297
Number of pages18
ISBN (Electronic)978-3-030-02149-8
ISBN (Print)978-3-030-02148-1
DOIs
Publication statusPublished - 6-Oct-2018

Publication series

NameRelational and Algebraic Methods in Computer Science
Volume11194
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Keywords

  • Dynamic gossip
  • Kleene algebra with tests (KAT)
  • Network programming language
  • NetKAT
  • Peer-to-peer communication

Cite this