Model Type Original Parameters Property Type Modysh ePMC probFD mcsta PRISM PET Storm-static
beb MDP Modest 4-8-7 LineSeized P TO INC 21.7 95.7
beb MDP Modest 5-16-15 LineSeized P TO 1.2 TO TO
consensus MDP PRISM 4-4 disagree P TO 5.9 3.7 5.4 TO 1.4
consensus MDP PRISM 4-4 steps_min E TO 5.0 2.0 3.8 1.0
consensus MDP PRISM 6-2 disagree P TO 139.3 46.0 74.7 TO 19.7
consensus MDP PRISM 6-2 steps_min E TO 112.4 42.6 85.3 23.4
csma MDP PRISM 3-4 all_before_max P TO 84.0 2.6 29.8 35.7 8.3
csma MDP PRISM 3-4 time_max E TO 74.0 3.0 9.2 8.3
csma MDP PRISM 4-2 all_before_max P TO 152.2 1.3 26.7 22.1 4.9
csma MDP PRISM 4-2 time_max E TO 151.3 2.0 7.6 4.8
eajs MDP PRISM 5-250-11 ExpUtil E TO ERR 8.0 10.7 29.2
eajs MDP PRISM 6-300-13 ExpUtil E TO ERR 23.1 34.0 93.0
echoring MDP Modest 100 MaxOffline1 P TO INC 2.5 28.9
elevators MDP PPDDL b-11-9 goal P 4.8 INC 0.3 7.2 4.8
exploding-blocksworld MDP PPDDL 10 goal P TO INC 23.5 TO TO
firewire MDP PRISM false-36-800 deadline Pb TO 10.5 19.2
pacman MDP PRISM 100 crash P TO TO 148.6 TO ERR 272.5
pacman MDP PRISM 60 crash P 532.1 TO 70.7 TO 114.0 117.0
pnueli-zuck MDP PRISM 5 live P 0.3 14.5 422.6 2.0 1.3 0.3 2.4
pnueli-zuck MDP PRISM 10 live P 0.6 TO TO ERR 10.9 0.4 ERR
rabin MDP PRISM 10 live P 0.3 TO TO TO 54.2 0.5 ERR
rectangle-tireworld MDP PPDDL 11 goal P 4.7 INC 2.6 4.1 12.2
resource-gathering MDP PRISM 1300-100-100 expgold Eb TO 16.7 24.7
resource-gathering MDP PRISM 1300-100-100 expsteps E TO 96.0 25.3 17.7
resource-gathering MDP PRISM 1300-100-100 prgoldgem Pb TO 10.5 TO 49.6
tireworld MDP PPDDL 45 goal P 0.3 INC 0.1 212.8 TO
triangle-tireworld MDP PPDDL 441 goal P 0.7 INC 0.2 TO TO
wlan MDP PRISM 4-0 sent P TO 21.7 2.7 6.6 TO 1.7
wlan MDP PRISM 4-0 cost_min E 1.6 53.5 9.4 12.3 2.3
wlan MDP PRISM 5-0 sent P TO 92.5 15.7 19.2 TO 6.6
wlan MDP PRISM 5-0 cost_min E 1.9 370.6 65.1 54.8 9.5
wlan MDP PRISM 6-0 sent P TO 476.0 119.1 73.9 TO 26.4
wlan MDP PRISM 6-0 cost_min E 2.5 TO 482.5 285.7 43.1
zenotravel MDP PPDDL 4-2-2 goal P 9.3 INC 0.5 17.8 11.2
zeroconf MDP PRISM 1000-8-false correct_max P TO 54.3 6.8 130.7 8.8 13.3
zeroconf MDP PRISM 1000-8-false correct_min P INC 57.8 10.4 67.8 0.9 10.5