Formal foundations of routing in networks
Algebraic structures such as semirings have long provided the mathematical basis for framing path-related questions such as connectivity and least-cost paths in communication networks. A long series of work starting from Berge and Carre’ up to recent work by Hoefner & Moeller show that algorithmic solutions to these problems, such as those given by Dijkstra and by Roy/Floyd/Warshall, can be algebraically derived within a framework of cost semirings.
Packet-switching networks additionally require being able to define filters and describe complex sets of paths. The theory of Kleene Algebras with Tests, specialised for networks yields a domain-specific algebraic language (NetKAT of Foster, Kozen, Silva et al.) in which reachability properties of packet switching networks can be expressed and proved (using co-algebraic techniques).
Real networks however require complex protocols for Routing, i.e, establishing "good" paths satisfying certain desired properties along which packets may be forwarded. The Routing Algebra framework of Sobrinho, Griffin, et al provides a formalism in which a large family of routing policies can be expressed and about which correctness conditions can be proven with respect to given routing mechanisms.
The generality of the structure and behaviour of modern-day networks requires more abstract treatments, such as the Axiomatic Basis of Communication suggested by Karsten et al., in which minimal assumptions about abstract switches are used to formulate fundamental notions in networks such as naming, addresses, peers, tunnels, paths, namespaces etc. We conclude with a reformulation of these axioms using Linear-time Temporal Logic, using which questions about message deliverability can be expressed even in the presence of mobility (Mobile IP), message encryption (TOR) and other dynamic features of networks.
February 10, 2018 2:46 Europe/Helsinki (GMT +02:00)
local organizers, ewscs18(at)cs.ioc.ee
EWSCS'18 page: http://cs.ioc.ee/ewscs/2018/