| Model | Type | Original | Parameters | Property | Type | Storm | Storm-static | mcsta |
|---|---|---|---|---|---|---|---|---|
| bluetooth | DTMC | PRISM | 1 | time | E | 10.4 | TO / 10.4 | |
| coupon | DTMC | PGCL | 9-4-5 | collect_all_bounded | Pb | 4.7 | 273.2 / 5.3 | INC |
| coupon | DTMC | PGCL | 9-4-5 | exp_draws | E | 4.5 | 534.0 / 4.4 | 31.7 |
| coupon | DTMC | PGCL | 15-4-5 | collect_all_bounded | Pb | TO | TO / 1726.0 | TO / TO |
| coupon | DTMC | PGCL | 15-4-5 | exp_draws | E | 1389.0 | TO / 1409.3 | TO / TO |
| crowds | DTMC | PRISM | 5-20 | positive | P | 2.8 | 15.8 / 2.6 | 8.7 |
| crowds | DTMC | PRISM | 6-20 | positive | P | 3.0 | 117.7 / 3.0 | 44.1 |
| egl | DTMC | PRISM | 10-2 | messagesB | E | 3.7 | 911.4 / 3.7 | 291.3 / 289.2 |
| egl | DTMC | PRISM | 10-2 | unfairA | P | 3.8 | 822.0 / 1.7 | 184.0 / 198.0 |
| egl | DTMC | PRISM | 10-8 | messagesB | E | 16.5 | TO / 15.8 | TO / TO |
| egl | DTMC | PRISM | 10-8 | unfairA | P | 26.0 | TO / 2.7 | TO / 1409.3 |
| haddad-monmege | DTMC | PRISM | 100-0.7 | exp_steps | E | 0.1 | INC / INC | TO |
| haddad-monmege | DTMC | PRISM | 100-0.7 | target | P | 0.1 | INC / INC | TO |
| herman | DTMC | PRISM | 15 | steps | E | 181.1 | 158.0 / 3.2 | |
| nand | DTMC | PRISM | 40-4 | reliable | P | 8.5 | INC / 7.4 | 6.9 |
| nand | DTMC | PRISM | 60-4 | reliable | P | 34.5 | INC / 32.6 | 31.1 |
| oscillators | DTMC | PRISM | 8-10-0.1-1-0.1-1.0 | power_consumption | E | 210.2 | 193.0 | |
| oscillators | DTMC | PRISM | 8-10-0.1-1-0.1-1.0 | time_to_synch | E | INC | INC | |
| cluster | CTMC | PRISM | 128-2000-20 | premium_steady | S | TO | TO | |
| cluster | CTMC | PRISM | 128-2000-20 | qos1 | Pb | |||
| cluster | CTMC | PRISM | 64-2000-20 | below_min | Eb | |||
| embedded | CTMC | PRISM | 8-12 | actuators | P | INC | INC / INC | INC |
| embedded | CTMC | PRISM | 8-12 | up_time | E | INC | INC / INC | INC |
| fms | CTMC | PRISM | 8 | productivity | S | TO | TO | |
| kanban | CTMC | PRISM | 5 | throughput | S | TO | TO / TO | |
| majority | CTMC | PRISM | 2100 | change_state | Pb | |||
| mapk_cascade | CTMC | PRISM | 4-30 | activated_time | E | TO | TO | 22.3 |
| mapk_cascade | CTMC | PRISM | 4-30 | reactions | Eb | |||
| philosophers | CTMC | GreatSPN | 16-1 | MaxPrReachDeadlockTB | Pb | |||
| philosophers | CTMC | GreatSPN | 16-1 | MaxPrReachDeadlock | P | 1.5 | 38.8 / 1.4 | 14.4 |
| philosophers | CTMC | GreatSPN | 16-1 | MinExpTimeDeadlock | E | TO | TO / TO | INC |
| philosophers | CTMC | GreatSPN | 20-1 | MaxPrReachDeadlockTB | Pb | |||
| philosophers | CTMC | GreatSPN | 20-1 | MaxPrReachDeadlock | P | 2.0 | TO / 2.4 | TO / 1347.9 |
| philosophers | CTMC | GreatSPN | 20-1 | MinExpTimeDeadlock | E | TO | TO | TO / TO |
| polling | CTMC | PRISM | 18-16 | s1_before_s2 | P | TO | TO / TO | 530.0 |
| speed-ind | CTMC | PRISM | 2100 | change_state | Pb | |||
| beb | MDP | Modest | 4-8-7 | LineSeized | P | 32.4 | 162.3 / 30.8 | 290.8 |
| beb | MDP | Modest | 5-16-15 | LineSeized | P | TO | TO | TO / TO |
| consensus | MDP | PRISM | 4-4 | disagree | P | TO | TO | INC |
| consensus | MDP | PRISM | 4-4 | steps_min | E | TO | TO | INC |
| consensus | MDP | PRISM | 6-2 | disagree | P | TO | TO / TO | 342.6 |
| consensus | MDP | PRISM | 6-2 | steps_min | E | 3.6 | TO / 3.6 | 212.1 |
| csma | MDP | PRISM | 3-4 | all_before_max | P | 6.2 | 16.9 / 6.1 | 44.9 |
| csma | MDP | PRISM | 3-4 | time_max | E | TO | TO / TO | 6.8 |
| csma | MDP | PRISM | 4-2 | all_before_max | P | 6.9 | 10.4 / 6.4 | 28.9 |
| csma | MDP | PRISM | 4-2 | time_max | E | TO | TO / TO | 4.9 |
| eajs | MDP | PRISM | 5-250-11 | ExpUtil | E | 19.4 | 57.6 / 18.5 | 17.6 |
| eajs | MDP | PRISM | 6-300-13 | ExpUtil | E | 45.2 | 187.5 / 48.6 | 52.1 |
| echoring | MDP | Modest | 100 | MaxOffline1 | P | 59.9 | 59.9 | 19.5 |
| elevators | MDP | PPDDL | b-11-9 | goal | P | 8.9 | 9.0 | 8.6 |
| exploding-blocksworld | MDP | PPDDL | 10 | goal | P | TO | TO | TO / TO |
| firewire | MDP | PRISM | false-36-800 | deadline | Pb | 27.4 | 33.8 / 27.8 | INC / INC |
| pacman | MDP | PRISM | 100 | crash | P | 72.0 | 626.7 / 71.4 | 295.1 |
| pacman | MDP | PRISM | 60 | crash | P | 31.7 | 274.7 / 31.0 | 132.9 |
| pnueli-zuck | MDP | PRISM | 5 | live | P | 1.0 | 4.3 / 0.9 | 3.2 |
| pnueli-zuck | MDP | PRISM | 10 | live | P | 2.3 | TO / 2.6 | TO / TO |
| rabin | MDP | PRISM | 10 | live | P | 1.9 | TO / 2.1 | TO / TO |
| rectangle-tireworld | MDP | PPDDL | 11 | goal | P | 22.9 | 22.9 / 22.9 | 7.6 |
| resource-gathering | MDP | PRISM | 1300-100-100 | expgold | Eb | 47.5 | 65.2 / 1.5 | |
| resource-gathering | MDP | PRISM | 1300-100-100 | expsteps | E | TO | TO | 159.0 |
| resource-gathering | MDP | PRISM | 1300-100-100 | prgoldgem | Pb | 50.8 | 91.4 / 46.5 | |
| tireworld | MDP | PPDDL | 45 | goal | P | TO | TO | 551.6 / 595.4 |
| triangle-tireworld | MDP | PPDDL | 441 | goal | P | TO | TO | TO / TO |
| wlan | MDP | PRISM | 4-0 | sent | P | 2.2 | 3.4 / 2.2 | 4.5 |
| wlan | MDP | PRISM | 4-0 | cost_min | E | 6.0 | 4.1 / 4.5 | 14.7 |
| wlan | MDP | PRISM | 5-0 | sent | P | 3.4 | 12.9 / 3.3 | 25.0 |
| wlan | MDP | PRISM | 5-0 | cost_min | E | 12.6 | 15.6 / 12.0 | 104.5 |
| wlan | MDP | PRISM | 6-0 | sent | P | 5.8 | 50.9 / 5.7 | 173.5 |
| wlan | MDP | PRISM | 6-0 | cost_min | E | 40.7 | 61.9 / 38.4 | 788.0 |
| zenotravel | MDP | PPDDL | 4-2-2 | goal | P | 7.0 | 24.5 / 6.3 | 11.4 |
| zeroconf | MDP | PRISM | 1000-8-false | correct_max | P | TO | TO | 212.9 |
| zeroconf | MDP | PRISM | 1000-8-false | correct_min | P | 31.6 | 31.0 | 18.1 |
| bitcoin-attack | MA | Modest | 20-6 | P_MWinMax | Pb | |||
| cabinets | MA | Galileo | 3-2-true | Unavailability | S | ERR | ERR | |
| cabinets | MA | Galileo | 3-2-true | Unreliability | Pb | |||
| dpm | MA | Modest | 4-8-5 | PmaxQueuesFullBound | Pb | |||
| dpm | MA | Modest | 6-6-5 | PminQueue1Full | P | TO | TO | 28.1 |
| ftpp | MA | Galileo | 2-2-true | Unavailability | S | TO | TO | |
| ftwc | MA | Modest | 8-5 | TimeMax | E | TO | TO | INC |
| ftwc | MA | Modest | 8-5 | TimeMin | E | TO | TO | INC |
| hecs | MA | Galileo | false-1-1 | Unreliability | Pb | |||
| hecs | MA | Galileo | false-2-2 | Unreliability | Pb | |||
| hecs | MA | Galileo | false-3-2 | Unreliability | Pb | |||
| readers-writers | MA | GreatSPN | 40 | exp_time_many_requests | E | TO | TO | 45.8 |
| readers-writers | MA | GreatSPN | 40 | prtb_many_requests | Pb | |||
| sms | MA | Galileo | 3-true | Unreliability | Pb | |||
| sms | MA | Galileo | 3-true | Unavailability | S | 13.4 | 14.7 / 12.5 | |
| stream | MA | PRISM-MA | 1000 | exp_buffertime | E | 9.7 | 9.7 | 170.6 |
| stream | MA | PRISM-MA | 1000 | pr_underrun | P | 2.7 | 2.7 | 1.5 |
| stream | MA | PRISM-MA | 1000 | pr_underrun_tb | Pb | |||
| vgs | MA | Galileo | 5-10000 | MaxPrReachFailedTB | Pb | |||
| vgs | MA | Galileo | 5-10000 | MinExpTimeFailed | E | 0.2 | 0.2 | TO |
| firewire-pta | PTA | PRISM | 30-5000 | deadline | Pb | 466.2 | ||
| firewire-pta | PTA | PRISM | 30-5000 | eventually | P | 57.1 | 56.5 | 18.2 |
| repudiation_malicious | PTA | PRISM | 20 | deadline | Pb | |||
| repudiation_malicious | PTA | PRISM | 20 | eventually | P | |||
| wlan-large | PTA | Modest | 2 | E_or | E | 45.6 | 45.8 | 20.6 |
| wlan-large | PTA | Modest | 2 | P_max | P | 9.3 | 9.3 | 59.8 |
| zeroconf-pta | PTA | PRISM | 200 | deadline | Pb | 0.6 | ||
| zeroconf-pta | PTA | PRISM | 200 | incorrect | P | 0.4 | 0.4 / 0.4 | 0.6 |