Skip to main content

On the impact of modelling choices for distributed information spread – a comparative study


Ansgar Fehnker and Rena Bakhshi


Free University of Amsterdam


We consider a distributed shuffling algorithm for sharing data in a distributed network. Nodes executing the algorithm periodically contact each other, and exchange data. The behavior of the algorithm is probabilistic in nature; a node chooses a random peer, and sends a random subset of its local data. Moreover, the algorithm exhibits nondeterministic behavior; the order in which nodes initiate an exchange is not specified.

For the shuffling algorithm we build several formal models using the probabilistic model checker PRISM. Despite the well known state-space explosion problem, we were able to model a network of up to 15 nodes. In addition, we implement two equational models in Matlab, a discrete model and its continuous alternative, as well as the algorithm itself in the peer-to-peer network simulator PeerSim. By comparing different modelling frameworks, we further explore the impact of modelling choices, such as different scheduling policies and the notion of rounds. The comparison of different models allowed us to discover hidden assumptions in these alternative modelling frameworks, which helps with the interpretation of the obtained results.

BibTeX Entry

    author           = {Fehnker, Ansgar and Bakhshi, Rena},
    month            = sep,
    year             = {2009},
    keywords         = {model checking, prism, shuffling algorithm, peersim},
    title            = {On the Impact of Modelling Choices for Distributed Information Spread -- A Comparative Study},
    booktitle        = {International Conference on Quantitative Evaluation of SysTems}


Served by Apache on Linux on seL4.