Population protocols (Angluin et al., PODC 2004) are a formal model of sensor networks consisting of identical, finite-stae 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., CONCUR 2015, improved version to appear in 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, and on some experimental results.
Javier Esparza holds the Chair for Foundations of Software Reliability and Theoretical Computer Science at the Technische Universität München since 2007. Previously he held the Chair of Software Reliability and Security at the University of Stuttgart (2003-2007), the Chair of Theoretical Computer Science at the University of Edinburgh (2001-2003), and worked as Associate Professor at the Technische Universität München (1994-2001). He has co-authored a book on Free Choice Petri nets with Jörg Desel, and a book on the unfolding approach to Model Checking with Keijo Heljanko. He has published over 150 scientific papers in the fields of automatic program verification, program analysis, concurrency theory, and automata theory. Javier Esparza has contributed to the theory Petri nets, and was one of the initiators of the unfolding approach to model checking, the automata-theoretic approach to software model checking, and the verification of infinite-state systems. More recently he has conducted research on the fundamentals of program analysis and the verification of parametrized and stochastic systems. His group has developed several verification tools, including Moped and jMoped and Rabinizer. Javier Esparza received a honorary doctorate in Informatics from the Masaryk University of Brno in 2009 and is member of Academia Europaea since 2011.
For additional information: https://www7.in.tum.de/~esparz