Automatic analysis of expected termination time for population protocols

DOI10.4230/LIPICS.CONCUR.2018.33MaRDI QIDQ5009451zbMATH OpenOpenAlexFDO

Authors Michael Blondin, Javier Esparza, Antonin Kučera

Publication date 4 August 2021

Full work available at URL https://arxiv.org/abs/1807.00331

zbMATH Keywords

expected termination timeperformance analysispopulation protocols

Mathematics Subject Classification ID

Network protocols (68M12) Distributed systems (68M14) Wireless sensor networks as related to computer science (68M18) Analysis of algorithms (68W40)

Abstract: Population protocols are a formal model of sensor networks consisting of identical mobile devices. Two devices can interact and thereby change their states. Computations are infinite sequences of interactions in which the interacting devices are chosen uniformly at random. In well designed population protocols, for every initial configuration of devices, and for every computation starting at this configuration, all devices eventually agree on a consensus value. We address the problem of automatically computing a parametric bound on the expected time the protocol needs to reach this consensus. We present the first algorithm that, when successful, outputs a function f(n) such that the expected time to consensus is bound by O(f(n)), where n is the number of devices executing the protocol. We experimentally show that our algorithm terminates and provides good bounds for many of the protocols found in the literature.

Recommendations

• Advances in parameterized verification of population protocols
• Verification of population protocols
• Verification of Population Protocols
• Brief Announcement
• Verification of Immediate Observation Population Protocols

Cites work

• Automated recurrence analysis for almost-linear expected-runtime bounds
• Automatic average-case analysis of algorithms
• Computation in networks of passively mobile finite-state sensors
• Computation in networks of passively mobile finite-state sensors
• Convergence speed of binary interval consensus
• Fast and exact majority in population protocols
• How long, O Bayesian network, will I sample thee? A program analysis perspective on expected sampling times
• scientific article; zbMATH DE number 7204593 (Why is no real title available?)
• Large flocks of small birds: on the minimal size of population protocols
• Speed faults in computation by chemical reaction networks
• Time-space trade-offs in population protocols
• Verification of population protocols
• Weakest precondition reasoning for expected run-times of probabilistic programs

Cited in

(3)

• Explicit and tight bounds of the convergence time of average-based population protocols
• Population protocols: beyond runtime analysis
• Tight complexity analysis of population protocols with cover times -- the ZebraNet example

Describes a project that uses

Uses Software

• z3

This page was built for publication: Automatic analysis of expected termination time for population protocols

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5009451)