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.

Additional Metadata
Keywords Dynamic gossip, Kleene algebra with tests (KAT), NetKAT, Network programming language, Peer-to-peer communication
Persistent URL dx.doi.org/10.1007/978-3-030-02149-8_17
Series Lecture Notes in Computer Science
Conference International Conference on Relational and Algebraic Methods in Computer Science
Citation
Gattinger, M, & Wagemaker, J. (2018). Towards an analysis of dynamic gossip in NetKAT. In Lecture Notes in Computer Science/Lecture Notes in Artificial Intelligence (pp. 280–297). doi:10.1007/978-3-030-02149-8_17