Model Type Original Parameters Property Type Storm Storm-static mcsta PRISM PET
bluetooth DTMC PRISM 1 time E 10.4 TO / 12.2 18.3 / 17.8
coupon DTMC PGCL 9-4-5 collect_all_bounded Pb 4.7 273.2 / 4.8 31.4
coupon DTMC PGCL 9-4-5 exp_draws E 4.5 189.2 / 4.4 31.0
coupon DTMC PGCL 15-4-5 collect_all_bounded Pb TO TO / TO TO / TO
coupon DTMC PGCL 15-4-5 exp_draws E 1398.2 TO / 1495.7 TO / TO
crowds DTMC PRISM 5-20 positive P 2.6 15.5 / 2.5 7.7 10.9 / 10.8 TO
crowds DTMC PRISM 6-20 positive P 3.0 115.5 / 2.8 38.6 56.2 / 56.3 TO
egl DTMC PRISM 10-2 messagesB E 3.8 929.2 / 3.7 286.7 / 290.0 420.4 / 3.3
egl DTMC PRISM 10-2 unfairA P 3.8 822.6 / 1.7 187.4 / 198.4 54.0 / 1.9 ERR
egl DTMC PRISM 10-8 messagesB E 16.5 TO / 15.7 TO / TO 99.1 / 99.4
egl DTMC PRISM 10-8 unfairA P 26.1 TO / 2.8 TO / 1412.4 17.5 / 17.6 ERR
haddad-monmege DTMC PRISM 100-0.7 exp_steps E 0.1 TO / 0.1 TO ERR / 1.6
haddad-monmege DTMC PRISM 100-0.7 target P 0.1 INC / 0.1 TO ERR / 4.7 TO
herman DTMC PRISM 15 steps E 4.2 22.7 / 3.2 16.1 / 15.9
nand DTMC PRISM 40-4 reliable P 8.7 18.7 / 7.8 6.9 16.1 / 16.1 TO
nand DTMC PRISM 60-4 reliable P 36.3 90.1 / 33.9 31.5 49.7 / 48.8 TO
oscillators DTMC PRISM 8-10-0.1-1-0.1-1.0 power_consumption E 210.7 189.3 85.9 / 86.1
oscillators DTMC PRISM 8-10-0.1-1-0.1-1.0 time_to_synch E 208.1 193.0 86.6 / 86.3
cluster CTMC PRISM 128-2000-20 premium_steady S 174.5 175.2 732.3 67.6 / 65.6
cluster CTMC PRISM 128-2000-20 qos1 Pb 457.1 450.2 / 581.1 TO 629.9 / 636.0
cluster CTMC PRISM 64-2000-20 below_min Eb 932.3 925.2 / 1238.9 51.3 / 51.3
embedded CTMC PRISM 8-12 actuators P 0.8 0.8 / 0.7 17.6 1.7 / 1.7 41.3
embedded CTMC PRISM 8-12 up_time E 0.7 0.7 / 0.7 34.9 1.7 / 1.7
fms CTMC PRISM 8 productivity S TO TO TO 91.4 / 91.7
kanban CTMC PRISM 5 throughput S 259.6 224.5 / 258.6 30.5 / 30.6
majority CTMC PRISM 2100 change_state Pb 65.4 65.1 TO 97.3 / 97.8
mapk_cascade CTMC PRISM 4-30 activated_time E 5.8 5.8 9.7 ERR / ERR
mapk_cascade CTMC PRISM 4-30 reactions Eb 235.4 192.0 / 229.5 256.4 / 255.9
philosophers CTMC GreatSPN 16-1 MaxPrReachDeadlockTB Pb 105.5 98.3 / 102.9 84.3
philosophers CTMC GreatSPN 16-1 MaxPrReachDeadlock P 1.5 38.7 / 1.4 14.4
philosophers CTMC GreatSPN 16-1 MinExpTimeDeadlock E 34.4 44.8 / 32.4 26.4
philosophers CTMC GreatSPN 20-1 MaxPrReachDeadlockTB Pb TO TO TO / TO
philosophers CTMC GreatSPN 20-1 MaxPrReachDeadlock P 1.9 TO / 2.3 1797.4 / 1305.8
philosophers CTMC GreatSPN 20-1 MinExpTimeDeadlock E TO TO TO / TO
polling CTMC PRISM 18-16 s1_before_s2 P 45.2 203.3 / 42.3 275.5 136.0 / 145.0 TO
speed-ind CTMC PRISM 2100 change_state Pb 252.2 251.7 TO 241.1 / 241.1
beb MDP Modest 4-8-7 LineSeized P 41.3 159.9 / 36.5 46.6
beb MDP Modest 5-16-15 LineSeized P TO TO TO / TO
consensus MDP PRISM 4-4 disagree P 2.5 2.5 5.9 23.2 / 23.1 TO
consensus MDP PRISM 4-4 steps_min E 2.8 2.7 5.8 51.7 / 51.8
consensus MDP PRISM 6-2 disagree P 8.0 54.8 / 8.0 107.2 309.7 / 310.7 TO
consensus MDP PRISM 6-2 steps_min E 3.9 71.4 / 4.2 94.7 1103.4 / 984.4
csma MDP PRISM 3-4 all_before_max P 6.6 16.8 / 6.3 5.9 121.3 / 121.4 59.0
csma MDP PRISM 3-4 time_max E 8.9 16.8 / 8.0 6.7 65.7 / 65.4
csma MDP PRISM 4-2 all_before_max P 7.2 10.3 / 6.5 3.1 65.4 / 65.3 37.2
csma MDP PRISM 4-2 time_max E 6.4 10.1 / 5.9 4.5 58.0 / 58.6
eajs MDP PRISM 5-250-11 ExpUtil E 19.4 58.4 / 18.4 17.6 53.8 / 53.8
eajs MDP PRISM 6-300-13 ExpUtil E 46.0 187.6 / 43.9 52.1 166.6 / 166.7
echoring MDP Modest 100 MaxOffline1 P 59.4 59.0 5.6
elevators MDP PPDDL b-11-9 goal P 8.9 9.0 13.5 / 8.0
exploding-blocksworld MDP PPDDL 10 goal P TO TO TO / TO
firewire MDP PRISM false-36-800 deadline Pb 27.6 33.8 / 27.7 32.1 / 32.1
pacman MDP PRISM 100 crash P 73.3 622.1 / 72.6 293.5 TO / TO ERR
pacman MDP PRISM 60 crash P 32.0 270.8 / 31.3 133.6 TO / TO 248.3
pnueli-zuck MDP PRISM 5 live P 0.9 4.3 / 0.9 3.7 1.7 / 1.7 0.7
pnueli-zuck MDP PRISM 10 live P 2.2 TO / 2.4 TO / TO 14.9 / 15.0 1.0
rabin MDP PRISM 10 live P 1.9 TO / 2.3 TO / TO 60.6 / 67.6 1.3
rectangle-tireworld MDP PPDDL 11 goal P 23.0 22.9 / 23.0 7.4 / 7.6
resource-gathering MDP PRISM 1300-100-100 expgold Eb 47.7 65.5 / 1.5 37.3 / 37.3
resource-gathering MDP PRISM 1300-100-100 expsteps E 38.4 38.4 153.7 ERR / ERR
resource-gathering MDP PRISM 1300-100-100 prgoldgem Pb 48.9 90.9 / 46.1 23.5 / 23.5 TO
tireworld MDP PPDDL 45 goal P TO TO 424.4 / 476.9
triangle-tireworld MDP PPDDL 441 goal P TO TO TO / TO
wlan MDP PRISM 4-0 sent P 2.2 3.3 / 2.2 4.4 9.9 / 9.9 TO
wlan MDP PRISM 4-0 cost_min E 4.8 4.0 / 4.5 15.0 58.6 / 57.1
wlan MDP PRISM 5-0 sent P 3.4 12.8 / 3.3 24.8 27.3 / 27.6 TO
wlan MDP PRISM 5-0 cost_min E 12.7 15.4 / 11.7 102.4 453.8 / 436.7
wlan MDP PRISM 6-0 sent P 6.0 51.0 / 5.7 173.0 100.3 / 99.8 TO
wlan MDP PRISM 6-0 cost_min E 40.4 61.6 / 38.2 788.8 TO / TO
zenotravel MDP PPDDL 4-2-2 goal P 7.2 24.4 / 7.0 36.2 / 11.2
zeroconf MDP PRISM 1000-8-false correct_max P 25.9 25.6 13.4 221.1 / 220.8 24.5
zeroconf MDP PRISM 1000-8-false correct_min P 23.1 22.8 16.4 120.4 / 119.9 5.8
bitcoin-attack MA Modest 20-6 P_MWinMax Pb 20.5 26.4 / 20.4 163.5
cabinets MA Galileo 3-2-true Unavailability S 57.0 57.1 63.0
cabinets MA Galileo 3-2-true Unreliability Pb 30.3 30.3 / 39.0 29.4
dpm MA Modest 4-8-5 PmaxQueuesFullBound Pb TO TO TO
dpm MA Modest 6-6-5 PminQueue1Full P 59.1 58.3 24.9
ftpp MA Galileo 2-2-true Unavailability S TO TO TO / TO
ftwc MA Modest 8-5 TimeMax E 68.4 68.4 246.3
ftwc MA Modest 8-5 TimeMin E 65.4 65.3 232.9
hecs MA Galileo false-1-1 Unreliability Pb 0.2 0.2 1.6
hecs MA Galileo false-2-2 Unreliability Pb 0.1 0.1 143.4
hecs MA Galileo false-3-2 Unreliability Pb 0.4 0.4 TO
readers-writers MA GreatSPN 40 exp_time_many_requests E 24.9 25.2 21.7
readers-writers MA GreatSPN 40 prtb_many_requests Pb 544.5 490.5 / 552.1 TO
sms MA Galileo 3-true Unreliability Pb 0.1 0.1 0.8
sms MA Galileo 3-true Unavailability S 13.7 14.8 / 12.5
stream MA PRISM-MA 1000 exp_buffertime E 9.5 9.5 171.7
stream MA PRISM-MA 1000 pr_underrun P 2.8 2.7 1.4
stream MA PRISM-MA 1000 pr_underrun_tb Pb 8.1 8.2 15.1
vgs MA Galileo 5-10000 MaxPrReachFailedTB Pb 0.3 0.3 TO
vgs MA Galileo 5-10000 MinExpTimeFailed E 0.2 0.2 TO
firewire-pta PTA PRISM 30-5000 deadline Pb 468.3
firewire-pta PTA PRISM 30-5000 eventually P 57.5 57.6 18.4 / 18.2
repudiation_malicious PTA PRISM 20 deadline Pb
repudiation_malicious PTA PRISM 20 eventually P
wlan-large PTA Modest 2 E_or E 47.9 48.2 20.5
wlan-large PTA Modest 2 P_max P 9.2 9.3 4.8
zeroconf-pta PTA PRISM 200 deadline Pb 0.6
zeroconf-pta PTA PRISM 200 incorrect P 0.4 0.4 / 0.4 0.6