Model Type Original Parameters Property Type Storm.sparse Storm.hybrid Storm.dd Storm.ddbisim Storm.sound Storm.exact
beb MDP Modest 4-8-7 LineSeized P 127.7 16.7 28.5 22.6 130.3 334.6
beb MDP Modest 5-16-15 LineSeized P MO TO TO MO MO MO
bitcoin-attack MA Modest 20-6 P_MWinMax Pb 2.2 NS NS 1.1 2.0 NS
bluetooth DTMC PRISM 1 time E TO MO 7.1 8.6 TO TO
cabinets MA Galileo 3-2-true Unavailability S 82.0 NS NS NS 95.7 MO
cabinets MA Galileo 3-2-true Unreliability Pb 45.8 NS NS NS 37.3 NS
cluster CTMC PRISM 128-2000-20 premium_steady S 29.5 6.9 NS 55.8 109.9 MO
cluster CTMC PRISM 128-2000-20 qos1 Pb 65.8 84.5 NS 114.8 80.3 NS
cluster CTMC PRISM 64-2000-20 below_min Eb 137.9 116.7 NS 154.4 123.7 NS
consensus MDP PRISM 4-4 disagree P 1.1 2.4 71.6 1.8 1.8 8.8
consensus MDP PRISM 4-4 steps_min E 2.2 4.4 31.8 1.9 2.0 4.3
consensus MDP PRISM 6-2 disagree P 27.6 28.1 158.4 3.9 42.7 TO
consensus MDP PRISM 6-2 steps_min E 29.8 55.0 59.4 8.7 58.5 TO
coupon DTMC PGCL 15-4-5 collect_all_bounded Pb MO NS NS 913.9 MO MO
coupon DTMC PGCL 15-4-5 exp_draws E MO MO TO 804.9 MO MO
coupon DTMC PGCL 9-4-5 collect_all_bounded Pb MO NS NS 3.4 MO MO
coupon DTMC PGCL 9-4-5 exp_draws E 139.1 95.6 92.0 3.6 184.2 MO
crowds DTMC PRISM 5-20 positive P 13.2 5.8 4.1 1.9 12.6 44.1
crowds DTMC PRISM 6-20 positive P 120.9 67.4 5.5 2.2 97.0 295.0
csma MDP PRISM 3-4 all_before_max P 13.2 3.3 8.3 10.6 11.6 24.4
csma MDP PRISM 3-4 time_max E 17.7 6.0 138.9 9.0 18.3 52.7
csma MDP PRISM 4-2 all_before_max P 7.9 3.8 16.9 5.5 8.1 15.7
csma MDP PRISM 4-2 time_max E 7.6 4.7 102.2 6.5 12.2 19.4
dpm MA Modest 4-8-5 PmaxQueuesFullBound Pb 38.7 NS NS 58.1 42.8 NS
dpm MA Modest 6-6-5 PminQueue1Full P 81.7 NS NS MO 86.7 MO
eajs MDP PRISM 5-250-11 ExpUtil E 38.6 17.7 66.7 12.7 58.2 97.7
eajs MDP PRISM 6-300-13 ExpUtil E 132.1 110.6 196.9 30.1 200.7 297.1
echoring MDP Modest 100 MaxOffline1 P 59.2 NS NS NS 70.6 141.9
egl DTMC PRISM 10-2 messagesB E MO 485.7 2.4 1.5 MO MO
egl DTMC PRISM 10-2 unfairA P 720.2 0.8 0.8 2.7 710.7 MO
egl DTMC PRISM 10-8 messagesB E MO MO 15.4 9.7 MO MO
egl DTMC PRISM 10-8 unfairA P MO 1.3 2.1 15.1 MO MO
elevators MDP PPDDL b-11-9 goal P 6.9 MO MO MO 7.8 23.3
embedded CTMC PRISM 8-12 actuators P 0.1 0.5 NS 0.8 1.4 0.5
embedded CTMC PRISM 8-12 up_time E 3.1 12.4 NS 12.4 3.9 0.6
exploding-blocksworld MDP PPDDL 10 goal P MO MO MO MO MO MO
firewire-pta PTA PRISM 30-5000 eventually P 385.7 NS NS NS 371.0 546.7
firewire MDP PRISM false-36-800 deadline Pb 33.3 NS NS 18.1 33.5 352.7
fms CTMC PRISM 8 productivity S 85.7 87.0 NS TO TO MO
ftpp MA Galileo 2-2-true Unavailability S TO NS NS NS TO MO
ftwc MA Modest 8-5 TimeMax E INC NS NS NS 66.4 1526.5
ftwc MA Modest 8-5 TimeMin E INC NS NS NS 40.7 TO
haddad-monmege DTMC PRISM 100-0.7 exp_steps E INC INC INC INC TO 0.1
haddad-monmege DTMC PRISM 100-0.7 target P INC INC INC INC TO 0.1
hecs MA Galileo false-1-1 Unreliability Pb 0.2 NS NS NS 0.2 NS
hecs MA Galileo false-2-2 Unreliability Pb 86.4 NS NS NS 114.9 NS
hecs MA Galileo false-3-2 Unreliability Pb MO NS NS NS MO MO
herman DTMC PRISM 15 steps E 24.6 3.0 73.3 2.0 26.0 TO
kanban CTMC PRISM 5 throughput S 48.3 32.6 NS TO 198.4 MO
majority CTMC PRISM 2100 change_state Pb 21.3 49.8 NS 52.0 25.5 NS
mapk_cascade CTMC PRISM 4-30 activated_time E 2.7 13.5 NS 18.5 4.6 TO
mapk_cascade CTMC PRISM 4-30 reactions Eb 134.8 105.8 NS 110.6 104.4 NS
nand DTMC PRISM 40-4 reliable P 13.2 4.9 42.3 657.7 13.3 65.6
nand DTMC PRISM 60-4 reliable P 62.7 21.1 TO MO 59.6 MO
oscillators DTMC PRISM 8-10-0.1-1-0.1-1.0 power_consumption E 297.9 MO MO MO 400.2 475.7
oscillators DTMC PRISM 8-10-0.1-1-0.1-1.0 time_to_synch E 302.3 MO MO MO 400.8 481.2
pacman MDP PRISM 100 crash P 324.4 47.3 240.4 MO 377.1 518.7
pacman MDP PRISM 60 crash P 157.9 20.8 29.7 MO 163.4 200.9
philosophers CTMC GreatSPN 16-1 MaxPrReachDeadlock P 32.0 0.7 NS 143.0 32.3 115.2
philosophers CTMC GreatSPN 16-1 MaxPrReachDeadlockTB Pb 54.0 27.0 NS 143.5 45.9 NS
philosophers CTMC GreatSPN 16-1 MinExpTimeDeadlock E 40.1 17.6 NS 144.9 41.0 TO
philosophers CTMC GreatSPN 20-1 MaxPrReachDeadlock P MO 1.0 NS MO MO MO
philosophers CTMC GreatSPN 20-1 MaxPrReachDeadlockTB Pb MO MO NS MO MO MO
philosophers CTMC GreatSPN 20-1 MinExpTimeDeadlock E MO MO NS MO MO MO
pnueli-zuck MDP PRISM 10 live P MO 1.3 1.2 MO MO MO
pnueli-zuck MDP PRISM 5 live P 4.9 0.7 0.7 2.5 5.9 10.5
polling CTMC PRISM 18-16 s1_before_s2 P 118.6 11.2 NS MO 134.3 MO
rabin MDP PRISM 10 live P MO 1.0 1.0 4.9 MO MO
readers-writers MA GreatSPN 40 exp_time_many_requests E 19.4 NS NS MO 20.4 MO
readers-writers MA GreatSPN 40 prtb_many_requests Pb TO NS NS MO TO NS
rectangle-tireworld MDP PPDDL 11 goal P 13.0 19.7 19.8 20.2 12.7 13.1
resource-gathering MDP PRISM 1300-100-100 expgold Eb 34.3 27.5 1.1 1.3 36.5 TO
resource-gathering MDP PRISM 1300-100-100 expsteps E 21.7 23.1 109.2 307.3 34.7 99.3
resource-gathering MDP PRISM 1300-100-100 prgoldgem Pb 66.3 28.2 19.0 322.7 62.2 TO
sms MA Galileo 3-true Unavailability S 18.6 NS NS NS 16.3 51.1
sms MA Galileo 3-true Unreliability Pb 0.1 NS NS NS 0.1 NS
speed-ind CTMC PRISM 2100 change_state Pb 103.2 116.8 NS 187.0 90.3 NS
stream MA PRISM-MA 1000 exp_buffertime E 7.5 NS NS 230.4 7.6 26.7
stream MA PRISM-MA 1000 pr_underrun P 25.3 NS NS 427.6 29.5 48.4
stream MA PRISM-MA 1000 pr_underrun_tb Pb 7.5 NS NS 351.4 6.6 NS
tireworld MDP PPDDL 45 goal P TO TO 1321.5 TO TO MO
triangle-tireworld MDP PPDDL 441 goal P MO MO MO MO MO MO
vgs MA Galileo 5-10000 MaxPrReachFailedTB Pb TO MO TO TO TO TO
vgs MA Galileo 5-10000 MinExpTimeFailed E TO TO MO TO TO TO
wlan-large PTA Modest 2 E_or E 37.8 NS NS NS 1582.6 114.8
wlan-large PTA Modest 2 P_max P 6.2 NS NS NS 7.1 19.4
wlan MDP PRISM 4-0 cost_min E 3.6 12.1 29.8 128.6 3.7 7.8
wlan MDP PRISM 4-0 sent P 3.0 1.1 1.1 125.1 2.8 5.4
wlan MDP PRISM 5-0 cost_min E 13.1 16.5 89.1 794.7 14.4 28.9
wlan MDP PRISM 5-0 sent P 11.2 1.8 1.8 859.9 12.6 21.8
wlan MDP PRISM 6-0 cost_min E 58.7 37.8 325.9 TO 59.3 122.8
wlan MDP PRISM 6-0 sent P 49.7 3.3 3.3 TO 47.3 94.1
zenotravel MDP PPDDL 4-2-2 goal P 14.5 4.3 4.6 19.9 15.6 24.8
zeroconf-pta PTA PRISM 200 incorrect P 0.1 NS NS NS 0.1 0.1
zeroconf MDP PRISM 1000-8-false correct_max P 17.9 17.4 268.8 103.3 22.0 TO
zeroconf MDP PRISM 1000-8-false correct_min P 16.9 16.7 666.8 99.7 21.3 49.9