License: 
Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSTTCS.2016.27
URN: urn:nbn:de:0030-drops-68628
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2016/6862/
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, 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.
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:1--27:14},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-027-9},
ISSN = {1868-8969},
year = {2016},
volume = {65},
editor = {Akash Lal and S. Akshay and Saket Saurabh and Sandeep Sen},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
address = {Dagstuhl, Germany},
URL = {http://drops.dagstuhl.de/opus/volltexte/2016/6862},
URN = {urn:nbn:de:0030-drops-68628},
doi = {10.4230/LIPIcs.FSTTCS.2016.27},
annote = {Keywords: parameterized systems, population protocols, probabilistic model checking, probabilistic linear-time specifications, decidability}
}
|
Keywords: |
|
parameterized systems, population protocols, probabilistic model checking, probabilistic linear-time specifications, decidability |
|
Collection: |
|
36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016) |
|
Issue Date: |
|
2016 |
|
Date of publication: |
|
10.12.2016 |
