Succinct Population Protocols

Population models are a model of distributed computation by finite-state, anonymous and identical agents. Population protocols compute predicates in a population by reaching a lasting consensus through random pairwise interactions. A classical result establishes that population protocols compute exactly the predicates definable in Presburger arithmetic, the first-order theory of the natural numbers with addition. However, the best known upper bound for the number of states required per agent in a population protocol is exponential, where the predicate is given as quantifier-free formula with coefficients encoded in binary. We show that every Presburger predicate can be represented succinctly in population protocols: For every quantifier-free formula, there exists an equivalent population protocol where the number of states per agents is polynomial in the size of the formula. Our proof is constructive and may lead to space-efficient synthesis of multi-agent systems in low-resource environments, such as robot swarms, where each agent has very little memory at its disposal. Moreover, as opposed to a previous succinct construction for fragments of Presburger arithmetic presented at STACS’2018, our new construction does not need any additional agents besides the input agents. This is joint work with Michael Blondin and Javier Esparza.

Authors

• Stefan Jaax.

Keywords

No keywords are indexed for this paper.