IMITATOR

IMITATOR: Experiments Data for ICECCS 2018

Case Studies Related to Offline timed pattern matching under uncertainty

IMITATOR

The version of IMITATOR used to run the experiments is IMITATOR v2.10.4.

Download

Case studies

We present in the following table a list of case studies to which parametric timed pattern matching was applied.

Benchmark: gear

Model PTPM PTPMopt
|X| |P| Raw word Model Length Time frame Parsing States Matches Time Result States Time Result
2 3 gear_1000.tsv gear_1000.imi 1467 1000 0.02 4453 379 1.6 gear_1000.res 3322 0.94 gear_1000-maxp1.res
gear_2000.tsv gear_2000.imi 2837 2000 0.33 8633 739 2.14 gear_2000.res 6422 1.7 gear_2000-maxp1.res
gear_3000.tsv gear_3000.imi 4595 3000 0.77 14181 1247 3.63 gear_3000.res 10448 2.85 gear_3000-maxp1.res
gear_4000.tsv gear_4000.imi 5839 4000 1.23 17865 1546 4.68 gear_4000.res 13233 3.74 gear_4000-maxp1.res
gear_5000.tsv gear_5000.imi 7301 5000 1.94 22501 1974 5.88 gear_5000.res 16585 4.79 gear_5000-maxp1.res
gear_6000.tsv gear_6000.imi 8995 6000 2.96 27609 2404 7.28 gear_6000.res 20413 5.76 gear_6000-maxp1.res
gear_7000.tsv gear_7000.imi 10316 7000 4 31753 2780 8.38 gear_7000.res 23419 6.86 gear_7000-maxp1.res
gear_8000.tsv gear_8000.imi 11831 8000 5.39 36301 3159 9.75 gear_8000.res 26832 7.87 gear_8000-maxp1.res
gear_9000.tsv gear_9000.imi 13183 9000 6.86 40025 3414 10.89 gear_9000.res 29791 8.61 gear_9000-maxp1.res
gear_10000.tsv gear_10000.imi 14657 10000 8.7 44581 3816 12.15 gear_10000.res 33141 9.89 gear_10000-maxp1.res

Benchmark: accel

Model PTPM PTPMopt
|X| |P| Raw word Model Length Time frame Parsing States Matches Time Result States Time Result
2 3 accel_1000.tsv accel_1000.imi 2559 1000 0.27 6504 2 1.6 accel_1000.res 6502 1.85 accel_1000-minp10.res
accel_2000.tsv accel_2000.imi 4894 2000 0.86 12429 2 3.04 accel_2000.res 12426 3.57 accel_2000-minp10.res
accel_3000.tsv accel_3000.imi 7799 3000 2.21 19922 7 4.98 accel_3000.res 19908 6.06 accel_3000-minp10.res
accel_4000.tsv accel_4000.imi 10045 4000 3.74 25520 3 6.51 accel_4000.res 25514 7.55 accel_4000-minp10.res
accel_5000.tsv accel_5000.imi 12531 5000 6.01 31951 9 8.19 accel_5000.res 31926 9.91 accel_5000-minp10.res
accel_6000.tsv accel_6000.imi 15375 6000 9.68 39152 7 10.14 accel_6000.res 39129 12.39 accel_6000-minp10.res
accel_7000.tsv accel_7000.imi 17688 7000 113.4 45065 9 11.61 accel_7000.res 45039 14.06 accel_7000-minp10.res
accel_8000.tsv accel_8000.imi 20299 8000 18.45 51660 10 13.52 accel_8000.res 51629 16.23 accel_8000-minp10.res
accel_9000.tsv accel_9000.imi 22691 9000 24.33 57534 11 15.33 accel_9000.res 57506 18.21 accel_9000-minp10.res
accel_10000.tsv accel_10000.imi 25137 10000 31.35 63773 13 16.9 accel_10000.res 63739 20.61 accel_10000-minp10.res

Benchmark: blowup

Model PTPM PTPMopt
|X| |P| Raw word Model Length Time frame Parsing States Matches Time Result States Time Result
3 5 blowup-200.imi 200 101 0.01 20602 5050 15.31 blowup-200.res 515 0.24 blowup-200-minp1.res
blowup-400.imi 400 202 0.02 81202 20100 82.19 blowup-400.res 1015 0.49 blowup-400-minp1.res
blowup-600.imi 600 301 0.03 322402 45150 158.5 blowup-600.res 1508 0.59 blowup-600-minp1.res
blowup-800.imi 800 405 0.04 242202 80200 342.9 blowup-800.res 2008 0.83 blowup-800-minp1.res
blowup-1000.imi 1000 503 0.1 377752 125250 625.4 blowup-1000.res 2508 1.08 blowup-1000-minp1.res

Description of the Case Studies

Gear and Accel

Benchmark Gear inspired by the scenario of monitoring the gear change of an automatic transmission system. We conducted simulation of the model of an automatic transmission system [HAF14]. We used S-TaLiRo to generate an input to this model; it generates a gear change signal that is fed to the model. A gear is chosen from {g_1,g_2,g_3,g_4}. The generated gear change is recorded in a timed word.

The of benchmark Accel is also constructed from the Simulink model of the automated transmission system [HAF14]. For this benchmark, the (discretized) value of three state variables are recorded in W: engine RPM (discretized to "high" and "low" with a certain threshold), velocity (discretized to "high" and "low" with a certain threshold), and 4 gear positions. We used S-TaLiRo to generate a input sequence of gear change.

Blowup

As a third experiment, we considered an original (toy) benchmark that acts as a worst case situation for parametric timed pattern matching [AHW18].

Calling IMITATOR

For all case studies, the following command was used for PTPM:

> ./imitator [case_study.imi] -mode EFunsafe -no-inclusion-test-in-EF -incl -verbose experiments -output-result

For all case studies, the following command was used for PTPMopt:

> ./imitator [case_study.imi] -mode [EFmin|EFmax] -no-inclusion-test-in-EF -incl -verbose experiments -output-result -output-prefix [case_study-minP1|maxp1|minp10.imi]

References

[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]
[HAF14]
Bardh Hoxha, Houssam Abbas, Georgios E. Fainekos: Benchmarks for Temporal Logic Requirements for Automotive Systems. ARCH@CPSWeek 2014: 25-30

Contact

Étienne André