Notice to GitKraken users: A vulnerability has been found in the SSH key generation of GitKraken versions 7.6.0 to 8.0.0 (https://www.gitkraken.com/blog/weak-ssh-key-fix). If you use GitKraken and have generated a SSH key using one of these versions, please remove it both from your local workstation and from your LRZ GitLab profile.

21.10.2021, 9:00 - 11:00: Due to updates GitLab may be unavailable for some minutes between 09:00 and 11:00.

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

Philipp Meyer's avatar
Philipp Meyer committed
4
Tool for efficient verification of population protocols
Philipp Meyer's avatar
Philipp Meyer committed
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/).
Philipp Meyer's avatar
Philipp Meyer committed
15

16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
Input
------

Peregrine takes a single population protocol as input.
The following example shows how a protocol is encoded:

```
population protocol "Majority Protocol" {
    states { a b a_small b_small}
    transitions { t1 t2 t3 t4 }
    arcs { { a, b } -> t1 -> { a_small, b_small }
           { b, a_small } -> t2 -> { b, b_small }
           { a, b_small } -> t3 -> { a, a_small }
           { a_small, b_small } -> t4 -> { a_small, a_small }
         }
    initial { a b }
    true { a a_small }
33
    false { b b_small }
34
35
36
37
}


```
38
39
* After the keyword *population protocol* the name of the protocol is given in
quotes.
40

41
42
43
* Finite sets are specified in braces
through space- or comma-separated lists of  names.
Names consist of alphanumerical characters or underscores.
44

45
* The set of states is given after the identifier *states*.
46

47
* In order to make transitions identifiable,
Stefan Jaax's avatar
Stefan Jaax committed
48
each transition must be given a name after the  keyword *transitions*.
49

Stefan Jaax's avatar
Stefan Jaax committed
50
* Transitions are defined after the keyword *arcs*; there must be one definition
51
  for each transition name.
52

53
54
* The set following the keyword *initial* specifies states that can
belong to an initial population.
55

56
* The sets following the keywords *true* and *false* identify the states
57
58
59
60
that map to true and false, respectively.



Philipp Meyer's avatar
Philipp Meyer committed
61
62
63
Usage
-------

64
Peregrine is run from the command line.
Stefan Jaax's avatar
Stefan Jaax committed
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88

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
```

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

Stefan Jaax's avatar
Stefan Jaax committed
92
* Layered Termination: protocol is layered in a way that every fair run of the protocol
Stefan Jaax's avatar
Stefan Jaax committed
93
94
will eventually reach a terminal population where no more change occurs.
* Strong Consensus: every terminal population reachable from an initial population
95
  forms a consensus. Moreover, the boolean value of the consensus must be unique
Stefan Jaax's avatar
Stefan Jaax committed
96
97
98
99
100
101
102
103
  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.

104
Peregrine offers fine-grained control over the solution methods and the
Stefan Jaax's avatar
Stefan Jaax committed
105
106
107
108
109
110
verbosity of the output.
To see all options, enter:
```bash
    peregrine --help
```

111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
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`.

Philipp Meyer's avatar
Philipp Meyer committed
135
136
137
Authors
-------

Philipp Meyer's avatar
Philipp Meyer committed
138
139
* Philipp Meyer (<meyerphi@in.tum.de>)
* Stefan Jaax (<jaax@in.tum.de>)
Philipp Meyer's avatar
Philipp Meyer committed
140

Stefan Jaax's avatar
Stefan Jaax committed
141
142
References
--------
Stefan Jaax's avatar
Stefan Jaax committed
143
* 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].
Stefan Jaax's avatar
Stefan Jaax committed
144

Philipp Meyer's avatar
Philipp Meyer committed
145
146
Licence
-------
Philipp Meyer's avatar
Philipp Meyer committed
147
Peregrine is licensed under the GPLv3, see [LICENSE.md](LICENSE.md) for details.
Philipp Meyer's avatar
Philipp Meyer committed
148
149
150

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