# 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 protocolFormat:

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

*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.