Paper Info
Title
Succinct Population Protocols for Presburger Arithmetic.
Abstract
In [5], Angluin et al. proved that population protocols compute exactly the predicates definable in Presburger arithmetic (PA), the first-order theory of addition. As part of this result, they presented a procedure that translates any formula phi of quantifier-free PA with remainder predicates (which has the same expressive power as full PA) into a population protocol with 2(O(poly vertical bar phi vertical bar))) states that computes phi. More precisely, the number of states of the protocol is exponential in both the bit length of the largest coefficient in the formula, and the number of nodes of its syntax tree. In this paper, we prove that every formula phi of quantifier-free PA with remainder predicates is computable by a leaderless population protocol with O(poly vertical bar phi vertical bar)) states. Our proof is based on several new constructions, which may be of independent interest. Given a formula phi of quantifier-free PA with remainder predicates, a first construction produces a succinct protocol (with O(vertical bar phi vertical bar(3)) leaders) that computes phi; this completes the work initiated in [8], where we constructed such protocols for a fragment of PA. For large enough inputs, we can get rid of these leaders. If the input is not large enough, then it is small, and we design another construction producing a succinct protocol with one leader that computes phi. Our last construction gets rid of this leader for small inputs.
Year
DOI
Venue
2020
10.4230/LIPIcs.STACS.2020.40
Leibniz International Proceedings in Informatics
Keywords
DocType
Volume
Population protocols,Presburger arithmetic,state complexity
Conference
154
ISSN
Citations 
PageRank 
1868-8969
0
0.34
References 
Authors
0
5
Name
Order
Citations
PageRank
Michael Blondin1279.06
Javier Esparza277060.33
Blaise Genest330425.09
Martin Helfrich400.34
Stefan Jaax552.13