Model Checking Optimisation-Based Congestion Control Models.
(Proceedings) the 12th International Workshop on Concurrency, Specification and Programming (CS&P 2009).
(pp. 386 - 397).
Warsaw University Press
28 - 30 September 2009 Abstract: Model checking has been widely applied for veriﬁcation of network protocols, particularly on the sequences of interactions between protocol entities. Alternatively, optimisation has been used to reason about the large scale dynamics of networks, particularly with regard to congestion and rate control protocols such as TCP. This paper intends to provide a bridge and explore synergies between these two approaches. An optimisation-based congestion control algorithm was usually being assumed as synchronous in the sense that all agents act on the same time schedule, while some literature like  suggested the existence of asynchronous algorithms that have been proved stable. We carry over the duality structure of the underlying optimisation models and explore systematically these options of composition frameworks with formal semantics. The nondeterminism of interleaving between active agents represents discrete approximations of those optimisation-based congestion control algorithms with a hierarchy of expressiveness. We then use branching-time temporal logic to specify formally the convergence criteria for the system dynamics. Through model checking, convergence of those algorithms can be witnessed in the form of the sequences of interactions between primal and dual agents. Moreover, the number of steps for a system to converge at a stable equilibrium point can also be quantiﬁed. However, these discrete transition models cannot always converge due to discretisation and relaxation of synchrony, but the counterexamples returned from the model checker NuSMV reveal certain realistic issue where the continuous state space is a less ﬁt. We report on our experiences in using the abstractions of model checking to capture features of the continuous dynamics typical of optimisation-based approaches.
|Title:||Model Checking Optimisation-Based Congestion Control Models|
|Event:||the 12th International Workshop on Concurrency, Specification and Programming (CS&P 2009)|
|Dates:||2009-09-28 - 2009-09-30|
|Keywords:||Concurrency, Specification, Model Checking, Optimisation|
|UCL classification:||UCL > School of BEAMS > Faculty of Engineering Science > Computer Science|
Archive Staff Only