Peregrine 2.0: Explaining Correctness of Population Protocols through Stage Graphs

TL;DR

Peregrine 2.0 introduces stage graphs for verifying population protocols, enabling analysis of non-terminating protocols and providing interactive visualization tools for better understanding.

Contribution

The paper presents Peregrine 2.0 with a new verification engine based on stage graphs, allowing analysis of protocols with infinite executions and improved visualization.

Findings

Stage graphs are succinct proof certificates for protocol correctness.

Peregrine 2.0 can verify protocols with non-terminating executions.

Interactive visualization enhances protocol analysis.

Abstract

We present a new version of Peregrine, the tool for the analysis and parameterized verification of population protocols introduced in [Blondin et al., CAV'2018]. Population protocols are a model of computation, intensely studied by the distributed computing community, in which mobile anonymous agents interact stochastically to perform a task. Peregrine 2.0 features a novel verification engine based on the construction of stage graphs. Stage graphs are proof certificates, introduced in [Blondin et al., CAV'2020], that are typically succinct and can be independently checked. Moreover, unlike the techniques of Peregrine 1.0, the stage graph methodology can verify protocols whose executions never terminate, a class including recent fast majority protocols. Peregrine 2.0 also features a novel proof visualization component that allows the user to interactively explore the stage graph generated for a given protocol.