Esparza, Javier ;
Ganty, Pierre ;
Leroux, Jérôme ;
Majumdar, Rupak
Model Checking Population Protocols
Abstract
Population protocols are a model for parameterized systems in which a set of identical, anonymous, finitestate 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 (semilinear predicates) of a subclass of protocols (the wellspecified ones). However, the modeling power of protocols go beyond computation of semilinear 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 wellspecified computation of predicates.
In this paper, we characterize the decidability frontier for the model checking problem for population protocols against probabilistic lineartime specifications. We show that the model checking problem is decidable for qualitative objectives, but as hard as the reachability problem for Petri nets  a wellknown hard problem without known elementary algorithms. On the other hand, model checking is undecidable for quantitative properties.
BibTeX  Entry
@InProceedings{esparza_et_al:LIPIcs:2016:6862,
author = {Javier Esparza and Pierre Ganty and J{\'e}r{\^o}me Leroux and Rupak Majumdar},
title = {{Model Checking Population Protocols}},
booktitle = {36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
pages = {27:127:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959770279},
ISSN = {18688969},
year = {2016},
volume = {65},
editor = {Akash Lal and S. Akshay and Saket Saurabh and Sandeep Sen},
publisher = {Schloss DagstuhlLeibnizZentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2016/6862},
URN = {urn:nbn:de:0030drops68628},
doi = {10.4230/LIPIcs.FSTTCS.2016.27},
annote = {Keywords: parameterized systems, population protocols, probabilistic model checking, probabilistic lineartime specifications, decidability}
}
2016
Keywords: 

parameterized systems, population protocols, probabilistic model checking, probabilistic lineartime specifications, decidability 
Seminar: 

36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)

Issue date: 

2016 
Date of publication: 

2016 