Wednesday 9 May 2012, 11h
Bldg I, 1st floor
Microsoft Research – Inria Joint Centre
Parc Orsay UniversitéRouting in Equilibrium (with help from ssreflect)
Timothy G. Griffin , University of CambridgeSome path problems cannot be modelled using semirings because the associated algebraic structure is not distributive. Rather than attempting to compute globally optimal paths with such structures, it may be sufficient in some cases to find locally optimal paths — paths that represent a stable local equilibrium. For example, this is the type of routing system that has evolved to connect Internet Service Providers (ISPs) where link weights implement bilateral commercial relationships between them. Previous work has shown that routing equilibria can be computed for some non-distributive algebras using algorithms in the Bellman-Ford family. However, no polynomial time bound was known for such algorithms. In this talk, we show that routing equilibria can be computed using Dijkstra’s algorithm for one class of non-distributive structures. This provides the first polynomial time algorithm for computing locally optimal solutions to path problems.
This is joint work with João Luís Sobrinho presented at the 19th International Symposium on Mathematical Theory of Networks and Systems (MTNS 2010). You can find the paper here. I have recently formulated the results of this paper using Coq+ssrelfect, and I will discuss the ways in which this helped clarify/rectify some of the more murky bits of the paper.