SPIN'16 Paper - Supporting Material
Paper:
"Finite-Horizon Bisimulation Minimisation for Probabilistic Systems"
Nishanthan Kamaleson, David Parker and Jonathan E. Rowe
Models and Properties
Included below are the models and properties for the examples and case studies included in the paper.
-
Crowds: an anonymity protocol (TotalRuns=3, CrowdSize=5)
[RR98],
[Shm04]
-
Model: crowds.pm
-
Property file: crowds.pctl
-
Parameters:
- CrowdSize number of good crowd members: e.g. 5,10,15,20
- TotalRuns number of protocol runs: e.g. 3,4,5,6
-
EGL: a contract signing protocol (N=5, L=2)
[EGL85],
[NS06]
-
Model: egl.pm
-
Property file: egl.pctl
-
Parameters:
- N number of pairs of secrets: >1 e.g. 2,4,6,...
- L number of bits per secret: e.g. 2,4,6,...
-
NAND: NAND multiplexing (N=20, K=1)
[vN56],
[NPKS05]
-
Model: nand.pm
-
Property file: nand.pctl
-
Parameters:
- N number of inputs in each bundle: e.g. 20,40,60,...
- K number of restorative stages: e.g 1,2,3,...
-
Approximate majority: a population protocol
[AAE08]
(these models are, for convenience, specified as weighted DTMCs,
which can be built in PRISM by overriding the model type to be a CTMC and then normalising)
-
Simple genetic algorithms
[Vos99]:
"tournament"
(these models are, for convenience, specified as weighted DTMCs,
which can be built in PRISM by overriding the model type to be a CTMC and then normalising)
-
Models: tournament N : 4,5,8,10 (the agent with the highest value wins) and
-
Property files: tournament N : 4,5,8,10
-
Parameters:
- N fitness value
- K number of agents
-
Simple genetic algorithms
[Vos99]:
"modulus" variant
(these models are, for convenience, specified as weighted DTMCs,
which can be built in PRISM by overriding the model type to be a CTMC and then normalising)
-
Models: modulo N : 7, 9 (the sum of the two scores is used modulo N)
-
Property files: Modulo N : 7, 9
-
Parameters:
- N fitness value
- K number of agents