Verification of population protocols

Javier Esparza
Technische Universität München
Friday, 22 April, 2016 - 14:00
NO Solvay (5th floor)
Population protocols (Angluin et al., 2006) are a formal model of sensor networks consisting of identical mobile devices. When two devices come into the range of each other, they interact and change their states. Computations are infinite sequences of pairwise interactions where the interacting processes are picked by a fair scheduler. 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 predicates computable by well-specified protocols have been extensively studied, the two basic verification problems remain open: is a given protocol well-specified? Does a protocol compute a given predicate? In the first part of the talk we study these problems. In the second part we discuss the more general question of checking if a population protocol with a random scheduler satisfies a PLTL property.