Advances in parameterized verification of population protocols

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review


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.

Original languageEnglish
Title of host publicationComputer Science - Theory and Applications - 12th International Computer Science Symposium in Russia, CSR 2017, Proceedings
EditorsPascal Weil
PublisherSpringer Verlag
Number of pages8
ISBN (Print)9783319587462
StatePublished - 2017
Event12th International Computer Science Symposium in Russia, CSR 2017 - Kazan, Russian Federation
Duration: 8 Jun 201712 Jun 2017

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume10304 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference12th International Computer Science Symposium in Russia, CSR 2017
Country/TerritoryRussian Federation


Dive into the research topics of 'Advances in parameterized verification of population protocols'. Together they form a unique fingerprint.

Cite this