Moore-Machine Filtering
for Timed and Untimed
Pattern Matching
Masaki Waga1 and Ichiro Hasuo1
National Institute of Informatics1
2 Oct. 2018, EMSOFT 2018
The authors are supported by JST ERATO HASUO Metamathematics for Systems Design Project (No. JPMJER1603),
and JSPS Grants-in-Aid No. 15KT0012 & 18J22498.

1

M. Waga (NII)

IoT / Embedded Systems
Connected via Network
Network

ServerEmbedded Systems

2

M. Waga (NII)

IoT / Embedded Systems
Connected via Network
Network

ServerEmbedded Systems
Monitoring!!

2M. Waga (NII)

Timed Pattern Matching[Ulus et al., FORMATS’14]

Input
•

Time-series data (Logs of a car/ a robot)
e.g., The gear of a car: high at 0.1s, low at 0.2s, …

•

Real-time spec. (Spec. useful for debugging)e.g., Frequent gear change of a car

Output•

The intervals where the spec. is satisfied in the log
e.g., Frequent gear change in 0.2s-0.7s
3M. Waga (NII)

Remote Monitoringhigh 0.1
low 0.2
low 0.5：

SensorSpec.

Log(0.2, 0.5)
(0.23, 0.55)(0.31, 0.6)：

feedback
Monitor

4M. Waga (NII)

Remote Monitoringhigh 0.1low 0.2
low 0.5：

SensorSpec.

Log(0.2, 0.5)
(0.23, 0.55)(0.31, 0.6)：

feedback
Monitor• Huge data size
• Limited network capacity

Reduce the size!!

4

M. Waga (NII)

Remote Monitoringhigh 0.1
low 0.2
low 0.5：

SensorSpec.

Log(0.2, 0.5)
(0.23, 0.55)(0.31, 0.6)：

feedback
Monitor• Huge data size
• Limited network capacity• Timed Pattern Matching

Reduce the size!!

• Assumption: Too Heavyfor embedded systems

4

M. Waga (NII)Naive Remote Monitor
high 0.1low 0.2
low 0.5：

SensorSpec.

Log(0.2, 0.5)
(0.23, 0.55)(0.31, 0.6)：

feedback
MonitorContribution: Filter for Remote Monitor
Removed!!

SensorFilterhigh 0.1
low 0.2
low 0.5
：

Log
5

Spec.

Same Result(soundness)(0.2, 0.5)
(0.23, 0.55)(0.31, 0.6)：

feedback
Monitor
M. Waga (NII)Naive Remote Monitor
high 0.1
low 0.2
low 0.5：

SensorSpec.

Log(0.2, 0.5)
(0.23, 0.55)(0.31, 0.6)：

feedback
MonitorContribution: Filter for Remote Monitor
Removed!!

SensorFilterhigh 0.1
low 0.2
low 0.5：

Log

Moore machine
5Spec.

Same Result(soundness)(0.2, 0.5)
(0.23, 0.55)(0.31, 0.6)：

feedback
Monitor
M. Waga (NII)Moore Machine
DFA + state-dependent output
Input
Output• Efficient (linear time)• Hardware implementable
6

M. Waga (NII)

Contribution
high 0.1
low 0.2
low 0.5：

high 0.1
low 0.2
low 0.5：

SensorSpec.

FilterMonitor

Moore machine filter from NFA / TA
• Soundness (the result is the same)• Implementation & experiment• Data size ≈ 1/100 — 1/2•

7

M. Waga (NII)Related Works
Timed Pattern Matching• Offline Algorithm• [Ulus+, FORMATS’14]• Online Algorithm• [Ulus+, TACAS’16]• Optimization (skipping)• [Waga+, FORMATS’16]• [Waga+, FORMATS’17]

Filtering for Pattern Matching• Multiple string• [Salmela+, JEA'06]• [Kandhan+, PVLDB'10]• regular expression• (different problem)• [Liu+, ACNS’12]：This Work
8M. Waga (NII)Spec.

OutlineTheoretical preparation

SensorFilterMonitor• Moore Machine Filter for Untimed Pattern Matching

•

•

•

Spec.: NFA A•

Log: word (w ∈ Σ*)

Main Problem

Moore Machine Filter for Timed Pattern Matching•

Spec.: TA A•

Log: timed word (w ∈ (Σ × R>0)*)

Experiments (timed)
9M. Waga (NII)

(Untimed) Pattern Matching
Input

Log

Outputindices・Word w ∈ Σ*・NFA A

Match(w, A) = {(i,j) | w(i,j) ∈ L(A)}Spec.

Examplew = dbadcdc
L(A) = dc*{ba|dc}

w(1,3) = dba ∈ L(A)Match(w, A)= {(1,3), (4,7)}10

w(4,7) = dcdc ∈ L(A)M. Waga (NII)

Idea: Filtering by Masking
Mask subwords not matching (ab|cd)d*0w = acddaSensor

w =⊥cdd⊥

FilterMonitor
Masked!!

GoalConstruct a sound and efficient filterby a Moore machine
DFA + state-dependent output
11M. Waga (NII)Overview of Filteringw
Input Word

a1

a2

a3

a4a5

⊥

⊥

Queue Size N = 2⊥⊥

read char.

✘✘mask / pass

Output Word

12

M. Waga (NII)Overview of Filteringw
Input Word

a1a2

a3

a4a5

⊥

⊥

Queue⊥⊥✘✘

Output Word

13

M. Waga (NII)Overview of Filteringw
a1

Input Word

a2a3a4a5

⊥

⊥

Queue

Output Word

⊥⊥✘✘

⊥

Pop the queue
and write

13

M. Waga (NII)Overview of Filteringw
a1

Input Word

a2a3a4a5

⊥

⊥

Queue

Output Word

⊥

a⊥1

✘

✘

Read and push⊥

Pop the queueand write

13

M. Waga (NII)Overview of Filteringw
Input Word

a1a2a3a4

⊥

a5

⊥

Queue

Output Word

⊥a12

✘

✘

⊥

14

M. Waga (NII)Overview of Filteringw
Input Word

a1a2a3a4

⊥

a5

⊥

Queue

Output Word

⊥

⊥a12

✘

✘⊥
Pop the queueand write
14

M. Waga (NII)Overview of Filteringw
Input Word

a1a2a3a4

⊥

a5

⊥

Queue

Output Word

⊥

a⊥1a2

✘
✓✘

Read and pu✘→✓⊥
Pop the queueand write
14M. Waga (NII)Overview of Filteringw
Input Word

a1a2a3a4

⊥

a5

⊥

Queue

Output Word

⊥

a1a23

✓

✘

⊥

15M. Waga (NII)Overview of Filteringw
Input Word

a1a2

a3a4

⊥

a5

⊥

Queue

Output Word

⊥⊥

a21a3

✘
✓✘a1
✓: Write the char.
15M. Waga (NII)

Rea

Overview of FilteringwInput Word

a1a2a3a4a5

⊥

⊥

Queue

Output Word⊥

⊥a2a34✘✘a116

M. Waga (NII)Overview of Filteringw
Input Word

a1a2a3a4a5

⊥

⊥

Queue

Output Word

⊥

⊥a1a4

✘

✘

⊥
✘: Write ⊥16a32

M. Waga (NII)Overview of Filteringw
Input Worda1

a2

a3a4a5⊥⊥a4a5• some chars are masked• maskedremovablew′
Output Word

⊥

⊥

a117

⊥

⊥

M. Waga (NII)

Untimed Filter Construction
1. add a counter to each state← Count: distance from the init. state mod N
2. powerset construction← Moore machine (deterministic)
3. add queue

18

M. Waga (NII)

Idea of Mask / UnmaskQueue•

Surely Unused•

Surely Used•

Not Sureaiai+1… ai+N-1✓✓…

✘Mask (✘)
Pass (✓)

Pass (✓)
19

M. Waga (NII)Properties of Untimed
Moore Machine Filter
Log: w = a1 a2 . . . an<latexit sha1_base64="jxbqHSTMN2MzC8LJSdH4zuGc7ps=">AAAB/nicbVBNS8NAFHzxs9avqODFy2IRPJWkCOpBKHrxWMHYQhvCZrtpl242YXejlNqDf8WLBxWv/g5v/hs3bQ7aOvBgmHnDvp0w5Uxpx/m2FhaXlldWS2vl9Y3NrW17Z/dOJZkk1CMJT2QrxIpyJqinmea0lUqK45DTZji4yv3mPZWKJeJWD1Pqx7gnWMQI1kYK7P0HdIFw4JqpoU430cowUQ7silN1JkDzxC1IBQo0AvvLhEkWU6EJx0q1XSfV/ghLzQin43InUzTFZIB7tG2owDFV/mhy/xgdGaWLokSaERpN1N+JEY6VGsah2Yyx7qtZLxf/89qZjs78ERNppqkg04eijCOdoLwM1GWSEs2HhmAimbkVkT6WmGhTWV6CO/vleeLVqudV5+akUr8s2ijBARzCMbhwCnW4hgZ4QOARnuEV3qwn68V6tz6mqwtWkdmDP7A+fwA9ZZPf</latexit>

Pattern: A<latexit sha1_base64="FCmEzdlEaHIm6bhFbz/Gjv3WW1w=">AAAB8XicbVBNSwMxFHxbv2r9qnr0EiyCp7IrgnqrevFYwbWF7VKyabYNzSZLkhXK0p/hxYOKV/+NN/+N2XYP2joQGGbeI/MmSjnTxnW/ncrK6tr6RnWztrW9s7tX3z941DJThPpEcqm6EdaUM0F9wwyn3VRRnEScdqLxbeF3nqjSTIoHM0lpmOChYDEj2Fgp6CXYjAjm+fW0X2+4TXcGtEy8kjSgRLtf/+oNJMkSKgzhWOvAc1MT5lgZRjid1nqZpikmYzykgaUCJ1SH+SzyFJ1YZYBiqewTBs3U3xs5TrSeJJGdLCLqRa8Q//OCzMSXYc5EmhkqyPyjOOPISFTcjwZMUWL4xBJMFLNZERlhhYmxLdVsCd7iycvEP2teNd3780brpmyjCkdwDKfgwQW04A7a4AMBCc/wCm+OcV6cd+djPlpxyp1D+APn8wfaUpEq</latexit><latexit

Queue size: N

Thm. (soundness)
Our filter Moore machine M does not change the result of theuntimed pattern matching problem.
Thm. (finite completeness)
Our filter Moore machine M masks any unused char. if wehave max{|w| | w ∈ L(A)} ≤ N < ∞.
Thm. (monotonicity)
The Moore machine filter with N-length queue does not mask
more events than the filter with with mN-length queue.
20

M. Waga (NII)Spec.

OutlineTheoretical preparation

SensorFilterMonitor• Moore Machine Filter for Untimed Pattern Matching

•

•

•

Spec.: NFA A•

Log: word (w ∈ Σ*)

Main Problem

Moore Machine Filter for Timed Pattern Matching•

Spec.: TA A•

Log: timed word (w ∈ (Σ × R>0)*)

Experiments (timed)
21

M. Waga (NII)

Timed Pattern Matching[Ulus et al., FORMATS’14]
Log
OutputInput

・Timed Word w ∈ (Σ×R>0)* Match(w, A) =・TA A

Examplew={(t,t′) | w|(t,t′) ∈ L(A)}Spec.
Find frequent
gear change

high lowlowhigh

0 0.1 0.2

0.5

0.7 t

Intervals where spec.
is satisfied
high, x < 1

A = starts0

low /x := 0s1s2$, x < 1s3

low , x < 1

Match(w, A)= {(t,t′) | 0.2 ≤ t < 0.5, 0.7 < t′}
22

M. Waga (NII)

Timed Filter Construction
1. add a counter to each state← Count: distance from the init. state mod N
2. powerset construction← impossible for timed automata(state space will be infinite)
Overapproximation!!

3. add queue
23

M. Waga (NII)One-Clock Determinization[Krichen & Tripakis, FMSD’09]
Thm.
For any TA A, there exists a DRTA Art s.t. L(A) ⊆ L(Art)DRTA : (deterministic real-time autom.)•Restricted form of TA•

Guard: the duration at the source state•Transition function<latexit sha1_base64="It5UNuxu3jRtMeo9joehaxuZrY0=">AAACInicbVDLSgMxFM3UV62vUZdugkWomzIVQe2qqAuXrTq20BlKJr3ThmYeJBmhDP0XN/6KGxe+VoIfY6atoK0HAifn3Mu993gxZ1JZ1qeRW1hcWl7JrxbW1jc2t8ztnTsZJYKCTSMeiZZHJHAWgq2Y4tCKBZDA49D0BheZ37wHIVkU3qphDG5AeiHzGSVKSx2z6lwCV6SKG9hRLACJS84N6wXk5+sERPU9L70edVKnB9gaHWorwo1CxyxaZWsMPE8qU1JEU9Q75rvTjWgSQKgoJ1K2K1as3JQIxSiHUcFJJMSEDkgP2pqGRM930/GNI3yglS72I6FfqPBY/d2RkkDKYeDpymxjOetl4n9eO1H+qZuyME4UhHQyyE841jdmgeEuE0AVH2pCqGB6V0z7RBCqdKxZCJXZk+eJfVQ+K1uN42LtfJpGHu2hfVRCFXSCaugK1ZGNKHpAT+gFvRqPxrPxZnxMSnPGtGcX/YHx9Q2Ff6KK</latexit>: Q ⇥ (⌃ ⇥ R 0 ) ! Q
24

M. Waga (NII)

Timed Filter Construction
1. add a counter to each state← Count: distance from the init. state mod N
2. One-clock determinization← DRTA: similar to DFA

3. add queue

25

M. Waga (NII)Properties of Timed
Moore Machine FilterThm. (soundness)
Our filter Moore machine M does not change the result ofthe timed pattern matching problem.

Completeness does not hold26

experimental results

M. Waga (NII)Spec.

OutlineTheoretical preparation

SensorFilterMonitor• Moore Machine Filter for Untimed Pattern Matching

•

•

•

Spec.: NFA A•

Log: word (w ∈ Σ*)

Main Problem

Moore Machine Filter for Timed Pattern Matching•

Spec.: TA A•

Log: timed word (w ∈ (Σ × R>0)*)

Experiments (timed)
27

M. Waga (NII)Research Questions
Sensor••FilterMonitor

RQ1: Does our filter Moore machine mask many
events?
•Theoretically, only soundness•

Queue size vs. filtering rate

RQ2: Is our filter Moore machine online capable?
•Linear time? Constant memory usage?
28

M. Waga (NII)Environment of Experiment•

MacBook Pro Early 2013•

Intel Core i5 2.6 GHz and DDR3 1600MHz 8 GB•

Mac OS 10.13.4•

clang-900.0.39.2 with optimization flag -O3•

Used 3 benchmarks (Accel, Gear, Torque)
Automotive
29

M. Waga (NII)RQ1: Filtering Rate
Length of the Filtered Timed Word [⇥105 ]Accel

18Sensor

N =1
N =2
N =3
N =4

N =5
N = 10NOT FILTEREDFilterMonitor

N: size of queue

12600612

N=10 looksenough(length: 1/100)

18

Length of the Input Timed Word [⇥105 ]30

M. Waga (NII)RQ1: Filtering Rate (Cont’d)SensorFilterMonitor
Gear

64

N =1N =2N =3N =4N =5N = 10
NOT FILTERED
Length of the Filtered Timed Word [⇥105 ]Length of the Filtered Timed Word [⇥105 ]TorqueN=2 looks
enough48 (length: 1/2)

32160016324864

Length of the Input Timed Word [⇥105 ]3112N =1
N =2
N =3N =4N =5N = 10NOT FILTERED

N=2 looks
enough8 (length: 1/3)

40048

12Length of the Input Timed Word [⇥105 ]M. Waga (NII)RQ2: Execution Time
TorqueAccel
N =5N = 100.6

N =5N = 101632481.40.70.4064

Length of the Input Timed Word [⇥100000]

Gear

0.20N =3N =42.10N =1N =20.4061218Length of the Input Timed Word [⇥100000]

Linear Execution Time

Execution Time [s]Execution Time [s]0.8

N =3N =4Execution Time [s]N =1N =22.8

N =1N =2N =3N =4N =5N = 100.30.20.1004812Length of the Input Timed Word [⇥100000]

32M. Waga (NII)RQ2: Memory Usage
TorqueAccel
N =5N = 102000

N =3N =41632

N =5N = 101820
1807
1794
1781

1920

048

64Length of the Input Timed Word [⇥105 ]

Gear
1840
1760

N =1
N =2

1833

061218Length of the Input Timed Word [⇥105 ]Constant Memory Usage

Memory Usage [kbyte]

Memory Usage [kbyte]

2080

N =3N =4

Memory Usage [kbyte]

N =1N =21833

N =1N =2

N =3N =4N =5N = 101786
1739
1692
1645

04812Length of the Input Timed Word [⇥105 ]33

M. Waga (NII)ConclusionSensor

FilterMonitor•

We proposed Moore machine filter for untimed/
timed pattern matching•

Reduces the data size to send•

online capable•(omitted in this talk) it also accelerates timed
pattern matching.

34

M. Waga (NII)Future Works•

Case study in an embedded system•

Extension to distributed systems••Many sensor node vs one central server

Hardware Implementation (e.g., FPGA, ASIC)

35

M. Waga (NII)