QComp 2019 Benchmarks

↪ | DTMC | CTMC | MDP | MA | PTA

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

DTMC Benchmarks

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`			9-4-5	exp_draws	E
`4`			15-4-5	collect_all_bounded	Pb
`5`			15-4-5	exp_draws	E
`6`	crowds	PRISM	5-20	positive	P
`7`	crowds	PRISM	6-20	positive	P
`8`	egl	PRISM	10-2	messagesB	E
`9`			10-2	unfairA	P
`10`			10-8	messagesB	E
`11`			10-8	unfairA	P
`12`	haddad-monmege	PRISM	100-0.7	exp_steps	E
`13`	haddad-monmege	PRISM	100-0.7	target	P
`14`	herman	PRISM	15	steps	E
`15`	nand	PRISM	40-4	reliable	P
`16`	nand	PRISM	60-4	reliable	P
`17`	oscillators	PRISM	8-10-0.1-1-0.1-1.0	power_consumption	E
`18`	oscillators	PRISM	8-10-0.1-1-0.1-1.0	time_to_synch	E

CTMC Benchmarks

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`			128-2000-20	premium_steady	S
`22`	embedded	PRISM	8-12	actuators	P
`23`	embedded	PRISM	8-12	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`	mapk_cascade	PRISM	4-30	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

MDP Benchmarks

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`	beb	Modest	5-16-15	LineSeized	P
`39`	consensus	PRISM	4-4	disagree	P
`40`			4-4	steps_min	E
`41`			6-2	disagree	P
`42`			6-2	steps_min	E
`43`	csma	PRISM	3-4	all_before_max	P
`44`			3-4	time_max	E
`46`			4-2	all_before_max	P
`47`			4-2	time_max	E
`48`	eajs	PRISM	5-250-11	ExpUtil	E
`49`	eajs	PRISM	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`	pacman	PRISM	100	crash	P
`55`	pnueli-zuck	PRISM	5	live	P
`56`	pnueli-zuck	PRISM	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`			4-0	cost_min	E
`66`			5-0	sent	P
`67`			5-0	cost_min	E
`68`			6-0	sent	P
`69`			6-0	cost_min	E
`70`	zenotravel	PPDDL	4-2-2	goal	P
`71`	zeroconf	PRISM	1000-8-false	correct_max	P
`72`	zeroconf	PRISM	1000-8-false	correct_min	P

MA Benchmarks

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`	cabinets	Galileo	3-2-true	Unreliability	Pb
`76`	dpm	Modest	4-8-5	PmaxQueuesFullBound	Pb
`77`	dpm	Modest	6-6-5	PminQueue1Full	P
`78`	ftpp	Galileo	2-2-true	Unavailability	S
`79`	ftwc	Modest	8-5	TimeMax	E
`80`	ftwc	Modest	8-5	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`	readers-writers	GreatSPN	40	prtb_many_requests	Pb
`86`	sms	Galileo	3-true	Unreliability	Pb
`87`	sms	Galileo	3-true	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`	vgs	Galileo	5-10000	MinExpTimeFailed	E

PTA Benchmarks

8 probabilistic timed automaton benchmark instances:

	Model	Original	Parameters	Property	Type
`93`	firewire-pta	PRISM	30-5000	deadline	Pb
`94`	firewire-pta	PRISM	30-5000	eventually	P
`95`	repudiation_malicious	PRISM	20	deadline	Pb
`96`	repudiation_malicious	PRISM	20	eventually	P
`97`	wlan-large	Modest	2	E_or	E
`98`	wlan-large	Modest	2	P_max	P
`99`	zeroconf-pta	PRISM	200	deadline	Pb
`100`	zeroconf-pta	PRISM	200	incorrect	P