Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH scholarly article en Esparza, Javier; Ganty, Pierre; Majumdar, Rupak; Weil-Kennedy, Chana http://www.dagstuhl.de/lipics License
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-95695
URL:

; ; ;

Verification of Immediate Observation Population Protocols

pdf-format:


Abstract

Population protocols (Angluin et al., PODC, 2004) are a formal model of sensor networks consisting of identical mobile devices. Two devices can interact and thereby change their states. Computations are infinite sequences of interactions satisfying a strong fairness constraint. A population protocol is well-specified if for every initial configuration C of devices, and every computation starting at C, all devices eventually agree on a consensus value depending only on C. If a protocol is well-specified, then it is said to compute the predicate that assigns to each initial configuration its consensus value. In a previous paper we have shown that the problem whether a given protocol is well-specified and the problem whether it computes a given predicate are decidable. However, in the same paper we prove that both problems are at least as hard as the reachability problem for Petri nets. Since all known algorithms for Petri net reachability have non-primitive recursive complexity, in this paper we restrict attention to immediate observation (IO) population protocols, a class introduced and studied in (Angluin et al., PODC, 2006). We show that both problems are solvable in exponential space for IO protocols. This is the first syntactically defined, interesting class of protocols for which an algorithm not requiring Petri net reachability is found.

BibTeX - Entry

@InProceedings{esparza_et_al:LIPIcs:2018:9569,
  author =	{Javier Esparza and Pierre Ganty and Rupak Majumdar and Chana Weil-Kennedy},
  title =	{{Verification of Immediate Observation Population Protocols}},
  booktitle =	{29th International Conference on Concurrency Theory  (CONCUR 2018)},
  pages =	{31:1--31:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-087-3},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{118},
  editor =	{Sven Schewe and Lijun Zhang},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2018/9569},
  URN =		{urn:nbn:de:0030-drops-95695},
  doi =		{10.4230/LIPIcs.CONCUR.2018.31},
  annote =	{Keywords: Population protocols, Immediate Observation, Parametrized verification}
}

Keywords: Population protocols, Immediate Observation, Parametrized verification
Seminar: 29th International Conference on Concurrency Theory (CONCUR 2018)
Issue date: 2018
Date of publication: 2018


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI