Model | Type | Original | Parameters | Property | Type | Storm.sparse | Storm.hybrid | Storm.dd | Storm.ddbisim | Storm.sound | Storm.exact |
---|---|---|---|---|---|---|---|---|---|---|---|
beb | MDP | Modest | 4-8-7 | LineSeized | P | 127.7 | 16.7 | 28.5 | 22.6 | 130.3 | 334.6 |
beb | MDP | Modest | 5-16-15 | LineSeized | P | MO | TO | TO | MO | MO | MO |
bitcoin-attack | MA | Modest | 20-6 | P_MWinMax | Pb | 2.2 | NS | NS | 1.1 | 2.0 | NS |
bluetooth | DTMC | PRISM | 1 | time | E | TO | MO | 7.1 | 8.6 | TO | TO |
cabinets | MA | Galileo | 3-2-true | Unavailability | S | 82.0 | NS | NS | NS | 95.7 | MO |
cabinets | MA | Galileo | 3-2-true | Unreliability | Pb | 45.8 | NS | NS | NS | 37.3 | NS |
cluster | CTMC | PRISM | 128-2000-20 | premium_steady | S | 29.5 | 6.9 | NS | 55.8 | 109.9 | MO |
cluster | CTMC | PRISM | 128-2000-20 | qos1 | Pb | 65.8 | 84.5 | NS | 114.8 | 80.3 | NS |
cluster | CTMC | PRISM | 64-2000-20 | below_min | Eb | 137.9 | 116.7 | NS | 154.4 | 123.7 | NS |
consensus | MDP | PRISM | 4-4 | disagree | P | 1.1 | 2.4 | 71.6 | 1.8 | 1.8 | 8.8 |
consensus | MDP | PRISM | 4-4 | steps_min | E | 2.2 | 4.4 | 31.8 | 1.9 | 2.0 | 4.3 |
consensus | MDP | PRISM | 6-2 | disagree | P | 27.6 | 28.1 | 158.4 | 3.9 | 42.7 | TO |
consensus | MDP | PRISM | 6-2 | steps_min | E | 29.8 | 55.0 | 59.4 | 8.7 | 58.5 | TO |
coupon | DTMC | PGCL | 15-4-5 | collect_all_bounded | Pb | MO | NS | NS | 913.9 | MO | MO |
coupon | DTMC | PGCL | 15-4-5 | exp_draws | E | MO | MO | TO | 804.9 | MO | MO |
coupon | DTMC | PGCL | 9-4-5 | collect_all_bounded | Pb | MO | NS | NS | 3.4 | MO | MO |
coupon | DTMC | PGCL | 9-4-5 | exp_draws | E | 139.1 | 95.6 | 92.0 | 3.6 | 184.2 | MO |
crowds | DTMC | PRISM | 5-20 | positive | P | 13.2 | 5.8 | 4.1 | 1.9 | 12.6 | 44.1 |
crowds | DTMC | PRISM | 6-20 | positive | P | 120.9 | 67.4 | 5.5 | 2.2 | 97.0 | 295.0 |
csma | MDP | PRISM | 3-4 | all_before_max | P | 13.2 | 3.3 | 8.3 | 10.6 | 11.6 | 24.4 |
csma | MDP | PRISM | 3-4 | time_max | E | 17.7 | 6.0 | 138.9 | 9.0 | 18.3 | 52.7 |
csma | MDP | PRISM | 4-2 | all_before_max | P | 7.9 | 3.8 | 16.9 | 5.5 | 8.1 | 15.7 |
csma | MDP | PRISM | 4-2 | time_max | E | 7.6 | 4.7 | 102.2 | 6.5 | 12.2 | 19.4 |
dpm | MA | Modest | 4-8-5 | PmaxQueuesFullBound | Pb | 38.7 | NS | NS | 58.1 | 42.8 | NS |
dpm | MA | Modest | 6-6-5 | PminQueue1Full | P | 81.7 | NS | NS | MO | 86.7 | MO |
eajs | MDP | PRISM | 5-250-11 | ExpUtil | E | 38.6 | 17.7 | 66.7 | 12.7 | 58.2 | 97.7 |
eajs | MDP | PRISM | 6-300-13 | ExpUtil | E | 132.1 | 110.6 | 196.9 | 30.1 | 200.7 | 297.1 |
echoring | MDP | Modest | 100 | MaxOffline1 | P | 59.2 | NS | NS | NS | 70.6 | 141.9 |
egl | DTMC | PRISM | 10-2 | messagesB | E | MO | 485.7 | 2.4 | 1.5 | MO | MO |
egl | DTMC | PRISM | 10-2 | unfairA | P | 720.2 | 0.8 | 0.8 | 2.7 | 710.7 | MO |
egl | DTMC | PRISM | 10-8 | messagesB | E | MO | MO | 15.4 | 9.7 | MO | MO |
egl | DTMC | PRISM | 10-8 | unfairA | P | MO | 1.3 | 2.1 | 15.1 | MO | MO |
elevators | MDP | PPDDL | b-11-9 | goal | P | 6.9 | MO | MO | MO | 7.8 | 23.3 |
embedded | CTMC | PRISM | 8-12 | actuators | P | 0.1 | 0.5 | NS | 0.8 | 1.4 | 0.5 |
embedded | CTMC | PRISM | 8-12 | up_time | E | 3.1 | 12.4 | NS | 12.4 | 3.9 | 0.6 |
exploding-blocksworld | MDP | PPDDL | 10 | goal | P | MO | MO | MO | MO | MO | MO |
firewire-pta | PTA | PRISM | 30-5000 | eventually | P | 385.7 | NS | NS | NS | 371.0 | 546.7 |
firewire | MDP | PRISM | false-36-800 | deadline | Pb | 33.3 | NS | NS | 18.1 | 33.5 | 352.7 |
fms | CTMC | PRISM | 8 | productivity | S | 85.7 | 87.0 | NS | TO | TO | MO |
ftpp | MA | Galileo | 2-2-true | Unavailability | S | TO | NS | NS | NS | TO | MO |
ftwc | MA | Modest | 8-5 | TimeMax | E | INC | NS | NS | NS | 66.4 | 1526.5 |
ftwc | MA | Modest | 8-5 | TimeMin | E | INC | NS | NS | NS | 40.7 | TO |
haddad-monmege | DTMC | PRISM | 100-0.7 | exp_steps | E | INC | INC | INC | INC | TO | 0.1 |
haddad-monmege | DTMC | PRISM | 100-0.7 | target | P | INC | INC | INC | INC | TO | 0.1 |
hecs | MA | Galileo | false-1-1 | Unreliability | Pb | 0.2 | NS | NS | NS | 0.2 | NS |
hecs | MA | Galileo | false-2-2 | Unreliability | Pb | 86.4 | NS | NS | NS | 114.9 | NS |
hecs | MA | Galileo | false-3-2 | Unreliability | Pb | MO | NS | NS | NS | MO | MO |
herman | DTMC | PRISM | 15 | steps | E | 24.6 | 3.0 | 73.3 | 2.0 | 26.0 | TO |
kanban | CTMC | PRISM | 5 | throughput | S | 48.3 | 32.6 | NS | TO | 198.4 | MO |
majority | CTMC | PRISM | 2100 | change_state | Pb | 21.3 | 49.8 | NS | 52.0 | 25.5 | NS |
mapk_cascade | CTMC | PRISM | 4-30 | activated_time | E | 2.7 | 13.5 | NS | 18.5 | 4.6 | TO |
mapk_cascade | CTMC | PRISM | 4-30 | reactions | Eb | 134.8 | 105.8 | NS | 110.6 | 104.4 | NS |
nand | DTMC | PRISM | 40-4 | reliable | P | 13.2 | 4.9 | 42.3 | 657.7 | 13.3 | 65.6 |
nand | DTMC | PRISM | 60-4 | reliable | P | 62.7 | 21.1 | TO | MO | 59.6 | MO |
oscillators | DTMC | PRISM | 8-10-0.1-1-0.1-1.0 | power_consumption | E | 297.9 | MO | MO | MO | 400.2 | 475.7 |
oscillators | DTMC | PRISM | 8-10-0.1-1-0.1-1.0 | time_to_synch | E | 302.3 | MO | MO | MO | 400.8 | 481.2 |
pacman | MDP | PRISM | 100 | crash | P | 324.4 | 47.3 | 240.4 | MO | 377.1 | 518.7 |
pacman | MDP | PRISM | 60 | crash | P | 157.9 | 20.8 | 29.7 | MO | 163.4 | 200.9 |
philosophers | CTMC | GreatSPN | 16-1 | MaxPrReachDeadlock | P | 32.0 | 0.7 | NS | 143.0 | 32.3 | 115.2 |
philosophers | CTMC | GreatSPN | 16-1 | MaxPrReachDeadlockTB | Pb | 54.0 | 27.0 | NS | 143.5 | 45.9 | NS |
philosophers | CTMC | GreatSPN | 16-1 | MinExpTimeDeadlock | E | 40.1 | 17.6 | NS | 144.9 | 41.0 | TO |
philosophers | CTMC | GreatSPN | 20-1 | MaxPrReachDeadlock | P | MO | 1.0 | NS | MO | MO | MO |
philosophers | CTMC | GreatSPN | 20-1 | MaxPrReachDeadlockTB | Pb | MO | MO | NS | MO | MO | MO |
philosophers | CTMC | GreatSPN | 20-1 | MinExpTimeDeadlock | E | MO | MO | NS | MO | MO | MO |
pnueli-zuck | MDP | PRISM | 10 | live | P | MO | 1.3 | 1.2 | MO | MO | MO |
pnueli-zuck | MDP | PRISM | 5 | live | P | 4.9 | 0.7 | 0.7 | 2.5 | 5.9 | 10.5 |
polling | CTMC | PRISM | 18-16 | s1_before_s2 | P | 118.6 | 11.2 | NS | MO | 134.3 | MO |
rabin | MDP | PRISM | 10 | live | P | MO | 1.0 | 1.0 | 4.9 | MO | MO |
readers-writers | MA | GreatSPN | 40 | exp_time_many_requests | E | 19.4 | NS | NS | MO | 20.4 | MO |
readers-writers | MA | GreatSPN | 40 | prtb_many_requests | Pb | TO | NS | NS | MO | TO | NS |
rectangle-tireworld | MDP | PPDDL | 11 | goal | P | 13.0 | 19.7 | 19.8 | 20.2 | 12.7 | 13.1 |
resource-gathering | MDP | PRISM | 1300-100-100 | expgold | Eb | 34.3 | 27.5 | 1.1 | 1.3 | 36.5 | TO |
resource-gathering | MDP | PRISM | 1300-100-100 | expsteps | E | 21.7 | 23.1 | 109.2 | 307.3 | 34.7 | 99.3 |
resource-gathering | MDP | PRISM | 1300-100-100 | prgoldgem | Pb | 66.3 | 28.2 | 19.0 | 322.7 | 62.2 | TO |
sms | MA | Galileo | 3-true | Unavailability | S | 18.6 | NS | NS | NS | 16.3 | 51.1 |
sms | MA | Galileo | 3-true | Unreliability | Pb | 0.1 | NS | NS | NS | 0.1 | NS |
speed-ind | CTMC | PRISM | 2100 | change_state | Pb | 103.2 | 116.8 | NS | 187.0 | 90.3 | NS |
stream | MA | PRISM-MA | 1000 | exp_buffertime | E | 7.5 | NS | NS | 230.4 | 7.6 | 26.7 |
stream | MA | PRISM-MA | 1000 | pr_underrun | P | 25.3 | NS | NS | 427.6 | 29.5 | 48.4 |
stream | MA | PRISM-MA | 1000 | pr_underrun_tb | Pb | 7.5 | NS | NS | 351.4 | 6.6 | NS |
tireworld | MDP | PPDDL | 45 | goal | P | TO | TO | 1321.5 | TO | TO | MO |
triangle-tireworld | MDP | PPDDL | 441 | goal | P | MO | MO | MO | MO | MO | MO |
vgs | MA | Galileo | 5-10000 | MaxPrReachFailedTB | Pb | TO | MO | TO | TO | TO | TO |
vgs | MA | Galileo | 5-10000 | MinExpTimeFailed | E | TO | TO | MO | TO | TO | TO |
wlan-large | PTA | Modest | 2 | E_or | E | 37.8 | NS | NS | NS | 1582.6 | 114.8 |
wlan-large | PTA | Modest | 2 | P_max | P | 6.2 | NS | NS | NS | 7.1 | 19.4 |
wlan | MDP | PRISM | 4-0 | cost_min | E | 3.6 | 12.1 | 29.8 | 128.6 | 3.7 | 7.8 |
wlan | MDP | PRISM | 4-0 | sent | P | 3.0 | 1.1 | 1.1 | 125.1 | 2.8 | 5.4 |
wlan | MDP | PRISM | 5-0 | cost_min | E | 13.1 | 16.5 | 89.1 | 794.7 | 14.4 | 28.9 |
wlan | MDP | PRISM | 5-0 | sent | P | 11.2 | 1.8 | 1.8 | 859.9 | 12.6 | 21.8 |
wlan | MDP | PRISM | 6-0 | cost_min | E | 58.7 | 37.8 | 325.9 | TO | 59.3 | 122.8 |
wlan | MDP | PRISM | 6-0 | sent | P | 49.7 | 3.3 | 3.3 | TO | 47.3 | 94.1 |
zenotravel | MDP | PPDDL | 4-2-2 | goal | P | 14.5 | 4.3 | 4.6 | 19.9 | 15.6 | 24.8 |
zeroconf-pta | PTA | PRISM | 200 | incorrect | P | 0.1 | NS | NS | NS | 0.1 | 0.1 |
zeroconf | MDP | PRISM | 1000-8-false | correct_max | P | 17.9 | 17.4 | 268.8 | 103.3 | 22.0 | TO |
zeroconf | MDP | PRISM | 1000-8-false | correct_min | P | 16.9 | 16.7 | 666.8 | 99.7 | 21.3 | 49.9 |