Model-bounded monitoringof hybrid systems
Masaki Waga1, Étienne André2, Ichiro Hasuo3
Kyoto University1, Université de Lorraine2,National Institute of Informatics3
ICCPS 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

3M. Waga (Kyoto U.)

Monitoring
Speci cation: No (v > 120)

✘v
120

tfi

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

t
fi

5

M. Waga (Kyoto U.)

Signal InterpolationSpeci cation: No (v > 120)

v

120

tfi

6M. Waga (Kyoto U.)

Signal Interpolation
Speci cation: No (v > 120)

v

120

tfi

7M. Waga (Kyoto U.)

Signal Interpolation
Speci cation: No (v > 120)

v

120

tfi

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

120

tfi

9M. Waga (Kyoto U.)

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

dv<Kdtv

120tfi10M. 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 with

dv
<Kdt

dv
<Kdtv

120

tfi

11M. 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 boundingmodel ho(an LHA)¬

Knowledge(bounding model)

overapproximates

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

proposedLHA
monitort249250¬ )?

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  4G2

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

251
252

w

t

246
248

Lmon(A. Linear Hybrid Automata

245
247

a 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.)

Algorithm:
Bounded-time Reachability
v

120

t

14

M. Waga (Kyoto U.)

Algorithm:
Bounded-time Reachability
v

120

t

14

M. Waga (Kyoto U.)

Algorithm:
Bounded-time Reachability
v

120

t

14

M. Waga (Kyoto U.)

Algorithm:
Bounded-time Reachability
v

120

t

14

M. Waga (Kyoto U.)

Algorithm:
Bounded-time Reachability
v

120

t

14

M. Waga (Kyoto U.)

Algorithm:
Bounded-time Reachabilityv

120t14M. Waga (Kyoto U.)

Algorithm:
Bounded-time Reachability
Feasible execution withdv<Kdtv

120t

14

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

15

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.500
Dedicated impl.
≈ 10x faster123 4 5 6 7Length [⇥100]

1689 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 was
faster for dim. > 62Future work:
further optimization

2.5

33.5 4 4.5Dimension
175

5.5

6

M. Waga (Kyoto U.)

Conclusions•

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

Algorithms + implementations
Idea: bounded-time reachability• Experiment → e ectively monitorable

ff

18

M. Waga (Kyoto U.)