Model Type Original Parameters Property Type epmc mcsta modes Storm ModestFRETpiLRTDP PRISM PRISM-TUM DFTRES probFD
bluetooth DTMC PRISM 1 time E ERR TO / 11.0 13.6 / 12.9
coupon DTMC PGCL 9-4-5 collect_all_bounded Pb 65.6 / 53.7 342.4 / 305.4 340.5 / 5.7
coupon DTMC PGCL 9-4-5 exp_draws E 495.8 107.2 / 93.4 14.8 / 12.9 215.3 / 5.8
coupon DTMC PGCL 15-4-5 collect_all_bounded Pb TO / TO TO / INC TO / 528.1
coupon DTMC PGCL 15-4-5 exp_draws E ERR TO / TO 34.2 / 27.8 TO / 503.4
crowds DTMC PRISM 5-20 positive P 40.3 16.7 / 11.4 1633.2 / 1375.7 17.3 / 4.1 7.0 / 7.2 TO
crowds DTMC PRISM 6-20 positive P 200.4 78.0 / 58.8 1421.3 / 1145.0 138.0 / 4.5 27.8 / 12.4 TO
egl DTMC PRISM 10-2 messagesB E TO 338.2 / 327.4 303.2 / INC 1157.0 / 4.1 90.6 / 2.3
egl DTMC PRISM 10-2 unfairA P TO 237.0 / 227.6 402.4 / 380.2 1050.6 / 3.2 54.4 / 1.8 TO
egl DTMC PRISM 10-8 messagesB E TO TO / TO 1248.9 / 1206.1 TO / 19.8 1431.5 / 63.5
egl DTMC PRISM 10-8 unfairA P TO 1641.8 / 1528.9 1434.8 / 1330.3 TO / 5.1 512.9 / 16.2 TO
haddad-monmege DTMC PRISM 100-0.7 exp_steps E TO INC / INC ERR / ERR INC / 0.1 ERR / 1.6
haddad-monmege DTMC PRISM 100-0.7 target P INC INC / TO ERR / ERR INC / 0.0 ERR / 4.5 TO
herman DTMC PRISM 15 steps E ERR 25.9 / 6.2 8.8 / 5.6
nand DTMC PRISM 40-4 reliable P 75.0 13.7 / 6.7 1645.1 / 1239.4 21.9 / 12.5 89.1 / 15.5 TO
nand DTMC PRISM 60-4 reliable P 432.8 50.9 / 28.7 TO / 1354.1 104.5 / 52.3 566.5 / 43.1 TO
oscillators DTMC PRISM 8-10-0.1-1-0.1-1.0 power_consumption E 311.3 TO / ERR ERR / TO 301.4 / 203.5 61.2 / 61.1
oscillators DTMC PRISM 8-10-0.1-1-0.1-1.0 time_to_synch E 323.8 ERR / ERR TO / ERR 302.0 / 207.8 60.9 / 59.9
cluster CTMC PRISM 128-2000-20 premium_steady S 220.0 INC / 17.4 24.9 / 8.4
cluster CTMC PRISM 128-2000-20 qos1 Pb 179.0 TO / TO TO / INC 155.3 1097.7 / 633.1
cluster CTMC PRISM 64-2000-20 below_min Eb TO / INC 310.6 96.5 / 52.0
embedded CTMC PRISM 8-12 actuators P 11.9 INC / INC ERR / INC 0.1 0.8 / 1.5 17.7 / 2.5
embedded CTMC PRISM 8-12 up_time E ERR INC / INC ERR / 1681.5 0.1 0.8 / 1.5
fms CTMC PRISM 8 productivity S TO 145.4 490.6 / 90.6
kanban CTMC PRISM 5 throughput S 326.5 INC / 79.7 ERR / 30.2
majority CTMC PRISM 2100 change_state Pb 43.5 TO / TO TO / INC 34.5 184.3 / 101.3
mapk_cascade CTMC PRISM 4-30 activated_time E 14.3 9.3 / 8.4 1215.3 / 1182.9 4.1 462.9 / 10.4
mapk_cascade CTMC PRISM 4-30 reactions Eb 253.7 / 249.7 192.5 677.9 / 252.8
philosophers CTMC GreatSPN 16-1 MaxPrReachDeadlockTB Pb 167.9 249.2 / 235.9 TO / INC 80.0 / 67.9
philosophers CTMC GreatSPN 16-1 MaxPrReachDeadlock P 130.5 33.3 / 23.2 2.2 / 2.1 57.6 / 1.9
philosophers CTMC GreatSPN 16-1 MinExpTimeDeadlock E 39.2 / 26.1 146.1 / 139.4 64.1 / 43.9
philosophers CTMC GreatSPN 20-1 MaxPrReachDeadlockTB Pb TO TO / TO TO / INC TO / TO
philosophers CTMC GreatSPN 20-1 MaxPrReachDeadlock P TO TO / TO 2.6 / 2.6 TO / 2.6
philosophers CTMC GreatSPN 20-1 MinExpTimeDeadlock E TO / TO 201.7 / 208.1 TO / TO
polling CTMC PRISM 18-16 s1_before_s2 P 1646.6 435.1 / 386.3 ERR / 1681.5 206.9 / 26.0 990.6 / 66.3 TO
speed-ind CTMC PRISM 2100 change_state Pb 172.1 TO / TO TO / INC 137.3 580.3 / 240.3
beb MDP Modest 4-8-7 LineSeized P 407.0 86.1 / 66.0 ERR / 1.6 171.1 / 43.4 TO
beb MDP Modest 5-16-15 LineSeized P TO TO / TO ERR / 2.0 TO ERR
consensus MDP PRISM 4-4 disagree P 16.3 5.3 / 4.1 1.8 TO 14.2 / 11.2 TO
consensus MDP PRISM 4-4 steps_min E 20.4 4.6 / 3.7 2.2 8.9 / 9.0
consensus MDP PRISM 6-2 disagree P 348.8 81.1 / 77.7 38.7 / 6.8 TO 327.7 / 145.9 TO
consensus MDP PRISM 6-2 steps_min E 461.8 84.5 / 79.3 48.3 / 4.6 188.6 / 186.0
csma MDP PRISM 3-4 all_before_max P 132.7 10.2 / 8.5 19.0 48.5 / 40.9 71.0
csma MDP PRISM 3-4 time_max E 133.0 12.9 / 11.3 19.6 / 12.0 17.8 / 17.9
csma MDP PRISM 4-2 all_before_max P 289.2 6.3 / 5.2 11.8 43.3 / 43.6 41.8
csma MDP PRISM 4-2 time_max E 298.7 8.1 / 6.9 11.8 / 8.3 14.5 / 14.5
eajs MDP PRISM 5-250-11 ExpUtil E ERR 27.5 / 21.4 69.9 / 17.6 21.4 / 21.7
eajs MDP PRISM 6-300-13 ExpUtil E ERR 80.4 / 65.2 223.8 / 32.3 66.2 / 67.7
echoring MDP Modest 100 MaxOffline1 P INC 18.5 / 16.7 92.8 TO
elevators MDP PPDDL b-11-9 goal P 56.4 15.1 / 13.4 ERR / 98.7 10.3 0.9 0.5
exploding-blocksworld MDP PPDDL 10 goal P TO TO / TO TO ERR 39.9
firewire MDP PRISM false-36-800 deadline Pb 36.9 / 36.6 59.2
pacman MDP PRISM 100 crash P TO 205.7 / 189.0 593.9 / 83.6 TO / TO TO
pacman MDP PRISM 60 crash P TO 93.9 / 84.2 260.8 / 32.0 TO / TO 227.5
pnueli-zuck MDP PRISM 5 live P 25.6 5.2 / 4.2 ERR / 1.9 7.6 / 1.2 0.9 1.3 / 1.3 2.3 TO
pnueli-zuck MDP PRISM 10 live P TO TO / TO ERR / 5.7 TO / 3.4 1.5 14.3 / 14.3 2.4 TO
rabin MDP PRISM 10 live P TO TO / TO ERR / 1.6 TO / 3.0 1.0 66.7 / 66.5 2.4 TO
rectangle-tireworld MDP PPDDL 11 goal P 5.7 131.6 / 129.1 22.3 129.4 3.8
resource-gathering MDP PRISM 1300-100-100 expgold Eb 64.1 / 3.1 36.4 / 36.8
resource-gathering MDP PRISM 1300-100-100 expsteps E INC 197.8 / 194.5 30.6 52.7 / 52.4
resource-gathering MDP PRISM 1300-100-100 prgoldgem Pb 95.9 45.2 / 23.5
tireworld MDP PPDDL 45 goal P TO 496.6 / 460.2 TO TO 0.1
triangle-tireworld MDP PPDDL 441 goal P TO TO / TO TO 1.7 0.3
wlan MDP PRISM 4-0 sent P 42.3 8.3 / 6.2 ERR / 1.8 4.8 9.7 / 9.7 139.8
wlan MDP PRISM 4-0 cost_min E 103.1 25.7 / 25.2 5.5 20.8 / 20.8
wlan MDP PRISM 5-0 sent P 183.4 38.1 / 36.1 ERR / 1.9 17.2 26.3 / 26.3 TO
wlan MDP PRISM 5-0 cost_min E 689.3 183.1 / 180.8 21.6 95.4 / 95.7
wlan MDP PRISM 6-0 sent P 1094.9 264.1 / 257.5 ERR / 2.0 68.2 95.4 / 95.8 TO
wlan MDP PRISM 6-0 cost_min E TO 1433.3 / 1411.7 92.2 542.4 / 542.1
zenotravel MDP PPDDL 4-2-2 goal P 45.2 28.8 / 26.5 ERR / 34.6 26.5 1.0 0.9
zeroconf MDP PRISM 1000-8-false correct_max P 57.5 12.5 / 9.6 26.8 TO 195.4 / 194.6 17.1
zeroconf MDP PRISM 1000-8-false correct_min P 61.5 16.9 / 14.1 24.6 110.6 / 110.5 3.4
bitcoin-attack MA Modest 20-6 P_MWinMax Pb 1.0 / 0.9 TO
cabinets MA Galileo 3-2-true Unavailability S 98.4 1027.4 / 1160.0
cabinets MA Galileo 3-2-true Unreliability Pb 72.6 / 67.9 ERR / INC 49.0 TO / TO
dpm MA Modest 4-8-5 PmaxQueuesFullBound Pb 295.4 / 293.1 TO
dpm MA Modest 6-6-5 PminQueue1Full P 44.6 / 31.9 64.3
ftpp MA Galileo 2-2-true Unavailability S TO 46.2 / 31.3
ftwc MA Modest 8-5 TimeMax E INC / INC INC / 99.8
ftwc MA Modest 8-5 TimeMin E INC / INC INC / 50.8
hecs MA Galileo false-1-1 Unreliability Pb 5.1 / 2.4 ERR / INC 0.1 / 0.1 95.7 / 96.1
hecs MA Galileo false-2-2 Unreliability Pb 182.7 / 165.7 ERR / 1681.9 3.1 / 0.1 131.6 / 117.7
hecs MA Galileo false-3-2 Unreliability Pb TO / TO ERR / INC TO / 0.7 TO / TO
readers-writers MA GreatSPN 40 exp_time_many_requests E 28.4 / 24.8 144.6 / 139.4 28.9
readers-writers MA GreatSPN 40 prtb_many_requests Pb TO / TO 279.9 / 262.9 TO
sms MA Galileo 3-true Unreliability Pb 1.1 / 1.0 TO / 1681.4 0.1 TO / TO
sms MA Galileo 3-true Unavailability S 21.5 186.0 / 180.8
stream MA PRISM-MA 1000 exp_buffertime E 214.8 / 212.3 12.2
stream MA PRISM-MA 1000 pr_underrun P 2.5 / 1.7 36.8
stream MA PRISM-MA 1000 pr_underrun_tb Pb 33.7 / 32.0 11.3
vgs MA Galileo 5-10000 MaxPrReachFailedTB Pb TO / TO 0.2 / 0.1 TO
vgs MA Galileo 5-10000 MinExpTimeFailed E TO / TO 0.2 / 0.2 TO
firewire-pta PTA PRISM 30-5000 deadline Pb TO / 811.7 6.1 / 6.6
firewire-pta PTA PRISM 30-5000 eventually P 218.6 / 155.8 ERR / 3.9 776.4 0.9 / 0.9
repudiation_malicious PTA PRISM 20 deadline Pb 22.8 / 24.3
repudiation_malicious PTA PRISM 20 eventually P 1.0 / 1.0
wlan-large PTA Modest 2 E_or E 72.1 / 39.7 53.9
wlan-large PTA Modest 2 P_max P 8.0 / 4.2 46.1
zeroconf-pta PTA PRISM 200 deadline Pb 1.0 / 0.9 1.2 / 1.2
zeroconf-pta PTA PRISM 200 incorrect P 0.9 / 0.9 ERR / INC 0.6 0.8 / 0.8