2026-07-20T12:07:17Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5377 2024-03-06T10:36:33Z ddc:004 open_access

Verification of Population Protocols Esparza, Javier Ganty, Pierre Leroux, Jérôme Majumdar, Rupak Population protocols Petri nets parametrized verification 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. While the predicates computable by well-specified protocols have been extensively studied, the two basic verification problems remain open: is a given protocol well-specified? Does a protocol compute a given predicate? We prove that both problems are decidable. Our results also prove decidability of a natural question about home spaces of Petri nets. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Javier Esparza and Pierre Ganty and Jérôme Leroux and Rupak Majumdar 2015 Is Part Of LIPIcs, Volume 42, 26th International Conference on Concurrency Theory (CONCUR 2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CONCUR.2015.470 urn:nbn:de:0030-drops-53770 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2015.470 eng https://creativecommons.org/licenses/by/3.0/legalcode