TY - GEN
T1 - Verification of population protocols
AU - Esparza, Javier
AU - Ganty, Pierre
AU - Leroux, Jérôme
AU - Majumdar, Rupak
N1 - Publisher Copyright:
© Javier Esparza, Pierre Ganty, Jérôme Leroux, and Rupak Majumdar; licensed under Creative Commons License CC-BY.
PY - 2015/8/1
Y1 - 2015/8/1
N2 - 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.
AB - 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.
KW - Parametrized verification
KW - Petri nets
KW - Population protocols
UR - http://www.scopus.com/inward/record.url?scp=84958249699&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.CONCUR.2015.470
DO - 10.4230/LIPIcs.CONCUR.2015.470
M3 - Conference contribution
AN - SCOPUS:84958249699
T3 - Leibniz International Proceedings in Informatics, LIPIcs
SP - 470
EP - 482
BT - 26th International Conference on Concurrency Theory, CONCUR 2015
A2 - Aceto, Luca
A2 - de Frutos Escrig, David
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
T2 - 26th International Conference on Concurrency Theory, CONCUR 2015
Y2 - 1 September 2015 through 4 September 2015
ER -