QComp 2020 Benchmarks

 |  DTMC  |  CTMC  |  MDP  |  MA  |  PTA

These are the benchmarks used for the performance evaluation of QComp 2020, which are the same as used in QComp 2019 to allow for a direct comparison of the competitions' results.

DTMC Benchmarks

18 discrete-time Markov chain benchmark instances:

Model Original Parameters Property Type
1bluetoothPRISM1timeE
2couponPGCL9-4-5collect_all_boundedPb
3exp_drawsE
415-4-5collect_all_boundedPb
5exp_drawsE
6crowdsPRISM5-20positiveP
76-20positiveP
8eglPRISM10-2messagesBE
9unfairAP
1010-8messagesBE
11unfairAP
12haddad-monmegePRISM100-0.7exp_stepsE
13targetP
14hermanPRISM15stepsE
15nandPRISM40-4reliableP
1660-4reliableP
17oscillatorsPRISM8-10-0.1-1-0.1-1.0power_consumptionE
18time_to_synchE

CTMC Benchmarks

18 continuous-time Markov chain benchmark instances:

Model Original Parameters Property Type
19clusterPRISM64-2000-20below_minEb
20128-2000-20qos1Pb
21premium_steadyS
22embeddedPRISM8-12actuatorsP
23up_timeE
24fmsPRISM8productivityS
25kanbanPRISM5throughputS
26majorityPRISM2100change_statePb
27mapk_cascadePRISM4-30activated_timeE
28reactionsEb
29philosophersGreatSPN16-1MaxPrReachDeadlockTBPb
30MaxPrReachDeadlockP
31MinExpTimeDeadlockE
3220-1MaxPrReachDeadlockTBPb
33MaxPrReachDeadlockP
34MinExpTimeDeadlockE
35pollingPRISM18-16s1_before_s2P
36speed-indPRISM2100change_statePb

MDP Benchmarks

36 Markov decision process benchmark instances:

Model Original Parameters Property Type
37bebModest4-8-7LineSeizedP
385-16-15LineSeizedP
39consensusPRISM4-4disagreeP
40steps_minE
416-2disagreeP
42steps_minE
43csmaPRISM3-4all_before_maxP
44time_maxE
464-2all_before_maxP
47time_maxE
48eajsPRISM5-250-11ExpUtilE
496-300-13ExpUtilE
50echoringModest100MaxOffline1P
51elevatorsPPDDLb-11-9goalP
51exploding-blocksworldPPDDL10goalP
52firewirePRISMfalse-36-800deadlinePb
53pacmanPRISM60crashP
54100crashP
55pnueli-zuckPRISM5liveP
5610liveP
57rabinPRISM10liveP
58rectangle-tireworldPPDDL11goalP
59resource-gatheringPRISM1300-100-100expgoldEb
60expstepsE
61prgoldgemPb
62tireworldPPDDL45goalP
63triangle-tireworldPPDDL441goalP
64wlanPRISM4-0sentP
65cost_minE
665-0sentP
67cost_minE
686-0sentP
69cost_minE
70zenotravelPPDDL4-2-2goalP
71zeroconfPRISM1000-8-falsecorrect_maxP
72correct_minP

MA Benchmarks

20 Markov automaton benchmark instances:

Model Original Parameters Property Type
73bitcoin-attackModest20-6P_MWinMaxPb
74cabinetsGalileo3-2-trueUnavailabilityS
75UnreliabilityPb
76dpmModest4-8-5PmaxQueuesFullBoundPb
776-6-5PminQueue1FullP
78ftppGalileo2-2-trueUnavailabilityS
79ftwcModest8-5TimeMaxE
80TimeMinE
81hecsGalileofalse-1-1UnreliabilityPb
82false-2-2UnreliabilityPb
83false-3-2UnreliabilityPb
84readers-writersGreatSPN40exp_time_many_requestsE
85prtb_many_requestsPb
86smsGalileo3-trueUnreliabilityPb
87UnavailabilityS
88streamPRISM-MA1000exp_buffertimeE
89pr_underrunP
90pr_underrun_tbPb
91vgsGalileo5-10000PrReachFailedTBPb
92MinExpTimeFailedE

PTA Benchmarks

8 probabilistic timed automaton benchmark instances:

Model Original Parameters Property Type
93firewire-ptaPRISM30-5000deadlinePb
94eventuallyP
95repudiation_maliciousPRISM20deadlinePb
96eventuallyP
97wlan-largeModest2E_orE
98P_maxP
99zeroconf-ptaPRISM200deadlinePb
100incorrectP