UCL logo

UCL Discovery

UCL home » Library Services » Electronic resources » UCL Discovery

Model Checking Optimisation-Based Congestion Control Models

Lomuscio, A; Strulo, B; Walker, N; Wu, P; (2009) Model Checking Optimisation-Based Congestion Control Models. In: (Proceedings) the 12th International Workshop on Concurrency, Specification and Programming (CS&P 2009). (pp. 386 - 397). Warsaw University Press

Full text not available from this repository.

Abstract

28 - 30 September 2009 Abstract: Model checking has been widely applied for verification 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 [1] 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 quantified. 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 fit. We report on our experiences in using the abstractions of model checking to capture features of the continuous dynamics typical of optimisation-based approaches.

Type:Proceedings paper
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: edit this record