Model-bounded monitoringof hybrid systems
Masaki Waga1, Étienne André2, Ichiro Hasuo3
Kyoto University1, Université de Lorraine2,National Institute of Informatics318 May 2021, MT-CPS 2021
This work is partially supported by JST ACT-X Grant No. JPMJAX200U, by JST ERATO HASUO Metamathematics for Systems
Design Project (No. JPMJER1603), by JSPS Grant-in-Aid No. 18J22498, and by ANRNRF ProMiS (ANR-19-CE25-0015).

1

M. Waga (Kyoto U.)

Safety Critical CPSs

https://www.abc15.com/news/region-southeast-valley/chandler/waymo-car-involved-in-chandler-arizona-crashhttps://www.bbc.com/news/technology-48308852

2M. Waga (Kyoto U.)

Monitoring
Speci cation: No (v > 120)

v
120

fi

3

M. Waga (Kyoto U.)

Monitoring
Speci cation: No (v > 120)

✘v
120

t
fi

3

M. Waga (Kyoto U.)

Monitoring with SamplingSpeci cation: No (v > 120)

✘v
120

t
fi

4

M. Waga (Kyoto U.)

Monitoring with SamplingSpeci cation: No (v > 120)

✔?
v
120

t
fi

5

M. Waga (Kyoto U.)

Monitoring with SamplingSpeci cation: No (v > 120)

✔?
v
120

tfi

5

M. Waga (Kyoto U.)Signal Interpolation
Speci cation: No (v > 120)

v120

tfi

6M. Waga (Kyoto U.)

Signal Interpolation
Speci cation: No (v > 120)

v120

t
fi

7

M. Waga (Kyoto U.)

Signal Interpolation
Speci cation: No (v > 120)

v

120

t
fi

8

M. Waga (Kyoto U.)

Signal Interpolation
Speci cation: No (v > 120)

v

120

t
fi

8

M. Waga (Kyoto U.)

Signal Interpolation
Speci cation: No (v > 120)

✘?

v

120t
fi

9

M. Waga (Kyoto U.)

Interpolation with Prior
Knowledge
Speci cation: No (v > 120)
Impossible because

dv
<Kdtv

120

tfi

10

M. Waga (Kyoto U.)

Model-Bounded Monitoring
Speci cation: No (v > 120)

Our Contribution

Knowledge(bounding model)
dv
<Kdtv

120

tfi

11M. Waga (Kyoto U.)

Model-Bounded Monitoring
Speci cation: No (v > 120)
Knowledge(bounding model)

Our Contribution

Feasible execution withdv
<Kdt

dv
<Kdtv

120

tfi

11

M. Waga (Kyoto U.)

Model-Bounded Monitoring
Speci cation: No (v > 120)

Our Contribution

Knowledge(bounding model)
dv
<Kdtv

120

fi

12M. Waga (Kyoto U.)

Model-Bounded Monitoring
Speci cation: No (v > 120)
Knowledge(bounding model)

Our Contribution

Feasible execution withdv
<Kdt

dv
<Kdtv

✔

120tfi12M. Waga (Kyoto U.)

Q. How to Represent
Bounding Model?

Model-Bounded Monitoring of Hybrid Systems
233
234
235
236
237
238
239
240
241
242
243
244

a bounding
model ho(an LHA)¬

Knowledge(bounding model)

overapproximates

dv
a “behavior” σ
a “log” w<K(a conti.-time(a discr.-time
dtsystem undersignal)
signal)sensormonitoring(~ sampler)xx(SUM)

proposedLHAmonitort249
250¬ )?

FigtheMhat[0,(raise an alert if yes)

Figure 4: Model-bounded monitoring of hybrid systems

Discrete modes

Derivative by
G = 40✓G = 35
PolyhedronG§ 2 [7.5, 8.5]
12G 1 = 40
G 2 = 35

✓0G§1 2 [7.5, 8.5]
G§2 2 [8.0, 9.0]

G1
G1

G2  4G24✓1
G§1 2 [11.0, 13.0]
G§2 2 [9.0, 11.0]

251
252

wt

246
248

Lmon(A. Linear Hybrid Automata

245247a safetyspecification φ

The LHA

13 platooning example, ex(a) A bounding model M for the01G§2 2 [8.0, 9.0]
G1G2 ✓2G§1 2 [7.5, 8.5]
G§2 2 [8.0, 9.0]

M. Waga (Kyoto U.)

Contributions•

Proposed model-bounded monitoring
Bounding model (knowledge): linear HAs ℳ•

Formalized with monitored language Lmon(ℳ)

Lmon(ℳ): possible discrete observations of ℳ
Algorithms + implementations
Idea: bounded-time reachability
Experiment → e ectively monitorable
14ff•

M. Waga (Kyoto U.)

Model-Bounded Monitoring

Our Contributiondv<KdtGiven• Bounding model in LHA ℳ• Safety Speci cation φ• Discrete Log w

No (v > 120)
v

120

t

Decide if the actual behavior might violate the spec.
v

v

120

120

✔
tt
fi

15

✘
M. Waga (Kyoto U.)

Model-Bounded Monitoring

Our Contribution

dv
<Kdt

Given

• Bounding model in LHA ℳ• Safety Speci cation φ• Discrete Log w

No (v > 120)
v

120

t

Decide if the actual behavior might violate the spec.
v

v

120

120

✔
tt
fi15

✘
M. Waga (Kyoto U.)

Monitored Language Lmon

Our Contribution

Combine cont. exec. of ℳ and disc. obs. of wLmon(ℳ) = { Discr. Obs w |v

120t
16M. Waga (Kyoto U.)

Monitored Language Lmon

Our Contribution

Combine cont. exec. of ℳ and disc. obs. of w
Lmon(ℳ) = { Discr. Obs w | ∃ exec. σ of ℳ s.t.
v

120t
16

M. Waga (Kyoto U.)

Monitored Language Lmon

Our Contribution

Combine cont. exec. of ℳ and disc. obs. of w
Lmon(ℳ) = { Discr. Obs w | ∃ exec. σ of ℳ s.t.
w is a sample of σ }
v

120t
16

M. Waga (Kyoto U.)

Work ow ofModel-bounded Monitoring
1. Construct an LHA ℳ¬φ from bounding model ℳ
and spec. φ

Idea: Product of LHAs
2. Check if w ∈ Lmon(ℳ¬φ)
Idea: Bounded-time reachability analysis

fl17

M. Waga (Kyoto U.)

Algorithm:
Bounded-time Reachability
v

120

t

18

M. Waga (Kyoto U.)

Algorithm:
Bounded-time Reachability
v

120

t

18

M. Waga (Kyoto U.)

Algorithm:
Bounded-time Reachability
v

120

t

18

M. Waga (Kyoto U.)

Algorithm:
Bounded-time Reachability
v

120t

18

M. Waga (Kyoto U.)

Algorithm:
Bounded-time Reachability
v

120

t

18

M. Waga (Kyoto U.)

Algorithm:
Bounded-time Reachability
v

120t

18

M. Waga (Kyoto U.)

Algorithm:
Bounded-time Reachability
Feasible execution with

dv
<Kdtv

120t

18

M. Waga (Kyoto U.)

Algorithm:
Bounded-time Reachability
Feasible execution with

dv
<Kdtv

120t
bounded18

M. Waga (Kyoto U.)

Implementations
Approach 1: Utilize existing model-checker (PHAVerLite)
Pros: Highly-optimized reachability analysis impl.
Approach 2: Implement dedicated monitor (HAMoni)
Pros: Best performance in theory

19M. Waga (Kyoto U.)

Environment of Experiments•

Used 3 benchmarks on adaptive cruise controller (ACC)+ 1 robot navigation (NAV) benchmark•

ACC: Cars should not be too close (or no physicalcontact)

For scalability analysis••

NAV: Do not enter an unsafe region
Amazon EC2 c4.large instance / Ubuntu 18.04 LTS (64 bit)
•For false alarmsanalysis

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

20

M. Waga (Kyoto U.)

Experiment Results
Changing Observation Length

Exec. time [sec.]

PHAVerLite, dim. 3, " = 2.0
PHAVerLite, dim. 3, " = 0.9
HAMoni, dim. 3, " = 2.0
HAMoni, dim. 3, " = 0.9
2.5
21.5
10.5
00
Dedicated impl.
≈ 10x faster123 4 5 6 7Length [⇥100]

2189 10> 5000
samples / sec.
M. Waga (Kyoto U.)

Experiment Results

Execution time [sec.]

Changing Model Dimension

1000
100
1010.10.01
0.001

PHAVerLite, len. 100, " = 2.0
PHAVerLite, len. 100, " = 0.9
HAMoni, len. 100, " = 2.0
HAMoni, len. 100, " = 0.9

Existing tool wasfaster for dim. > 62Future work:
further optimization

2.5

3

3.5 4 4.5Dimension
225

5.5

6

M. Waga (Kyoto U.)

Experiment Results
max. di erence from the threshold

False Alarms
0.35

NAV

0.3
0.25
0.2
0.15
0.1
0.05
00200

400

600

800

1000

shortest sampling interval without false alarms [ms.]ffFalse alarm for “verysafe” exec.
→ sampling is coarse

23M. Waga (Kyoto U.)

Conclusions•Proposed model-bounded monitoring
Bounding model (knowledge): linear HAs ℳ•

Formalized with monitored language Lmon(ℳ)

Lmon(ℳ): possible discrete observations of ℳ
Algorithms + implementations
Idea: bounded-time reachability
Experiment → e ectively monitorable24ff•

M. Waga (Kyoto U.)