Peregrine

Peregrine is a tool for the design, parameterized verification and simulation of population protocols.

Peregrine is a tool for the analysis of population protocols.
Population protocols are a model of computation very much studied by the distributed computing community, in which mobile anonymous agents interact stochastically to achieve a common task. Peregrine allows users to design protocols, to simulate them both manually and automatically, to gather statistics of properties such as convergence speed, and to verify correctness automatically.

Peregrine allows the user to specify protocols either through an editor or as simple scripts, and to analyze them via a graphical interface. The analysis features of Peregrine include manual step-by-step simulation; automatic sampling; statistics generation of average convergence speed; detection of incorrect executions through simulation; and formal verification of correctness. The first four features are supported for all protocols, while verification is supported for silent protocols, a large subclass of protocols.

Download and Installation

Source Code

The latest version is 0.1 and was released on 2018-07-11. It can be downloaded here:

Detailed build and usage instructions can be found in README.md.

Binaries

For Windows users we offer an installer with precompiled 64-bit binaries. It can be downloaded here:

Contact

For feedback, comments and questions contact Stefan and Michael.

Citing

If you want to cite Peregrine in an academic publication, please use the following reference: