TY - GEN
T1 - Advances in parameterized verification of population protocols
AU - Esparza, Javier
N1 - Publisher Copyright:
© Springer International Publishing AG 2017.
PY - 2017
Y1 - 2017
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85019250337&partnerID=8YFLogxK
U2 - 10.1007/978-3-319-58747-9_2
DO - 10.1007/978-3-319-58747-9_2
M3 - Conference contribution
AN - SCOPUS:85019250337
SN - 9783319587462
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 7
EP - 14
BT - Computer Science - Theory and Applications - 12th International Computer Science Symposium in Russia, CSR 2017, Proceedings
A2 - Weil, Pascal
PB - Springer Verlag
T2 - 12th International Computer Science Symposium in Russia, CSR 2017
Y2 - 8 June 2017 through 12 June 2017
ER -