# zbMATH — the first resource for mathematics

Verification of population protocols. (English) Zbl 1364.68081
Summary: Population protocols [D. Angluin et al., in: Proceedings of the 23rd annual ACM symposium on principles of distributed computing, PODC’04. New York, NY: Association for Computing Machinery (ACM). 290–299 (2004; Zbl 1321.68058)] 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 [D. Angluin et al., in: Proceedings of the 25th annual ACM symposium on principles of distributed computing, PODC’06. New York, NY: Association for Computing Machinery (ACM). 292–299 (2006; Zbl 1314.68054)].

##### MSC:
 68M12 Network protocols 03B70 Logic in computer science 68Q60 Specification and verification (program logics, model checking, etc.)
Coq; PAT
Full Text: