Affiliations: Department of Computing, Imperial College London, London, UK. a.lomuscio@imperial.ac.uk | BT Innovate, Adastral Park, UK. ben.strulo@bt.com | BT Innovate, Adastral Park, UK. nigel.g.walker@bt.com | Department of Computer Science, University College London, London, UK. p.wu@cs.ucl.ac.uk
Note: [] Address for correspondence: Lab of Computer Science, P.O.Box 8718, Beijing 100190, China
Abstract: Model checking has been widely applied to the verification of network protocols. Alternatively, optimisation based approaches have been proposed 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 first bridge and explore synergies between these two approaches. We consider a series of discrete approximations to the optimisation based congestion control algorithms. Then we use branching time temporal logic to specify formally the convergence criteria for the system dynamics and present results from implementing these algorithms on a state-of-the-art model checker. We report on our experiences in using the abstraction of model checking to capture features of the continuous dynamics typical of optimisation based approaches.
Keywords: Model Checking, Distributed Optimisation, Congestion Control, Convergence
