PV1 ⊧ Peregrineverifies that a population protocol computes a user-specified predicate

Tool for the analysis and parameterized verification of population protocols

Application domain/field

• Population protocols
• Distributed computing
• Parameterized verification

Type of tool

Analysis tool

Expected input

Population protocol

Format:

Graphical editor or Python script

Expected output

Depends on the option chosen to analyse a protocol. For verification it will show whether correctness could be proven or not. If not, then it can give a counterexample.

Internals

Peregrine has several options for analysing a protocol, including:

• Manual step-by-step simulation
• Automatic sampling
• Statistics generation of average convergence speed
• Detection of incorrect executions through simulation
• Formal verification (only for silent protocols): This proves correctness for all of the infinitely many initial configurations. It verifies that a population protocol computes a given predicate. This predicate needs to be specified by the user in quantifier-free Presburger arithmetic

A protocol computes a predicate $\phi$ if, for every initial configuration $C$, all fair executions from $C$ lead to a lasting consensus $\phi (C)\in \{0,1\}$. Uses Z3 to check satisfiability of Presburger arithmetic formulas.

Comments

On scalability of Peregrine (from the CAV 2018 paper): "Currently, Peregrine can verify protocols with up to a hundred states and a few thousands transitions. The bottleneck is the size of the constraint system."