Below are details of all the models in the benchmark suite, grouped by type. Click on the name of a model to browse the model/property files. "Name" gives a short, unique name that can be used to refer to each model unambiguously, for example in a table of experimental results. "Model reference" gives a citation to the paper in which the model (PRISM or otherwise) was presented, if there is one. Other references, e.g. to the original system being modelled, are also given.
| Name | Full name | Model reference | Type | Parameters (+ explanation & suggested values) |
Links | Notes & other references |
| bluetooth | Bluetooth device discovery | [DKNP06] | DTMC |
mrec (number of replies received: e.g. 1,2) |
www | |
| brp | Bounded retransmission protocol | [DJJL01] | DTMC |
N (number of chunks in a file: e.g. 16,32,64) MAX (maximum number of retransmissions: e.g. 2,3,4,5) |
www | [DJJL01] presents the MDP model. An earlier, non-probabilistic model can be found in [HSV94]. |
| crowds | Crowds protocol | [Shm04] | DTMC |
CrowdSize (number of good crowd members: e.g. 5,10,15,20) TotalRuns (number of protocol runs: e.g. 3,4,5,6) |
www | The protocol is from [RR98]. |
| egl | Contract signing protocol of Even, Goldreich & Lempel | [NS06] | DTMC |
N (number of pairs of secrets: e.g. 2,4,6) L (number of bits per secret: e.g. 2,4,6) |
www | The protocol is from [EGL85]. |
| herman | Self-stabilisation protocol of Herman | [KNP12a] | DTMC |
N (number of processes (must be odd): e.g. 3,5,7,9) |
www | The protocol is from [Her90]. |
| nand | NAND multiplexing | [NPKS05] | DTMC |
N (number of inputs in each bundle: e.g. 20,40,60) K (number of restorative stages: e.g. 1,2,3) |
www | NAND multiplexing is from [vN56]. |
| leader_sync | Synchronous leader election protocol of Itai & Rodeh | DTMC |
N (number of processes: e.g. 3,4,5,6) K (range of probabilistic choice: e.g. 2,3,4,5) |
www | The protocol is from [IR90]. |
Links: [source] [model stats] [properties]
| Name | Full name | Model reference | Type | Parameters (+ explanation & suggested values) |
Links | Notes & other references |
| consensus | Shared coin protocol from the randomised consensus algorithm of Aspnes and Herlihy | [KNS01a] | MDP |
N (number of processes: e.g. 2,4,6,8,10) K (bounds on random walk: any value > 1) |
www | The protocol is from [AH90]. |
| csma | IEEE 802.3 CSMA/CD (Carrier Sense, Multiple Access with Collision Detection) protocol | [KNSW07] | MDP |
N (number of stations: e.g. 2,3,4) K (maximum backoff count: e.g. 2,4,6) |
www | PTA model |
| firewire | IEEE 1394 FireWire root contention protocol | [KNS03b] | MDP |
delay (maximum wire transmission delay, in units of 10ns: 3 or 36) |
www | PTA model from [KNS03b] based on TA model from [SS01]. |
| firewire_abst | IEEE 1394 FireWire root contention protocol (abstract model) | [KNS03b] | MDP |
delay (maximum wire transmission delay, in units of 10ns: 3 or 36) |
www | PTA model from [KNS03b] based on manual abstraction from [SV99]. |
| firewire_dl | IEEE 1394 FireWire root contention protocol (abstract model, with timer for deadline properties | [KNS03b] | MDP |
delay (maximum wire transmission delay, in units of 10ns: 3 or 36) deadline (timer deadline, in units of 10ns: e.g. 200,400,600) |
www | Extension of firewire_abst model above. |
| firewire_impl_dl | IEEE 1394 FireWire root contention protocol (with timer for deadline properties) | [KNS03b] | MDP |
delay (maximum wire transmission delay, in units of 10ns: 3 or 36) deadline (timer deadline, in units of 10ns: e.g. 200,400,600) |
www | Extension of firewire model above. |
| wlan | IEEE 802.11 wireless LAN | [KNS02a] | MDP |
BOFF (maximum backoff counter: e.g. 0,1,2,3) COL (maximum collision counter: only >0 if needed for property) |
www | PTA model |
| wlan_dl | IEEE 802.11 wireless LAN | [KNS02a] | MDP |
BOFF (maximum backoff counter: e.g. 0,1,2,3) deadline (timer deadline: e.g. 40,60,80) |
www | Extension of wlan model above. |
| zeroconf | IPv4 Zeroconf network configuration protocol | [KNPS06] | MDP |
N (number of existing nodes: e.g. 20,1000) K (number of probes sent (4 in standard): e.g. 2,4,6,8) reset (whether or not to clear messages on restart: e.g. 1,) |
www | PTA model. The protocol is from [CAG02]. |
| zeroconf_dl | IPv4 Zeroconf network configuration protocol (with timer for deadline properties) | [KNPS06] | MDP |
N (number of existing nodes: e.g. 20,1000) K (number of probes sent (4 in standard): e.g. 2,4,6,8) reset (whether or not to clear messages on restart: e.g. 1,) deadline (timer deadline: e.g. 20,40,60) |
www | Extension of zeroconf model above. The protocol is from [CAG02]. |
Links: [source] [model stats] [properties]
Note: "PTA model" indicates that the MDP was constructed from a probabilistic timed automaton (PTA) using digital clock semantics [KNPS06].
| Name | Full name | Model reference | Type | Parameters (+ explanation & suggested values) |
Links | Notes & other references |
| cluster | Workstation cluster | [HHK00] | CTMC |
N (number of workstations in each sub-cluster: e.g. 2,4,8) |
www | |
| embedded | Embedded control system | [MCT94] | CTMC |
MAX_COUNT (limit on allowed number of consecutive cycles skipped: e.g. 2,3,4) |
www | [MCT94] is a stochastic Petri net model. The PRISM model appears in [KNP04c], [KNP07b]. |
| erlangen | Erlangen mainframe | [GHP24] | CTMC |
size1 (Low priority job queue size: e.g. 10,20,30,40) size2 (High priority job queue size: e.g. 4,5,8,10) |
The original (TIPP) model appears in [HM94], [HHM95]. | |
| fms | Flexible manufacturing system | [CT93] | CTMC |
n (max number of parts per machine: e.g. 1,2,3) |
www | |
| kanban | Kanban manufacturing system | [CT96] | CTMC |
t (max jobs per machine: e.g. 1,2,3) |
www | |
| mapk_cascade | MAPK cascade | [HF96] | CTMC |
N (initial amount of MAPK/MAPKK and MAPKKK: e.g. 1,2,3) |
www | A PRISM model appears in [KNP08a]. |
| polling | Cyclic server polling system | [IT90] | CTMC |
N (number of stations handled by the server: e.g. 4,5,6) |
www | |
| tandem | Tandem queueing network | [HKMKS99] | CTMC |
c (queue capacity: e.g. 5,7,15,31) |
www |
Links: [source] [model stats] [properties]
| Name | Full name | Model reference | Type | Parameters (+ explanation & suggested values) |
Links | Notes & other references |
| csma | IEEE 802.3 CSMA/CD (Carrier Sense, Multiple Access with Collision Detection) protocol | [KNSW07] | PTA |
K (maximum backoff count: e.g. 2,4,6) COL (maximum number of collisions: 4,8) |
www | Number of stations is fixed at N=2. |
| csma_abst | IEEE 802.3 CSMA/CD (Carrier Sense, Multiple Access with Collision Detection) protocol (abstract model) | PTA |
K (maximum backoff count: e.g. 2,4,6) |
Number of stations is fixed at N=2. | ||
| firewire | IEEE 1394 FireWire root contention protocol | [KNS03b] | PTA |
delay (maximum wire transmission delay, in units of 10ns: 3 or 36) |
www | PTA model from [KNS03b] based on TA model from [SS01]. |
| firewire_abst | IEEE 1394 FireWire root contention protocol (abstract model) | [KNS03b] | PTA |
delay (maximum wire transmission delay, in units of 10ns: 3 or 36) |
www | PTA model from [KNS03b] based on manual abstraction from [SV99]. |
| repudiation_honest | Non-repudiation protocol (with honest recipient) | PTA | www | The protocol is due to Markowitch & Roggeman [MR99]. | ||
| repudiation_malicious | Non-repudiation protocol (with malicious recipient) | PTA | www | The protocol is due to Markowitch & Roggeman [MR99]. | ||
| zeroconf | IPv4 Zeroconf network configuration protocol | [KNPS06] | PTA | www | The protocol is from [CAG02]. |
Links: [source] [model stats] [properties]
Note: Model sizes are not available for PTAs since the whole (infinite-state) model is never explicitly constructed.
| Name | Full name | Model reference | Type | Parameters (+ explanation & suggested values) |
Links | Notes & other references |
| avoid | Avoid-The-Observer game | [CKWW20] | SMG |
X_MAX (grid width: e.g. 10,15,20) Y_MAX (grid height: e.g. 10,15,20) |
||
| dice | Simple dice game | SMG |
N (Max number of throws per player: e.g. 10,25,50) |
Example distributed with PRISM-games. | ||
| hallway_human | Hallway-Human game | [CKWW20] | SMG |
X_MAX (grid width: e.g. 5,8,10) Y_MAX (grid height: e.g. 5,8,10) |
||
| investors | Futures market investor | [CFK+13b] | SMG |
N (number of investors: e.g. 2,3) vmax (maximum share value: e.g. 10,20,50) |
Based on a model originally from [MM07]. | |
| safe_nav | Safe human-robot navigation | [JJK+18] | SMG |
N (grid size: e.g. 8) feat (feature configuration: e.g. A,B,C,D) |
www | Auto-generated model files. |
| task_graph | Task-graph scheduling with faults | [KNP19] | SMG |
N (number of tasks: e.g. 6,9) k1 (max number of faults for processor 1: e.g. 5,10,15) k2 (max number of faults for processor 2: e.g. 5,10,15) |
www | Generated from TPTG model (task_graph9_tptg.prism) via digital clocks translation. Extends a TA model from [BFLM11]. |
Links: [source] [model stats] [properties]
Note: We use the names stochastic multi-player game (SMG) and turn-based stochastic game (TSG) interchangeably.