Online Parametric Timed
Pattern Matching with
Automata-Based Skipping
Masaki Waga1,2,3 and Étienne André4,5,1
National Institute of Informatics1, SOKENDAI2,JSPS Research Fellow3,LIPN, Université Paris 13, CNRS4, JFLI, UMI CNRS5
7 May 2019, NFM 2019
This work is partially supported by JST ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603),
by JSPS Grants-in-Aid No. 15KT0012 & 18J22498 and by the ANR national research program PACS (ANR-14-CE28-0002).

1

M. Waga (NII)ParameterizedSpecification

Monitoring

Online Parametric Timed
Pattern Matching with
Automata-Based SkippingMasaki Waga1,2,3 and Étienne André4,5,1
National Institute of Informatics1, SOKENDAI2,JSPS Research Fellow3,LIPN, Université Paris 13, CNRS4, JFLI, UMI CNRS5
7 May 2019, NFM 2019
This work is partially supported by JST ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603),
by JSPS Grants-in-Aid No. 15KT0012 & 18J22498 and by the ANR national research program PACS (ANR-14-CE28-0002).

1

M. Waga (NII)Why Monitoring?
Exhaustive formal method(e.g. model checking, reachability analysis)•The system is correct/incorrect for any execution•

We need system model (white box)

•Scalability is a big issue

Monitoring•

The system is correct/incorrect for the given execution•

We do not need system model (black box is OK)•Usually scalable
2M. Waga (NII)

(Non-Parametric) Timed Pattern Matching[Ulus+, FORMATS’14, Waga+, FORMATS’16]

Input
•

Time-series data•

System log••

e.g., change of engine rotation (ω) / velocity (v) of a carv↑ at 0.1s, ω↓ at 0.2s, …

Real-time spec.
•Spec. useful for debugging•e.g., unexpected behavior of a carω gets high and remains v gets high > 2 s. later

Output• The intervals where the spec. is satisfied in the log• e.g., The above behavior occurs in 0.8s-3.4s
3M. Waga (NII)Parametric Timed Pattern Matching[André, Hasuo, & Waga, ICECCS’18]

Input
•

Time-series data•

System log••

e.g., change of engine rotation (ω) / velocity (v) of a carv↑ at 0.1s, ω↓ at 0.2s, …

Parametric Real-time spec.
•Spec. useful for debugging (with parameters)•e.g., unexpected behavior of a car (with parameters)
ω gets high and remains v gets high p s. later

Output• The intervals + param. valuation, s.t. the spec. is satisfied in the log• e.g., The above behavior occurs in 0.8s-3.4s, p = 2.5
4M. Waga (NII)Parametric Timed Pattern Matching[André, Hasuo, & Waga, ICECCS’18]

Input•Time-series data•

System log••

e.g., change of engine rotation (ω) / velocity (v) of a carv↑ at 0.1s, ω↓ at 0.2s, …

Parametric Real-time spec.
•Spec. useful for debugging (with parameters)•e.g., unexpected behavior of a car (with parameters)
ω gets high and remains v gets high p s. laterp > 2 : satisfied (unexpected beh.)p ≤ 2 : violated (expected beh.)

Output• The intervals + param. valuation, s.t. the spec. is satisfied in the log• e.g., The above behavior occurs in 0.8s-3.4s, p = 2.5
4M. Waga (NII)PTPM for Periods Detection
Imaginary Example: Electrocardiography (Atrial/Ventricular Spikes)
InputAS VSAS VSAS VS

0.1 0.3

0.7 0.8

1.4 1.6ASVS8.59.0$, t < 103…

Shorter Period
A0AS /x := 0startVS, x < p2 , t < 10/x := 0, y := 0

VS /x := 0, y := 0

AS, x < p1 , t < 10/x := 00AVAS
10.5t
Longer Period$, t < 10AS,x < p1 , t < 10/x := 0V

VS, x < p2 , p3 < y < p4 , t < 10/x := 0, y := 0

OutputMatch(w, A) = {(t,t′,v) | t ∈ [0,0.1), t′ ∈ (1.4, 1.6], v(p1) > 0.6, v(p2) > 0.2, …}∪ … ∪ {(t,t′,v) | t ∈ [1.6, 8.5), t′ ∈ (10.5,∞), v(p1) > 1.5,v(p2) > 0.5}
5M. Waga (NII)

Contribution•

Give a specialized alg. for parametric timed pattern matching•[André, Hasuo, & Waga, ICECCS’18] IMITATOR-based
Model Checker for PTA•

Optimized the algorithm with skipping from string matching (FJS)•Implementation + experiment•

we have 3 new Alg. + IMITATOR-based:
naive, parametric/non-parametric skipping•

Our algorithms are much faster than IMITATOR-basedalgorithm
6

M. Waga (NII)Outline•

Motivation + Introduction•

Technical Part••

The parametric timed pattern matching problem•

Naive algorithm for Parametric TPM [Alg. 1]•Skipping optimization for Parametric TPM•

Parametric Skipping Algorithm [Alg. 2]•

Non-Parametric Skipping Algorithm [Alg. 3]

Experiment
7

M. Waga (NII)Parametric Timed Pattern Matching[André, Hasuo, & Waga, ICECCS’18]

Input
•

ExampleTimed word w ∈ (Σ×R>0)*

w=System log• PTA A••A =startParameterized spec.

!" !# v # !"v"

0 0.1 0.4 0.7 1.03.5 t!" /x := 0!"v" , x = pv"$3p: Duration between ω↑ and v↑

Output••Match(w, A ) ={(t,t′,v) | w|(t,t′) ∈ L(v(A))}
Interval (t,t′) + param. val. v
s.t. spec. is satisfied

8Match(w, A )={(t,t′,v) | 0.7 ≤ t < 1.0,3.5 < t′, v(p) = 2.5}
M. Waga (NII)Outline•

Motivation + Introduction•

Technical Part••

The parametric timed pattern matching problem•

Naive algorithm for Parametric TPM [Alg. 1]•Skipping optimization for Parametric TPM•

Parametric Skipping Algorithm [Alg. 2]•Non-Parametric Skipping Algorithm [Alg. 3]

Experiment
9M. Waga (NII)

Idea of our (naive)
online algorithm
follow the transitions of PTA+
abstraction of clock/param. val.
by convex polyhedra

10

M. Waga (NII)Our online (naive) algorithm
0.7 ≤ t < 1.0, p ∈ R,x=0

start!" /x := 0v" , x = p!"v"$3↓t!" !# v # !"v"

0 0.1 0.4 0.7 1.0t
3.5

11

M. Waga (NII)Our online (naive) algorithm
0.7 ≤ t < 1.0, p ∈ R, 0.7 ≤ t < 1.0, p ∈ R,
x=0x=0start!" /x := 0v" , x = p!"v"$3↓↓t!" !# v # !"v"

0 0.1 0.4 0.7 1.0t
3.5

11M. Waga (NII)Our online (naive) algorithm
0.7 ≤ t < 1.0, p ∈ R, 0.7 ≤ t < 1.0, p ∈ R,
x=0
x=0

start

!" /x := 00.7 ≤ t < 1.0,p = 2.5, x = 2.5v" , x = p!"v"$↓↓t↓!" !# v # !"v"

0 0.1 0.4 0.7 1.0t
3.5

113

M. Waga (NII)Our online (naive) algorithm
0.7 ≤ t < 1.0, p ∈ R, 0.7 ≤ t < 1.0, p ∈ R,
x=0
x=0start!" /x := 00.7 ≤ t < 1.0,
p = 2.5, x = 2.5v" , x = p!"↓↓t

FOUND!!
0.7 ≤ t < 1.0,3.5 < t′p =2.5v"$↓↓t′!" !# v # !"v"

0 0.1 0.4 0.7 1.0

t
3.5

113

M. Waga (NII)Our online (naive) algorithm
0 ≤ t < 0.1, p ∈ R,
x=0start

0 ≤ t < 0.1, p ∈ R,
x=0!" /x := 0v" , x = p!"v"$3↓ ↓t!" !# v # !"v"

0 0.1 0.4 0.7 1.0t
3.5

12

M. Waga (NII)Our online (naive) algorithm
0.1 ≤ t < 0.4, p ∈ R,
x=0start!" /x := 0v" , x = p!"v"$3↓t!" !# v # !"v"

0 0.1 0.4 0.7 1.0t
3.5

13

M. Waga (NII)Our online (naive) algorithm
0.4 ≤ t < 0.7, p ∈ R,
x=0start!" /x := 0v" , x = p!"v"$3↓t!" !# v # !"v"

0 0.1 0.4 0.7 1.0t
3.5

14

M. Waga (NII)Our online (naive) algorithm
0.7 ≤ t < 1.0, p ∈ R, 0.7 ≤ t < 1.0, p ∈ R,
x=0
x=0start!" /x := 00.7 ≤ t < 1.0,
p = 2.5, x = 2.5v" , x = p!"↓↓t

FOUND!!
0.7 ≤ t < 1.0,3.5 < t′p =2.5v"$↓↓t′!" !# v # !"v"

0 0.1 0.4 0.7 1.0t
3.5

15

3

M. Waga (NII)Outline•

Motivation + Introduction•Technical Part••

The parametric timed pattern matching problem•

Naive algorithm for Parametric TPM [Alg. 1]•Skipping optimization for Parametric TPM•

Parametric Skipping Algorithm [Alg. 2]•

Non-Parametric Skipping Algorithm [Alg. 3]

Experiment
16

M. Waga (NII)Motivation: Skip Unnecessary
Our online (naive) Trials
algorithm

Our online (naive) algorithm
0 ≤ t < 0.1, p ∈ R

0 ≤ t < 0.1, p ∈ R!" /x := 0start

0.1 ≤ t < 0.4, p ∈ Rv" , x = p!"v"$3!" /x := 0start$v"

3↓t↓ ↓t!" !# v # !"v"

Our online(naive)algorithm
0 0.1 0.4
0.7 1.0
3.5 t!" !# v # !"v"

0 0.1 0.4 0.7 1.0

3.5 t

Our online (naive) algorithmM. Waga (NII)

M. Waga (NII)

10110.4 ≤ t < 0.7, p ∈ R

startv" , x = p!"!" /x := 0v" , x = p!"v"$0.7 ≤ t < 1.0, p ∈ R

3start↓t

0.7 ≤ t < 1.0, p ∈ R!" /x := 00.7 ≤ t < 1.0,p = 2.5v" , x = p!"↓↓t

FOUND!!
0.7 ≤ t < 1.0,3.5 < t′p =2.5v"$↓↓t′!" !# v # !"v"!" !# v # !"v"

0 0.1 0.4 0.7 1.0

3.5 t

0 0.1 0.4 0.7 1.0

3.5 t

13

12

3

M. Waga (NII)

M. Waga (NII)

Can we skip some of them?

(Usually) Yes!! by skipping from string matching
17

M. Waga (NII)

Idea of Skipping from String Matching•For each length n ∈ N, check if
Over-approx. of the read
timed word∩ n-shift + accepted timed words = ∅before the matching trials.
• Emptyno need to try n-shift•

Over-approx. using location l ∈ L (finite)• In PTA, we also use param. val. v: P → R• Infinite but represented by convex polyhedra
18M. Waga (NII)Skipping from Non-Parametricto Parametric
Skipping for TA [Waga+, FORMATS’17]
For each l ∈ L, n ∈ N, if L(Al)・T(Σ) ∩ Tn(Σ)・L(A) = ∅Over-approx. of the read
timed word

n-shift + accepted timed words(Parametric) Skipping for PTA [Contribution, Alg. 2]
For each l ∈ L, v: P → R n ∈ N, if there is v′: P → R s.t.
L(v(Al))・T(Σ) ∩ Tn(Σ)・L(v′(A)) = ∅Over-approx. of the read timed
word for the given param. val. v

n-shift + accepted timed words
for some param. val. v′
M. Waga (NII)
19

Skipping from Non-Parametricto Parametric
Skipping for TA [Waga+, FORMATS’17]
For each l ∈ L, n ∈ N, if L(Al)・T(Σ) ∩ Tn(Σ)・L(A) = ∅Over-approx. of the readtimed wordn-shift + accepted timed words(Parametric) Skipping for PTA [Contribution, Alg. 2]For each l ∈ L, v: P → R n ∈ N, if there is v′: P → R s.t.
RuntimeOverhead!!

L(v(Al))・T(Σ) ∩ Tn(Σ)・L(v′(A)) = ∅Over-approx. of the read timed
word for the given param. val. v

n-shift + accepted timed words
for some param. val. v′
M. Waga (NII)
19

Skipping with Less Overhead(Parametric) Skipping for PTA [Contribution, Alg. 2]
For each l ∈ L, v: P → R n ∈ N, if there is v′: P → R s.t.
More overhead
better approx.

L(v(Al))・T(Σ) ∩ Tn(Σ)・L(v′(A)) = ∅Over-approx. of the read timed
word for the given param. val. v

n-shift + accepted timed words
for some param. val. v′

Trade oﬀ!!

(Non-Parametric) Skipping for PTA [Contribution, Alg. 3]
For each l ∈ L, n ∈ N, if there is v, v′: P → R s.t.
Less overhead
worse approx.

L(v(Al))・T(Σ) ∩ Tn(Σ)・L(v′(A)) = ∅Over-approx. of the read timed
word for some param. val. v

n-shift + accepted timed words
for some param. val. v′
M. Waga (NII)
20Outline•

Motivation + Introduction•

Technical Part••

The parametric timed pattern matching problem•

Naive algorithm for Parametric TPM [Alg. 1]•Skipping optimization for Parametric TPM•

Parametric Skipping Algorithm [Alg. 2]•

Non-Parametric Skipping Algorithm [Alg. 3]

Experiment
21

M. Waga (NII)RQ: Which is the fastest
algorithm?
Contribution[André, Hasuo, & Waga, ICECCS’18]•

Probably, IMITATOR-based is not very fast••

Algorithms• Naive• Parametric Skip
• Non-Parametric Skip
• IMITATOR-basedit solves more general problem (model checking)Param. Skip vs. Non-Param. Skip•

Better over-approx. vs. Less Overhead
22M. Waga (NII)Environment of Experiment•

Amazon EC2 c4.large instance•

2.9 GHz Intel Xeon E5-2666 v3, 2 vCPUs, 3.75 GiB RAM•

Ubuntu 18.04 LTS (64 bit)

•GCC 7.3.0 with optimization flag -O3•

Used 4 benchmarks••

Automotive: Accel, Gear
Performance forextreme inputs

Toy: Blowup, OnlyTiming
23

M. Waga (NII)Comparison with IMITATOR
Table 2: Execution time for Gear [s]|w|No Skip1467
28374595
5839
7301
60x 8995faster 10315
11831
13183
14657

0.04
0.07250.124
0.15850.201
0.241
0.28150.322
0.3505
0.392

Non-Param. Param.
IMITATOR
Skip
Skip
0.05
0.0805
0.13
0.156
0.193
0.23150.269
0.301
0.3245
0.361

0.05
0.09
0.14050.17
0.21150.25050.2875
0.325
0.353
0.395

1.781
3.319
5.512
7.132
8.909
10.76812.77814.72416.45318.319

Table 3: Execution time for Accel [s]|w|

No Skip

2559
4894
7799
10045
12531
15375
17688
20299
22691
25137

0.03
0.06050.10050.13
0.1610.1985
0.22650.261
0.288
0.3205

Non-Param. Param.
IMITATOR
Skip
Skip
0.05150.0605
0.071
0.08
0.09
0.10050.10950.115
0.121
0.13150.06
0.0705
0.08
0.09
0.1
0.113
0.12150.1325
0.143
0.159

2.332
4.663
7.532
9.731
12.503
15.58317.75421.04023.04425.815200x
fasterTable 4: Execution time for Blowup [s] Table 5: Execution time for OnlyTiming [s]|w|

No Skip

2000
4000
6000
8000
10000

66.75
267.795
601.335
1081.421678.15

Non-Param. Param.
Skip
Skip
68.0125
271.642611.7821081.25
1688.22IMITATOR

67.9735 OutOfMemory
269.084 OutOfMemory
607.58 OutOfMemory1079 OutOfMemory
1694.53 OutOfMemoryout of memory!!
0.4|w| No Skip
1000 0.0995
2000 0.191
3000 0.2905
4000 0.3905
5000 0.488
6000 0.588
24

Non-Param. Param.
IMITATOR
Skip
Skip
0.13050.23
0.32650.426
0.52250.6235

0.11
0.191
0.273
0.35250.4325
0.517

1.690
3.518
5.499
7.396
9.123
11.00520x
fasterM. Waga (NII)
0.35

14657

0.392

0.361

0.395

18.31925137 0.3205

0.13150.15925.815

Comparison among ours
(Accel & Gear)

Table 4: Execution time for Blowup [s] Table 5: Execution time for OnlyTiming [s]No Skip

2000
4000
6000
8000
10000

66.75
267.795
601.335
1081.421678.15

Non-Param. Param.
Skip
Skip
68.0125
271.642611.7821081.25
1688.22IMITATOR

67.9735 OutOfMemory
269.084 OutOfMemory
607.58 OutOfMemory1079 OutOfMemory
1694.53 OutOfMemory

Execution Time [s]

Accel
0.4
0.35
0.3
0.25
0.2
0.15
0.1
0.05
01800
1600
1400
1200
1000
800
600
400
2000|w| No Skip

1000 0.0995
2000 0.191
3000 0.2905
4000 0.3905
5000 0.488
6000 0.588

No Skip
Parametric Skip
Non-Parametric Skip

00.35

Execution Time [s]

|w|

0.25

Gear

1.690
3.518
5.499
7.396
9.123
11.005

0.15
0.1
0.05
000.7

Execution Time [s]

0.11
0.191
0.273
0.35250.43250.517

0.2

50 100 150 200 250
Number of Events [⇥100]

300

No Skip
Parametric Skip
Non-Parametric Skip

0.6

• No Skip has the steepest slope
Execution Time [s]0.13050.23
0.32650.426
0.52250.6235No Skip
Parametric Skip
Non-Parametric Skip

0.3

20 40 60 80 100 120 140 160
Number of Events [⇥100]
No Skip
Parametric Skip
Non-Parametric Skip

Non-Param. Param.
IMITATORSkip
Skipworst scalability

0.50.4• Parametric Skip is slower than Non-Parametric
Skip dueto the overhead
20 30 40 50 60 70 80 90 100 25

0.3
0.2
0.1
010203040

M. Waga (NII)

5060

0.4
0.35
0.3
0.25
0.2
0.15
0.1
0.05
00.35

No Skip
Parametric Skip
Non-Parametric Skip

No Skip
Parametric Skip
Non-Parametric Skip

1800
1600
1400
1200
1000
800
600
40020000Execution Time [s]

0.25

0.2

0.150.10.05

020 40 60 80 100 120 140 160
Number of Events [⇥100]

Blowup00.7

No Skip
Parametric Skip
Non-Parametric Skip

Execution Time [s]Execution Time [s]Execution Time [s]Comparison among ours
(Blowup & OnlyTiming)
0.3

OnlyTiming

300

No Skip
Parametric Skip
Non-Parametric Skip

0.6
0.5
0.4
0.3
0.2
0.1
020 30 40 50 60 70 80 90 100
Number of Events [⇥100]

50 100 150 200 250
Number of Events [⇥100]

1020304050
Number of Events [⇥100]

60

Fig. 4: Execution time for the benchmarks with parameters which MONAA cannot• Blowup:
Skipping does not help muchhandle: Gear (above left), Accel (above right), Blowup (below left), and• Exponential
OnlyTiming (belowright) vs. constant speed up by skipping
blowup• OnlyTiming: No Skip has the steepest slope

worst scalability

Parametric Skip is the fastest due to the better over-approx.
26

M. Waga (NII)Conclusion•

Give a specialized alg. for param. timed pattern matching•

Optimized the algorithm by skipping from string matching•

Our algorithms are much faster than the state-of-the-art(IMITATOR-based algorithm)•Param. vs. Non-Param. Skipping depends on the Autom.

27

M. Waga (NII)Future Works•

Hybrid of Parametric/Non-Parametric Skipping•

Maybe the best trade-off•

More expressive logic (e.g., FOL)

•Case study•

not only automotive domain but also medical
CPS or IoT (security)
28

M. Waga (NII)

Appendix

29

M. Waga (NII)Why Autom? not TL or RE?
Cons.
•

Difficult to write (and read?) for the end userPros.
•More straightforward online monitoring algorithm•

Optimization technique from untimed to timed•

TRE → TA, MITL → TA are possible
Easy 😃

e.g., Skipping in this talkNot easy…😟

•TA as common platform•

In our industrial collaboration, we use TRE → TA30

M. Waga (NII)