Symbolic Monitoring against
Specifications Parametric in
Time and Data
Masaki Waga1,2,3 , Étienne André4,5,1, and Ichiro Hasuo1,2National Institute of Informatics1, SOKENDAI2,JSPS Research Fellow3,LIPN, Université Paris 13, CNRS4, JFLI, UMI CNRS5
16 July 2019, CAV 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).

1M. 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
2

M. Waga (NII)Spec. with Parameters
Concrete Spec. Example
the total amount of 7-days withdrawal by user Bob
should be < 1,000 USD
We do not know the best thresholds.
→ Parametrize and Synthesize!!
(Instead of True/False)
Parametric Spec. Example
the total amount of p-days withdrawal by user N
should be < T USD
3M. Waga (NII)Symbolic Monitoring[Contribution]

Input
•

Time-series data••

System log (event + data + timestamp)e.g.,

withdraw(Alice, 100) withdraw(Bob, 10)
0.7•

withdraw(Alice, 30)

1.2

2.7

t

Parameterized real-time spec. with data•

Spec. to be monitored•e.g., the total amount of p-days withdrawal by user N shouldbe < T USD

Output• All of the param. val. such that the log satisfies the spec.
e.g., (N, T, p) = (Alice, 140, 3.0), (Alice, 135, 4.0), (Bob, 20, 1.0), …
• Infinitely many → Symbolic representation•

4M. Waga (NII)Symbolic Monitoring[Contribution]

Input
•

Time-series data••

System log (event + data + timestamp)e.g.,

withdraw(Alice, 100) withdraw(Bob, 10)
1.2

0.7
•

withdraw(Alice, 30)
2.7tParameterized real-time spec. with data••

Spec. to be monitoredp (= 3.0)
e.g., the total amount of p-dayswithdrawal by user N should
withdraw(Alice, 30)100) withdraw(Bob, 10)
be withdraw(Alice,< T USD

0.7

1.2

2.7tOutput• All of the param. val. such that the log satisfies the spec.

e.g., (N, T, p) = (Alice, 140, 3.0), (Alice, 135, 4.0), (Bob, 20, 1.0), …
• Infinitely many → Symbolic representation•

4M. Waga (NII)Symbolic Monitoring[Contribution]

Input
•

Time-series data••

System log (event + data + timestamp)e.g.,

withdraw(Alice, 100) withdraw(Bob, 10)
0.7•

withdraw(Alice, 30)

1.2

2.7

t

Parameterized real-time spec. with data•

Spec. to be monitored•p (= 4.0)
e.g., the total amount of p-dayswithdrawal by user N should
be <T USD
withdraw(Alice, 30)
withdraw(Alice,100) withdraw(Bob, 10)

0.7

1.2

2.7

Output• All of the param. val. such that the log satisfies the spec.

te.g., (N, T, p) = (Alice, 140, 3.0), (Alice, 135, 4.0), (Bob, 20, 1.0), …
• Infinitely many → Symbolic representation•

4M. Waga (NII)Symbolic Monitoring[Contribution]

Input
•

Time-series data••

System log (event + data + timestamp)e.g.,

withdraw(Alice, 100) withdraw(Bob, 10)
0.7•withdraw(Alice, 30)

1.2t

2.7

Parameterized real-time spec. with data••Spec. to be monitored1.0)
e.g., the total amount of p-daysp (=withdrawalby user N should
withdraw(Alice, 30)100) withdraw(Bob, 10)
be <withdraw(Alice,T USD

0.7

1.2

Output• All of the param. val. such that the log satisfies the spec.

2.7

te.g., (N, T, p) = (Alice, 140, 3.0), (Alice, 135, 4.0), (Bob, 20, 1.0), …
• Infinitely many → Symbolic representation•4M. Waga (NII)

Contribution•

Introduced parametric timed data automata (PTDA)•••

PTDA: Non-deterministic finite automata (NFA)+ timing constraints + data + parameters

Gave symbolic monitoring algorithm over a PTDA spec.
•

Symbolically synthesize all the feasible param. val. wrt. log•(Potentially) infinitely many param. val.
→ symbolic representation/operations

Implementation + experiments → Scalable!!
5M. Waga (NII)Outline•

Motivation + Introduction•

Technical Part•

Parametric timed data automata (PTDA)••

Symbolic monitoring algorithm••

PTDA: NFA + timing constraints + data + param.

Idea: follow trans. (+ non-deterministic branching)Experiments
6M. Waga (NII)PTDA: NFA + time + data +parameters
NFA
withdraw
start

l0

withdraw
withdraw

l1"

l2

withdraw

7M. Waga (NII)PTDA: NFA + time + data +parameters
Timed Automaton (TA)withdrawt<7

withdraw
start

l0

withdraw/t := 0l1", t = 7l2

withdraw
t<78

M. Waga (NII)PTDA: NFA + time + data +parameters
Timed Data Automaton (TDA)
withdraw(u, a)withdraw(u, a)t < 7, u 6= Bob
withdraw(u, a), u = Bob", t = 7/t := 0, sum := asum < 10, 000l0l1
l2
start
withdraw(u, a)t < 7, u = Bob/sum := sum + a
9M. Waga (NII)PTDA: NFA + time + data +parameters
Parametric Timed Data Automaton (PTDA)
withdraw(u, a)withdraw(u, a)t < p, u 6= N
withdraw(u, a), u = N", t = p/t := 0, sum := asum < T
l0
l1
start

l2

withdraw(u, a)t < p, u = N/sum := sum + a
10M. Waga (NII)Data Type (D, DE, DU)

D: infinite domain

DE: Boolean expression (for guards)
DU: updates (for variable updates/assignments)•(Explained Later) Our symbolic monitoringalgorithm works for any data type with somesymbolic operations•

e.g., Strings (S), Rationals (Q), …
11M. Waga (NII)Outline•

Motivation + Introduction•

Technical Part•

Parametric timed data automata (PTDA)••

Symbolic monitoring algorithm••

PTDA: NFA + timing constraints + data + param.

Idea: follow trans. (+ non-deterministic branching)Experiments
12M. Waga (NII)

Idea of our SymbolicMonitoring Algorithm
follow the transitions of PTDA+
abstraction of clock/data/param. val.
(e.g., by convex polyhedra or lists of forbidden strings)+Non-deterministic branching by breadth first search()

13

M. Waga (NII)Symbolic Monitoring by
Following Transitions
withdraw(u, a)
N ∈ S, p ∈ Q, T ∈ Q
t < p, u 6= N
t = 0, sum = 0
withdraw(u, a), u = N", t = p/t := 0, sum := asum < T
l0
l1startLog

l2

withdraw(u, a)t < p, u = N/sum := sum + awithdraw(Alice, 100) @0.7
withdraw(Bob, 10) @1.2
withdraw(Alice, 30) @2.7
14

M. Waga (NII)Symbolic Monitoring byFollowing Transitions
N = Alice, p ∈ Q, T ∈ Q
t = 0, sum = 100
withdraw(u, a)
N ∈ S, p ∈ Q, T ∈ Q
t < p, u 6= N
t = 0, sum = 0withdraw(u, a), u = N", t = p/t := 0, sum := asum < T
l0
l1
start

Log

l2

withdraw(u, a)t < p, u = N/sum := sum + a→withdraw(Alice,withdraw(Alice, 100)
100) @0.7@0.7withdraw(Bob, 10) @1.2
withdraw(Alice, 30) @2.7
14

M. Waga (NII)Symbolic Monitoring byFollowing Transitions
N = Alice, p ∈ Q, T ∈ Q
t = 0, sum = 100
withdraw(u, a)
N ∈ S, p ∈ Q, T ∈ Q
t < p, u 6= N
t = 0, sum = 0
withdraw(u, a), u = N", t = p/t := 0, sum := asum < Tl0
l1
start

Log

N = Alice, p = t, T > 100t ∈ [0,0.5), sum = 100l2

withdraw(u, a)t < p, u = N/sum := sum + a→withdraw(Alice,withdraw(Alice, 100)
100) @0.7@0.7
withdraw(Bob, 10) @1.2withdraw(Alice, 30) @2.7
14

M. Waga (NII)Symbolic Monitoring byFollowing Transitions
N = Alice, p ∈ Q, T ∈ Q
t = 0, sum = 100

N = Alice, p > t, T ∈ Q
t = 0.5, sum = 100

withdraw(u, a)
N ∈ S, p ∈ Q, T ∈ Qt < p, u 6= Nt = 0, sum = 0
withdraw(u, a), u = N", t = p/t := 0, sum := asum < Tl0l1startLog

N = Alice, p = t, T > 100t ∈ [0,0.5), sum = 100

l2withdraw(u, a)t < p, u = N/sum := sum + a→withdraw(Alice,withdraw(Alice, 100)
100) @0.7@0.7→withdraw(Bob,withdraw(Bob, 10)10) @1.2@1.2
withdraw(Alice, 30) @2.7
14

M. Waga (NII)Symbolic Monitoring byFollowing Transitions
N = Alice, p ∈ Q, T ∈ Q
t = 0, sum = 100

N = Alice, p > t, T ∈ Qt = 0.5, sum = 100

withdraw(u, a)
N ∈ S, p ∈ Q, T ∈ Qt < p, u 6= Nt = 0, sum = 0
withdraw(u, a), u = N", t = p/t := 0, sum := asum < Tl0
l1startLog

N = Alice, p = t, T > 100t ∈ [0,0.5), sum = 100

l2

N = Alice, p = t, T > 100t ∈ [0.5,2.0), sum = 100

withdraw(u, a)t < p, u = N/sum := sum + a→withdraw(Alice,withdraw(Alice, 100)
100) @0.7@0.7→withdraw(Bob,withdraw(Bob, 10)10) @1.2@1.2
withdraw(Alice, 30) @2.7
14

M. Waga (NII)Symbolic Monitoring byFollowing Transitions
N = Alice, p ∈ Q, T ∈ Q
t = 0, sum = 100N = Alice, p > t, T ∈ Qt = 0.5, sum = 100

withdraw(u, a)
N ∈ S, p ∈ Q, T ∈ Qt < p, u 6= N
t = 0, sum = 0withdraw(u, a), u = N", t = p/t := 0, sum := asum < T
l0
l1
start

Log

N = Alice, p > t, T ∈ Q
t = 2.0, sum = 130
N = Alice, p = t, T > 100t ∈ [0,0.5), sum = 100

l2

N = Alice, p = t, T > 100t ∈ [0.5,2.0), sum = 100

withdraw(u, a)t < p, u = N/sum := sum + a→withdraw(Alice,withdraw(Alice, 100)
100) @0.7@0.7→withdraw(Bob,withdraw(Bob, 10)10) @1.2@1.2→withdraw(Alice,withdraw(Alice, 30)30) @2.7@2.7
14

M. Waga (NII)Symbolic Monitoring byFollowing Transitions
N = Alice, p ∈ Q, T ∈ Q
t = 0, sum = 100

N = Alice, p > t, T ∈ Q
t = 0.5, sum = 100

withdraw(u, a)
N ∈ S, p ∈ Q, T ∈ Q
t < p, u 6= N
t = 0, sum = 0
withdraw(u, a), u = N", t = p/t := 0, sum := asum < Tl0l1startLog

withdraw(u, a)t < p, u = N/sum := sum + a

N = Alice, p > t, T ∈ Q
t = 2.0, sum = 130
N = Alice, p = t, T > 100t ∈ [0,0.5), sum = 100

l2

N = Alice, p = t, T > 100t ∈ [0.5,2.0), sum = 100
N = Alice, p = t, T > 130t ∈ [2.0,∞), sum = 130→withdraw(Alice,withdraw(Alice, 100)
100) @0.7@0.7→withdraw(Bob,withdraw(Bob, 10)10) @1.2@1.2→withdraw(Alice,withdraw(Alice, 30)30) @2.7@2.714M. Waga (NII)Symbolic Monitoring byFollowing Transitions
N = Alice, p ∈ Q, T ∈ Q
t = 0, sum = 100

N = Alice, p > t, T ∈ Q
t = 0.5, sum = 100

withdraw(u, a)
N ∈ S, p ∈ Q, T ∈ Q
t < p, u 6= N
t = 0, sum = 0
withdraw(u, a), u = N", t = p/t := 0, sum := asum < T
l0
l1
start

Log

withdraw(u, a)t < p, u = N/sum := sum + a→withdraw(Alice,withdraw(Alice, 100)
100) @0.7@0.7→withdraw(Bob,withdraw(Bob, 10)10) @1.2@1.2→withdraw(Alice,withdraw(Alice, 30)30) @2.7@2.7

N = Alice, p > t, T ∈ Q
t = 2.0, sum = 130
N = Alice, p = t, T > 100t ∈ [0,0.5), sum = 100

l2

N = Alice, p = t, T > 100t ∈ [0.5,2.0), sum = 100
N = Alice, p = t, T > 130t ∈ [2.0,∞), sum = 130

Result14M. Waga (NII)Termination of Symbolic
MonitoringThm.
Our symbolic monitoring algorithm terminates for any
data types (D, DE, DU) such that we can computerestriction, update, emptiness checking, and projection.
Examples•Strings (S) with lists (of forbidden strings)•Rationals (Q) with convex polyhedra
15M. Waga (NII)Outline•

Motivation + Introduction•

Technical Part•

Parametric timed data automata (PTDA)••

Symbolic monitoring algorithm••

PTDA: NFA + timing constraints + data + param.

Idea: follow trans. (+ non-deterministic branching)Experiments
16

M. Waga (NII)Environment of Experiments•

Data: strings (by lists) and rationals (by convex polyhedra)•Used 3 original benchmarks:•Copy: “The value of a signal should be copied to another signal”••

Dominant: “Detect a dominant withdrawal by a user”•••

Inspired by [Brim+, Information and Computation 236]

Inspired by [Basin+, RV-CuBES’17]

Periodic: Synthesize periods of periodic withdrawals(Explained later)

Amazon EC2 c4.large instance / Ubuntu 18.04 LTS (64 bit)
•2.9 GHz Intel Xeon E5-2666 v3, 2 vCPUs, 3.75 GiB RAM

17

M. Waga (NII)

479

6.3

Benchmark 3: Periodic

Our third benchmark Periodic is inspired by a parameter identification of peri481
odic withdrawals from one bank account. The actions ⌃ is ⌃ = {withdraw} and482
Dom(withdraw) = {a}, where a has a integer value representing the amount of483
the withdrawal. We randomly generated a set consisting of 10 timed data words484
of length 2,000 to 20,000. Each timed data word consists of the following three
Input
1: ofLog
485
kinds
periodic withdrawals:
480“Periodic" Benchmark• 486small
occursevery
timeunits
shortwithdrawals
period One withdrawal
occursevery 5±1
5 ± 1 timeunits.
The amount of

the withdrawal is 50 ± 3.
• 488middle
middle withdrawals
period One withdrawal
occursevery
every 5050±3± 3 timetime
units. The
amount ofoccursunits
489
the withdrawal is 1000 ± 40.
long withdrawals
period One withdrawal
occursevery
every 100
± 5 timetime
units. units
The amount of• 490large
occurs100±5491
the withdrawal is 5000 ± 20.
487

PTDA in Periodic is shown in Result
Input 2:TheSpec.
492

Values of tp1 and tp2

the right of Fig.withdraw(a)3. The PTDA matches
100
tp1tp200)
494
situations where, for80
withdraw(a)a >anyvp two successive
l0 of amount more than vp,
495
a  withdrawals
vp
tp1  c  tp260
l2496
the duration between
c := 0them is within
40497[tp1 , tp2 ]. By the symbolic monitoring,20498
one can identify the period of the peri499
odic withdrawals of amount greater than
00 1000 2000 3000 4000 5000
500
vp is in [tp1 , tp2 ]. An example of the vand Periodic (right)
The threshold (vp) of the withdrawal amount501lidity domain is shown in the right figure.
M. Waga502
The experiment result is in Fig.18
5. We observe that the execution
time is(NII)
linearmatching493

Execution Time
Copy

Dominant
Execution time [sec.]

Execution time [sec.]

7
65
4
3
2
100

5

10

15

20

25

30

35

40

160
140
120
100
80
60
40
200
2

Number of events [⇥1, 000]

Periodic

4

6

81012

14

16

18

20

Number of events [⇥1, 000]

• 20,000 entries in 1 - 2 min.
• Execution time is linear in all of three benchmarks• Much more efficient than the worst case!!
19M. Waga (NII)Related Works•

Symbolic Register Automata [D'Antoni+, CAV 2019]••

Register to remember previous information

MFOTL [Basin+, J. ACM 62(2) 2015] [Basin+, RV-CuBES 2017] (MonPoly)•Many common concepts
•

•
•

•

timing constraints, quantified variables, and aggregation

Concrete outputs

PSTL [Asarin+, RV 2011], [Bakhirkin+, HSCC 2018]•

It synthesizes the parameter valuations•

Specific to real-values / Signal-based

QTL [Havelund+, FMCAD 2017], [Havelund+, MT-CPS’18] (DejaVu)•They use BDD in monitoring, though their outputs are rather concrete•

no native support of timestamps
20

M. Waga (NII)Conclusion•

Introduced parametric timed data automata (PTDA)••

Gave symbolic monitoring algorithm over PTDA••

PTDA: NFA + timing constraints + data + parameters

Idea: follow trans. (+ non-deterministic branching)

Implementation + experiments•

about 20,000 entries in 1 or 2 min
21

M. Waga (NII)Future Works•Use BDD for more “symbolic” monitoring•

Employ polarity for further efficiency••

Polarity: Either only expr < p or only expr > pInference when D is finite•If D = {a,b,c}, neither a nor b22c
M. Waga (NII)