Thursday, February 25, 2016
Venue: IST Austria
Population protocols are a model for parameterized systems in which a set of identical, anonymous, finite-state processes interact pairwise through rendezvous synchronization. In each step, the pair of interacting processes is chosen by a random scheduler. Angluin et al. (PODS 2004) studied population protocols as a distributed computation model. They characterized the computational power in the limit (semi-linear predicates) of a subclass of protocols (the well-specified ones). However, the modeling power of protocols go beyond computation of semi-linear predicates and they can be used to study a wide range of distributed protocols, such as asynchronous leader election or consensus, stochastic evolutionary processes, or chemical reaction networks. Correspondingly, one is interested in checking specifications on these protocols that go beyond the well-specified computation of predicates.
We characterize the decidability frontier for the model checking problem for population protocols against
probabilistic linear-time specifications. We show that the model checking problem is decidable for qualitative objectives, but as hard as the reachability problem for Petri nets. However, it is undecidable for quantitative properties. Our decidability proof uses techniques from Petri net theory, and the characterization of limit behaviors of population protocols. In particular, our results show decidability of the following basic verification problems: Is a given protocol well-specified (i.e., computes a predicate in the sense of Angluin et al.)? Does a protocol compute a given predicate?
[Joint work with Javier Esparza, Pierre Ganty, and Jerome Leroux]