## Abstract

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).

Original language | English |
---|---|

Pages (from-to) | 191-215 |

Number of pages | 25 |

Journal | Acta Informatica |

Volume | 54 |

Issue number | 2 |

DOIs | |

State | Published - 1 Mar 2017 |

## Keywords

- C.2.2
- D.2.4
- F.3.1