The IMITATOR benchmarks library (v2.0 alpha)

• Home
• Download
• Benchmarks
• Publications
• FAQ
• Contact
• Links

The IMITATOR benchmarks library (v2.0 alpha)

This page presents the official IMITATOR benchmarks library. These models have been accumulated over the years from scientific publications, and from industrial collaborations.

As of today, the library contains 34 benchmarks with 78 different models and 118 properties.

The library is under constant construction.

New metrics will soon appear too (number of parametric clocks, size of the state space using the symbolic zone graph…)

For robustness analysis, the reference valuation can be obtained in the IM column.

Benchmark	Source	Categories										Metrics									Property							Execution
		Academic	Automotive	Educ.	Hardw.	Industrial	ProdCons	Protocol	RTS	Sched	Toy	|PTA|	|X|	|P|	|D|	|L|	|Act|	L/U?	Inv?	SW?	Reach.	Safety	AF	Pattern	Opt.	Cycle	IM	time
And-Or	[CC05]	yes	no	no	yes	no	no	no	no	no	no	4	4	12	0	27	8	yes	no	no	no	no	yes	no	yes	no	3.01 s
Bounded retransmission protocol	[DKRT97]	yes	no	no	no	yes	no	yes	yes	no	no	6	7	2	12	22	12	Not L/U	yes	no	no	yes	no	no	no	no	no	248.35 s
Not-Not-And circuit	[ACR16]	yes	no	no	yes	no	no	no	no	no	no	5	5	6	0	8	20	L/U-PTA	yes	no	no	yes	no	no	no	no	no	?
Not-Not-And circuit	[ACR16]	yes	no	no	yes	no	no	no	no	no	no	5	5	6	0	8	20	L/U-PTA	yes	no	no	no	no	no	no	no	yes	?
3NotAnd	[ACR16]	yes	no	no	yes	no	no	no	no	no	no	5	5	10	0	22	9	L/U-PTA	yes	no	no	yes	no	no	no	no	no	?
3NotAnd	[ACR16]	yes	no	no	yes	no	no	no	no	no	no	5	5	10	0	22	9	L/U-PTA	yes	no	no	no	no	no	no	no	yes	?
3NotAnd	[ACR16]	yes	no	no	yes	no	no	no	no	no	no	5	5	10	0	22	9	L/U-PTA	yes	no	no	no	no	no	no	no	yes	H.S.
coffee machine		no	no	yes	no	no	no	no	no	no	yes	1	2	3	0	4	4	Not L/U	yes	no	yes	no	no	no	no	no	no	?
coffee machine		no	no	yes	no	no	no	no	no	no	yes	1	2	3	0	4	4	Not L/U	yes	no	no	no	yes	no	no	no	no	?
coffee machine		no	no	yes	no	no	no	no	no	no	yes	1	2	3	0	4	4	Not L/U	yes	no	no	no	no	no	no	no	yes	?
Coffee machine + drinker		no	no	yes	no	no	no	no	no	no	yes	2	4	6	1	8	4	Not L/U	yes	no	no	yes	no	no	no	no	no	?
Coffee machine + drinker		no	no	yes	no	no	no	no	no	no	yes	2	4	6	1	8	4	Not L/U	yes	no	no	no	no	no	no	no	yes	?
Coffee machine + unbounded drinker		no	no	yes	no	no	no	no	no	no	yes	2	4	6	1	8	4	Not L/U	yes	no	no	yes	no	no	no	no	no	?
Coffee machine + unbounded drinker		no	no	yes	no	no	no	no	no	no	yes	2	4	6	1	8	4	Not L/U	yes	no	no	no	no	no	no	no	yes	?
CSMA/CD	[KNSW07]	yes	no	no	no	yes	no	yes	yes	no	no	3	3	3	0	19	9	Not L/U	yes	no	yes	no	no	no	no	no	no	H.S.
CSMA/CD	[KNSW07]	yes	no	no	no	yes	no	yes	yes	no	no	3	3	3	0	19	9	Not L/U	yes	no	no	no	yes	no	no	no	no	?
CSMA/CD	[KNSW07]	yes	no	no	no	yes	no	yes	yes	no	no	3	3	3	0	19	9	Not L/U	yes	no	no	no	no	no	no	no	yes	?
CSMA/CD	[KNSW07]	yes	no	no	no	yes	no	yes	yes	no	no	3	3	3	0	525	9	Not L/U	yes	no	yes	no	no	no	no	no	no	H.S.
CSMA/CD	[KNSW07]	yes	no	no	no	yes	no	yes	yes	no	no	3	3	3	0	525	9	Not L/U	yes	no	no	no	yes	no	no	no	no	?
CSMA/CD	[KNSW07]	yes	no	no	no	yes	no	yes	yes	no	no	3	3	3	0	525	9	Not L/U	yes	no	no	no	no	no	no	no	yes	?
CSMA/CD	[KNSW07]	yes	no	no	no	yes	no	yes	yes	no	no	3	3	3	0	4115	9	Not L/U	yes	no	yes	no	no	no	no	no	no	H.S.
CSMA/CD	[KNSW07]	yes	no	no	no	yes	no	yes	yes	no	no	3	3	3	0	4115	9	Not L/U	yes	no	no	no	yes	no	no	no	no	?
CSMA/CD	[KNSW07]	yes	no	no	no	yes	no	yes	yes	no	no	3	3	3	0	4115	9	Not L/U	yes	no	no	no	no	no	no	no	yes	?
CSMA/CD	[KNSW07]	yes	no	no	no	yes	no	yes	yes	no	no	3	3	3	0	8213	9	Not L/U	yes	no	yes	no	no	no	no	no	no	H.S.
CSMA/CD	[KNSW07]	yes	no	no	no	yes	no	yes	yes	no	no	3	3	3	0	8213	9	Not L/U	yes	no	no	no	yes	no	no	no	no	?
CSMA/CD	[KNSW07]	yes	no	no	no	yes	no	yes	yes	no	no	3	3	3	0	8213	9	Not L/U	yes	no	no	no	no	no	no	no	yes	?
Fischer (L/U-PTA)	[AHV93]	yes	no	no	no	no	no	yes	yes	no	no	3	2	4	0	10	10	L/U-PTA	no	no	no	yes	no	no	no	no	no	0.04 s
Fischer (L/U-PTA)	[HRSV02]	yes	no	no	no	no	no	yes	yes	no	no	2	2	4	1	8	0	L/U-PTA	yes	no	no	yes	no	no	no	no	no	H.S.
Fischer (L/U-PTA)	[HRSV02]	yes	no	no	no	no	no	yes	yes	no	no	2	2	4	1	8	0	L/U-PTA	yes	no	no	no	no	no	no	no	yes	?
Fischer (L/U-PTA)	[HRSV02]	yes	no	no	no	no	no	yes	yes	no	no	3	3	4	1	12	0	L/U-PTA	yes	no	no	yes	no	no	no	no	no	H.S.
Fischer (L/U-PTA)	[HRSV02]	yes	no	no	no	no	no	yes	yes	no	no	3	3	4	1	12	0	L/U-PTA	yes	no	no	no	no	no	no	no	yes	?
Fischer (timed CSP)		yes	no	no	no	no	no	yes	yes	no	no	2	2	2	2	10	12	L/U-PTA	yes	no	no	yes	no	no	no	no	no	?
Fischer (timed CSP)		yes	no	no	no	no	no	yes	yes	no	no	2	2	2	2	10	12	L/U-PTA	yes	no	no	no	no	no	no	no	yes	H.S.
Fischer (timed CSP)		yes	no	no	no	no	no	yes	yes	no	no	3	3	2	2	15	18	L/U-PTA	yes	no	no	yes	no	no	no	no	no	?
Fischer (timed CSP)		yes	no	no	no	no	no	yes	yes	no	no	3	3	2	2	15	18	L/U-PTA	yes	no	no	no	no	no	no	no	yes	H.S.
Fischer (unknown origin)		yes	no	no	no	no	no	yes	yes	no	no	3	2	2	1	9	11	L/U-PTA	yes	no	no	yes	no	no	no	no	no	?
Fischer (unknown origin)		yes	no	no	no	no	no	yes	yes	no	no	3	2	2	1	9	11	L/U-PTA	yes	no	no	no	no	no	no	no	yes	?
Fischer-PS08	[PS08]	yes	no	no	no	no	no	yes	yes	no	no	4	2	2	1	13	8	L/U-PTA	no	no	no	yes	no	no	no	no	no	?
Fischer-PS08	[PS08]	yes	no	no	no	no	no	yes	yes	no	no	4	2	2	1	13	8	L/U-PTA	no	no	no	no	no	no	no	no	yes	?
Fischer-PS08	[PS08]	yes	no	no	no	no	no	yes	yes	no	no	5	3	2	1	18	12	L/U-PTA	no	no	no	yes	no	no	no	no	no	?
Fischer-PS08	[PS08]	yes	no	no	no	no	no	yes	yes	no	no	5	3	2	1	18	12	L/U-PTA	no	no	no	no	no	no	no	no	yes	?
Fischer-PS08	[PS08]	yes	no	no	no	no	no	yes	yes	no	no	6	4	2	1	23	16	L/U-PTA	no	no	no	yes	no	no	no	no	no	?
Fischer-PS08	[PS08]	yes	no	no	no	no	no	yes	yes	no	no	6	4	2	1	23	16	L/U-PTA	no	no	no	no	no	no	no	no	yes	?
Fischer-PS08	[PS08]	yes	no	no	no	no	no	yes	yes	no	no	7	5	2	1	28	20	L/U-PTA	no	no	no	yes	no	no	no	no	no	?
Fischer-PS08	[PS08]	yes	no	no	no	no	no	yes	yes	no	no	7	5	2	1	28	20	L/U-PTA	no	no	no	no	no	no	no	no	yes	?
Fischer-PS08	[PS08]	yes	no	no	no	no	no	yes	yes	no	no	12	10	2	1	53	40	L/U-PTA	no	no	no	yes	no	no	no	no	no	?
Fischer-PS08	[PS08]	yes	no	no	no	no	no	yes	yes	no	no	12	10	2	1	53	40	L/U-PTA	no	no	no	no	no	no	no	no	yes	?
Flip-flop	[CC07]	yes	no	no	yes	no	no	no	no	no	no	5	5	2	0	52	12	U-PTA	yes	no	no	yes	no	no	no	no	no	0.031 s
Flip-flop	[CC07]	yes	no	no	yes	no	no	no	no	no	no	5	5	2	0	52	12	U-PTA	yes	no	no	no	no	no	no	no	yes	?
Flip-flop	[CC07]	yes	no	no	yes	no	no	no	no	no	no	5	5	4	0	52	12	U-PTA	yes	no	no	yes	no	no	no	no	no	?
Flip-flop	[CC07]	yes	no	no	yes	no	no	no	no	no	no	5	5	4	0	52	12	U-PTA	yes	no	no	no	no	no	no	no	yes	?
Jobshop i jobs, 4 tasks		no	no	no	no	no	no	no	no	yes	no	2	2	8	4	18	4	Not L/U	yes	no	yes	no	no	no	yes	no	no	?
Jobshop i jobs, 4 tasks		no	no	no	no	no	no	no	no	yes	no	2	2	8	4	18	4	Not L/U	yes	no	no	no	no	no	no	no	yes	?
Jobshop i jobs, 4 tasks		no	no	no	no	no	no	no	no	yes	no	2	3	12	4	27	3	Not L/U	yes	no	yes	no	no	no	yes	no	no	5.58 s
Jobshop i jobs, 4 tasks		no	no	no	no	no	no	no	no	yes	no	2	3	12	4	27	3	Not L/U	yes	no	no	no	no	no	no	no	yes	?
Jobshop i jobs, 4 tasks		no	no	no	no	no	no	no	no	yes	no	4	4	16	4	36	4	Not L/U	yes	no	yes	no	no	no	yes	no	no	?
Jobshop i jobs, 4 tasks		no	no	no	no	no	no	no	no	yes	no	4	4	16	4	36	4	Not L/U	yes	no	no	no	no	no	no	no	yes	T.O.
Cooking noodles		no	no	yes	no	no	no	no	no	no	yes	1	2	2	0	4	4	Not L/U	yes	no	no	yes	no	no	no	no	no	?
Nuclear plant		no	no	yes	no	no	no	no	no	no	yes	1	2	4	0	6	6	Not L/U	yes	no	no	yes	no	no	no	no	no	?
Packaging		yes	no	no	no	no	yes	no	no	no	no	3	2	2	0	10	6	L/U-PTA	yes	no	yes	no	no	no	no	no	no	?
Packaging		yes	no	no	no	no	yes	no	no	no	no	3	2	2	0	10	6	L/U-PTA	yes	no	no	no	no	no	no	no	yes	?
Producer-consumer	[KP12]	yes	no	no	no	no	yes	no	no	no	no	5	5	6	0	16	11	L/U-PTA	yes	no	yes	no	no	no	no	no	no	T.O.
Producer-consumer	[KP12]	yes	no	no	no	no	yes	no	no	no	no	5	5	6	0	20	15	L/U-PTA	yes	no	yes	no	no	no	no	no	no	?
Producer-consumer	[KP12]	yes	no	no	no	no	yes	no	no	no	no	6	6	6	0	18	12	L/U-PTA	yes	no	yes	no	no	no	no	no	no	?
Producer-consumer	[KP12]	yes	no	no	no	no	yes	no	no	no	no	6	6	6	0	21	15	L/U-PTA	yes	no	yes	no	no	no	no	no	no	?
Root contention protocol	[CS01]	no	no	no	no	yes	no	yes	yes	no	no	5	6	5	6	48	16	L/U-PTA	yes	no	yes	no	no	no	no	no	no	1.07 s
Root contention protocol	[CS01]	no	no	no	no	yes	no	yes	yes	no	no	5	6	5	6	48	16	L/U-PTA	yes	no	no	no	yes	no	no	no	no	?
Root contention protocol	[CS01]	no	no	no	no	yes	no	yes	yes	no	no	5	6	5	6	48	16	L/U-PTA	yes	no	no	no	yes	no	no	no	no	?
SSLAF14 test 1	[SSLAF13]	no	no	no	no	no	no	yes	yes	no	no	7	16	2	2	42	23	Not L/U	yes	yes	no	yes	no	no	no	no	no	0.33 s
SSLAF14 test 2	[SSLAF13]	no	no	no	no	no	no	yes	yes	no	no	6	14	2	4	45	26	Not L/U	yes	yes	no	yes	no	no	no	no	no	T.O.
NP-FPS-3tasks	[JLR13]	yes	no	no	no	no	no	yes	yes	no	no	4	6	2	0	17	3	Not L/U	yes	no	no	yes	no	no	no	no	no	?
NP-FPS-3tasks	[JLR13]	yes	no	no	no	no	no	yes	yes	no	no	4	6	2	0	17	3	U-PTA	yes	no	no	yes	no	no	no	no	no	1.03 s
NP-FPS-3tasks	[JLR13]	yes	no	no	no	no	no	yes	yes	no	no	4	6	2	0	17	3	U-PTA	yes	no	no	yes	no	no	no	no	no	?
NP-FPS-3tasks	[JLR13]	yes	no	no	no	no	no	yes	yes	no	no	4	6	2	0	17	3	U-PTA	yes	no	no	yes	no	no	no	no	no	?
NP-FPS-3tasks	[JLR13]	yes	no	no	no	no	no	yes	yes	no	no	4	6	2	0	17	3	U-PTA	yes	no	no	yes	no	no	no	no	no	65.23 s
SLAF14	[SLAF14]	yes	no	no	no	no	no	yes	yes	no	no	8	13	2	3	47	17	Not L/U	yes	yes	no	yes	no	no	no	no	no	1.49 s
SLAF14	[SLAF14]	yes	no	no	no	no	no	yes	yes	no	no	12	21	2	0	153	29	Not L/U	yes	yes	no	yes	no	no	no	no	no	14.61 s
FMTV Challenge 1A	[SAL15]	no	no	no	no	yes	no	yes	yes	no	no	3	3	3	5	15	9	Not L/U	yes	no	yes	no	no	no	yes	no	no	6.97 s
FMTV Challenge 1A	[SAL15]	no	no	no	no	yes	no	yes	yes	no	no	3	3	3	7	15	12	Not L/U	yes	no	yes	no	no	no	yes	no	no	87.39 s
FMTV Challenge 2	[SAL15]	no	no	no	no	yes	no	yes	yes	no	no	6	9	2	0	87	21	Not L/U	yes	yes	yes	no	no	no	yes	no	no	1.61 s
SIMOP	[ACDFR09]	no	no	no	no	yes	no	no	no	no	no	5	8	2	0	46	16	Not L/U	yes	no	yes	no	no	no	no	no	no	?
SIMOP	[ACDFR09]	no	no	no	no	yes	no	no	no	no	no	5	8	2	0	46	16	Not L/U	yes	no	no	no	no	no	no	no	yes	?
SIMOP	[ACDFR09]	no	no	no	no	yes	no	no	no	no	no	5	8	3	0	46	16	Not L/U	yes	no	yes	no	no	no	no	no	no	T.O.
SIMOP	[ACDFR09]	no	no	no	no	yes	no	no	no	no	no	5	8	3	0	46	16	Not L/U	yes	no	no	no	no	no	no	no	yes	?
train1PTA		no	no	yes	no	no	no	no	no	no	yes	1	2	3	0	5	4	Not L/U	yes	no	no	yes	no	no	no	no	no	?
train1PTA		no	no	yes	no	no	no	no	no	no	yes	1	2	3	0	5	4	Not L/U	yes	no	no	no	no	no	no	no	yes	?
TrainAHV93	[AHV93]	yes	no	no	no	no	no	no	no	no	no	3	3	6	0	12	8	L/U-PTA	no	no	no	yes	no	no	no	no	no	0.01 s
TrainAHV93	[AHV93]	yes	no	no	no	no	no	no	no	no	no	3	3	6	0	12	8	L/U-PTA	no	no	no	yes	no	no	no	no	no	?
SPSMALL	[CEFX09][Andre10]	no	no	no	yes	yes	no	no	no	no	no	11	11	2	0	52	25	Not L/U	yes	no	yes	no	no	no	no	no	no	?
SPSMALL	[CEFX09][Andre10]	no	no	no	yes	yes	no	no	no	no	no	11	11	2	0	52	25	Not L/U	yes	no	no	no	no	no	no	no	yes	0.96 s
WFAS	[BBLS15]	yes	no	no	no	no	no	no	no	no	no	3	4	2	0	10	4	Not L/U	yes	no	no	yes	no	no	no	no	no	H.S.
WFAS	[BBLS15]	yes	no	no	no	no	no	no	no	no	no	3	4	2	0	10	4	Not L/U	yes	no	no	no	no	no	no	no	yes	?
WFAS	[BBLS15]	yes	no	no	no	no	no	no	no	no	no	3	4	2	0	10	4	Not L/U	yes	no	no	no	no	no	no	no	yes	?
accel	[HAF14][AHW18]	no	yes	no	no	yes	no	no	no	no	no	2	2	3	0	2574	10	Not L/U	yes	no	yes	no	no	no	no	no	no	1.25 s
accel	[HAF14][AHW18]	no	yes	no	no	yes	no	no	no	no	no	2	2	3	0	4909	10	Not L/U	yes	no	yes	no	no	no	no	no	no	?
accel	[HAF14][AHW18]	no	yes	no	no	yes	no	no	no	no	no	2	2	3	0	7814	10	Not L/U	yes	no	yes	no	no	no	no	no	no	?
accel	[HAF14][AHW18]	no	yes	no	no	yes	no	no	no	no	no	2	2	3	0	10060	10	Not L/U	yes	no	yes	no	no	no	no	no	no	?
accel	[HAF14][AHW18]	no	yes	no	no	yes	no	no	no	no	no	2	2	3	0	12546	10	Not L/U	yes	no	yes	no	no	no	no	no	no	?
accel	[HAF14][AHW18]	no	yes	no	no	yes	no	no	no	no	no	2	2	3	0	15390	10	Not L/U	yes	no	yes	no	no	no	no	no	no	?
accel	[HAF14][AHW18]	no	yes	no	no	yes	no	no	no	no	no	2	2	3	0	17703	10	Not L/U	yes	no	yes	no	no	no	no	no	no	?
accel	[HAF14][AHW18]	no	yes	no	no	yes	no	no	no	no	no	2	2	3	0	20314	10	Not L/U	yes	no	yes	no	no	no	no	no	no	?
accel	[HAF14][AHW18]	no	yes	no	no	yes	no	no	no	no	no	2	2	3	0	22706	10	Not L/U	yes	no	yes	no	no	no	no	no	no	?
accel	[HAF14][AHW18]	no	yes	no	no	yes	no	no	no	no	no	2	2	3	0	25152	10	Not L/U	yes	no	yes	no	no	no	no	no	no	12.67 s
gear	[HAF14][AHW18]	no	yes	no	no	yes	no	no	no	no	no	2	2	3	0	1475	6	Not L/U	yes	no	yes	no	no	no	no	no	no	0.77 s
gear	[HAF14][AHW18]	no	yes	no	no	yes	no	no	no	no	no	2	2	3	0	2845	6	Not L/U	yes	no	yes	no	no	no	no	no	no	?
gear	[HAF14][AHW18]	no	yes	no	no	yes	no	no	no	no	no	2	2	3	0	4603	6	Not L/U	yes	no	yes	no	no	no	no	no	no	?
gear	[HAF14][AHW18]	no	yes	no	no	yes	no	no	no	no	no	2	2	3	0	5847	6	Not L/U	yes	no	yes	no	no	no	no	no	no	?
gear	[HAF14][AHW18]	no	yes	no	no	yes	no	no	no	no	no	2	2	3	0	7309	6	Not L/U	yes	no	yes	no	no	no	no	no	no	?
gear	[HAF14][AHW18]	no	yes	no	no	yes	no	no	no	no	no	2	2	3	0	9003	6	Not L/U	yes	no	yes	no	no	no	no	no	no	?
gear	[HAF14][AHW18]	no	yes	no	no	yes	no	no	no	no	no	2	2	3	0	10323	6	Not L/U	yes	no	yes	no	no	no	no	no	no	?
gear	[HAF14][AHW18]	no	yes	no	no	yes	no	no	no	no	no	2	2	3	0	11839	6	Not L/U	yes	no	yes	no	no	no	no	no	no	?
gear	[HAF14][AHW18]	no	yes	no	no	yes	no	no	no	no	no	2	2	3	0	13191	6	Not L/U	yes	no	yes	no	no	no	no	no	no	?
gear	[HAF14][AHW18]	no	yes	no	no	yes	no	no	no	no	no	2	2	3	0	14665	6	Not L/U	yes	no	yes	no	no	no	no	no	no	7.42 s
blowup	[AHW18]	no	no	no	no	no	no	no	no	no	yes	2	3	5	0	208	4	Not L/U	yes	no	yes	no	no	no	no	no	no	?
blowup	[AHW18]	no	no	no	no	no	no	no	no	no	yes	2	3	5	0	408	4	Not L/U	yes	no	yes	no	no	no	no	no	no	?
blowup	[AHW18]	no	no	no	no	no	no	no	no	no	yes	2	3	5	0	608	4	Not L/U	yes	no	yes	no	no	no	no	no	no	?
blowup	[AHW18]	no	no	no	no	no	no	no	no	no	yes	2	3	5	0	808	4	Not L/U	yes	no	yes	no	no	no	no	no	no	?
blowup	[AHW18]	no	no	no	no	no	no	no	no	no	yes	2	3	5	0	1008	4	Not L/U	yes	no	yes	no	no	no	no	no	no	?

References

[ACDFR09]

Étienne André, Thomas Chatain, Olivier De Smet, Laurent Fribourg and Silvain Ruel. Synthèse de contraintes temporisées pour une architecture d’automatisation en réseau. In Didier Lime and Olivier H. Roux (eds.), MSR’09, Journal Européen des Systèmes Automatisés 43(7-9), Hermès, pages 1049–1064, 2009.

[ACR16]

Étienne André, Thomas Chatain and César Rodríguez. Preserving Partial Order Runs in Parametric Time Petri Nets. Transactions on Embedded Computing Systems 16(2), pages 43:1–43:26, December 2016. (English) [PDF | BibTeX]

[AHV93]

Rajeev Alur, Thomas A. Henzinger, Moshe Y. Vardi: Parametric real-time reasoning. STOC 1993: 592-601.

[AHW18]

Étienne André, Ichiro Hasuo and Masaki Waga (和賀 正樹). Offline timed pattern matching under uncertainty. In Anthony Widjaja Lin and Jun Sun (eds.), ICECCS’18, IEEE CPS, pages 10–10, December 2018. (English) [BibTeX | Slides]

[Andre10]

Étienne André. An Inverse Method for the Synthesis of Timing Parameters in Concurrent Systems. Ph.D. thesis, Laboratoire Spécification et Vérification, ENS Cachan, France, December 2010.

[BBLS15]

Nikola Beneš, Peter Bezděk, Kim Guldstrand Larsen, Jirí Srba: Language Emptiness of Continuous-Time Parametric Timed Automata. In ICALP 2015, Part II, volume 9135 of LNCS, pages 69-81. Springer, 2015.

[CC05]

Robert Clarisó, Jordi Cortadella. Verification of Concurrent Systems with Parametric Delays Using Octahedra. In ACSD’05, 2005.

[CC07]

Robert Clarisó, Jordi Cortadella. The Octahedron Abstract Domain. In Science of Computer Programming 64(1), pages 115-139, 2007.

[CEFX09]

Rémy Chevallier, Emmanuelle Encrenaz-Tiphène, Laurent Fribourg, and Weiwen Xu. Timed verification of the generic architecture of a memory circuit using parametric timed automata. Formal Methods in System Design, 34(1):59–81, 2009.

[CS01]

Aurore Collomb-Annichini and Mihaela Sighireanu. Parameterized Reachability Analysis of the IEEE 1394 Root Contention Protocol using TReX. In Proceedings of the Real-Time Tools Workshop (RT-TOOLS’2001).

[DKRT97]

Pedro R. D’Argenio, Joost-Pieter Katoen, Theo C. Ruys, Jan Tretmans: The Bounded Retransmission Protocol Must Be on Time! TACAS 1997: 416-431.

[HAF14]

Bardh Hoxha, Houssam Abbas, Georgios E. Fainekos: Benchmarks for Temporal Logic Requirements for Automotive Systems. ARCH@CPSWeek 2014: 25-30

[HRSV02]

Thomas Hune, Judi Romijn, Mariëlle Stoelinga, Frits W. Vaandrager: Linear parametric model checking of timed automata. J. Log. Algebr. Program. 52-53: 183-220 (2002)

[JLR13]

Aleksandra Jovanović, Didier Lime, and Olivier H. Roux. Integer parameter synthesis for timed automata. In TACAS, volume 7795 of Lecture Notes in Computer Science, pages 401–415. Springer, 2013.

[KNSW07]

Marta Kwiatkowska, Gethin Norman, Jeremy Sproston, and Fuzhi Wang. Symbolic Model Checking for Probabilistic Timed Automata. Information and Computation, 205(7), pages 1027-1077. July 2007.

[KP12]

Michał Knapik, Wojciech Penczek: Bounded Model Checking for Parametric Timed Automata. Trans. Petri Nets and Other Models of Concurrency 5: 141-159 (2012)

[PS08]

Wojciech Penczek, Maciej Szreter. SAT-based Unbounded Model Checking of Timed Automata. Fundam. Inform. 85(1-4): 425-440 (2008)

[SAL15]

Sun Youcheng, Étienne André and Giuseppe Lipari. Verification of Two Real-Time Systems Using Parametric Timed Automata. In Sophie Quinton and Tullio Vardanega (eds.), WATERS’15, July 2015. (English) [PDF (author version)]

[SLAF14]

Giuseppe Lipari, Sun Youcheng (孙有程), Étienne André and Laurent Fribourg. Toward Parametric Timed Interfaces for Real-Time Components. In Étienne André and Goran Frehse (eds.), SynCoP’14, EPTCS 145, pages 49–64, April 2014. (English) [PDF | BibTeX]

[SSLAF13]

Sun Youcheng, Romain Soulat, Giuseppe Lipari, Étienne André and Laurent Fribourg. Parametric Schedulability Analysis of Fixed Priority Real-Time Distributed Systems. In Cyrille Artho and Peter Ölveczky (eds.), FTSCS’13, Volume 419 of Communications in Computer and Information Science, Springer, pages 212–228, October 2013. (English) [PDF (author version) | Slides]