@article{Esparza2017,
    Abstract = {Population protocols (Angluin et al. in 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 computational power of well-specified protocols has been extensively studied, the two basic verification problems remain open: Is a given protocol well specified? Does a given protocol compute a given predicate? We prove that both problems are decidable by reduction to the reachability problem of Petri nets. We also give a new proof of the fact that the predicates computed by well-defined protocols are those definable in Presburger arithmetic (Angluin et al. in PODC, 2006).},
    Author = {Esparza, Javier and Ganty, Pierre and Leroux, J{\'e}r{\^o}me and Majumdar, Rupak},
    File = {10.1007\%2Fs00236-016-0272-3 (0) - a - a - p.pdf},
    ISSN = {1432-0525},
    Journal = {Acta Informatica},
    Month = {Mar},
    Number = {2},
    Pages = {191--215},
    Title = {Verification of population protocols},
    URL = {https://doi.org/10.1007/s00236-016-0272-3},
    Volume = {54},
    Year = {2017},
    bdsk-url-1 = {https://doi.org/10.1007/s00236-016-0272-3},
    date-added = {2018-03-26 09:27:04 +0000},
    date-modified = {2018-03-26 09:27:04 +0000},
    day = {01},
    doi = {10.1007/s00236-016-0272-3}
}

@article{Esparza2017, Abstract = {Population protocols (Angluin et al. in 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 computational power of well-specified protocols has been extensively studied, the two basic verification problems remain open: Is a given protocol well specified? Does a given protocol compute a given predicate? We prove that both problems are decidable by reduction to the reachability problem of Petri nets. We also give a new proof of the fact that the predicates computed by well-defined protocols are those definable in Presburger arithmetic (Angluin et al. in PODC, 2006).}, Author = {Esparza, Javier and Ganty, Pierre and Leroux, J{\'e}r{\^o}me and Majumdar, Rupak}, File = {10.1007\%2Fs00236-016-0272-3 (0) - a - a - p.pdf}, ISSN = {1432-0525}, Journal = {Acta Informatica}, Month = {Mar}, Number = {2}, Pages = {191--215}, Title = {Verification of population protocols}, URL = {https://doi.org/10.1007/s00236-016-0272-3}, Volume = {54}, Year = {2017}, bdsk-url-1 = {https://doi.org/10.1007/s00236-016-0272-3}, date-added = {2018-03-26 09:27:04 +0000}, date-modified = {2018-03-26 09:27:04 +0000}, day = {01}, doi = {10.1007/s00236-016-0272-3} }