IMITATOR

The IMITATOR benchmarks library (v2.0)

This is not the latest version of the library; see the newest version instead.

This page presents the official IMITATOR benchmarks library, as of version 2.0, released in August 2021. These models have been accumulated over the years from scientific publications, and from industrial collaborations.

The library is described in [AMP21].

In this v2.0 version, the library contains 56 benchmarks with 119 different models and 216 properties.

The entire library in v2.0 can be downloaded on Zenodo, including all benchmarks, properties, and scripts to produce this page: doi.org/10.5281/zenodo.4730980.

BenchmarkJaniSourceCategoriesMetricsProperties
Ac.Auto.Educ.Hard.Ind.Mon.Prod.Prot.RTSSched.ToyUnsol.Scal.Gen.|IPTA||X|Inv.?<>1 clocks?L/U?Sil.?stDet.?|P||discr. Var||Act||L|avg(|L|)|T|avg(|T|)PropertyTime|States||comp. States|
accel accel-1000 [HAF14][AHW18] Auto. Ind. Mon. yes yes 2 2 true false not L/U true true 3 0 11 2574 1287.0 2592 1296.0 EF 2.846 s. 6504 6504
EFpmin 3.161 s. 6502 6504
accel-10000 [HAF14][AHW18] Auto. Ind. Mon. yes yes 2 2 true false not L/U true true 3 0 11 25152 12576.0 25170 12585.0 EF 24.602 s. 63773 63773
EFpmin 28.575 s. 63741 63759
accel-2000 [HAF14][AHW18] Auto. Ind. Mon. yes yes 2 2 true false not L/U true true 3 0 11 4909 2454.5 4927 2463.5 EF 5.316 s. 12429 12429
EFpmin 6.794 s. 12426 12429
accel-3000 [HAF14][AHW18] Auto. Ind. Mon. yes yes 2 2 true false not L/U true true 3 0 11 7814 3907.0 7832 3916.0 EF 9.035 s. 19922 19922
EFpmin 10.284 s. 19907 19916
accel-4000 [HAF14][AHW18] Auto. Ind. Mon. yes yes 2 2 true false not L/U true true 3 0 11 10060 5030.0 10078 5039.0 EF 8.329 s. 25520 25520
EFpmin 13.733 s. 25514 25518
accel-5000 [HAF14][AHW18] Auto. Ind. Mon. yes yes 2 2 true false not L/U true true 3 0 11 12546 6273.0 12564 6282.0 EF 16.149 s. 31951 31951
EFpmin 15.770 s. 31926 31939
accel-6000 [HAF14][AHW18] Auto. Ind. Mon. yes yes 2 2 true false not L/U true true 3 0 11 15390 7695.0 15408 7704.0 EF 17.222 s. 39152 39152
EFpmin 18.175 s. 39129 39142
accel-7000 [HAF14][AHW18] Auto. Ind. Mon. yes yes 2 2 true false not L/U true true 3 0 11 17703 8851.5 17721 8860.5 EF 18.170 s. 45065 45065
EFpmin 21.349 s. 45039 45053
accel-8000 [HAF14][AHW18] Auto. Ind. Mon. yes yes 2 2 true false not L/U true true 3 0 11 20314 10157.0 20332 10166.0 EF 22.128 s. 51660 51660
EFpmin 26.750 s. 51629 51644
accel-9000 [HAF14][AHW18] Auto. Ind. Mon. yes yes 2 2 true false not L/U true true 3 0 11 22706 11353.0 22724 11362.0 EF 25.346 s. 57534 57534
EFpmin 22.254 s. 57506 57522
ALR15_fig1 ALR15_fig1 [ALR15] Ac. Toy Unsol. no no 1 2 false false U-PTA true true 1 0 4 4 4.0 4 4.0 CycleThrough NE (Uns.)
EF NE (Uns.)
AndOr AndOr [CC05] Ac. Hard. no no 3 4 true false L/U-PTA false true 12 0 8 20 6.6 44 14.6 IM 0.145 s. 21 32
pattern 6.670 s. 19 22
ATM fig1_DCLXZL18-fixed [DCLXZL18] Ac. Toy no no 1 3 true false not L/U true true 3 0 9 5 5.0 9 9.0 CycleThrough 0.005 s. 11 14
DeadlockFree 0.022 s. 13 30
EF 0.003 s. 7 9
blowup blowup-1000 [AHW18] Mon. Toy yes yes 2 3 true false not L/U true true 5 0 5 1008 504.0 1011 505.5 EF TO (Term.)
EFpmin 2.936 s. 2681 3242
blowup-200 [AHW18] Mon. Toy yes yes 2 3 true false not L/U true true 5 0 5 208 104.0 211 105.5 EF 112.797 s. 20602 20602
EFpmin 0.470 s. 558 678
blowup-400 [AHW18] Mon. Toy yes yes 2 3 true false not L/U true true 5 0 5 408 204.0 411 205.5 EF 780.789 s. 81202 81202
EFpmin 1.001 s. 1091 1322
blowup-600 [AHW18] Mon. Toy yes yes 2 3 true false not L/U true true 5 0 5 608 304.0 611 305.5 EF 2617.989 s. 181802 181802
EFpmin 1.445 s. 1615 1954
blowup-800 [AHW18] Mon. Toy yes yes 2 3 true false not L/U true true 5 0 5 808 404.0 811 405.5 EF TO (Term.)
EFpmin 2.148 s. 2159 2612
BlT09_fig1 BlT09_fig1 [BlT09] Toy no no 1 2 false false L/U-PTA true true 2 0 7 4 4.0 7 7.0 CycleThrough 0.001 s. 4 8
BRPAAPP21 BRPAAPP21_GFSinRC [AAPP21] Prot. no no 5 4 true false not L/U true false 4 9 18 16 3.2 30 6.0 CycleThrough 1.142 s. 653 887
BRPAAPP21_GSinFSdk [AAPP21] Prot. no no 5 4 true false not L/U true false 4 9 18 16 3.2 34 6.8 CycleThrough 13.782 s. 6795 9451
BRPAAPP21_GSinFSnok [AAPP21] Prot. no no 5 4 true false not L/U true false 4 9 18 16 3.2 33 6.6 CycleThrough 0.057 s. 35 36
BRPAAPP21_RC [AAPP21] Prot. no no 4 4 true false not L/U true false 4 9 20 15 3.7 28 7.0 AGnot 2.408 s. 455 708
BRPDKRT97 BRPDKRT97 [DKRT97] Ac. Ind. Prot. RTS no no 6 6 true false not L/U true false 2 11 20 22 3.6 52 8.6 AGnot 480.383 s. 3114 6450
IM 6270.361 s. 74949 135718
Coffee coffee Educ. Toy no no 1 2 true false not L/U false true 3 0 4 4 4.0 6 6.0 EF 0.002 s. 6 8
IM 0.045 s. 61 95
CoffeeDrinker coffeeDrinker Educ. Toy no no 2 4 true false not L/U true false 6 1 7 8 4.0 14 7.0 AGnot 0.077 s. 46 72
IM 3.211 s. 995 1620
coffeeDrinker_toolpaper Educ. Toy no no 2 3 true false not L/U true false 3 1 6 8 4.0 14 7.0 AGnot 0.036 s. 22 23
AGnot2 0.037 s. 22 23
AGnot3 0.038 s. 22 23
IM 0.022 s. 13 23
pattern 0.010 s. 15 15
pattern2 0.009 s. 15 15
coffeeDrinker_unbounded Educ. Toy no no 2 4 true false not L/U true true 6 1 7 8 4.0 13 6.5 AGnot TO (Term.)
CSMACD CSMACD-bc1 [KNSW07] Ac. Ind. Prot. RTS yes yes 3 3 true false not L/U false false 3 0 9 19 6.3 39 13.0 EF 0.017 s. 37 60
IM 1.007 s. 511 1625
CSMACD-bc10 [KNSW07] Ac. Ind. Prot. RTS yes yes 3 3 true false not L/U false false 3 0 9 8213 2737.6 24567 8189.0 EF 0.018 s. 37 60
IM 5238.929 s. 680105 1706787
CSMACD-bc5 [KNSW07] Ac. Ind. Prot. RTS yes yes 3 3 true false not L/U false false 3 0 9 267 89.0 759 253.0 EF 0.018 s. 37 60
IM 30.643 s. 16221 42967
CSMACD-bc6 [KNSW07] Ac. Ind. Prot. RTS yes yes 3 3 true false not L/U false false 3 0 9 525 175.0 1527 509.0 EF 0.019 s. 37 60
IM 71.808 s. 37177 96179
CSMACD-bc9 [KNSW07] Ac. Ind. Prot. RTS yes yes 3 3 true false not L/U false false 3 0 9 4115 1371.6 12279 4093.0 EF 0.028 s. 57 100
IM 2605.683 s. 504337 1268139
Cycle1 Cycle1 Ac. Toy Unsol. no no 1 2 true false U-PTA true true 1 0 1 1 1.0 1 1.0 Cycle NE (Uns.)
Cycles_2 infinite-2 [AAPP21] Ac. Toy Unsol. no no 1 2 true false U-PTA true true 1 0 3 2 2.0 3 3.0 Cycle 0.002 s. 8 10
CycleThrough 0.001 s. 4 5
Cycles_5 infinite-5 [AAPP21] Ac. Toy Unsol. no no 1 2 true false U-PTA true true 1 0 1 1 1.0 1 1.0 Cycle NE (Uns.)
CycleThrough NE (Uns.)
Cycles_5_6 infinite-5_6 [AAPP21] Ac. Toy Unsol. no no 1 2 true false U-PTA true true 1 0 3 2 2.0 3 3.0 Cycle NE (Uns.)
CycleThrough NE (Uns.)
Cycles_exU_noloop exU_noloop Ac. Toy Unsol. no no 1 2 true false U-PTA true true 1 0 2 2 2.0 2 2.0 CycleThrough NE (Uns.)
Cycles_noSolution infinite-noSolution [AAPP21] Ac. Toy Unsol. no no 1 2 true false U-PTA true true 1 0 1 1 1.0 1 1.0 Cycle NE (Uns.)
CycleThrough NE (Uns.)
Cycles_notFiniteDisjunction infinite-notFiniteDisjunction [AAPP21] Ac. Toy Unsol. no no 1 2 true false not L/U true true 1 0 3 2 2.0 3 3.0 Cycle NE (Uns.)
CycleThrough NE (Uns.)
Cycles_Rplus infinite-Rplus [AAPP21] Ac. Toy Unsol. no no 1 2 true false not L/U true true 2 0 1 1 1.0 1 1.0 Cycle NE (Uns.)
CycleThrough NE (Uns.)
Cycles_Zero infinite-Zero Ac. Toy Unsol. no no 1 2 true false not L/U true true 1 0 1 1 1.0 1 1.0 Cycle NE (Uns.)
CycleThrough NE (Uns.)
Fischer2 fischer_2 Ac. Prot. RTS no no 3 2 true false L/U-PTA false true 2 1 11 9 3.0 23 7.6 AGnot 0.022 s. 35 90
IM TO (Term.)
FischerAHV93 FischerAHV93 [AHV93] Ac. Prot. RTS no no 3 2 false false L/U-PTA true true 4 0 16 13 4.3 32 10.6 AGnot 0.018 s. 33 71
FischerHRSV02 fischerHRSV02_2 [HRSV02] Ac. Prot. RTS nb of proc. no 2 2 true false L/U-PTA true true 4 1 12 8 4.0 12 6.0 AGnot TO (Term.)
IM TO (Term.)
fischerHRSV02_3 [HRSV02] Ac. Prot. RTS nb of proc. no 3 3 true false L/U-PTA true true 4 1 18 12 4.0 18 6.0 AGnot TO (Term.)
IM TO (Term.)
FischerPAT fischerPAT2 Ac. Prot. RTS nb of proc. no 2 2 true false L/U-PTA false false 2 2 12 10 5.0 14 7.0 AGnot 0.086 s. 26 173
IM TO (Term.)
fischerPAT3 Ac. Prot. RTS nb of proc. no 3 3 true false L/U-PTA false false 2 2 18 15 5.0 21 7.0 AGnot 2.173 s. 178 2656
IM TO (Term.)
FischerPS08 FischerPS08-10 [PS08] Ac. Prot. RTS yes yes 12 10 false false L/U-PTA true true 2 1 41 53 4.4 181 15.0 AGnot TO (Term.)
IM TO (Term.)
FischerPS08-2 [PS08] Ac. Prot. RTS yes yes 4 2 false false L/U-PTA true true 2 1 9 13 3.2 21 5.2 AGnot 0.019 s. 38 48
IM TO (Term.)
FischerPS08-3 [PS08] Ac. Prot. RTS yes yes 5 3 false false L/U-PTA true true 2 1 13 18 3.6 34 6.8 AGnot 0.306 s. 330 516
IM TO (Term.)
FischerPS08-4 [PS08] Ac. Prot. RTS yes yes 6 4 false false L/U-PTA true true 2 1 17 23 3.8 49 8.1 AGnot 10.693 s. 4365 8550
IM TO (Term.)
FischerPS08-5 [PS08] Ac. Prot. RTS yes yes 7 5 false false L/U-PTA true true 2 1 21 28 4.0 66 9.4 AGnot 1887.661 s. 76557 175661
IM TO (Term.)
Flipflop flipflop-2D [CC07] Ac. Hard. no no 5 5 true false U-PTA false true 2 0 12 49 9.8 142 28.4 IM 0.009 s. 13 14
IM2 0.008 s. 11 13
pattern 0.010 s. 12 14
flipflop-4D [CC07] Ac. Hard. no no 5 5 true false U-PTA false true 4 0 12 49 9.8 142 28.4 IM 0.012 s. 13 15
IM2 0.012 s. 11 14
pattern 0.140 s. 53 60
FMTV1 FMTV_1_A1 [SAL15] Ind. Prot. RTS no no 3 3 true false not L/U true false 3 5 14 15 5.0 21 7.0 EF 9.128 s. 564 1020
EFpmax 8.271 s. 611 1036
EFpmin 12.429 s. 568 1014
FMTV_1_A3 [SAL15] Ind. Prot. RTS no no 3 3 true false not L/U true false 3 7 18 15 5.0 28 9.3 EF 82.296 s. 2744 4580
EFpmax 67.978 s. 3082 4831
EFpmin 107.228 s. 2626 4427
FMTV2 FMTV_2 [SAL15] Ind. Prot. RTS no no 6 9 true true not L/U true true 2 0 28 87 14.5 129 21.5 EF 2.132 s. 376 493
gear gear-1000 [HAF14][AHW18] Auto. Ind. Mon. yes yes 2 2 true false not L/U true true 3 0 7 1475 737.5 1481 740.5 EF 2.135 s. 4453 4453
EFpmin 1.687 s. 3374 3753
gear-10000 [HAF14][AHW18] Auto. Ind. Mon. yes yes 2 2 true false not L/U true true 3 0 7 14665 7332.5 14671 7335.5 EF 19.387 s. 44581 44581
EFpmin 19.026 s. 33419 37235
gear-2000 [HAF14][AHW18] Auto. Ind. Mon. yes yes 2 2 true false not L/U true true 3 0 7 2845 1422.5 2851 1425.5 EF 3.608 s. 8633 8633
EFpmin 3.412 s. 6485 7224
gear-3000 [HAF14][AHW18] Auto. Ind. Mon. yes yes 2 2 true false not L/U true true 3 0 7 4603 2301.5 4609 2304.5 EF 6.187 s. 14181 14181
EFpmin 5.913 s. 10554 11801
gear-4000 [HAF14][AHW18] Auto. Ind. Mon. yes yes 2 2 true false not L/U true true 3 0 7 5847 2923.5 5853 2926.5 EF 9.066 s. 17865 17865
EFpmin 7.206 s. 13354 14900
gear-5000 [HAF14][AHW18] Auto. Ind. Mon. yes yes 2 2 true false not L/U true true 3 0 7 7309 3654.5 7315 3657.5 EF 10.355 s. 22501 22501
EFpmin 10.104 s. 16718 18692
gear-6000 [HAF14][AHW18] Auto. Ind. Mon. yes yes 2 2 true false not L/U true true 3 0 7 9003 4501.5 9009 4504.5 EF 11.906 s. 27609 27609
EFpmin 9.978 s. 20603 23007
gear-7000 [HAF14][AHW18] Auto. Ind. Mon. yes yes 2 2 true false not L/U true true 3 0 7 10323 5161.5 10329 5164.5 EF 14.073 s. 31753 31753
EFpmin 13.665 s. 23629 26409
gear-8000 [HAF14][AHW18] Auto. Ind. Mon. yes yes 2 2 true false not L/U true true 3 0 7 11839 5919.5 11845 5922.5 EF 15.960 s. 36301 36301
EFpmin 14.892 s. 27062 30221
gear-9000 [HAF14][AHW18] Auto. Ind. Mon. yes yes 2 2 true false not L/U true true 3 0 7 13191 6595.5 13197 6598.5 EF 17.960 s. 40025 40025
EFpmin 17.171 s. 30051 33465
IMPO IMPO [ACR16] Ac. Hard. no no 5 5 true false L/U-PTA false true 6 0 8 20 4.0 30 6.0 AGnot 0.013 s. 12 15
IM 0.008 s. 6 10
IMPOloop IMPOloop [ACR16] Ac. Hard. no no 5 5 true false L/U-PTA false true 10 0 9 22 4.4 37 7.4 AGnot 2.269 s. 56 71
IM 0.021 s. 4 8
IM2 TO (Term.)
JLR15_Fig6 JLR15_Fig6 [JLR15] Toy Unsol. no no 1 2 true false L/U-PTA true true 2 0 2 2 2.0 2 2.0 EF NE (Uns.)
Jobshop jobshop_2_4 [AM01] RTS Sched. no no 2 2 true false not L/U false true 8 4 4 18 9.0 16 8.0 EF 0.142 s. 80 130
IM 2.399 s. 1213 1567
jobshop_3_4 [AM01] RTS Sched. no no 3 3 true false not L/U false true 12 4 3 27 9.0 24 8.0 EF 10.972 s. 1458 3178
IM TO (Term.)
jobshop_4_4 [AM01] RTS Sched. no no 4 4 true false not L/U false true 16 4 4 36 9.0 32 8.0 EF TO (Term.)
LA02 LA02-2_10param [LA02] RTS no ? 3 3 true true not L/U false true 10 0 21 36 12.0 222 74.0 EF 583.381 s. 840 1089
LA02-2_5param [LA02] RTS no ? 3 3 true true not L/U false true 5 0 21 36 12.0 222 74.0 EF 4.404 s. 704 928
LA02-2_inst [LA02] RTS no ? 3 3 true true not L/U false true 0 0 21 36 12.0 222 74.0 EF 0.260 s. 309 462
LA02-3_15param [LA02] RTS no ? 4 4 true true not L/U false true 15 0 31 53 13.2 588 147.0 EF TO (Term.)
LA02-3_1param_wm0j1 [LA02] RTS no ? 4 4 true true not L/U false true 1 0 31 53 13.2 588 147.0 EF 115.719 s. 7898 19803
LA02-3_5param [LA02] RTS no ? 4 4 true true not L/U false true 5 0 31 53 13.2 588 147.0 EF TO (Term.)
LA02-3_inst [LA02] RTS no ? 4 4 true true not L/U false true 0 0 31 53 13.2 588 147.0 EF 38.533 s. 5494 13106
LA02_deadline-2_11param [LA02] RTS no ? 3 3 true true not L/U false true 11 0 21 36 12.0 222 74.0 EF 109.095 s. 840 1089
EFpmin 2.812 s. 808 1089
LA02_deadline-2_1param [LA02] RTS no ? 3 3 true true not L/U false true 1 0 21 36 12.0 222 74.0 EF 0.283 s. 338 494
EFpmin 0.265 s. 336 494
LA02_deadline-3_16param [LA02] RTS no ? 4 4 true true not L/U false true 16 0 31 53 13.2 588 147.0 EF TO (Term.)
EFpmin TO (Term.)
LA02_deadline-3_1param [LA02] RTS no ? 4 4 true true not L/U false true 1 0 31 53 13.2 588 147.0 EF 38.734 s. 6320 14070
EFpmin 37.742 s. 6295 14070
LA02_deadline-3_2param [LA02] RTS no ? 4 4 true true not L/U false true 2 0 31 53 13.2 588 147.0 EF 93.734 s. 9585 19878
EFpmin 81.826 s. 9457 19866
LA02_deadline-3_6param [LA02] RTS no ? 4 4 true true not L/U false true 6 0 31 53 13.2 588 147.0 EF TO (Term.)
EFpmin TO (Term.)
Noodles NoodlesCooking Educ. Toy no no 1 2 true false not L/U false true 2 0 4 5 5.0 5 5.0 AGnot 0.001 s. 5 5
NP_FPS_3tasks JLR13_3tasks_npfp [JLR13] Ac. Prot. RTS no no 4 6 true false not L/U true true 2 0 15 17 4.2 54 13.5 AGnot 77.308 s. 580 1093
JLR13_3tasks_npfp-100_0 [JLR13] Ac. Prot. RTS no no 4 6 true false U-PTA true true 2 0 15 17 4.2 54 13.5 AGnot 2.463 s. 338 429
JLR13_3tasks_npfp-100_2 [JLR13] Ac. Prot. RTS no no 4 6 true false U-PTA true true 2 0 15 17 4.2 54 13.5 AGnot 92.199 s. 425 4544
JLR13_3tasks_npfp-50_0 [JLR13] Ac. Prot. RTS no no 4 6 true false U-PTA true true 2 0 15 17 4.2 54 13.5 AGnot 2.119 s. 296 419
JLR13_3tasks_npfp-50_2 [JLR13] Ac. Prot. RTS no no 4 6 true false U-PTA true true 2 0 15 17 4.2 54 13.5 AGnot 37.502 s. 392 2181
NuclearPlant NuclearPlant Educ. Toy no no 1 2 true false not L/U false true 4 0 6 6 6.0 8 8.0 AGnot 0.007 s. 8 9
Packaging packaging [ABBCR16] Ac. Prod. no no 3 2 true false L/U-PTA false true 2 0 6 10 3.3 16 5.3 AGnot TO (Term.)
ProdCons Pipeline_KP12_2_3 [KP12] Ac. Prod. yes no 5 5 true false L/U-PTA true true 6 0 12 16 3.2 15 3.0 EF TO (Term.)
Pipeline_KP12_2_5 [KP12] Ac. Prod. yes no 5 5 true false L/U-PTA true true 6 0 16 20 4.0 19 3.8 EF TO (Term.)
Pipeline_KP12_3_2 [KP12] Ac. Prod. yes no 6 6 true false L/U-PTA true true 6 0 13 18 3.0 17 2.8 EF TO (Term.)
Pipeline_KP12_3_3 [KP12] Ac. Prod. yes no 6 6 true false L/U-PTA true true 6 0 16 21 3.5 20 3.3 EF TO (Term.)
RCP RCP_CS01 [CS01] Ind. Prot. RTS no no 5 6 true false L/U-PTA true false 5 6 20 30 6.0 82 16.4 EF 2.415 s. 709 890
Researcher researcher Educ. Toy no no 1 2 true true not L/U true false 4 1 6 4 4.0 9 9.0 AGnot 0.016 s. 11 20
CycleThrough 0.004 s. 7 8
CycleThrough2 1.071 s. 367 812
DeadlockFree NE (Uns.)
EF 0.015 s. 11 20
EF2 0.109 s. 41 138
EFpmin 0.070 s. 27 100
IM 0.518 s. 179 464
pattern 0.907 s. 154 425
pattern2 0.013 s. 16 20
pattern3 0.002 s. 4 4
researcher_globaltime Educ. Toy no no 1 3 true true not L/U true false 4 1 6 4 4.0 9 9.0 EFtmin 0.105 s. 43 99
SIMOP simop2 [ACDFR09] Ind. no no 5 8 true false not L/U true true 2 0 25 46 9.2 72 14.4 EF TO (Term.)
IM TO (Term.)
simop3 [ACDFR09] Ind. no no 5 8 true false not L/U true true 3 0 25 46 9.2 72 14.4 EF TO (Term.)
IM TO (Term.)
SLAF14 SLAF14_3 [SLAF14] Ac. Prot. RTS yes no 8 13 true true not L/U true false 2 3 20 47 5.8 81 10.1 AGnot 2.850 s. 505 703
SLAF14_5 [SLAF14] Ac. Prot. RTS yes no 12 21 true true not L/U true true 2 0 34 153 12.7 243 20.2 AGnot 29.934 s. 3248 6461
SPSMALL spsmall [CEFX09][Andre10] Hard. Ind. no no 11 11 true false not L/U false false 2 0 25 52 4.7 145 13.1 AGnot 1.001 s. 279 354
IM 0.089 s. 34 42
SSLAF13_1 SSLAF13_test1 [SSLAF13] Prot. RTS yes yes 7 16 true true not L/U false false 2 2 23 42 6.0 146 20.8 AGnot 0.532 s. 76 152
SSLAF13_2 SSLAF13_test2 [SSLAF13] Prot. RTS yes yes 6 14 true true not L/U false false 2 4 26 45 7.5 154 25.6 AGnot 6074.735 s. 36191 42696
Synth_int01 synthint01 Ac. Toy Unsol. no no 1 2 true false U-PTA true true 1 0 2 2 2.0 2 2.0 EF NE (Uns.)
Synth_InvN synthInvN Ac. Toy Unsol. no no 1 2 true false not L/U true true 1 0 2 2 2.0 2 2.0 EF NE (Uns.)
Synth_N synthN Ac. Toy Unsol. no no 1 2 true false not L/U true true 1 0 2 2 2.0 2 2.0 EF NE (Uns.)
Synth_pN synthpN Ac. Toy Unsol. no no 1 2 true false not L/U true true 2 0 2 2 2.0 2 2.0 EF NE (Uns.)
Synth_pNplusq synthpNplusq [AHV93] Ac. Toy Unsol. no no 1 2 false false not L/U true true 3 0 2 2 2.0 2 2.0 EF NE (Uns.)
Synth_Rplus synthRplus Ac. Toy Unsol. no no 1 2 true false L-PTA true true 1 0 2 2 2.0 2 2.0 EF NE (Uns.)
Train1PTA Train1PTA Educ. Toy no no 1 2 true false not L/U false true 3 0 4 5 5.0 6 6.0 AGnot 0.002 s. 6 7
IM 0.004 s. 7 12
IM2 0.005 s. 7 12
IM3 0.002 s. 4 6
TrainAHV93 TrainAHV93 [AHV93] Ac. no no 3 3 false false L/U-PTA false true 6 0 8 12 4.0 12 4.0 AGnot 0.003 s. 4 4
IM 0.123 s. 79 116
UntimedLanguage untimedLanguage [ALR16] Ac. Toy Unsol. no no 1 2 true false not L/U false false 1 0 3 4 4.0 6 6.0 EF NE (Uns.)
WFAS WFAS_BBLS15 [BBLS15] Ac. no no 3 4 true false not L/U true false 2 0 10 10 3.3 23 7.6 AGnot TO (Term.)
IM 0.127 s. 27 64
IM2 0.039 s. 17 29

References

[AAPP21]
Étienne André, Jaime Arias, Laure Petrucci and Jaco van de Pol. Iterative bounded synthesis for efficient cycle detection in parametric timed automata. In Jan Friso Groote and Kim G. Larsen (eds.), TACAS’21, March 2021. To appear. Creative Commons Attribution 3.0 Unported (CC BY 3.0) (English) [data]
[ABBCR16]
Lăcrămioara Aştefănoaei, Saddek Bensalem, Marius Bozga, Chih-Hong Cheng, Harald Ruess: Compositional Parameter Synthesis. FM 2016: 60-68
[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]
[ALR15]
Étienne André, Didier Lime and Olivier H. Roux. Integer-Complete Synthesis for Bounded Parametric Timed Automata. In Mikołaj Bojańczyk, Sławomir Lasota and Igor Potapov (eds.), RP’15, LNCS 9328, Springer, pages 7–19, September 2015. DOI: 10.1007/978-3-319-24537-9_2 (English) [PDF (author version) | BibTeX | Slides]🌐
[ALR16]
Étienne André, Didier Lime and Olivier H. Roux. Decision Problems for Parametric Timed Automata. In Kazuhiro Ogata and Mark Lawford (eds.), ICFEM’16, Springer LNCS, pages 400–416, November 2016. Acceptance rate: 42%. DOI: 10.1007/978-3-319-47846-3_25 (English) [PDF (author version) | BibTeX | Slides]🌐
[AM01]
Yasmina Abdeddaïm, Oded Maler: Job-Shop Scheduling Using Timed Automata. CAV 2001: 478-492🌐
[AMP21]
Étienne André, Dylan Marinho and Jaco van de Pol. A Benchmarks Library for Extended Timed Automata. In Frédéric Loulergue and Franz Wotawa (eds.), TAP’21, Springer LNCS 12740, pages 39-50, June 2021. DOI: 10.1007/978-3-030-79379-1_3 (English) [PDF (author version) | BibTeX | data | 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.
[BlT09]
Laura Bozzelli, Salvatore La Torre: Decision problems for lower/upper bound parametric timed automata. Formal Methods Syst. Des. 35(2): 121-151 (2009)🌐
[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).
[DCLXZL18]
Liyun Dai, Taolue Chen, Zhiming Liu, Bican Xia, Naijun Zhan, Kim G. Larsen: Parameter Synthesis Problems for one parametric clock Timed Automata. arXiv abs/1809.07177 (2018)
[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.
[JLR15]
Aleksandra Jovanović, Didier Lime, and Olivier H. Roux. Integer parameter synthesis for real-time systems. IEEE Transactions on Software Engeneering 41(5): 445-461 (2015).
[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)
[LA02]
http://bach.istc.kobe-u.ac.jp/csp2sat/jss/
[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. Creative Commons Attribution 3.0 Unported (CC BY 3.0) (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]