> Details

van Bergerem, Steffen [Author]; Guttenberg, Roland [Author]; Kiefer, Sandra [Author]; Mascle, Corto [Author]; Waldburger, Nicolas [Author]; Weil-Kennedy, Chana [Author] ; Steffen van Bergerem and Roland Guttenberg and Sandra Kiefer and Corto Mascle and Nicolas Waldburger and Chana Weil-Kennedy [Contributor]

Verification of Population Protocols with Unordered Data

Reference
management

Bookmarks

Remove from
bookmarks

Share this on Whatsapp

Close

Bookmarks



You can manage bookmarks using lists, please log in to your user account for this.
  • Media type: Text; E-Article; Electronic Conference Proceeding
  • Title: Verification of Population Protocols with Unordered Data
  • Contributor: van Bergerem, Steffen [Author]; Guttenberg, Roland [Author]; Kiefer, Sandra [Author]; Mascle, Corto [Author]; Waldburger, Nicolas [Author]; Weil-Kennedy, Chana [Author]
  • Published: Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2024
  • Language: English
  • DOI: https://doi.org/10.4230/LIPIcs.ICALP.2024.156
  • Keywords: Well-specification ; Distributed computing ; Population protocols ; Parameterized verification
  • Origination:
  • Footnote: Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
  • Description: Population protocols are a well-studied model of distributed computation in which a group of anonymous finite-state agents communicates via pairwise interactions. Together they decide whether their initial configuration, i. e., the initial distribution of agents in the states, satisfies a property. As an extension in order to express properties of multisets over an infinite data domain, Blondin and Ladouceur (ICALP'23) introduced population protocols with unordered data (PPUD). In PPUD, each agent carries a fixed data value, and the interactions between agents depend on whether their data are equal or not. Blondin and Ladouceur also identified the interesting subclass of immediate observation PPUD (IOPPUD), where in every transition one of the two agents remains passive and does not move, and they characterised its expressive power. We study the decidability and complexity of formally verifying these protocols. The main verification problem for population protocols is well-specification, that is, checking whether the given PPUD computes some function. We show that well-specification is undecidable in general. By contrast, for IOPPUD, we exhibit a large yet natural class of problems, which includes well-specification among other classic problems, and establish that these problems are in ExpSpace. We also provide a lower complexity bound, namely coNExpTime-hardness.
  • Access State: Open Access