Model Type Original Parameters Property Type Storm Storm-static mcsta PRISM PET modes DFTRES STAMINA
bluetooth DTMC PRISM 1 time E 10.4 TO / 12.4 17.8 / 17.8
coupon DTMC PGCL 9-4-5 collect_all_bounded Pb 4.7 273.9 / 4.8 31.3 1.3
coupon DTMC PGCL 9-4-5 exp_draws E 4.5 187.3 / 4.4 30.4 1.2
coupon DTMC PGCL 15-4-5 collect_all_bounded Pb TO TO / TO TO / TO 35.2
coupon DTMC PGCL 15-4-5 exp_draws E 1396.6 TO / 1446.4 TO / TO 1.2
crowds DTMC PRISM 5-20 positive P 2.7 15.5 / 2.6 7.1 7.7 / 7.7 TO / TO 1.8 13.1 / 15.0
crowds DTMC PRISM 6-20 positive P 3.0 115.0 / 3.0 34.6 37.3 / 37.3 TO / TO 1.7 70.3 / 36.1
egl DTMC PRISM 10-2 messagesB E 3.8 935.5 / 3.7 294.5 / 288.7 418.5 / 3.3 1.5
egl DTMC PRISM 10-2 unfairA P 3.8 823.9 / 1.6 185.4 / 200.1 53.8 / 1.8 ERR / TO 1.6
egl DTMC PRISM 10-8 messagesB E 16.5 TO / 15.6 TO / TO 100.1 / 98.8 2.0
egl DTMC PRISM 10-8 unfairA P 26.0 TO / 2.7 TO / 1409.3 17.5 / 17.6 ERR 2.0
haddad-monmege DTMC PRISM 100-0.7 exp_steps E 0.1 TO / 0.1 TO ERR / 1.6 TO
haddad-monmege DTMC PRISM 100-0.7 target P 0.1 INC / 0.1 TO ERR / 5.2 TO TO TO / TO
herman DTMC PRISM 15 steps E 4.3 22.7 / 3.5 10.4 / 10.4
nand DTMC PRISM 40-4 reliable P 8.6 18.8 / 7.8 7.2 16.1 / 16.5 TO / TO 1.6
nand DTMC PRISM 60-4 reliable P 35.6 90.3 / 33.4 31.6 48.0 / 48.4 TO / TO 1.7
oscillators DTMC PRISM 8-10-0.1-1-0.1-1.0 power_consumption E 210.1 193.3 84.6 / 84.8
oscillators DTMC PRISM 8-10-0.1-1-0.1-1.0 time_to_synch E 210.0 193.2 84.8 / 85.2
cluster CTMC PRISM 128-2000-20 premium_steady S 116.8 116.7 337.4 13.6 / 13.9 1.3
cluster CTMC PRISM 128-2000-20 qos1 Pb 445.5 444.6 / 568.4 TO 630.5 / 1104.4 TO INC
cluster CTMC PRISM 64-2000-20 below_min Eb 616.8 611.8 / 820.2 9.2 / 9.1 TO
embedded CTMC PRISM 8-12 actuators P 0.3 0.3 / 0.7 6.8 1.7 / 1.7 87.2 596.6
embedded CTMC PRISM 8-12 up_time E 0.3 0.3 / 0.7 10.1 1.7 / 1.7 19.2
fms CTMC PRISM 8 productivity S TO TO TO 72.2 / 72.0 1.4
kanban CTMC PRISM 5 throughput S 102.7 99.3 / 100.0 18.4 / 18.7 1.3
majority CTMC PRISM 2100 change_state Pb 63.0 62.7 TO 96.9 / 181.7 25.8 898.8
mapk_cascade CTMC PRISM 4-30 activated_time E 4.0 4.0 4.4 ERR / ERR 1.6
mapk_cascade CTMC PRISM 4-30 reactions Eb 238.0 191.4 / 233.3 INC / INC 1.3
philosophers CTMC GreatSPN 16-1 MaxPrReachDeadlockTB Pb 76.4 77.5 / 74.1 78.9 1146.8
philosophers CTMC GreatSPN 16-1 MaxPrReachDeadlock P 1.5 39.0 / 1.5 14.4 1.3
philosophers CTMC GreatSPN 16-1 MinExpTimeDeadlock E 27.6 44.3 / 28.0 21.6 1.3
philosophers CTMC GreatSPN 20-1 MaxPrReachDeadlockTB Pb TO TO TO / TO TO
philosophers CTMC GreatSPN 20-1 MaxPrReachDeadlock P 1.9 TO / 2.2 1799.6 / 1320.1 1.3
philosophers CTMC GreatSPN 20-1 MinExpTimeDeadlock E TO TO TO / TO 1.3
polling CTMC PRISM 18-16 s1_before_s2 P 24.8 186.3 / 22.8 165.6 42.2 / 39.8 TO 7.9
speed-ind CTMC PRISM 2100 change_state Pb 242.6 242.9 TO 239.9 / 570.0 38.1 TO
beb MDP Modest 4-8-7 LineSeized P 38.8 159.4 / 36.7 46.1
beb MDP Modest 5-16-15 LineSeized P TO TO TO / TO
consensus MDP PRISM 4-4 disagree P 1.4 1.4 2.6 10.7 / 10.8 TO / TO
consensus MDP PRISM 4-4 steps_min E 1.4 1.4 2.9 25.6 / 25.4
consensus MDP PRISM 6-2 disagree P 10.4 36.7 / 10.4 43.0 118.6 / 118.6 TO / ERR
consensus MDP PRISM 6-2 steps_min E 3.7 41.2 / 4.0 45.8 446.3 / 402.1
csma MDP PRISM 3-4 all_before_max P 6.7 16.8 / 6.2 6.1 120.8 / 121.2 51.7
csma MDP PRISM 3-4 time_max E 8.9 17.1 / 8.2 6.7 59.0 / 58.9
csma MDP PRISM 4-2 all_before_max P 7.2 10.4 / 6.5 3.1 65.4 / 65.0 37.2
csma MDP PRISM 4-2 time_max E 6.5 10.1 / 5.9 4.2 52.9 / 53.3
eajs MDP PRISM 5-250-11 ExpUtil E 19.5 58.1 / 18.4 17.9 53.7 / 53.7
eajs MDP PRISM 6-300-13 ExpUtil E 45.6 189.0 / 43.6 53.3 166.8 / 166.2
echoring MDP Modest 100 MaxOffline1 P 60.1 58.9 5.7
elevators MDP PPDDL b-11-9 goal P 8.8 9.1 7.4 / 8.1
exploding-blocksworld MDP PPDDL 10 goal P TO TO TO / TO
firewire MDP PRISM false-36-800 deadline Pb 29.6 33.8 / 27.8 31.0 / 31.0
pacman MDP PRISM 100 crash P 73.8 611.6 / 74.6 295.0 TO / TO ERR / ERR
pacman MDP PRISM 60 crash P 32.4 269.6 / 31.1 134.8 TO / TO 110.7 / TO
pnueli-zuck MDP PRISM 5 live P 0.9 4.3 / 0.9 3.1 1.7 / 1.7 0.6 / 295.0
pnueli-zuck MDP PRISM 10 live P 2.4 TO / 2.4 TO / TO 14.9 / 15.0 0.8
rabin MDP PRISM 10 live P 1.9 TO / 2.2 TO / TO 60.4 / 67.8 0.9
rectangle-tireworld MDP PPDDL 11 goal P 23.1 22.9 / 23.0 7.5 / 7.4
resource-gathering MDP PRISM 1300-100-100 expgold Eb 47.5 65.1 / 1.5 37.2 / 37.2
resource-gathering MDP PRISM 1300-100-100 expsteps E 37.7 37.7 156.2 ERR / ERR
resource-gathering MDP PRISM 1300-100-100 prgoldgem Pb 48.9 90.9 / 44.0 23.5 / 23.7 TO
tireworld MDP PPDDL 45 goal P TO TO 359.6 / 407.0
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.6 4.0 / 4.2 15.0 66.1 / 67.8
wlan MDP PRISM 5-0 sent P 3.4 12.9 / 3.6 24.8 27.5 / 27.4 TO
wlan MDP PRISM 5-0 cost_min E 12.6 15.5 / 11.7 102.8 455.8 / 547.5
wlan MDP PRISM 6-0 sent P 6.0 50.9 / 5.7 173.1 100.1 / 99.9 TO
wlan MDP PRISM 6-0 cost_min E 40.4 61.4 / 38.5 787.3 TO / TO
zenotravel MDP PPDDL 4-2-2 goal P 6.9 24.4 / 6.6 19.2 / 11.0
zeroconf MDP PRISM 1000-8-false correct_max P 25.4 25.2 13.2 213.8 / 213.6 13.7 / INC
zeroconf MDP PRISM 1000-8-false correct_min P 20.8 20.7 15.0 111.2 / 110.8 1.0 / INC
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 55.1 54.5 63.0 5.3 / 3.0
cabinets MA Galileo 3-2-true Unreliability Pb 28.2 28.0 / 39.6 29.1 138.7 / 125.2
dpm MA Modest 4-8-5 PmaxQueuesFullBound Pb 9.1 9.1 7.5
dpm MA Modest 6-6-5 PminQueue1Full P 57.8 57.5 23.1
ftpp MA Galileo 2-2-true Unavailability S TO TO TO / TO 24.6 / 5.1
ftwc MA Modest 8-5 TimeMax E 24.4 24.5 82.0
ftwc MA Modest 8-5 TimeMin E 23.3 23.4 78.4
hecs MA Galileo false-1-1 Unreliability Pb 0.1 0.1 1.6 4.7 / 1.4
hecs MA Galileo false-2-2 Unreliability Pb 0.1 0.1 144.3 7.5 / 2.6
hecs MA Galileo false-3-2 Unreliability Pb 0.4 0.4 TO 379.1 / 129.3
readers-writers MA GreatSPN 40 exp_time_many_requests E 20.0 20.4 12.8
readers-writers MA GreatSPN 40 prtb_many_requests Pb 522.8 450.7 / 516.1 TO
sms MA Galileo 3-true Unreliability Pb 0.1 0.1 0.8 3.2 / 0.7
sms MA Galileo 3-true Unavailability S 13.7 14.8 / 12.4 3.3 / 0.9
stream MA PRISM-MA 1000 exp_buffertime E 9.5 9.5 154.1
stream MA PRISM-MA 1000 pr_underrun P 2.7 2.7 1.5
stream MA PRISM-MA 1000 pr_underrun_tb Pb 5.1 5.1 13.9
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.8
firewire-pta PTA PRISM 30-5000 eventually P 56.8 57.3 17.0 / 18.4
repudiation_malicious PTA PRISM 20 deadline Pb
repudiation_malicious PTA PRISM 20 eventually P
wlan-large PTA Modest 2 E_or E 47.5 47.7 20.5
wlan-large PTA Modest 2 P_max P 9.3 9.3 4.9
zeroconf-pta PTA PRISM 200 deadline Pb 0.6
zeroconf-pta PTA PRISM 200 incorrect P 0.4 0.4 / 0.4 0.6