These are the benchmarks used for the performance evaluation of QComp 2019:

18 discrete-time Markov chain benchmark instances:

Model | Original | Parameters | Property | Type | |
---|---|---|---|---|---|

1 | bluetooth | PRISM | 1 | time | E |

2 | coupon | PGCL | 9-4-5 | collect_all_bounded | Pb |

3 | exp_draws | E | |||

4 | 15-4-5 | collect_all_bounded | Pb | ||

5 | exp_draws | E | |||

6 | crowds | PRISM | 5-20 | positive | P |

7 | 6-20 | positive | P | ||

8 | egl | PRISM | 10-2 | messagesB | E |

9 | unfairA | P | |||

10 | 10-8 | messagesB | E | ||

11 | unfairA | P | |||

12 | haddad-monmege | PRISM | 100-0.7 | exp_steps | E |

13 | target | P | |||

14 | herman | PRISM | 15 | steps | E |

15 | nand | PRISM | 40-4 | reliable | P |

16 | 60-4 | reliable | P | ||

17 | oscillators | PRISM | 8-10-0.1-1-0.1-1.0 | power_consumption | E |

18 | time_to_synch | E |

18 continuous-time Markov chain benchmark instances:

Model | Original | Parameters | Property | Type | |
---|---|---|---|---|---|

19 | cluster | PRISM | 64-2000-20 | below_min | Eb |

20 | 128-2000-20 | qos1 | Pb | ||

21 | premium_steady | S | |||

22 | embedded | PRISM | 8-12 | actuators | P |

23 | up_time | E | |||

24 | fms | PRISM | 8 | productivity | S |

25 | kanban | PRISM | 5 | throughput | S |

26 | majority | PRISM | 2100 | change_state | Pb |

27 | mapk_cascade | PRISM | 4-30 | activated_time | E |

28 | reactions | Eb | |||

29 | philosophers | GreatSPN | 16-1 | MaxPrReachDeadlockTB | Pb |

30 | MaxPrReachDeadlock | P | |||

31 | MinExpTimeDeadlock | E | |||

32 | 20-1 | MaxPrReachDeadlockTB | Pb | ||

33 | MaxPrReachDeadlock | P | |||

34 | MinExpTimeDeadlock | E | |||

35 | polling | PRISM | 18-16 | s1_before_s2 | P |

36 | speed-ind | PRISM | 2100 | change_state | Pb |

36 Markov decision process benchmark instances (where the csma instance with property `some_before` may still be replaced by a different model or instance):

Model | Original | Parameters | Property | Type | |
---|---|---|---|---|---|

37 | beb | Modest | 4-8-7 | LineSeized | P |

38 | 5-16-15 | LineSeized | P | ||

39 | consensus | PRISM | 4-4 | disagree | P |

40 | steps_min | E | |||

41 | 6-2 | disagree | P | ||

42 | steps_min | E | |||

43 | csma | PRISM | 3-4 | all_before_max | P |

44 | time_max | E | |||

46 | 4-2 | all_before_max | P | ||

47 | time_max | E | |||

48 | eajs | PRISM | 5-250-11 | ExpUtil | E |

49 | 6-300-13 | ExpUtil | E | ||

50 | echoring | Modest | 100 | MaxOffline1 | P |

51 | elevators | PPDDL | b-11-9 | goal | P |

51 | exploding-blocksworld | PPDDL | 10 | goal | P |

52 | firewire | PRISM | false-36-800 | deadline | Pb |

53 | pacman | PRISM | 60 | crash | P |

54 | 100 | crash | P | ||

55 | pnueli-zuck | PRISM | 5 | live | P |

56 | 10 | live | P | ||

57 | rabin | PRISM | 10 | live | P |

58 | rectangle-tireworld | PPDDL | 11 | goal | P |

59 | resource-gathering | PRISM | 1300-100-100 | expgold | Eb |

60 | expsteps | E | |||

61 | prgoldgem | Pb | |||

62 | tireworld | PPDDL | 45 | goal | P |

63 | triangle-tireworld | PPDDL | 441 | goal | P |

64 | wlan | PRISM | 4-0 | sent | P |

65 | cost_min | E | |||

66 | 5-0 | sent | P | ||

67 | cost_min | E | |||

68 | 6-0 | sent | P | ||

69 | cost_min | E | |||

70 | zenotravel | PPDDL | 4-2-2 | goal | P |

71 | zeroconf | PRISM | 1000-8-false | correct_max | P |

72 | correct_min | P |

20 Markov automaton benchmark instances:

Model | Original | Parameters | Property | Type | |
---|---|---|---|---|---|

73 | bitcoin-attack | Modest | 20-6 | P_MWinMax | Pb |

74 | cabinets | Galileo | 3-2-true | Unavailability | S |

75 | Unreliability | Pb | |||

76 | dpm | Modest | 4-8-5 | PmaxQueuesFullBound | Pb |

77 | 6-6-5 | PminQueue1Full | P | ||

78 | ftpp | Galileo | 2-2-true | Unavailability | S |

79 | ftwc | Modest | 8-5 | TimeMax | E |

80 | TimeMin | E | |||

81 | hecs | Galileo | false-1-1 | Unreliability | Pb |

82 | false-2-2 | Unreliability | Pb | ||

83 | false-3-2 | Unreliability | Pb | ||

84 | readers-writers | GreatSPN | 40 | exp_time_many_requests | E |

85 | prtb_many_requests | Pb | |||

86 | sms | Galileo | 3-true | Unreliability | Pb |

87 | Unavailability | S | |||

88 | stream | PRISM-MA | 1000 | exp_buffertime | E |

89 | pr_underrun | P | |||

90 | pr_underrun_tb | Pb | |||

91 | vgs | Galileo | 5-10000 | PrReachFailedTB | Pb |

92 | MinExpTimeFailed | E |

8 probabilistic timed automaton benchmark instances:

Model | Original | Parameters | Property | Type | |
---|---|---|---|---|---|

93 | firewire-pta | PRISM | 30-5000 | deadline | Pb |

94 | eventually | P | |||

95 | repudiation_malicious | PRISM | 20 | deadline | Pb |

96 | eventually | P | |||

97 | wlan-large | Modest | 2 | E_or | E |

98 | P_max | P | |||

99 | zeroconf-pta | PRISM | 200 | deadline | Pb |

100 | incorrect | P |