A Boyer-Moore Type
Algorithm forTimed Pattern Matching
Masaki Waga Takumi Akazaki Ichiro Hasuo
University of Tokyo
25 Aug 2016, FORMATS2016

M. Waga (UTokyo)

1Timed Pattern Matchingwith2
Boyer-Moore Type
Algorithm
M. Waga (UTokyo)

Timed Pattern MatchingwithBoyer-Moore Type
Algorithm
M. Waga (UTokyo)

Motivation
Logrunning

0

{

0.2

a

2.2b

a

0
0.2

1.2
a

2.5
2.2b

3.4
a

t

0
0.2

1.2
a

2.5
2.2b

3.4
a

t

0
0.2

1.2
a

2.5
2.2b

3.4
a

t

0

1.2

3.4

t

.. 2.5
.

a

b

a

1.2

2.5

3.4

t

monitoring
for failing

Timed pattern matching
can be used.
M. Waga (UTokyo)

Another Motivation

M. Waga (UTokyo)

Another Motivation
log with timestamp

0

a

b

a

1.2

2.5

3.4

t

M. Waga (UTokyo)

Another Motivation
pattern

log with timestamp

0

a

b

a

1.2

2.5

3.4

start

t

Send logs(activities)s0

a, 1 < x/x := 0

s1$, 1 < xs2Analyze logs withtimed pattern matching

M. Waga (UTokyo)

Another Motivation
pattern

log with timestamp

0

a

b

a

1.2

2.5

3.4

start

t

Send logs(activities)s0

a, 1 < x/x := 0

s1$, 1 < xs2Analyze logs withtimed pattern matching

Hit thejackpot!!

M. Waga (UTokyo)

Timed Pattern Matching
Input

timed automaton A

timed word w
a
0

1.2

b
2.5

a
3.4

Output0

Pattern

Target String(t, t ) w|(t,t0 ) 2 L(A)

t

start

0

0

a, 1 < x/x := 0s0$, 1 < x

s1

a

b

a

1.2

2.5

3.4

a

$

1.2

t

t0

s2

t

trimmedt

accepted by
start

s0

a, 1 < x/x := 0

s1$, 1 < xs2

M. Waga (UTokyo)

Timed Pattern Matching
Input

timed automaton A

timed word w
a
0

1.2

b
2.5

a
3.4

Output0

Pattern

Target String(t, t ) w|(t,t0 ) 2 L(A)

t

start

s0

a, 1 < x/x := 0

s1$, 1 < xs2

signal and timed regularexpression in [Ulus et al., 2014]

M. Waga (UTokyo)

Timed Pattern Matching
Input

timed automaton A

timed word w
a
0

1.2

A specification of faults

A log of a system

b
2.5

a
3.4

Output

t

start

s0

a, 1 < x/x := 0

s1$, 1 < xs2

The set ofintervals when faults aredetected

0(t, t ) w|(t,t0 ) 2 L(A)M. Waga (UTokyo)

Timed Pattern MatchingwithBoyer-Moore type
Algorithm
M. Waga (UTokyo)

TargetStringMatching

Pattern

Algorithms•NaiveStringStringPattern
Matching

StringRegularLanguage•NaiveTimed
Pattern
Matching

Timed
Timed
Word Automaton•Naive•Boyer-Moore•Boyer-Moore•Boyer-Moore

Contribution
M. Waga (UTokyo)

String Matching
Input●

Target String

Strings str : HERE_IS_A_SIMPLE_EXAMPLE
pat : EXAMPLE

OutputPattern{(i, j) | str (i, j) = pat} = {(18, 24)}

123456789012345678901234
HERE_IS_A_SIMPLE_EXAMPLE
EXAMPLE
M. Waga (UTokyo)

Naive Algorithm for
String Matching
HERE_IS_A_SIMPLE_EXAMPLE
EXAMPLE

From http://www.cs.utexas.edu/users/moore/best-ideas/string-searching/fstrposexample.html
M. Waga (UTokyo)

Naive Algorithm for
String Matching
HERE_IS_A_SIMPLE_EXAMPLE✗
EXAMPLE

From http://www.cs.utexas.edu/users/moore/best-ideas/string-searching/fstrposexample.html
M. Waga (UTokyo)

Naive Algorithm for
String Matching
HERE_IS_A_SIMPLE_EXAMPLE
EXAMPLE
EXAMPLE

From http://www.cs.utexas.edu/users/moore/best-ideas/string-searching/fstrposexample.html
M. Waga (UTokyo)

Naive Algorithm for
String Matching
HERE_IS_A_SIMPLE_EXAMPLE
EXAMPLE
EXAMPLE

From http://www.cs.utexas.edu/users/moore/best-ideas/string-searching/fstrposexample.html
M. Waga (UTokyo)

Naive Algorithm for
String Matching
HERE_IS_A_SIMPLE_EXAMPLE✗
EXAMPLE
EXAMPLE

From http://www.cs.utexas.edu/users/moore/best-ideas/string-searching/fstrposexample.html
M. Waga (UTokyo)

Naive Algorithm for
String Matching
HERE_IS_A_SIMPLE_EXAMPLE
EXAMPLE
EXAMPLE
EXAMPLE

From http://www.cs.utexas.edu/users/moore/best-ideas/string-searching/fstrposexample.html
M. Waga (UTokyo)

Naive Algorithm for
String Matching
HERE_IS_A_SIMPLE_EXAMPLE✗
EXAMPLE
EXAMPLE
EXAMPLE

From http://www.cs.utexas.edu/users/moore/best-ideas/string-searching/fstrposexample.html
M. Waga (UTokyo)

Naive Algorithm for
String Matching
HERE_IS_A_SIMPLE_EXAMPLE
EXAMPLE
EXAMPLE
EXAMPLE
EXAMPLE

From http://www.cs.utexas.edu/users/moore/best-ideas/string-searching/fstrposexample.html
M. Waga (UTokyo)

Naive Algorithm for
String Matching
HERE_IS_A_SIMPLE_EXAMPLE
EXAMPLE Found!
EXAMPLE
EXAMPLE
EXAMPLE
EXAMPLE⁝
EXAMPLE
From http://www.cs.utexas.edu/users/moore/best-ideas/string-searching/fstrposexample.html
M. Waga (UTokyo)

The Boyer-Moore Algorithm[Boyer & Moore, Commun. ACM '77]•

Optimisation by skipping characters•

SkipValue can be computed beforehand.
FiniteSkipValue : (⌃ ⇥ |pat|) ! Z 0
M. Waga (UTokyo)

The Boyer-Moore Algorithm[Boyer & Moore, Commun. ACM '77]
HERE_IS_A_SIMPLE_EXAMPLE
EXAMPLE

From http://www.cs.utexas.edu/users/moore/best-ideas/string-searching/fstrposexample.html
M. Waga (UTokyo)

The Boyer-Moore Algorithm[Boyer & Moore, Commun. ACM '77]
HERE_IS_A_SIMPLE_EXAMPLE✗
EXAMPLE

From http://www.cs.utexas.edu/users/moore/best-ideas/string-searching/fstrposexample.html
M. Waga (UTokyo)

The Boyer-Moore Algorithm[Boyer & Moore, Commun. ACM '77]
HERE_IS_A_SIMPLE_EXAMPLE✗
EXAMPLE“S” does not appear
in the pattern(EXAMPLE)

From http://www.cs.utexas.edu/users/moore/best-ideas/string-searching/fstrposexample.html
M. Waga (UTokyo)

The Boyer-Moore Algorithm[Boyer & Moore, Commun. ACM '77]
HERE_IS_A_SIMPLE_EXAMPLE✗
EXAMPLE
EXAMPLE“S” does not appear
in the pattern(EXAMPLE)

From http://www.cs.utexas.edu/users/moore/best-ideas/string-searching/fstrposexample.html
M. Waga (UTokyo)

The Boyer-Moore Algorithm[Boyer & Moore, Commun. ACM '77]
HERE_IS_A_SIMPLE_EXAMPLE✗✗
EXAMPLE
EXAMPLE“S” does not appear
in the pattern(EXAMPLE)

From http://www.cs.utexas.edu/users/moore/best-ideas/string-searching/fstrposexample.html
M. Waga (UTokyo)

The Boyer-Moore Algorithm[Boyer & Moore, Commun. ACM '77]
HERE_IS_A_SIMPLE_EXAMPLE✗✗
EXAMPLE
EXAMPLE“S” does not appear
in the pattern(EXAMPLE)

Same!
“P” appears here

From http://www.cs.utexas.edu/users/moore/best-ideas/string-searching/fstrposexample.html
M. Waga (UTokyo)

The Boyer-Moore Algorithm[Boyer & Moore, Commun. ACM '77]
HERE_IS_A_SIMPLE_EXAMPLE✗✗
EXAMPLE
EXAMPLE
EXAMPLE“S” does not appear
in the pattern(EXAMPLE)

Same!
“P” appears here

From http://www.cs.utexas.edu/users/moore/best-ideas/string-searching/fstrposexample.html
M. Waga (UTokyo)

The Boyer-Moore Algorithm[Boyer & Moore, Commun. ACM '77]
HERE_IS_A_SIMPLE_EXAMPLE✗✗
EXAMPLE
EXAMPLE
EXAMPLE“S” does not appear
in the pattern(EXAMPLE)

Same!
“P” appears here

From http://www.cs.utexas.edu/users/moore/best-ideas/string-searching/fstrposexample.html
M. Waga (UTokyo)

The Boyer-Moore Algorithm[Boyer & Moore, Commun. ACM '77]
HERE_IS_A_SIMPLE_EXAMPLE✗✗
EXAMPLE
EXAMPLE
EXAMPLE“S” does not appear
in the pattern(EXAMPLE)

Same!
“P” appears here

From http://www.cs.utexas.edu/users/moore/best-ideas/string-searching/fstrposexample.html
M. Waga (UTokyo)

The Boyer-Moore Algorithm[Boyer & Moore, Commun. ACM '77]
HERE_IS_A_SIMPLE_EXAMPLE✗✗
EXAMPLE
EXAMPLE
EXAMPLE“S” does not appear
in the pattern(EXAMPLE)

Same!
“P” appears here

From http://www.cs.utexas.edu/users/moore/best-ideas/string-searching/fstrposexample.html
M. Waga (UTokyo)

The Boyer-Moore Algorithm[Boyer & Moore, Commun. ACM '77]
HERE_IS_A_SIMPLE_EXAMPLE✗✗
EXAMPLE
EXAMPLE
EXAMPLE“S” does not appear
in the pattern(EXAMPLE)

Same!
“P” appears here

From http://www.cs.utexas.edu/users/moore/best-ideas/string-searching/fstrposexample.html
M. Waga (UTokyo)

The Boyer-Moore Algorithm[Boyer & Moore, Commun. ACM '77]
HERE_IS_A_SIMPLE_EXAMPLE✗ ✗✗EXAMPLE
EXAMPLE
EXAMPLE“S” does not appear
in the pattern(EXAMPLE)

Same!
“P” appears here

From http://www.cs.utexas.edu/users/moore/best-ideas/string-searching/fstrposexample.html
M. Waga (UTokyo)

The Boyer-Moore Algorithm[Boyer & Moore, Commun. ACM '77]
HERE_IS_A_SIMPLE_EXAMPLE✗ ✗✗EXAMPLE“I” does not
EXAMPLE
appear in the pattern
EXAMPLE“S” does not appear
in the pattern
EXAMPLE(EXAMPLE)

Same!
“P” appears here

From http://www.cs.utexas.edu/users/moore/best-ideas/string-searching/fstrposexample.html
M. Waga(UTokyo)

The Boyer-Moore Algorithm[Boyer & Moore, Commun. ACM '77]
HERE_IS_A_SIMPLE_EXAMPLE✗ ✗✗EXAMPLE“I” does not
EXAMPLE
appear in the pattern
EXAMPLE“S” does not appear
in better!
the pattern
We can do
EXAMPLE(EXAMPLE)
EXAMPLESame!
“P” appears here

From http://www.cs.utexas.edu/users/moore/best-ideas/string-searching/fstrposexample.html
M. Waga(UTokyo)

The Boyer-Moore Algorithm[Boyer & Moore, Commun. ACM '77]
HERE_IS_A_SIMPLE_EXAMPLE✗ ✗✗EXAMPLE“I” does not
EXAMPLE
appear in the pattern
EXAMPLE“S” does not appear
in better!
the pattern
We can do
EXAMPLE(EXAMPLE)
Given the previous
match EXAMPLE,
EXAMPLE
Same!
EXAMPLE“P” appears here

EXAMPLE✘
EXAMPLE✘
EXAMPLE✘
EXAMPLE✘
From
http://www.cs.utexas.edu/users/moore/best-ideas/string-searching/fstrposexample.html
EXAMPLE✘
M. Waga(UTokyo)
EXAMPLE ✔

The Boyer-Moore Algorithm[Boyer & Moore, Commun. ACM '77]
HERE_IS_A_SIMPLE_EXAMPLE✗ ✗✗EXAMPLE“I” does not
EXAMPLE
appear in the pattern
EXAMPLE“S” does not appear
in better!
the pattern
We can do
EXAMPLE(EXAMPLE)
Given the previous
match EXAMPLE,
EXAMPLE
Same!
EXAMPLE“P” appears here

EXAMPLE✘
EXAMPLE✘
EXAMPLE✘
EXAMPLE✘
From
http://www.cs.utexas.edu/users/moore/best-ideas/string-searching/fstrposexample.html
EXAMPLE✘
M. Waga(UTokyo)
EXAMPLE ✔

The Boyer-Moore Algorithm[Boyer & Moore, Commun. ACM '77]
HERE_IS_A_SIMPLE_EXAMPLE✗ ✗✗✗EXAMPLE“I” does not
EXAMPLE
appear in the pattern
EXAMPLE“S” does not appear
in better!
the pattern
We can do
EXAMPLE(EXAMPLE)
Given the previous
match EXAMPLE,
EXAMPLE
Same!
EXAMPLE“P” appears here

EXAMPLE✘
EXAMPLE✘
EXAMPLE✘
EXAMPLE✘
From
http://www.cs.utexas.edu/users/moore/best-ideas/string-searching/fstrposexample.html
EXAMPLE✘
M. Waga(UTokyo)
EXAMPLE ✔

The Boyer-Moore Algorithm[Boyer & Moore, Commun. ACM '77]
HERE_IS_A_SIMPLE_EXAMPLE✗ ✗✗✗EXAMPLE“I” does not
Same!
EXAMPLE
appear in the pattern
EXAMPLE“S” does not appear
in better!
the pattern
We can do
EXAMPLE(EXAMPLE)
Given the previous
match EXAMPLE,
EXAMPLE
Same!
EXAMPLE“P” appears here

“P” appears here
EXAMPLE✘
EXAMPLE✘
EXAMPLE✘
EXAMPLE✘
From
http://www.cs.utexas.edu/users/moore/best-ideas/string-searching/fstrposexample.html
EXAMPLE✘
M. Waga(UTokyo)
EXAMPLE ✔

The Boyer-Moore Algorithm[Boyer & Moore, Commun. ACM '77]
HERE_IS_A_SIMPLE_EXAMPLE✗ ✗✗✗EXAMPLE“I” does not
Same!
EXAMPLE
appear in the pattern
EXAMPLE“S” does not appear
in better!
the pattern
We can do
EXAMPLE(EXAMPLE)
Given the previous
match EXAMPLE,
EXAMPLE
Same!
EXAMPLE
EXAMPLE“P” appears here

“P” appears here
EXAMPLE✘
EXAMPLE✘
EXAMPLE✘
EXAMPLE✘
From
http://www.cs.utexas.edu/users/moore/best-ideas/string-searching/fstrposexample.html
EXAMPLE✘
M. Waga(UTokyo)
EXAMPLE ✔

The Boyer-Moore Algorithm[Boyer & Moore, Commun. ACM '77]
HERE_IS_A_SIMPLE_EXAMPLE✗ ✗✗✗EXAMPLE“I” does not
Same!
EXAMPLE
appear in the pattern
EXAMPLE“S” does not appear
in better!
the pattern
We can do
EXAMPLE(EXAMPLE)
Given the previous
match EXAMPLE,
EXAMPLE
Same!
EXAMPLE
EXAMPLE“P” appears here

“P” appears here
EXAMPLE✘
EXAMPLE✘
EXAMPLE✘
EXAMPLE✘
From
http://www.cs.utexas.edu/users/moore/best-ideas/string-searching/fstrposexample.html
EXAMPLE✘
M. Waga(UTokyo)
EXAMPLE ✔

The Boyer-Moore Algorithm[Boyer & Moore, Commun. ACM '77]
HERE_IS_A_SIMPLE_EXAMPLE✗ ✗✗✗EXAMPLE“I” does not
Same!
EXAMPLE
appear in the pattern
EXAMPLE“S” does not appear
in better!
the pattern
We can do
EXAMPLE(EXAMPLE)
Given the previous
match EXAMPLE,
EXAMPLE
Same!
EXAMPLE
EXAMPLE“P” appears here

“P” appears here
EXAMPLE✘
EXAMPLE✘
EXAMPLE✘
EXAMPLE✘
From
http://www.cs.utexas.edu/users/moore/best-ideas/string-searching/fstrposexample.html
EXAMPLE✘
M. Waga(UTokyo)
EXAMPLE ✔

The Boyer-Moore Algorithm[Boyer & Moore, Commun. ACM '77]
HERE_IS_A_SIMPLE_EXAMPLE✗ ✗✗✗EXAMPLE“I” does not
Same!
EXAMPLE
appear in the pattern
EXAMPLE“S” does not appear
in better!
the pattern
We can do
EXAMPLE(EXAMPLE)
Given the previous
match EXAMPLE,
EXAMPLE
Same!
EXAMPLE
EXAMPLE“P” appears here

“P” appears here
EXAMPLE✘
EXAMPLE✘
EXAMPLE✘
EXAMPLE✘
From
http://www.cs.utexas.edu/users/moore/best-ideas/string-searching/fstrposexample.html
EXAMPLE✘
M. Waga(UTokyo)
EXAMPLE ✔

The Boyer-Moore Algorithm[Boyer & Moore, Commun. ACM '77]
HERE_IS_A_SIMPLE_EXAMPLE✗ ✗✗✗EXAMPLE“I” does not
Same!
EXAMPLE
appear in the pattern
EXAMPLE“S” does not appear
in better!
the pattern
We can do
EXAMPLE(EXAMPLE)
Given the previous
match EXAMPLE,
EXAMPLE
Same!
EXAMPLE
EXAMPLE“P” appears here

“P” appears here
EXAMPLE✘
EXAMPLE✘
EXAMPLE✘
EXAMPLE✘
From
http://www.cs.utexas.edu/users/moore/best-ideas/string-searching/fstrposexample.html
EXAMPLE✘
M. Waga(UTokyo)
EXAMPLE ✔

The Boyer-Moore Algorithm[Boyer & Moore, Commun. ACM '77]
HERE_IS_A_SIMPLE_EXAMPLE✗ ✗✗✗EXAMPLE“I” does not
Same!
EXAMPLE
appear in the pattern
EXAMPLE“S” does not appear
in better!
the pattern
We can do
EXAMPLE(EXAMPLE)
Given the previous
match EXAMPLE,
EXAMPLE
Same!
EXAMPLE
EXAMPLE“P” appears here

“P” appears here
EXAMPLE✘
EXAMPLE✘
EXAMPLE✘
EXAMPLE✘
From
http://www.cs.utexas.edu/users/moore/best-ideas/string-searching/fstrposexample.html
EXAMPLE✘
M. Waga(UTokyo)
EXAMPLE ✔

The Boyer-Moore Algorithm[Boyer & Moore, Commun. ACM '77]
HERE_IS_A_SIMPLE_EXAMPLE✗ ✗✗✗EXAMPLE“I” does not
Same!
EXAMPLE
appear in the pattern
EXAMPLE“S” does not appear
in better!
the pattern
We can do
EXAMPLE(EXAMPLE)
Given the previous
match EXAMPLE,
EXAMPLE
Same!
EXAMPLE
EXAMPLE“P” appears here

“P” appears here
EXAMPLE✘
EXAMPLE✘
EXAMPLE✘
EXAMPLE✘
From
http://www.cs.utexas.edu/users/moore/best-ideas/string-searching/fstrposexample.html
EXAMPLE✘
M. Waga(UTokyo)
EXAMPLE ✔

The Boyer-Moore Algorithm[Boyer & Moore, Commun. ACM '77]
HERE_IS_A_SIMPLE_EXAMPLE✗ ✗✗✗EXAMPLE“I” does not
Same!
EXAMPLE
appear in the pattern
EXAMPLE“S” does not appear
in better!
the pattern
We can do
EXAMPLE(EXAMPLE)
Given the previous
match EXAMPLE,
EXAMPLE
Same!
EXAMPLE
EXAMPLE“P” appears here

“P” appears here
EXAMPLE✘Found!
EXAMPLE✘
EXAMPLE✘
EXAMPLE✘
From
http://www.cs.utexas.edu/users/moore/best-ideas/string-searching/fstrposexample.html
EXAMPLE✘
M. Waga(UTokyo)
EXAMPLE ✔

The Boyer-Moore Algorithm[Boyer & Moore, Commun. ACM '77]
HERE_IS_A_SIMPLE_EXAMPLE
Bottomline:✗ ✗✗✗Move the pattern by possibly
EXAMPLE
more than one.
“I” does not
Same!
EXAMPLE
appear in the pattern
EXAMPLE
Skip“S”
values:does not appear in
We can dothe
better!
EXAMPLE
pattern
We usetwo skipvalues.
Given
the previous
match
EXAMPLE,
EXAMPLE
Same!
EXAMPLE
EXAMPLE“P” appears here

“P” appears here
EXAMPLE✘Found!
EXAMPLE✘
EXAMPLE✘
EXAMPLE✘
From
http://www.cs.utexas.edu/users/moore/best-ideas/string-searching/fstrposexample.html
EXAMPLE✘
M. Waga(UTokyo)
EXAMPLE ✔

TargetStringMatching

Pattern

Algorithms•NaiveStringStringPattern
Matching

StringRegularLanguage•NaiveTimed
Pattern
Matching

Timed
Timed
Word Automaton•Naive•Boyer-Moore•Boyer-Moore•Boyer-Moore

Contribution
M. Waga (UTokyo)

Pattern Matching
Input

Target String●

String str : dbadcdc●

Regular Language L : dc*{ba|dc}

OutputPattern{(i, j) | str (i, j) 2 L} = {(1, 3), (4, 7)}
str (1, 3) = dba 2 L, str (4, 7) = dcd 2 L
M. Waga (UTokyo)

Naive Algorithm for
Pattern Matchingd b a d c d cd∈? L(dc*{ba|dc})

M. Waga (UTokyo)

Naive Algorithm for
Pattern Matchingd b a d c d cdd b∈? L(dc*{ba|dc})∈? L(dc*{ba|dc})

M. Waga (UTokyo)

Naive Algorithm for
Pattern Matchingd b a d c d cdFound!
d b
d b a✓∈? L(dc*{ba|dc})∈? L(dc*{ba|dc})∈? L(dc*{ba|dc})

M. Waga (UTokyo)

Naive Algorithm for
Pattern Matchingd b a d c d cdFound!
d b
d b a✓∈? L(dc*{ba|dc})∈? L(dc*{ba|dc})∈? L(dc*{ba|dc})⁝

d b a d c d c ∈? L(dc*{ba|dc})

M. Waga (UTokyo)

Naive Algorithm for
Pattern Matchingd b a d c d cdFound!
d b
d b a✓∈? L(dc*{ba|dc})∈? L(dc*{ba|dc})∈? L(dc*{ba|dc})⁝

d b a d c d c ∈? L(dc*{ba|dc})b∈? L(dc*{ba|dc})

M. Waga (UTokyo)

Naive Algorithm for
Pattern Matchingd b a d c d cdFound!
d b
d b a✓∈? L(dc*{ba|dc})∈? L(dc*{ba|dc})∈? L(dc*{ba|dc})⁝

d b a d c d c ∈? L(dc*{ba|dc})b∈? L(dc*{ba|dc})b a∈? L(dc*{ba|dc})

M. Waga (UTokyo)

Naive Algorithm for
Pattern Matchingd b a d c d cdFound!
d b
d b a✓∈? L(dc*{ba|dc})∈? L(dc*{ba|dc})∈? L(dc*{ba|dc})⁝

d b a d c d c ∈? L(dc*{ba|dc})b∈? L(dc*{ba|dc})b a∈? L(dc*{ba|dc})
Found!
⁝d c d c✓∈? L(dc*{ba|dc})
M. Waga (UTokyo)

The Boyer-Moore type Algorithm
for Pattern Matching[Watson & Watson, Sci. Comput. Program. '03]

d b a d c d ca
1. right to left b a
d b a✓

2. Skip by morethan 1!!

∈? L(dc*{ba|dc})∈? L(dc*{ba|dc})∈? L(dc*{ba|dc})d✗ ∈? L(dc*{ba|dc})c ∈? L(dc*{ba|dc})
d c ∈? L(dc*{ba|dc})
c d c ∈? L(dc*{ba|dc})
d c d c✓∈? L(dc*{ba|dc})
M. Waga (UTokyo)

The Boyer-Moore type Algorithm
for Pattern Matching[Watson & Watson, Sci. Comput. Program. '03]

d b a d c d ca
1. right to left b a
d b a✓∈? L(dc*{ba|dc})∈?c L(dc*{ba|dc})sba∈? L(dc*{ba|dc})
d
s
s
start
A= d
∈?s L(dc*{ba|dc})cc ∈? dL(dc*{ba|dc})s
d c ∈? L(dc*{ba|dc})
c d c ∈? L(dc*{ba|dc})
d c d c✓∈? L(dc*{ba|dc})
1

4

2. Skip by morethan 1!!

3

0

2

M. Waga (UTokyo)

The Boyer-Moore type Algorithm
for Pattern Matching[Watson & Watson, Sci. Comput. Program. '03]

d b a d c d ca
1. right to left b a
d b a✓∈? L(dc*{ba|dc})∈? L(dc*{ba|dc})∈? L(dc*{ba|dc})d∈? SimilarL(dc*{ba|dc})
to thecSkipValue∈? L(dc*{ba|dc})
in the Boyer2. Skip by mored Moorec ∈? algorithm
L(dc*{ba|dc})
for string
than 1!!
c d c ∈? L(dc*{ba|dc})
matching.
d c d c✓∈? L(dc*{ba|dc})
M. Waga (UTokyo)

The Boyer-Moore type Algorithm
for Pattern Matching[Watson & Watson, Sci. Comput. Program. '03]

For string matching:

FiniteSkipValue : (⌃ ⇥ |pat|) ! Z 0

For pattern matching:

Infinite!

SkipValue : ⌃ ⇥ sup |w| | w 2 L

We cannot
precompute
SkipValue!
!Z 0

M. Waga (UTokyo)

The Boyer-Moore type Algorithm
for Pattern Matching[Watson & Watson, Sci. Comput. Program. '03]

For string matching:

FiniteSkipValue : (⌃ ⇥ |pat|) ! Z 0

For pattern matching:

Infinite!

SkipValue : ⌃ ⇥ sup |w| | w 2 L

FiniteWe cannot
precompute
SkipValue!
!Z 0

SkipValue : ⌃ ⇥ {states of the pattern autom.} ! Z 0
M. Waga (UTokyo)

Timed Pattern MatchingwithBoyer-Moore type
Algorithm

Contribution
M. Waga (UTokyo)

Timed Word

Target[Alur & Dill,Theor. Comput. Sci. ’94] StringDef.
A timed word is( 1 , ⌧1 ), ( 2 , ⌧2 ), · · · , ( n , ⌧n )where 1 , 2 , · · · , n 2 ⌃ , and⌧1 , ⌧2 , · · · , ⌧n 2 R>0 such that
⌧1 < ⌧2 < · · · < ⌧n

a
0

1.2

b
2.5

a
3.4

t
M. Waga (UTokyo)

Timed Word Segment
Def. ( w|(t,t ) )

w=

2.8

0.8

0

0

w|(0.8,2.8) =

a

b

a

1.2

2.5

3.4

a

b

0 0.4

$

t

the terminal
character

1.7 2.0 t

M. Waga (UTokyo)

Timed Automata Pattern[Alur & Dill,Theor. Comput. Sci. '94]
guard

event

a, x > 1/x := 0

s1

reset
start

b, x > 1/x := 0s0a, x < 1s2

M. Waga (UTokyo)

Timed Pattern Matching
Input•

Target String

timed word

0

w
start

•

timed automaton A

Output0

Pattern{(t, t ) | t|(t,t0 ) 2 L(A)}

s0

a

b

a

1.2

2.5

3.4

a, 1 < x/x := 0(

s1$, 1 < x

s2

0.2

a

2.2b

a

0
0.2

1.2
a

2.5
2.2b

3.4
a

0
0.2

1.2
a

2.5
2.2b

3.4
a

0
0.2

1.2
a

2.5
2.2b

3.4
a

0

1.2

.. 2.5
.

t

3.4

)
t
t
t
t

M. Waga (UTokyo)

Timed Pattern MatchingEnd
points
(
)
t0

0.2

a

2.2b

a

0
0.2

1.2
a

2.5
2.2b

3.4
a

t

2

0
0.2

1.2
a

2.5
2.2b

3.4
a

t

1

0
0.2

1.2
a

2.5
2.2b

3.4
a

t

0

1.2

3.4

t

.. 2.5
.

0

1

2

t

Beginning points

Thm.
The answer of timed pattern matching for the spec.
written in timed automaton can be represented by finite
union of intervals of t, t0 , t0t
M. Waga (UTokyo)

TargetStringMatching

Pattern

Algorithms•NaiveStringStringPattern
Matching

StringRegularLanguage•NaiveTimed
Pattern
Matching

Timed
Timed
Word Automaton•Naive•Boyer-Moore•Boyer-Moore•Boyer-Moore

Contribution
M. Waga (UTokyo)

Naive Algorithm forTimed Pattern Matching
a
0

1.2

b
2.5

a
3.4

t

L(A)

M. Waga (UTokyo)

Naive Algorithm forTimed Pattern Matching
a
0

1.2

b
2.5

a
3.4

t

L(A)

M. Waga (UTokyo)

Naive Algorithm forTimed Pattern Matching
a
0

b

1.2

2.5

a
3.4

t

L(A)
L(A)

M. Waga (UTokyo)

Naive Algorithm forTimed Pattern Matching
a
0

b

1.2

a

2.5

3.4

t

L(A)
L(A)
L(A)
M. Waga (UTokyo)

Naive Algorithm forTimed Pattern Matching
a
0

b

1.2

2.5

a
3.4

t

L(A)
L(A)
L(A)
M. Waga (UTokyo)

Naive Algorithm forTimed Pattern Matching
Assume any point is OK

a
0

1.2

b

😐

start

3.4

$, x > 1

Constraint
0  t < 1.2

s0

b,

t

2.5

s1
a, x < 1

a

s3

$,

M. Waga (UTokyo)

Naive Algorithm forTimed Pattern Matching
read

a
0

1.2

b

😐

start

3.4

$, x > 1

Constraint
0  t < 1.2

s0

b,

t

2.5

s1
a, x < 1

a

s3

$,

M. Waga (UTokyo)

Naive Algorithm forTimed Pattern Matching
narrow the constraint

a
0

1.2

😐

b
2.5

s1

satisfya, x < 1😐

start$, x > 1

s0

b,

a
3.4

t

Constraint
0.2 < t < 1.2

s3$,

M. Waga (UTokyo)

Naive Algorithm forTimed Pattern Matching
try to insert $ (terminate character)

a
0

1.2

😐

b
2.5

s1
a, x < 1😐

start$, x > 1

s0

b,

s3

$,

a
3.4

t

Constraints
8><0.2 < t < 1.2
1.2 < t0  2.5>:
1 < x = t0 t

M. Waga (UTokyo)

Naive Algorithm forTimed Pattern Matching
a
0

1.2

😐

b

a

2.5

3.4

t

s1
a, x < 1😐

start$, x > 1

s0

b,

s3

$,

🙂

Answer8><0.2 < t < 1.2
0
1.2 < t  2.5
>
:
0
1<t
t

M. Waga (UTokyo)

Boyer-Moore Type Algorithm
for Timed Pattern Matching
a
0

b

1.2

a

2.5

t

3.4

left to right
L(A)
L(A)

Skip by morethan 1!!

M. Waga (UTokyo)

Boyer-Moore Type Algorithm
for Timed Pattern Matching
a
0

b

1.2

a

2.5

t

3.4

left to right
L(A)Similar to the
SkipValue in the L(A)Boyer-Moore typealgorithm for patternmatching.

Skip by morethan 1!!

M. Waga (UTokyo)

Boyer-Moore Type Algorithm
for Timed Pattern Matching
FiniteSkipValue : ⌃ ⇥ {states of the pattern autom.} ! Z 0

String Matching🙂

EXAMPLE

Difficulty: Uncountably many
comparison of
timed words.

EXAMPLE
EXAMPLE
EXAMPLE
EXAMPLE
EXAMPLE
EXAMPLE

✘
✘
✘
✘
✘
✔

Idea: Representation by a run of a region automaton
M. Waga (UTokyo)

Boyer-Moore Type Algorithm
for Timed Pattern Matching
Timed
Pattern Matching
Finiteab a )(0 0.6 1.5 2.1 taba
SkipValue : ⌃ ⇥ {states of the pattern autom.}!Z 0😐

0 0.5 1.3 2.0 t..
.

String Matchinga b()

EXAMPLE

0 0.6 1.1
a b
0 0.5 1.0

Difficulty: Uncountably many
comparison of
timed words.

🙂
t

7

t

..
EXAMPLE✘.
EXAMPLE✘ab(
EXAMPLE 0 0.6 1.1✘
EXAMPLE a b ✘EXAMPLE0 0.5 1.0.. ✘EXAMPLE . ✔

t
t

)

3

Idea: Representation by a run of a region automaton
M. Waga (UTokyo)

Region Automata[Alur & Dill,Theor. Comput. Sci. '94]

Timed Automaton

Region Automaton

start

$

s1
0<x<1

s1
a, x < 1$, x > 1

s0

s3

s3
x>1

a

start

s0
x=0
b

b,
x = 1/x := 0

s2

$,
x<1

States ⇥ ClockValues
is infinite

s2
x=0

$

s3
0<x<1

Regions = ClockValues/ ⇠RegionStates = States ⇥ Regions
is finite!
M. Waga (UTokyo)

Skip Value

over approx. of
acceptingwords (shifted)

(

a

b

0 0.6
a

b

0 0.6
a

1.5
b

0 0.5 1.3
a
0

..
.

0.7

) (

2.0 t
t
t

b

2.0 t

\

over approx.
of read words compareab

0 0.6 1.5
a b
0 0.6 1.1
a b
0 0.5 1.0
a b
0

..
.

0.7 1.2

)
t
t
t
t

?
=;

start

start

s1
x=0

a

s2
x<1

b

s1
x=0

start

s3
x>2

a

s2
x=0

b

s3
0<x<1

(s1 , s3 )x = 0, x0 > 2a(s2 , s2 )x < 1, x0 = 0b(s1 , s3 )x = 0, 0 < x0 < 1

is a run of R(A ⇥ A) ?
M. Waga (UTokyo)

Experiments●

Environment: MacBook Air Core i7-2677M
RAM 3.7GB●

Implemented in C++●

Show two cases out of five cases in the paper●

Used engine model of Simulink in Case1●

Case2 is taken from [Ulus et al., FORMATS '14]
M. Waga (UTokyo)

Case 1•

Close to our target application

w: sequential binarized (high/low) logs of the torqueof an engine simulation in Simulink

A = starts0

low , true
/x := 0

s1

high,
0<x<1

high,
0<x<1

s2

Match when thetorque is too high fora long time.
s3
high,
0<x<1

high, trues7$, true

s6

high,
1<x

s5

high,
0<x<1

s4

M. Waga (UTokyo)

Case 1300

naive
Boyer-Moore (without pre-processing)Boyer-Moore (with pre-processing)

Execution Time [ms]

250

about
twice faster

200

150

100

preprocessing is required
only once per pattern

50

0

0

50

100

150

200

250

300

350

400

Number of Events [⇥10000]

450

500

● Used the average of the 10 times run.
M. Waga (UTokyo)

Case 2●The cost of the precomputation is high.

●Taken from [Ulus et al., FORMATS ’14]

w : on/off switching of two states
p and q following geometrics4
distribution$, 80  t

A = start

R(A ⇥ A) has manystates. ( ⇡ 1014 )¬p, 0 < x  10/x := 0s0s1p, trueq, true¬q, 0 < y  10/y := 0q, true¬q, 0 < y  10/y := 0p, trues2

s3¬p, 0 < x  10/x := 0

M. Waga (UTokyo)

Case 2●The precomputation in our Boyer-Moore typealgorithm did not finish due to the lack of RAM.

●The number of regions increases
exponentially.
Q(bounded by |C|! · 2|C| · x2C (2cx + 2) )●●Using a zone automaton instead of a region
automaton may be a solution.

The naive algorithm worked well because it does
not use region automata.
M. Waga (UTokyo)

Conclusions andFuture Work●

Solved the timed pattern matching problem with
our Boyer-Moore type algorithm.
− About twice faster than the naive one at most
− Its space complexity is too large for someinstances●

Reduce the space complexity of its
precomputation− Using a zone automaton in place of a region

automaton?
M. Waga (UTokyo)