2018-10-29
Towards an analysis of dynamic gossip in NetKAT
Publication
Publication
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 | |
|---|---|
| , , , , | |
| doi.org/10.1007/978-3-030-02149-8_17 | |
| Lecture Notes in Computer Science | |
| International Conference on Relational and Algebraic Methods in Computer Science | |
| Organisation | 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 |
|
