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 access the individual files, or download the whole benchmark suite from the front page.

"Name" gives a short 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 given in the rightmost column.

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: 1 or 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: >1 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: [model sizes] [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 MDP N (number of stations: e.g. 2,3,4,...)
K (maximum backoff count: e.g. 2,4,6,...)
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 (as above)
deadline (timer deadline, in units of 10 ns: e.g. 200,400,600,...)
www Extension of "firewire_abs" model above.
firewire_impl_dl IEEE 1394 FireWire root contention protocol (with timer for deadline properties) [KNS03b] MDP delay (as above)
deadline (timer deadline, in units of 10 ns: e.g. 200,400,600,...)
www Extension of "firewire" model above.
wlan IEEE 802.11 wireless LAN [KNS02a] MDP BOFF (maximum backoff counter: eg. 0,1,2,3,...)
COL (maximum collision counter: only >0 if needed for property)
www PTA model.
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: true/false)
www PTA model. The protocol is from [CAG02].
zeroconf_dl IPv4 Zeroconf network configuration protocol (with timer for deadline properties) [KNPS06] MDP N, K and reset (as above)
deadline (timer deadline: e.g. 20,40,60,...)
www Extension of "zeroconf" model above. The protocol is from [CAG02].

Links: [model sizes] [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: 2, 4, 8, ...)
www
embedded Embedded control system [MCT94] CTMC MAX_COUNT (limit on allowed number of consecutive cycles skipped: 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: 1, 2, 3, ...)
www
kanban Kanban manufacturing system [CT96] CTMC t (max jobs per machine: 1, 2, 3, ...)
www
mapk_cascade MAPK cascade [HF96] CTMC N (initial amount of MAPK/MAPKK and MAPKKK: 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: 4, 5, 6, ...)
www
tandem Tandem queueing network [HKMKS99] CTMC c (queue capacity: 5, 7, 15, 31, ...)
www

Links: [model sizes] [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 PTA K (maximum backoff count: e.g. 2,4,6,...)
COL (maximum number of collisions: e.g. 4,8,...)
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 1ns: 30 or 360)
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 1ns: 30 or 360)
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: [properties]

NB: Model sizes are not available for PTAs since the whole (infinite-state) model is never explicitly constructed.

Benchmarks