| Model | Type | Original | Parameters | Property | Type | Storm | Storm-static | mcsta | PET | modes | DFTRES | STAMINA | ModestFRETpiLRTDP |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| bluetooth | DTMC | PRISM | 1 | time | E | 0.000 | ERR / 0.000 | ||||||
| coupon | DTMC | PGCL | 9-4-5 | collect_all_bounded | Pb | 0.000 | 0.000 / 0.000 | 0.448 | 0.000 | ||||
| coupon | DTMC | PGCL | 9-4-5 | exp_draws | E | 0.000 | 0.000 / 0.000 | 0.000 | 0.000 | ||||
| coupon | DTMC | PGCL | 15-4-5 | collect_all_bounded | Pb | ERR | ERR / ERR | ERR / ERR | 0.008 | ||||
| coupon | DTMC | PGCL | 15-4-5 | exp_draws | E | ERR | ERR / ERR | ERR / ERR | 0.000 | ||||
| crowds | DTMC | PRISM | 5-20 | positive | P | 0.000 | 0.000 / 0.000 | 0.000 | ERR / ERR | 0.000 | 0.006 / 0.006 | ||
| crowds | DTMC | PRISM | 6-20 | positive | P | 0.000 | 0.000 / 0.000 | 0.000 | ERR / ERR | 0.000 | 0.001 / 0.005 | ||
| egl | DTMC | PRISM | 10-2 | messagesB | E | 0.000 | ERR / 0.000 | 0.000 / 0.000 | 0.000 | ||||
| egl | DTMC | PRISM | 10-2 | unfairA | P | 0.000 | ERR / 0.000 | 0.000 / 0.000 | ERR / ERR | 0.000 | |||
| egl | DTMC | PRISM | 10-8 | messagesB | E | 0.000 | ERR / 0.000 | ERR / ERR | 0.001 | ||||
| egl | DTMC | PRISM | 10-8 | unfairA | P | 0.000 | ERR / 0.000 | ERR / ERR | ERR | 0.000 | |||
| haddad-monmege | DTMC | PRISM | 100-0.7 | exp_steps | E | 0.000 | 1.000 / 0.000 | 1.000 | ERR | ||||
| haddad-monmege | DTMC | PRISM | 100-0.7 | target | P | 0.000 | 0.286 / 0.000 | 1.000 | ERR | ERR | 1.000 / 1.000 | ||
| herman | DTMC | PRISM | 15 | steps | E | 0.000 | 0.000 / 0.000 | ||||||
| nand | DTMC | PRISM | 40-4 | reliable | P | 0.000 | 0.000 / 0.000 | 0.000 | ERR / ERR | 0.000 | |||
| nand | DTMC | PRISM | 60-4 | reliable | P | 0.000 | 0.000 / 0.000 | 0.000 | ERR / ERR | 0.001 | |||
| oscillators | DTMC | PRISM | 8-10-0.1-1-0.1-1.0 | power_consumption | E | 0.000 | 0.000 | ||||||
| oscillators | DTMC | PRISM | 8-10-0.1-1-0.1-1.0 | time_to_synch | E | 0.000 | 0.000 | ||||||
| cluster | CTMC | PRISM | 128-2000-20 | premium_steady | S | 0.000 | 0.000 | 0.000 | |||||
| cluster | CTMC | PRISM | 128-2000-20 | qos1 | Pb | 0.000 | 0.000 / 0.000 | ERR | 0.003 | 0.112 | |||
| cluster | CTMC | PRISM | 64-2000-20 | below_min | Eb | 0.000 | 0.000 / 0.000 | 0.012 | |||||
| embedded | CTMC | PRISM | 8-12 | actuators | P | 3.748 | 3.748 / 0.000 | 0.000 | 0.000 | 0.009 | |||
| embedded | CTMC | PRISM | 8-12 | up_time | E | 0.000 | 0.000 / 0.000 | 0.000 | 0.005 | ||||
| fms | CTMC | PRISM | 8 | productivity | S | 0.000 | 0.000 | 0.000 | |||||
| kanban | CTMC | PRISM | 5 | throughput | S | 0.000 | 0.000 / 0.000 | 0.000 | |||||
| majority | CTMC | PRISM | 2100 | change_state | Pb | 0.000 | 0.000 | ERR | 0.003 | ERR | |||
| mapk_cascade | CTMC | PRISM | 4-30 | activated_time | E | 0.000 | 0.000 | 0.000 | 0.000 | ||||
| mapk_cascade | CTMC | PRISM | 4-30 | reactions | Eb | 0.000 | 0.000 / 0.000 | 0.000 | |||||
| philosophers | CTMC | GreatSPN | 16-1 | MaxPrReachDeadlockTB | Pb | 0.000 | 0.000 / 0.000 | ERR | 0.019 | ||||
| philosophers | CTMC | GreatSPN | 16-1 | MaxPrReachDeadlock | P | 0.000 | 0.000 / 0.000 | 0.000 | 0.000 | ||||
| philosophers | CTMC | GreatSPN | 16-1 | MinExpTimeDeadlock | E | 0.000 | 0.000 / 0.000 | 0.000 | 0.000 | ||||
| philosophers | CTMC | GreatSPN | 20-1 | MaxPrReachDeadlockTB | Pb | ERR | ERR | ERR / ERR | 0.128 | ||||
| philosophers | CTMC | GreatSPN | 20-1 | MaxPrReachDeadlock | P | 0.000 | ERR / 0.000 | ERR / ERR | 0.000 | ||||
| philosophers | CTMC | GreatSPN | 20-1 | MinExpTimeDeadlock | E | ERR | ERR | ERR / ERR | 0.000 | ||||
| polling | CTMC | PRISM | 18-16 | s1_before_s2 | P | 0.000 | 0.000 / 0.000 | 0.000 | ERR | 0.002 | |||
| speed-ind | CTMC | PRISM | 2100 | change_state | Pb | 0.000 | 0.000 | ERR | 0.002 | ERR | |||
| beb | MDP | Modest | 4-8-7 | LineSeized | P | 0.000 | 0.000 / 0.000 | 0.000 | 0.000 | 0.000 | |||
| beb | MDP | Modest | 5-16-15 | LineSeized | P | ERR | ERR | ERR / ERR | 0.000 | 0.000 | |||
| consensus | MDP | PRISM | 4-4 | disagree | P | 0.000 | 0.000 | 0.000 | ERR / ERR | 0.806 | 4.567 | ||
| consensus | MDP | PRISM | 4-4 | steps_min | E | 0.000 | 0.000 | 0.000 | 0.106 | 0.919 | |||
| consensus | MDP | PRISM | 6-2 | disagree | P | 0.000 | 0.000 / 0.000 | 0.000 | ERR / ERR | 0.899 | 1.749 | ||
| consensus | MDP | PRISM | 6-2 | steps_min | E | 0.000 | 0.000 / 0.000 | 0.000 | 0.205 | 0.959 | |||
| csma | MDP | PRISM | 3-4 | all_before_max | P | 0.000 | 0.000 / 0.000 | 0.000 | 0.000 | 0.009 | |||
| csma | MDP | PRISM | 3-4 | time_max | E | 0.000 | 0.000 / 0.000 | 0.000 | 0.026 | 0.861 | |||
| csma | MDP | PRISM | 4-2 | all_before_max | P | 0.000 | 0.000 / 0.000 | 0.000 | 0.000 | 0.119 | |||
| csma | MDP | PRISM | 4-2 | time_max | E | 0.000 | 0.000 / 0.000 | 0.000 | 0.045 | 0.906 | |||
| eajs | MDP | PRISM | 5-250-11 | ExpUtil | E | 0.000 | 0.000 / 0.000 | 0.000 | 0.663 | 0.601 | |||
| eajs | MDP | PRISM | 6-300-13 | ExpUtil | E | 0.000 | 0.000 / 0.000 | 0.000 | 0.746 | 0.668 | |||
| echoring | MDP | Modest | 100 | MaxOffline1 | P | 0.000 | 0.000 | 0.000 | ERR | 704841.165 | |||
| elevators | MDP | PPDDL | b-11-9 | goal | P | 0.000 | 0.000 | 0.000 / 0.000 | ERR | 0.000 | |||
| exploding-blocksworld | MDP | PPDDL | 10 | goal | P | ERR | ERR | ERR / ERR | ERR | ERR | |||
| firewire | MDP | PRISM | false-36-800 | deadline | Pb | 0.000 | 0.000 / 0.000 | 1.000 / 1.000 | 0.031 | ||||
| pacman | MDP | PRISM | 100 | crash | P | 0.000 | 1.000 / 0.000 | 0.000 | ERR / ERR | 0.814 | 0.000 | ||
| pacman | MDP | PRISM | 60 | crash | P | 0.000 | 0.000 / 0.000 | 0.000 | 0.000 / ERR | 0.800 | 0.000 | ||
| pnueli-zuck | MDP | PRISM | 5 | live | P | 0.000 | 0.000 / 0.000 | 0.000 | 0.000 / 0.000 | 0.000 | 0.000 | ||
| pnueli-zuck | MDP | PRISM | 10 | live | P | 0.000 | ERR / 0.000 | ERR / ERR | 0.000 | 0.000 | 0.000 | ||
| rabin | MDP | PRISM | 10 | live | P | 0.000 | ERR / 0.000 | ERR / ERR | 0.000 | 0.000 | 0.000 | ||
| rectangle-tireworld | MDP | PPDDL | 11 | goal | P | 0.000 | 0.000 / 0.000 | 0.000 / 0.000 | ERR | 0.000 | |||
| resource-gathering | MDP | PRISM | 1300-100-100 | expgold | Eb | 0.000 | 0.000 / 0.000 | 1.000 | |||||
| resource-gathering | MDP | PRISM | 1300-100-100 | expsteps | E | 0.000 | 0.000 | 0.000 | ERR | 0.945 | |||
| resource-gathering | MDP | PRISM | 1300-100-100 | prgoldgem | Pb | 0.000 | 0.000 / 0.000 | ERR | 1.000 | ||||
| tireworld | MDP | PPDDL | 45 | goal | P | ERR | ERR | 0.000 / 0.000 | 0.083 | 0.000 | |||
| triangle-tireworld | MDP | PPDDL | 441 | goal | P | ERR | ERR | ERR / ERR | 0.000 | 0.000 | |||
| wlan | MDP | PRISM | 4-0 | sent | P | 0.000 | 0.000 / 0.000 | 0.000 | ERR | 1.000 | 1.000 | ||
| wlan | MDP | PRISM | 4-0 | cost_min | E | 0.000 | 0.000 / 0.000 | 0.000 | 0.001 | 0.000 | |||
| wlan | MDP | PRISM | 5-0 | sent | P | 0.000 | 0.000 / 0.000 | 0.000 | ERR | 1.000 | 1.000 | ||
| wlan | MDP | PRISM | 5-0 | cost_min | E | 0.000 | 0.000 / 0.000 | 0.000 | 0.004 | 0.000 | |||
| wlan | MDP | PRISM | 6-0 | sent | P | 0.000 | 0.000 / 0.000 | 0.000 | ERR | 1.000 | 1.000 | ||
| wlan | MDP | PRISM | 6-0 | cost_min | E | 0.000 | 0.000 / 0.000 | ERR | 0.000 | 0.000 | |||
| zenotravel | MDP | PPDDL | 4-2-2 | goal | P | 0.000 | 0.000 / 0.000 | 0.000 / 0.000 | ERR | 0.000 | |||
| zeroconf | MDP | PRISM | 1000-8-false | correct_max | P | 0.000 | 0.000 | 0.000 | 0.000 / ERR | 0.398 | 0.000 | ||
| zeroconf | MDP | PRISM | 1000-8-false | correct_min | P | 0.000 | 0.000 | 0.000 | 0.000 / 1.000 | 4.844 | 0.696 | ||
| bitcoin-attack | MA | Modest | 20-6 | P_MWinMax | Pb | 0.000 | 0.000 / 0.000 | ERR | 0.261 | ||||
| cabinets | MA | Galileo | 3-2-true | Unavailability | S | 0.000 | 0.000 | ERR | 0.000 / 0.000 | ||||
| cabinets | MA | Galileo | 3-2-true | Unreliability | Pb | 0.000 | 0.000 / 0.000 | ERR | 0.994 | 0.000 / 0.000 | |||
| dpm | MA | Modest | 4-8-5 | PmaxQueuesFullBound | Pb | 0.000 | 0.000 | ERR | 1.000 | ||||
| dpm | MA | Modest | 6-6-5 | PminQueue1Full | P | 0.000 | 0.000 | 0.000 | ERR | ||||
| ftpp | MA | Galileo | 2-2-true | Unavailability | S | ERR | ERR | ERR | 0.000 / 0.000 | ||||
| ftwc | MA | Modest | 8-5 | TimeMax | E | 0.000 | 0.000 | 0.000 | ERR | ||||
| ftwc | MA | Modest | 8-5 | TimeMin | E | 0.000 | 0.000 | 0.000 | ERR | ||||
| hecs | MA | Galileo | false-1-1 | Unreliability | Pb | 0.000 | 0.000 | ERR | 0.012 | 0.000 / 0.000 | |||
| hecs | MA | Galileo | false-2-2 | Unreliability | Pb | 0.000 | 0.000 | ERR | 0.008 | 0.000 / 0.000 | |||
| hecs | MA | Galileo | false-3-2 | Unreliability | Pb | 0.000 | 0.000 | ERR | 1.000 | 0.002 / 0.000 | |||
| readers-writers | MA | GreatSPN | 40 | exp_time_many_requests | E | 0.000 | 0.000 | 0.000 | 0.012 | ||||
| readers-writers | MA | GreatSPN | 40 | prtb_many_requests | Pb | 0.000 | 0.000 / 0.000 | ERR | 0.001 | ||||
| sms | MA | Galileo | 3-true | Unreliability | Pb | 0.000 | 0.000 | ERR | 0.008 | 0.000 / 0.000 | |||
| sms | MA | Galileo | 3-true | Unavailability | S | 0.000 | 0.000 / 0.000 | 0.000 | 0.000 / 0.000 | ||||
| stream | MA | PRISM-MA | 1000 | exp_buffertime | E | 0.000 | 0.000 | 0.000 | 0.034 | ||||
| stream | MA | PRISM-MA | 1000 | pr_underrun | P | 0.000 | 0.000 | 0.000 | 1.771 | ||||
| stream | MA | PRISM-MA | 1000 | pr_underrun_tb | Pb | 0.000 | 0.000 | ERR | 0.006 | ||||
| vgs | MA | Galileo | 5-10000 | MaxPrReachFailedTB | Pb | 0.000 | 0.000 | ERR | ERR | ERR / ERR | |||
| vgs | MA | Galileo | 5-10000 | MinExpTimeFailed | E | 0.000 | 0.000 | ERR | ERR | ||||
| firewire-pta | PTA | PRISM | 30-5000 | deadline | Pb | ERR | ERR | ||||||
| firewire-pta | PTA | PRISM | 30-5000 | eventually | P | 0.000 | 0.000 | 0.000 / 0.000 | ERR | ||||
| repudiation_malicious | PTA | PRISM | 20 | deadline | Pb | ||||||||
| repudiation_malicious | PTA | PRISM | 20 | eventually | P | ||||||||
| wlan-large | PTA | Modest | 2 | E_or | E | 0.000 | 0.000 | 0.000 | ERR | ||||
| wlan-large | PTA | Modest | 2 | P_max | P | 0.000 | 0.000 | 0.000 | ERR | ||||
| zeroconf-pta | PTA | PRISM | 200 | deadline | Pb | 0.000 | ERR | ||||||
| zeroconf-pta | PTA | PRISM | 200 | incorrect | P | 0.000 | 0.000 / 0.000 | 0.000 | ERR |