2020/07/15 by Javier Esparza, Martin Helfrich, Esparza, Javier +5
Computer Science · #Distributed systems and fault tolerance #Privacy-Preserving Technologies in Data #Cryptography and Data Security
paper · pdf · doi:10.48550/arxiv.2007.07638
We present a new version of Peregrine, the tool for the analysis and\nparameterized verification of population protocols introduced in [Blondin et\nal., CAV'2018]. Population protocols are a model of computation, intensely\nstudied by the distributed computing community, in which mobile anonymous\nagents interact stochastically to perform a task.\n Peregrine 2.0 features a novel verification engine based on the construction\nof stage graphs. Stage graphs are proof certificates, introduced in [Blondin et\nal., CAV'2020], that are typically succinct and can be independently checked.\nMoreover, unlike the techniques of Peregrine 1.0, the stage graph methodology\ncan verify protocols whose executions never terminate, a class including recent\nfast majority protocols. Peregrine 2.0 also features a novel proof\nvisualization component that allows the user to interactively explore the stage\ngraph generated for a given protocol.\n