Tight complexity analysis of population protocols with cover times - the ZebraNet example
Population protocols are a communication model for large sensor networks with resource-limited anonymous mobile agents. The agents move asynchronously and communicate via pairwise interactions. The original fairness assumption of this model involves a high level of asynchrony and prevents evaluation of the convergence time of a protocol (via deterministic means). The introduction of some “partial synchrony” in the model, under the form of cover times, is an extension that allows evaluating the time complexities. In this paper, we take advantage of this extension and study a data collection protocol used in the ZebraNet project for the wild-life tracking of zebras in a reserve in central Kenya. In ZebraNet, sensors are attached to zebras. The sensed data can be exchanged between the sensors and is collected regularly by a mobile base station crossing the area. The data collection protocol of ZebraNet has been analyzed through simulations. Here, we present a purely analytical study using the model of population protocols with cover times. Our first result states that, in the original protocol, some data may never be delivered to the base station. Motivated by this drawback, we propose two modified and correct protocols which are then used as the paper case studies. We prove their correctness and we compute their tight worst case time complexities. This analysis introduces several techniques that may prove useful in future studies of time in population protocols.