Symbolic Monitoring against Specification
Parametric in Time and Data
[1,2]
[3,4]
[1,2]
Masaki Waga , Étienne André , Ichiro Hasuo

SOKENDAI[1] / NII[2] / Université de Lorraine, CNRS, Inria, LORIA[3] / JFLI, UMI CNRS[4]BackgroundOur Solution

Runtime Verification (RV)

Symbolic Monitoring w/
Parametric Specifications

orContribution•

Introduced parametric timed data
automata (PTDA)• PTDA: NFA + clock/data variables +time/data parameters

Boolean Monitoring w/ Concrete Spec.
Runtime verification (or monitoring) isnot exhaustive butorit does not require system model•i.e., Blackbox systems are OK•

e.g., System w/
3rd-party components•

Unknown environment

representation

param.

{param. val. s.t.

and•• Idea: follow trans. using symbolic•(Potentially) infinitely many param. val.
→ symbolic representation/operations•

Experiments → Scalable!!

•Demo is available on Google Colab

Symbolic Monitoring w/ Parametric Spec.

Machine learning components•Gave symbolic monitoring algorithm over
a PTDA spec.

It tends to be scalable for complexsystems⋰}

the total amount of p-dayswithdrawal by user Nshould be < T USD•••• Clearly satisfied vs. Satisfied but nearwithdraw(Alice, 100) withdraw(Bob, 10)

e.g.,

1.2

2.7

•

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

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

Detail on PTDA
Example of a PTDA
withdraw(u, a)withdraw(u, a)t < p, u 6= N
withdraw(u, a), u = N", t = p/t := 0, sum := asum < Tl0l1start
withdraw(u, a)t < p, u = N/sum := sum + a

Q: What is “Data”?
A: Any triple (D, DE, DU)t

Synthesizes
periods of periodic
withdrawals

Periodic

160
140
120
100
80
60
40
20
0
2Output• All of the param. val. such that the log satisfies thespec.

the borderline

Scalability
Dominant

withdraw(Alice, 30)

Parameterized real-time spec. with data•

Detects dominant
withdrawals bya user

System log (event + data + timestamp)

0.7• e.g., What is the best threshold of “toolarge acceleration”?
than Boolean results[Contribution]

Time-series data•

Issues in RV• We want quantitative results ratherTool Demo

Symbolic Monitoring
Input• It is diﬃcult to determine the best
threshold in the spec.

Official Version arXiv Version

Execution time [sec.]•

the total amount of 7-dayswithdrawal by user Bob
should be < 1,000 USD}

••

4

6

8

10

12

14

16

18

20

Number of events [⇥1, 000]
• 20,000 entries in 1 - 2 min.
• Execution time is linear in these two benchmarks• Much more eﬃcient than the worst case!!
• Important lesson: these useful spec. can bemonitored eﬃciently

Symbolic Monitoring Algorithm
Idea of the 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 searchl2

In the algorithm, we
require a data structurewith some operations

D: infinite domain
DE: Boolean expression (for guards)
DU: updates (for variable updates/assignments)
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).

See also
an illustration!!

()

Termination
Thm.
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