Model	Type	Original	Parameters	Property	Type	Modysh	ePMC	probFD	mcsta	PRISM	PET	Storm-static
beb	MDP	Modest	4-8-7	LineSeized	P	TO	INC		21.7			95.7
beb	MDP	Modest	5-16-15	LineSeized	P	TO	1.2		TO			TO
consensus	MDP	PRISM	4-4	disagree	P	TO	5.9		3.7	5.4	TO	1.4
consensus	MDP	PRISM	4-4	steps_min	E	TO	5.0		2.0	3.8		1.0
consensus	MDP	PRISM	6-2	disagree	P	TO	139.3		46.0	74.7	TO	19.7
consensus	MDP	PRISM	6-2	steps_min	E	TO	112.4		42.6	85.3		23.4
csma	MDP	PRISM	3-4	all_before_max	P	TO	84.0		2.6	29.8	35.7	8.3
csma	MDP	PRISM	3-4	time_max	E	TO	74.0		3.0	9.2		8.3
csma	MDP	PRISM	4-2	all_before_max	P	TO	152.2		1.3	26.7	22.1	4.9
csma	MDP	PRISM	4-2	time_max	E	TO	151.3		2.0	7.6		4.8
eajs	MDP	PRISM	5-250-11	ExpUtil	E	TO	ERR		8.0	10.7		29.2
eajs	MDP	PRISM	6-300-13	ExpUtil	E	TO	ERR		23.1	34.0		93.0
echoring	MDP	Modest	100	MaxOffline1	P	TO	INC		2.5			28.9
elevators	MDP	PPDDL	b-11-9	goal	P	4.8	INC	0.3	7.2			4.8
exploding-blocksworld	MDP	PPDDL	10	goal	P	TO	INC	23.5	TO			TO
firewire	MDP	PRISM	false-36-800	deadline	Pb	TO			10.5			19.2
pacman	MDP	PRISM	100	crash	P	TO	TO		148.6	TO	ERR	272.5
pacman	MDP	PRISM	60	crash	P	532.1	TO		70.7	TO	114.0	117.0
pnueli-zuck	MDP	PRISM	5	live	P	0.3	14.5	422.6	2.0	1.3	0.3	2.4
pnueli-zuck	MDP	PRISM	10	live	P	0.6	TO	TO	ERR	10.9	0.4	ERR
rabin	MDP	PRISM	10	live	P	0.3	TO	TO	TO	54.2	0.5	ERR
rectangle-tireworld	MDP	PPDDL	11	goal	P	4.7	INC	2.6	4.1			12.2
resource-gathering	MDP	PRISM	1300-100-100	expgold	Eb	TO				16.7		24.7
resource-gathering	MDP	PRISM	1300-100-100	expsteps	E	TO			96.0	25.3		17.7
resource-gathering	MDP	PRISM	1300-100-100	prgoldgem	Pb	TO				10.5	TO	49.6
tireworld	MDP	PPDDL	45	goal	P	0.3	INC	0.1	212.8			TO
triangle-tireworld	MDP	PPDDL	441	goal	P	0.7	INC	0.2	TO			TO
wlan	MDP	PRISM	4-0	sent	P	TO	21.7		2.7	6.6	TO	1.7
wlan	MDP	PRISM	4-0	cost_min	E	1.6	53.5		9.4	12.3		2.3
wlan	MDP	PRISM	5-0	sent	P	TO	92.5		15.7	19.2	TO	6.6
wlan	MDP	PRISM	5-0	cost_min	E	1.9	370.6		65.1	54.8		9.5
wlan	MDP	PRISM	6-0	sent	P	TO	476.0		119.1	73.9	TO	26.4
wlan	MDP	PRISM	6-0	cost_min	E	2.5	TO		482.5	285.7		43.1
zenotravel	MDP	PPDDL	4-2-2	goal	P	9.3	INC	0.5	17.8			11.2
zeroconf	MDP	PRISM	1000-8-false	correct_max	P	TO	54.3		6.8	130.7	8.8	13.3
zeroconf	MDP	PRISM	1000-8-false	correct_min	P	INC	57.8		10.4	67.8	0.9	10.5