As seen in the output, Peregrine by default checks two properties:
*Layered Termination* and *Strong Consensus*:
* Layered Termination: every fair run of the protocol
* Layered Termination: protocol is layered in a way that every fair run of the protocol
will eventually reach a terminal population where no more change occurs.
* Strong Consensus: every terminal population reachable from an initial population
forms a consensus. Moreover, the boolean value of the consensus must be unique
@@ -113,6 +113,10 @@ Authors
* Philipp Meyer (<meyerphi@in.tum.de>)
* Stefan Jaax (<jaax@in.tum.de>)
References
--------
* Michael Blondin, Javier Esparza, Stefan Jaax, Philipp J. Meyer: “Towards Efficient Verification of Population Protocols”, 2017; [http://arxiv.org/abs/1703.04367 arXiv:1703.04367].
Licence
-------
Peregrine is licensed under the GPLv3, see [LICENSE.md](LICENSE.md) for details.
