Flow theory: Verification of rate-reservation protocols

The authors develop a simple theory of flows and show how to use this theory in verifying rate-reservation protocols in computing networks. The theory is based on discrete and nondeterministic mathematics, rather than the customary continuous or probabilistic mathematics. The theory features two types of flows, smooth and uniform, and four types of flow operators, limiters, compactors, expanders, and filters. Many rate-reservation protocols can be represented as linear networks of these flow operators. It is proved that, if the input flow to any of these networks is smooth or uniform, then the internal buffer and the delay in each operator in the network are bounded. This method is used to prove that a number of rate-reservation protocols (for example, stop-and-go, hierarchical round-robin, fair queuing and virtual clock) require bounded buffering and introduce bounded delay