Hybrid System Falsification andReinforcement Learning
Formal Method for Cyber-Physical Systems

Clovis EberhartDavid Sprunger

National Institute of Technology, JapanSOKENDAI lesson, July 1, 8, and 22

1 / 31

Quick reminder

Falsification:
method to find counterexamples to a property,
useful in the world of formal methods,
black-box method,
relies on optimisation algorithms.

Hybrid system:
continuous and discrete parameters,
non-linear behaviour,
very expressive.

Formulas:expressed in a temporal logic,
boolean and robustness semantics.

2 / 31

1

Refining robustness

2Time staging

3

Coverage-based falsification

3 / 31

Table of Contents

1

Refining robustness

2Time staging

3

Coverage-based falsification

4 / 31

Refining robustness

Why?
more expressivity (i.e., finer modelling)
more techniques (e.g., optimisation techniques work better)

Attention
more expressivity ; more complex algorithms

5 / 31

Refining robustness

Why?
more expressivity (i.e., finer modelling)
more techniques (e.g., optimisation techniques work better)

Attention
more expressivity ; more complex algorithms (here, however,only sliding-window algorithms)

5 / 31

Space-time robustness
Donzé, A. and Maler O. Robust satisfaction of temporal logic over real-valued
signals. FORMATS 2010.

Until now, robustness is spatial.
Problems:

6 / 31

Space-time robustness
Donzé, A. and Maler O. Robust satisfaction of temporal logic over real-valued
signals. FORMATS 2010.

Until now, robustness is spatial.
Problems:
all these signals verify 3[a,b] x > 0 with the same robustness

6 / 31

Space-time robustness
Donzé, A. and Maler O. Robust satisfaction of temporal logic over real-valued
signals. FORMATS 2010.

Until now, robustness is spatial.
Problems:
all these signals verify 3[a,b] x > 0 with the same robustness

the similarity between these two signals is lost when
computing ρ(σ, 3[a,b] x > 0)

6 / 31

Space-time robustness
Donzé, A. and Maler O. Robust satisfaction of temporal logic over real-valued
signals. FORMATS 2010.

Until now, robustness is spatial.
Problems:
all these signals verify 3[a,b] x > 0 with the same robustness

the similarity between these two signals is lost when
computing ρ(σ, 3[a,b] x > 0)

; missing a temporal component
6 / 31

Adding time
Assumption: set P = {p1 , . . . , pn } of atomic propositions.
Standard boolean semantics: χ(σ, ϕ, t).

Time robustness
θ− (σ, p, t) =χ(σ, p, t) · max {d ≥ 0 | ∀t 0 ∈ [t − d, t].χ(σ, p, t 0 ) = χ(σ, p, t)}
θ+ (σ, p, t) =χ(σ, p, t) · max {d ≥ 0 | ∀t 0 ∈ [t, t + d].χ(σ, p, t 0 ) = χ(σ, p, t)}θs (σ, ¬ϕ, t) = −θs (σ, ϕ, t)...

7 / 31Interpreting θ+ and θ−
θ+ (σ, ϕ, t) = s > 0: σ  ϕ for at least time s
θ+ (σ, ϕ, t) = s < 0: σ 2 ϕ for at least time sθ− (σ, ϕ, t) = s > 0: σ  ϕ since at least time sθ− (σ, ϕ, t) = s < 0: σ 2 ϕ since at least time s

8 / 31

Space-time Robustness
Assumption: atomic propositions are functions (e.g., x 2 + y 2 ).
Standard robustness semantics: ρ(σ, ϕ, t).

Space-time robustness
For any c ∈ R:
θc+ (σ, f , t) = θ+ (χc (σ, f , t)),θc− (σ, f , t) = θ− (χc (σ, f , t)),θcs (σ, ¬ϕ, t) = −θcs (σ, ϕ, t).
...
Interpretation:
θc+ (σ, ϕ, t) = s > 0: ρ(σ, ϕ, t) > c for at least time s,...

9 / 31

Space-time Robustness
Assumption: atomic propositions are functions (e.g., x 2 + y 2 ).
Standard robustness semantics: ρ(σ, ϕ, t).

Space-time robustness
For any c ∈ R:
θc+ (σ, f , t) = θ+ (χc (σ, f , t)),θc− (σ, f , t) = θ− (χc (σ, f , t)),θcs (σ, ¬ϕ, t) = −θcs (σ, ϕ, t).
...
Interpretation:
θc+ (σ, ϕ, t) = s > 0: ρ(σ, ϕ, t) > c for at least time s,...
Remarks:
hopefully more efficient
how to choose c?
not more expressive
9 / 31More flexibility
Akazaki T. and Hasuo I. Time robustness in MTL and expressivity in hybrid
system falsification. CAV 2015.

Spatial robustness:

Temporal robustness:

10 / 31

AvSTL
SyntaxAP = x < r | x ≤ r | x > r | x ≥ r
ϕ = > | ⊥ | AP | ¬ϕ | ϕ∨ϕ | ϕ∧ϕ | ϕ UI ϕ | ϕ RI ϕ | ϕ UI ϕ | ϕ RI ϕSemantics
ρ+ (σ, x < r , t) = max{0, r − σ(x)(t)}ρ− (σ, x < r , t) = min{0, r − σ(x)(t)}...
ρ+ (σ, ¬ϕ, t) = ρ− (σ, ϕ, t)Rb
1
ρ+ (σ, ϕ U[a,b] ψ, t) = b−aa ρ(σ, ϕ U[a,b]∩[0,τ ] ψ, t)dτ...

11 / 31

Example
Robustnesses: ρ+ , ρ−
ϕ = x ≥ 0:

ϕ = FI (x ≥ 0):

Consequences:
temporal aspects
spatial aspects
12 / 31

Expressivity
expeditiousness: F[0,a] ϕdeadline: F[0,a] ϕ ∨ F[a,b] ϕpersistence: G[0,a] ϕ ∧ G[a,b] ϕ

13 / 31Experimental results

14 / 31

Table of Contents

1Refining robustness

2Time staging

3

Coverage-based falsification

15 / 31

Time staging

Zhang, Z., Ernst, G., Sedwards, S., Arcaini, P., and Hasuo, I. Two-Layered
Falsification of Hybrid Systems Guided by Monte Carlo Tree Search. EMSOFT
2018.
Ernst, G., Sedwards, S., Zhang, Z., and Hasuo, I. Fast Falsification of Hybrid
Systems using Probabilistically Adaptive Input. QEST 2019.

Idea
σout causally dependent on σinoptimisation methods blind to this dependence; modify the algorithm to take it into account16 / 31

A picture is worth a thousand words

17 / 31High-Level Algorithm
Alternate between:Monte-Carlo Tree Search to find a good zone,
hill-climbing to find a good point in the zone.

18 / 31Monte-Carlo Tree Search

Each node equipped with:robustness estimate,
number of visits.
To choose a node, balance between:
an exploitation score (bigger with smaller robustness
estimates),
an exploration score (bigger with fewer visits to the node).
19 / 31

Robustness estimates
To get robustness estimates: complete the signal by purehill-climbing.
For example, for a newly-expanded node:

20 / 31Experimental results

Interpretation: MTCS explores more, so:better results on hard problems
slower on simple problems

21 / 31Adaptive Las Vegas Tree Search
To build signal σ incrementally:
randomly choose a level l of “granularity” (initially, low
granularity is favoured),choose σ 0 = Dl (σ), where Dl chooses “finer” signals for largel (shorter time, more precise value),
adapt Dl according to ρ(σσ 0 , ϕ, t).

22 / 31Experimental results

Interpretation:
falsifying signals are often coarse, or slight variations of such,
so explored very fast by this algorithm,robustness scores that concern discrete variables are hard tomanipulate for optimisation algorithm (not continuous)

23 / 31

Table of Contents

1

Refining robustness

2Time staging

3

Coverage-based falsification

24 / 31

Idea

Adimoolam, A., Dang, T., Donzé, A., Kapinski, J., and Jin, X. Classificationand coverage-based falsification for embedded control systems. CAV 2017.

Trade-off between:
define a coverage metric of the input space,alternate between:a global search to classify the search space into zones,
local searches on the promising zones to converge to aminimum.

25 / 31High-level algorithm
Input: tmax
Output: a u such that M(u) 2 ϕ
S = sample N points at random;
R = zones( S );while t < tmax dosubdivide( R );S += biased-sampling( R );S += singularity-sampling( R );S += local-search( R );end
for u in S doif ρ(u) < 0 thenreturn u
end
end
return None
26 / 31Subdivision
Goal: divide the search space into rectangles with different averagerobustnesses.
Input: R a list of rectangles, S a list of sampled points, K athreshold
Output: a list of subdivided rectangles
for r in R dopop(R, r );if |S ∩ r | > K thenH = argmin(ΓH (R, S), H hyperplane);push(R,r ∩ H − ,r ∩ H + );endendP
Γ(d,r ,p) (R, S) = x∈S∩R e(d,r ,p) (x)e(d,r ,p) (x) = max{p(ρ(x) − µ)(xd − r ), 0}

27 / 31

Samplings
Biased sampling
Goal: increase coverage and decrease robustness.
Idea: sample according to a weighted sum of two distributions:
Pci : proportional to the numbers of unoccupied cells inrectangle Ri ,Pri : takes into consideration how the robustness of sampled
points varies from the average.

Singularity sampling
Goal: sample more in rectangles with “singular” samples(robustness much lower than average in rectangle).

28 / 31

Local search

Goal: converge to a minimum faster by using local search with agood seed.

29 / 31Experimental results

Interpretation: other methods got caught in local minima.

30 / 31

Conclusion

different notions of robustness:
can be more expressive
can make algorithms more efficient

time staging:
explores morehence can resolve harder problems

coverage-based falsification:
theoretical result (if there exists an ε-robust counterexample,
there is a grid size such that will find it)
coverage helps falsification by exploring more, thus avoiding
local minima

31 / 31