Model Type Original Parameters Property Type Storm Storm-static mcsta PRISM PET modes DFTRES STAMINA ModestFRETpiLRTDP ePMC
bluetooth DTMC PRISM 1 time E 12.3 TO / 12.2 13.0 / 13.0 ERR
coupon DTMC PGCL 9-4-5 collect_all_bounded Pb 4.7 275.1 / 4.8 29.0 180.0
coupon DTMC PGCL 9-4-5 exp_draws E 4.5 186.3 / 4.9 31.0 9.8 INC
coupon DTMC PGCL 15-4-5 collect_all_bounded Pb TO TO / TO TO / TO TO
coupon DTMC PGCL 15-4-5 exp_draws E 1408.4 TO / 1409.8 TO / TO 19.7 INC
crowds DTMC PRISM 5-20 positive P 2.7 15.4 / 2.5 7.5 7.8 / 7.8 TO / TO 1475.5 TO / TO 64.1
crowds DTMC PRISM 6-20 positive P 3.0 115.0 / 2.8 37.3 37.3 / 37.4 TO / TO 1187.3 TO / TO 327.6
egl DTMC PRISM 10-2 messagesB E 3.7 923.8 / 3.7 287.8 / 292.3 362.3 / 2.4 300.3 TO
egl DTMC PRISM 10-2 unfairA P 3.8 822.1 / 1.7 188.1 / 197.9 47.5 / 1.7 ERR / TO 428.7 TO
egl DTMC PRISM 10-8 messagesB E 16.5 TO / 15.8 TO / TO 64.8 / 64.1 1259.7 TO
egl DTMC PRISM 10-8 unfairA P 26.0 TO / 2.8 TO / 1433.5 17.5 / 17.5 ERR 1406.6 TO
haddad-monmege DTMC PRISM 100-0.7 exp_steps E 0.1 INC / 0.1 INC INC / 1.5 TO
haddad-monmege DTMC PRISM 100-0.7 target P 0.1 INC / 0.1 INC ERR / 4.6 TO TO TO / TO ERR
herman DTMC PRISM 15 steps E 4.2 22.6 / 3.2 5.9 / 5.9 ERR
nand DTMC PRISM 40-4 reliable P 8.6 18.6 / 7.5 7.0 15.9 / 16.0 TO / TO 1040.5 93.6
nand DTMC PRISM 60-4 reliable P 34.6 88.9 / 31.5 31.0 47.2 / 47.4 TO / TO 1208.5 522.1
oscillators DTMC PRISM 8-10-0.1-1-0.1-1.0 power_consumption E 209.8 193.2 60.0 / 60.1 426.6
oscillators DTMC PRISM 8-10-0.1-1-0.1-1.0 time_to_synch E 210.5 192.6 60.2 / 60.3 424.6
cluster CTMC PRISM 128-2000-20 premium_steady S 34.0 34.2 554.4 65.3 / 65.4 1.4 1319.3
cluster CTMC PRISM 128-2000-20 qos1 Pb 153.5 153.0 / 186.3 TO 628.9 / 634.3 TO INC 178.9
cluster CTMC PRISM 64-2000-20 below_min Eb 307.4 308.1 / 406.8 51.1 / 51.4 TO
embedded CTMC PRISM 8-12 actuators P 0.1 0.1 / 0.7 INC 1.7 / 1.7 37.4 TO INC
embedded CTMC PRISM 8-12 up_time E 0.1 0.1 / 0.7 INC 1.7 / 1.7 TO INC
fms CTMC PRISM 8 productivity S 119.0 120.6 TO 91.5 / 91.5 23.6 TO
kanban CTMC PRISM 5 throughput S 54.6 61.2 / 51.3 30.5 / 30.4 INC TO
majority CTMC PRISM 2100 change_state Pb 32.3 32.4 TO 100.2 / 99.6 TO 904.1 44.6
mapk_cascade CTMC PRISM 4-30 activated_time E 3.7 3.7 7.8 11.5 / 11.5 871.3 12.5
mapk_cascade CTMC PRISM 4-30 reactions Eb 236.5 190.4 / 232.9 256.2 / 255.7 182.1
philosophers CTMC GreatSPN 16-1 MaxPrReachDeadlockTB Pb 46.3 57.9 / 51.3 81.2 TO INC
philosophers CTMC GreatSPN 16-1 MaxPrReachDeadlock P 1.5 39.5 / 1.4 14.5 1.7 INC
philosophers CTMC GreatSPN 16-1 MinExpTimeDeadlock E 29.8 44.8 / 27.7 24.1 98.4
philosophers CTMC GreatSPN 20-1 MaxPrReachDeadlockTB Pb TO TO TO / TO TO INC
philosophers CTMC GreatSPN 20-1 MaxPrReachDeadlock P 2.0 TO / 2.2 1796.9 / 1311.3 2.0 INC
philosophers CTMC GreatSPN 20-1 MinExpTimeDeadlock E TO TO TO / TO 128.9
polling CTMC PRISM 18-16 s1_before_s2 P 17.3 183.7 / 15.5 248.6 65.2 / 65.0 TO TO 877.6
speed-ind CTMC PRISM 2100 change_state Pb 125.9 126.3 TO 241.1 / 240.7 TO TO 177.2
beb MDP Modest 4-8-7 LineSeized P 29.2 157.7 / 27.8 46.4 TO INC
beb MDP Modest 5-16-15 LineSeized P TO TO TO / TO ERR 2.5
consensus MDP PRISM 4-4 disagree P 1.5 1.5 4.3 11.5 / 11.5 TO / TO TO 11.5
consensus MDP PRISM 4-4 steps_min E 2.3 2.2 3.6 8.9 / 9.0 TO 10.5
consensus MDP PRISM 6-2 disagree P 6.1 36.7 / 6.1 82.1 147.1 / 147.0 TO / ERR TO 245.8
consensus MDP PRISM 6-2 steps_min E 3.7 45.9 / 3.7 97.0 185.9 / 185.8 TO 237.6
csma MDP PRISM 3-4 all_before_max P 5.8 16.7 / 5.4 6.0 42.6 / 42.4 59.2 167.8
csma MDP PRISM 3-4 time_max E 8.8 17.3 / 7.9 6.7 17.8 / 17.8 TO 167.6
csma MDP PRISM 4-2 all_before_max P 6.7 10.3 / 6.0 3.1 38.5 / 38.8 38.9 355.8
csma MDP PRISM 4-2 time_max E 6.3 10.3 / 5.7 4.4 14.7 / 14.6 TO 358.3
eajs MDP PRISM 5-250-11 ExpUtil E 19.4 57.2 / 20.6 17.6 21.7 / 21.7 TO ERR
eajs MDP PRISM 6-300-13 ExpUtil E 45.7 185.3 / 43.6 51.5 67.3 / 67.3 TO ERR
echoring MDP Modest 100 MaxOffline1 P 58.7 58.9 5.5 TO INC
elevators MDP PPDDL b-11-9 goal P 8.9 9.0 13.2 / 7.9 3.0 INC
exploding-blocksworld MDP PPDDL 10 goal P TO TO TO / TO TO 2.1
firewire MDP PRISM false-36-800 deadline Pb 28.2 33.8 / 27.9 24.8 / 25.3
pacman MDP PRISM 100 crash P 73.5 632.4 / 74.2 299.8 TO / TO ERR / TO TO TO
pacman MDP PRISM 60 crash P 32.5 275.1 / 31.3 136.2 TO / TO 199.1 / TO TO TO
pnueli-zuck MDP PRISM 5 live P 0.9 4.3 / 1.0 4.1 1.7 / 1.7 0.7 / 1.8 1.0 31.5
pnueli-zuck MDP PRISM 10 live P 2.2 TO / 2.4 TO / TO 14.9 / 14.9 0.6 1.5 TO
rabin MDP PRISM 10 live P 1.9 TO / 2.1 TO / TO 68.0 / 57.0 1.2 1.0 TO
rectangle-tireworld MDP PPDDL 11 goal P 22.9 22.9 / 22.9 7.5 / 7.8 112.7 INC
resource-gathering MDP PRISM 1300-100-100 expgold Eb 47.8 65.1 / 1.5 37.2 / 37.3
resource-gathering MDP PRISM 1300-100-100 expsteps E 25.8 25.8 155.4 52.4 / 52.3 TO
resource-gathering MDP PRISM 1300-100-100 prgoldgem Pb 48.8 91.1 / 46.3 23.4 / 23.4 TO
tireworld MDP PPDDL 45 goal P TO TO 401.9 / 455.8 1.0 INC
triangle-tireworld MDP PPDDL 441 goal P TO TO TO / TO 2.0 2.6
wlan MDP PRISM 4-0 sent P 2.2 3.4 / 2.4 4.5 10.2 / 10.2 TO TO 57.8
wlan MDP PRISM 4-0 cost_min E 4.9 4.3 / 4.6 14.6 21.6 / 21.6 3.0 129.6
wlan MDP PRISM 5-0 sent P 3.4 12.8 / 3.3 24.9 27.5 / 27.5 TO TO 231.7
wlan MDP PRISM 5-0 cost_min E 14.5 17.1 / 13.5 104.7 97.4 / 96.9 3.5 829.3
wlan MDP PRISM 6-0 sent P 6.6 51.2 / 5.7 173.5 99.1 / 99.9 TO TO 1167.1
wlan MDP PRISM 6-0 cost_min E 53.1 72.5 / 49.9 788.1 542.9 / 543.0 3.5 TO
zenotravel MDP PPDDL 4-2-2 goal P 7.0 24.6 / 6.3 31.3 / 11.0 2.0 INC
zeroconf MDP PRISM 1000-8-false correct_max P 23.7 23.8 12.4 186.0 / 186.2 43.5 / TO TO 93.4
zeroconf MDP PRISM 1000-8-false correct_min P 20.8 20.7 15.9 95.6 / 95.6 1.2 / INC INC 95.1
bitcoin-attack MA Modest 20-6 P_MWinMax Pb 0.5 0.1 / 0.5 0.6
cabinets MA Galileo 3-2-true Unavailability S 57.1 56.9 63.3 TO / 1228.6
cabinets MA Galileo 3-2-true Unreliability Pb 38.0 37.7 / 39.9 29.4 TO / TO
dpm MA Modest 4-8-5 PmaxQueuesFullBound Pb 46.1 45.9 76.8
dpm MA Modest 6-6-5 PminQueue1Full P 57.9 57.4 25.0
ftpp MA Galileo 2-2-true Unavailability S TO TO TO / TO 47.0 / 27.4
ftwc MA Modest 8-5 TimeMax E INC INC INC
ftwc MA Modest 8-5 TimeMin E INC INC INC
hecs MA Galileo false-1-1 Unreliability Pb 0.1 0.1 1.6 114.4 / 120.1
hecs MA Galileo false-2-2 Unreliability Pb 0.1 0.1 143.4 131.4 / 125.1
hecs MA Galileo false-3-2 Unreliability Pb 0.3 0.3 TO TO / TO
readers-writers MA GreatSPN 40 exp_time_many_requests E 28.0 28.3 19.2
readers-writers MA GreatSPN 40 prtb_many_requests Pb 540.7 463.2 / 534.8 TO
sms MA Galileo 3-true Unreliability Pb 0.1 0.1 0.8 3.1 / 0.7
sms MA Galileo 3-true Unavailability S 13.5 14.8 / 12.3 3.5 / 0.8
stream MA PRISM-MA 1000 exp_buffertime E 11.0 11.1 162.5
stream MA PRISM-MA 1000 pr_underrun P 2.7 2.7 1.4
stream MA PRISM-MA 1000 pr_underrun_tb Pb 7.9 7.9 14.4
vgs MA Galileo 5-10000 MaxPrReachFailedTB Pb 0.2 0.2 TO TO / TO
vgs MA Galileo 5-10000 MinExpTimeFailed E 0.2 0.2 TO
firewire-pta PTA PRISM 30-5000 deadline Pb 468.6 7.1 / 7.7
firewire-pta PTA PRISM 30-5000 eventually P 57.7 57.2 19.0 / 19.4 1.4 / 1.4
repudiation_malicious PTA PRISM 20 deadline Pb 27.0 / 27.8
repudiation_malicious PTA PRISM 20 eventually P 1.4 / 1.4
wlan-large PTA Modest 2 E_or E 46.2 46.5 20.8
wlan-large PTA Modest 2 P_max P 9.2 9.3 4.9
zeroconf-pta PTA PRISM 200 deadline Pb 0.6 1.5 / 1.5
zeroconf-pta PTA PRISM 200 incorrect P 0.4 0.4 / 0.4 0.6 1.4 / 1.4