Verification of population protocols

• Published in: Acta informatica 2017-03, Vol.54 (2), p.191-215
• Main Authors: Esparza, Javier, Ganty, Pierre, Leroux, Jérôme, Majumdar, Rupak
• Format: Article
• Language: English
• Subjects: Algorithms; Arithmetic; Boolean; Computation; Computer Science; Computer Systems Organization and Communication Networks; Data Structures and Information Theory; Devices; Information Systems and Communication Service; Logics and Meanings of Programs; Mathematical analysis; Mobile communication systems; Networks; Original Article; Population; Program verification (computers); Protocol; Reduction; Sensors; Software Engineering/Programming and Operating Systems; Studies; Theory of Computation
• ISSN: 0001-5903; 1432-0525
• DOI: 10.1007/s00236-016-0272-3

Population protocols (Angluin et al. in PODC, 2004 ) 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 satisfying a strong fairness constraint. A population protocol is well specified if for every initial configuration C of devices, and every computation starting at C , all devices eventually agree on a consensus value depending only on C . If a protocol is well specified, then it is said to compute the predicate that assigns to each initial configuration its consensus value. While the computational power of well-specified protocols has been extensively studied, the two basic verification problems remain open: Is a given protocol well specified? Does a given protocol compute a given predicate? We prove that both problems are decidable by reduction to the reachability problem of Petri nets. We also give a new proof of the fact that the predicates computed by well-defined protocols are those definable in Presburger arithmetic (Angluin et al. in PODC , 2006 ).