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.

, , , ,
Lecture Notes in Computer Science
International Conference on Relational and Algebraic Methods in Computer Science
Centrum Wiskunde & Informatica, Amsterdam (CWI), The Netherlands

Gattinger, M, & Wagemaker, J. (2018). Towards an analysis of dynamic gossip in NetKAT. In RAMiCS 2018: Relational and Algebraic Methods in Computer Science (pp. 280–297). doi:10.1007/978-3-030-02149-8_17