Model Type Original Parameters Property Type Modysh ePMC probFD mcsta PRISM PET Storm-static
beb MDP Modest 3-4-3 LineSeized P 1.4 INC 0.3 0.0
blocksworld MDP PPDDL 5 goal P 0.5 INC 0.1 0.4 0.1
cdrive MDP PPDDL 6 goal P 1.2 INC 0.3 0.5 0.1
cdrive MDP PPDDL 10 goal P 10.3 INC 0.7 1.2 0.5
consensus MDP PRISM 2-2 steps_min E 1.6 0.3 1.3 0.0
consensus MDP PRISM 2-2 disagree P 0.9 0.3 1.3 0.7 0.0
consensus MDP PRISM 2-4 steps_min E 426.1 0.3 1.3 0.0
csma MDP PRISM 2-2 all_before_max P 0.3 INC 0.3 1.3 0.4 0.0
csma MDP PRISM 2-2 all_before_min P 0.6 INC 0.3 1.3 0.4 0.0
csma MDP PRISM 2-2 some_before P 0.3 INC 0.3 1.3 0.4 0.0
csma MDP PRISM 2-2 time_max E 14.8 INC 0.3 1.3 0.0
csma MDP PRISM 2-2 time_min E 10.2 INC 0.3 1.3 0.0
eajs MDP PRISM 2-100-5 ProbUtil Pb 1.0 INC 0.2
exploding-blocksworld MDP PPDDL 5 goal P 0.5 INC 0.1 0.6 0.5
firewire MDP PRISM false-3-200 time_max E 25.8 1.3 0.3 1.3 0.1
firewire MDP PRISM false-3-200 time_min E 2.9 1.4 0.4 1.3 0.1
firewire MDP PRISM false-3-200 deadline Pb 0.6 0.4 0.1
firewire MDP PRISM false-3-800 time_max E 25.7 1.2 0.3 1.3 0.1
firewire MDP PRISM false-3-800 time_min E 3.0 1.4 0.4 1.3 0.1
firewire MDP PRISM false-3-800 deadline Pb TO 0.6 0.3
firewire MDP PRISM false-36-200 time_max E TO 10.8 1.2 20.6 2.1
firewire MDP PRISM false-36-200 time_min E 3.7 9.2 2.8 15.4 2.1
firewire MDP PRISM false-36-200 deadline Pb 2.4 3.5 7.5
firewire_abst MDP PRISM 3 time_max E 1.1 INC 0.3 1.3 0.0
firewire_abst MDP PRISM 3 time_min E 0.8 INC 0.3 1.3 0.0
firewire_abst MDP PRISM 3 rounds E 0.3 INC 0.3 1.3 0.0
firewire_abst MDP PRISM 36 time_max E 3.0 INC 0.3 1.3 0.0
firewire_abst MDP PRISM 36 time_min E 0.7 INC 0.3 1.3 0.0
firewire_abst MDP PRISM 36 rounds E 0.3 INC 0.3 1.3 0.0
ij MDP PRISM 30 stable P 0.4 INC ERR ERR 1.3 ERR ERR
ij MDP PRISM 50 stable P 1.1 INC ERR TO 6.4 ERR ERR
philosophers-mdp MDP PRISM 30 eat P 0.5 INC TO ERR 87.3 2.1 ERR
triangle-tireworld MDP PPDDL 1681 goal P 10.5 INC 0.6 TO TO
csma MDP PRISM 2-4 time_max E 1675.6 INC 0.4 4.5 0.6
csma MDP PRISM 2-4 time_min E TO INC 0.4 1.3 0.1
csma MDP PRISM 2-4 some_before P 2.3 INC 0.3 1.3 1.4 0.1
csma MDP PRISM 2-4 all_before_max P 0.9 INC 0.4 1.3 0.8 0.1
csma MDP PRISM 2-4 all_before_min P 6.4 INC 0.3 1.3 0.1
csma MDP PRISM 3-2 time_max E TO INC 0.4 1.3 0.3
csma MDP PRISM 3-2 time_min E TO INC 0.5 1.3 0.3
csma MDP PRISM 3-2 some_before P 2.6 INC 0.4 1.3 1.8 0.2
csma MDP PRISM 3-2 all_before_max P 2.6 INC 0.4 2.5 1.3 0.3
csma MDP PRISM 3-2 all_before_min P 48.6 INC 0.4 1.3 0.2
wlan MDP PRISM 8-0 cost_min E 6.2 TO TO TO 968.9
wlan MDP PRISM 10-0 cost_min E 20.7 TO ERR TO TO
rabin MDP PRISM 15 live P 0.4 TO TO TO 216.0 0.9 ERR
rabin MDP PRISM 20 live P 0.4 TO TO ERR 919.1 1.5 ERR
rabin MDP PRISM 80 live P 1.6 TO TO TO ERR ERR ERR
rabin MDP PRISM 100 live P 2.2 TO TO ERR ERR ERR TO
pnueli-zuck MDP PRISM 20 live P 0.5 TO TO TO 245.3 0.9 TO
pnueli-zuck MDP PRISM 30 live P 0.8 TO TO TO TO 1.0 TO
pnueli-zuck MDP PRISM 60 live P 2.7 TO TO TO ERR 2.5 TO
pnueli-zuck MDP PRISM 100 live P 14.9 TO TO ERR TO ERR ERR
philosophers-mdp MDP PRISM 50 eat P 0.6 ERR TO ERR 488.2 9.5 ERR
philosophers-mdp MDP PRISM 80 eat P 0.9 ERR TO TO TO ERR ERR
philosophers-mdp MDP PRISM 100 eat P 1.1 ERR TO TO TO ERR ERR
ij MDP PRISM 60 stable P 1.9 INC TO ERR 16.4 ERR ERR
ij MDP PRISM 100 stable P 14.3 INC TO TO TO ERR TO