Document Open Access Logo

Model Checking Population Protocols

Authors Javier Esparza, Pierre Ganty, Jérôme Leroux, Rupak Majumdar



PDF
Thumbnail PDF

File

LIPIcs.FSTTCS.2016.27.pdf
  • Filesize: 0.52 MB
  • 14 pages

Document Identifiers

Author Details

Javier Esparza
Pierre Ganty
Jérôme Leroux
Rupak Majumdar

Cite AsGet BibTex

Javier Esparza, Pierre Ganty, Jérôme Leroux, and Rupak Majumdar. Model Checking Population Protocols. In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 27:1-27:14, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016)
https://doi.org/10.4230/LIPIcs.FSTTCS.2016.27

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.
Keywords
  • parameterized systems
  • population protocols
  • probabilistic model checking
  • probabilistic linear-time specifications
  • decidability

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail