Towards an analysis of dynamic gossip in NetKAT
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.
|Keywords||Dynamic gossip, Kleene algebra with tests (KAT), NetKAT, Network programming language, Peer-to-peer communication|
|Series||Lecture Notes in Computer Science|
|Conference||International Conference on Relational and Algebraic Methods in Computer Science|
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