README.md 4.33 KB
Newer Older
1
Peregrine
Philipp Meyer's avatar
Philipp Meyer committed
2 3
=======

4
Tool for efficient verification of population protocols
5 6 7

Installation
-------
8 9 10 11 12
In order to compile and install Peregrine, go to the project's main directory and enter
```bash
    sudo make install
```

13 14
Compilation requires the Glasgow Haskell Compiler [ghc >= 7.8.1](https://www.haskell.org/ghc/)
and the build system [cabal >= 1.22](https://www.haskell.org/cabal/).
15

16 17 18
Input
------

Stefan Jaax's avatar
Stefan Jaax committed
19 20
Peregrine takes a single population protocol as JSON-encoded input.
The following example shows the input format:
21 22

```
Stefan Jaax's avatar
Stefan Jaax committed
23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47
{
    "title": "Majority Protocol",
    "states": ["A", "a", "B", "b"],
    "transitions": [
                    { "name": "t1",
                      "pre": ["A", "B"],
                      "post": ["a", "b"]
                    },
                    { "name": "t2",
                      "pre": ["B", "a"],
                      "post": ["B", "b"]
                    },
                    { "name": "t3",
                      "pre": ["A", "b"],
                      "post": ["A", "a"]
                    },
                    { "name": "t4",
                      "pre": ["a", "b"],
                      "post": ["a", "a"]
                    }
                   ],
    initialStates: ["A", "B"],
    trueStates: ["A", "a"],
    predicate: "A >= B",
    description: "This protocol computes whether there are more B-states than A-states"
48 49 50 51 52
}


```

53 54 55
Usage
-------

56
Peregrine is run from the command line.
Stefan Jaax's avatar
Stefan Jaax committed
57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80

If you save the protocol from above in the file *majority.pp* and enter:
```bash
    peregrine majority.pp
```

You obtain the following output:
```
Peregrine - Efficient Verification of Population Protocols

Reading "majority.pp"
Analyzing Population protocol "Majority Protocol"

Checking layered termination
Checking layered termination with at most 1 layers
Checking layered termination with at most 2 layers
layered termination satisfied

Checking strong consensus
strong consensus satisfied

All properties satisfied
```

81
As seen in the output, Peregrine by default checks two properties:
Stefan Jaax's avatar
Stefan Jaax committed
82 83
*Layered Termination* and *Strong Consensus*:

84
* Layered Termination: protocol is layered in a way that every fair run of the protocol
Stefan Jaax's avatar
Stefan Jaax committed
85 86
will eventually reach a terminal population where no more change occurs.
* Strong Consensus: every terminal population reachable from an initial population
87
  forms a consensus. Moreover, the boolean value of the consensus must be unique
Stefan Jaax's avatar
Stefan Jaax committed
88 89 90 91 92 93 94 95
  for a given initial population.

If both Layered Termination and Strong Consensus are satsified, then the protocol
is *well-specified*, i.e. the protocol robustly computes a predicate defined
by the mapping from input population to its unique consensus value.
Note that the converse direction need not hold: there are well-specified protocols
that violate the conjunction of Strong Consensus and Layered Termination.

96
Peregrine offers fine-grained control over the solution methods and the
Stefan Jaax's avatar
Stefan Jaax committed
97 98 99 100 101 102
verbosity of the output.
To see all options, enter:
```bash
    peregrine --help
```

103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126
Benchmarks
-------

In the `benchmarks` directory, scripts and tools to generate protocols
and evaluate Peregrine on these benchmarks can be found.
To run the benchmarks, Peregrine needs to be installed.
To compile the table to display the results, additionally
[Python 3](https://www.python.org/) with the [pandas](http://pandas.pydata.org/) library and
[LaTeX](https://www.latex-project.org/) are required.

In order to reproduce the results from the paper
"Towards Efficient Verification of Population Protocols",
go to the folder `benchmarks` and run
```bash
    make podc
```
The results are then compiled to the file `results-podc.pdf`.

In order to run all benchmarks, go to the folder `benchmarks` and run
```bash
    make
```
The results are then compiled to the file `results-complete.pdf`.

127 128 129
Authors
-------

130 131
* Philipp Meyer (<meyerphi@in.tum.de>)
* Stefan Jaax (<jaax@in.tum.de>)
132

133 134
References
--------
Philipp Meyer's avatar
Philipp Meyer committed
135
* Michael Blondin, Javier Esparza, Stefan Jaax, Philipp J. Meyer: “Towards Efficient Verification of Population Protocols”, 2017; [arXiv:1703.04367](http://arxiv.org/abs/1703.04367).
136

Philipp Meyer's avatar
Philipp Meyer committed
137
License
138
-------
Philipp Meyer's avatar
Philipp Meyer committed
139
Peregrine is licensed under the GNU GPLv3, see [LICENSE.md](LICENSE.md) for details.
140 141 142

Logo by [Juan Lacruz](https://commons.wikimedia.org/wiki/User:Juan_lacruz), [Peregrine Falcon La Cañada](https://commons.wikimedia.org/wiki/File:Peregrine_Falcon_La_Cañada.jpg), [CC BY-SA 3.0](https://creativecommons.org/licenses/by-sa/3.0/legalcode).