Titel: KIK-Vortrag "Parameterized verification of populat..
Startdatum: 04 Juli
Startzeit: 16:00
Stoppzeit: 17:00Uhr
Veranstalter: FG Intelligente Eingebettete Systeme - Prof. Dr. Bernhard Sick
Ort: Wilhelmshöher Allee 71-73, Hörsaal 0315

Prof. Dr. Javier Esparza

 "Parameterized verification of population protocols"

Population protocols (Angluin et al., PODC 2004) are a formal model of sensor networks consisting of identical, finite-state 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 for every fair computation starting at C, all devices eventually agree on a consensus value that only depends 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. The main two verification problems for population protocols are: Is a given protocol well-specified? Does a given protocol compute a given predicate?

While the class of predicates computable by population protocols was already established in 2007 (Angluin et al., Distributed Computing), the decidability of the verification problems remained open until 2015, when my colleagues and I finally proved it (Esparza et al., Acta Informatica).  However, the complexity of our decision procedures is very high. We have recently identified a class of procotols that, while being as expressive as the complete class, is far more tractable.  I report on these results, to appear in PODC 2017, and on some experimental results.