Model Checking Population Protocols
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. (PODC 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.
In this paper, 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 - a well-known hard problem without known elementary algorithms. On the other hand, model checking is undecidable for quantitative properties.
parameterized systems
population protocols
probabilistic model checking
probabilistic linear-time specifications
decidability
27:1-27:14
Regular Paper
Javier
Esparza
Javier Esparza
Pierre
Ganty
Pierre Ganty
Jérôme
Leroux
Jérôme Leroux
Rupak
Majumdar
Rupak Majumdar
10.4230/LIPIcs.FSTTCS.2016.27
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode