Population protocols (Angluin et al. PODC, 2004) are a for-mal 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, much less is known about how to verify their correct-ness: Given a population protocol, is it well specified? Given a population protocol and a predicate, does the protocol compute the predicate? Given a well-specified protocol, can we automatically obtain a symbolic repre-sentation of the predicate it computes? We survey our recent work on this problem.
CITATION STYLE
Esparza, J. (2017). Advances in parameterized verification of population protocols. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10304 LNCS, pp. 7–14). Springer Verlag. https://doi.org/10.1007/978-3-319-58747-9_2
Mendeley helps you to discover research relevant for your work.