Clocked Population Protocols
James Aspnes · 2017
Population protocols are required to converge to the correct answer, and are subject to a fairness condition that guarantees eventual progress, but generally have no internal mechanism for detecting when this progress has occurred. We define an extension to the standard population protocol that provides each agent with a clock signal that indicates when the agent has waited long enough. To simplify the model, we represent "long enough" as an infinite time interval, and treat a clocked population protocol as operating over transfinite time. This gives a clean theoretical model that we show how to translate back into finite real-world executions where the clock ticks whenever the underlying protocol is looping or stuck.