www.prismmodelchecker.org

PRISM Benchmark Suite - Models

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.

Discrete-time Markov chains (DTMCs)

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 [HSV+94].
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].
hermans 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]

Markov decision processes (MDPs)

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

Continuous-time Markov chains (CTMCs)

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

Probabilistic timed automata (PTAs)

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.

Stochastic multi-player games (SMGs)

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.

Benchmarks