Temporal Logic-based reasoning about iBGP multipath dissemination

Integrating multipath technology with internet routing is becoming one of the most promising trends in building the next generation Internet system. However, incrementally evolving today´s Internet routing from single-path routing to multipath routing is a hard problem. One of the fundamental issues is route oscillation caused by routing policy conflicts. Failing in solving this problem will discourage further deployment of inter-domain multipath routing. The goal of this paper is to understand route oscillation in intra-domain multipath routing. To this end, we propose a formal policy representation model to represent the routing policies about multipath dissemination. Based on the proposed model, we present a Linear Temporal Logic-based framework to verify routing policies about multipath dissemination. The ability of the framework is demonstrated by analyzing iBGP multipath dissemination examples.