Speaker: Jana Wagemaker
Date and Time: Thursday, March 1st 2018, 16:00-17:30
Venue: ILLC Seminar Room F1.15, Science Park 107.
Title: Gossip in NetKAT.
Abstract. In this talk I will discuss my MoL thesis, where I combined the study of NetKAT with the study of dynamic gossip. NetKAT is a sound and complete network programming language based on Kleene algebra with tests, originally used to describe packets traveling through networks. It has a coalgebraic decision procedure deciding NetKAT equivalences. Dynamic gossip is a field in which it is studied how information spreads through a gossip graph, where the links in the gossip graph are changeable (dynamic). So far no sound and complete logic is available that describes dynamic gossip in a satisfactory way. In this talk we will discuss NetKAT in detail, and then explore the application of NetKAT to dynamic gossip. We will see that a change of perspective on NetKAT in which we keep track of the state of the switches in a network allows us to use NetKAT to model the Learn New Secrets Protocol, which is one of many gossip protocols. The addition to NetKAT to keep track of the state of switches is formalized and shown to remain sound and complete with respect to the packet-processing model. It is shown that the Dynamic Gossip notions of weak successfulness, strong successfulness and sun graph are formalizable in NetKAT and that an important theorem from Dynamic Gossip is also a theorem of NetKAT.