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: 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 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 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_abst" 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.
wlan_dl IEEE 802.11 wireless LAN [KNS02a] MDP deadline (timer deadline: eg. 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: 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 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: 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 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 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