arXiv:1803.06276v2 [cs.SY] 6 Apr 2018

Two-Layered Falsification of Hybrid Systems Guided by
Monte Carlo Tree Search
Zhenya Zhang

Ichiro Hasuo

zhangzy@nii.ac.jp
National Institute of Informatics

hasuo@nii.ac.jp
National Institute of Informatics

Gidon Ernst

Sean Sedwards

gidon@nii.ac.jp
National Institute of Informatics

University of Waterloo
sean.sedwards@uwaterloo.ca

ABSTRACT
Not many real-world hybrid systems are amenable to formal verification, due to their complexity and black box components. Optimizationbased falsification—a methodology of search-based testing that employs stochastic optimization—is thus attracting attention as an alternative quality assurance method. Inspired by the recent work that advocates coverage and exploration in falsification, we introduce a twolayered optimization framework that uses Monte Carlo tree search
(MCTS), a popular machine learning technique with solid mathematical and empirical foundations (e.g. in computer Go). MCTS
is used in the upper layer of our framework; it guides the lower
layer of local hill-climbing optimization, thus balancing exploration
and exploitation in a disciplined manner. We demonstrate the proposed framework through experiments with benchmarks from the
automotive domain.

Figure 1: From Boolean to robust semantics

of CPS: in the form of hybrid systems they comprise the discrete
dynamics of computers and the continuous dynamics of physical
components. Continuous dynamics combined with other features,
such as complexity (a modern car can contain 108 lines of code)
and black-box components (such as parts coming from external
suppliers), make it very hard to apply formal verification to CPS.
CCS CONCEPTS
An increasing number of researchers and practitioners are there•Computer systems organization → Embedded and cyber-physicalfore turning to optimization-based falsification as a quality assurance
systems; •Mathematics of computing → Stochastic control
measure for CPS. The problem is formalized as follows.
and optimization; •Theory of computation → Random search
heuristics;
The falsification problem

KEYWORDS
cyber-physical system, hybrid system, testing, falsification, stochastic optimization, temporal logic
ACM Reference format:
Zhenya Zhang, Ichiro Hasuo, Gidon Ernst, and Sean Sedwards. 2018. TwoLayered Falsification of Hybrid Systems Guided by
Monte Carlo Tree Search. In Proceedings of ACM International Conference on
Embedded Software, Torino, Italy, September 2018 (EMSOFT’18), 11 pages.
DOI:

1

INTRODUCTION

Hybrid Systems. Quality assurance of cyber-physical systems (CPS)
is a problem of great interest. Errors in CPS, such as cars and aircraft,
can lead to economic and social damage, including loss of human
lives. Unique challenges in quality assurance are posed by the nature
Permission to make digital or hard copies of part or all of this work for personal or
classroom use is granted without fee provided that copies are not made or distributed
for profit or commercial advantage and that copies bear this notice and the full citation
on the first page. Copyrights for third-party components of this work must be honored.
For all other uses, contact the owner/author(s).
EMSOFT’18, Torino, Italy
© 2018 Copyright held by the owner/author(s). .
DOI:

• Given: a model M (that takes an input signal u and yields
an output signal M(u)), and a specification φ (a temporal formula)
• Answer: error input, that is, an input signal u such that the
corresponding output M(u) violates φ
u
/ M M(u) /
6 |= φ ?
In the optimization-based falsification approach, the above falsification problem is turned into an optimization problem. This is possible
thanks to robust semantics of temporal formulas [16]. Instead of
the Boolean satisfaction relation v |= φ, robust semantics assigns
a quantity Jv, φK ∈ R ∪ {∞, −∞} that tells us, not only whether
φ is true or not (by the sign), but also how robustly the formula is
true or false. This allows one to employ hill-climbing optimization
(see Fig. 1): we iteratively generate input signals, in the direction
of decreasing robustness, hoping that eventually we hit negative
robustness.
Optimization-based falsification is a subclass of search-based testing: it adaptively chooses test cases (input signals u) based on previous observations. One can use stochastic algorithms for optimization, such as simulated annealing (SA), Global Nelder-Mead (GNM)
and covariance matrix adaptation evolution strategy (CMA-ES [5]),

EMSOFT’18, September 2018, Torino, Italy
which turn out to be much more scalable than model checking algorithms that rely on exhaustive search. Note also that the system
model M can be black box: observing the correspondence between
input u and output M(u) is enough. Observing an error M(u 0 ) for
some input u 0 is sufficient evidence for a system designer to know
that the system needs improvement. Besides these practical advantages, optimization-based falsification is an interesting topic from a
scientific point of view, combining formal and structural reasoning
with stochastic optimization.
The approach of optimization-based falsification was initiated
in [16] and has been actively pursued ever since [1, 3, 4, 10–13, 15,
29, 37, 38]. See [27] for a recent survey. There are now mature tools,
such as Breach [11] and S-Taliro [4], which work with industrystandard Simulink models.
The Exploration-Exploitation Trade-off in Falsification. In the study
of optimization-based falsification, the important role of coverage is
advocated by many authors [1, 10, 13, 29] (see also §5). One reason
is that in highly nonconvex optimization problems for falsification,
eager hill climbing can easily be trapped in local minima and thus
fail to find an error input (i.e. a global minimum) that exists elsewhere. Another reason is that coverage gives a certain degree of
confidence for absence of error input, in case search for error input
is unsuccessful.
This puts us in the exploration-exploitation trade-off,1 a typical
dilemma encountered in stochastic optimization and machine learning (more specifically in reinforcement/active learning). While exploitation guides us to pursue the direction that seems promising
based on the previous observations, we have to occasionally explore
in order to increase coverage and avoid local minima. Many common
stochastic hill-climbing algorithms, such as SA, GNM and CMA-ES,
contain implicit exploration mechanisms. At the same time, explicit methods for exploration in falsification have been pursued e.g.
in [1, 10, 13, 29] (see §5).
Contribution: Two-Layered Optimization for Falsification Guided by
Monte Carlo Tree Search. Our main contribution is, in the context of
hybrid system falsification, to balance exploration and exploitation in
a systematic and mathematically disciplined way using Monte Carlo
tree search (MCTS) [6, 28]. We integrate hill-climbing optimization
in MCTS, and obtain a two-layered optimization framework.
MCTS uses a search tree whose nodes are organized typically
according to causal relationships, and interleaves search (walking
down the already expanded tree, in a promising direction) with
playout (expanding a new node and estimating its reward). Typical
applications that allow such structured a search space are decision
problems such as games. In particular, MCTS currently attracts a lot
of attention thanks to its remarkable success in computer Go [36].
One principal cause for the success of MCTS is search strategies2 that
nicely balance exploration and exploitation. For example, the most
common search strategy called UCT (upper confidence tree [28]) is
derived from a solid theoretical background, namely the upper confidence bounds (UCB) strategy for the multi-armed bandit problem.
While MCTS is a relatively recent methodology, it has established

1 Also

called the variance-bias compromise in the literature.
called tree policies in the MCTS literature.

2 Often

Zhenya Zhang, Ichiro Hasuo, Gidon Ernst, and Sean Sedwards

Figure 2: Our two-layered optimization framework
vehicle speed

throttle
u1

v

u3
u2

u4
time

time

Figure 3: A piecewise constant input signal (one-dimensional,
throttle, left) for a simple automotive powertrain model, and
the corresponding output signal (one-dimensional, vehicle
speed, right).

its position in the rapidly growing community of machine learning.
See [6] for a survey.
Our framework uses robustness values as rewards in MCTS, and
employs hill-climbing optimization for playout in MCTS. This way
we integrate hill-climbing in Monte Carlo tree search in a systematic
way. In our two-layered framework (Fig. 2), the upper optimization
layer picks (by MCTS) a region in the input space, from which a
concrete input value should be sampled. The lower layer then picks
(by hill-climbing) an optimal concrete input value within the prescribed region. We also compute the robustness of the specification
under the chosen input. This value is fed back to the upper layer as
a reward, which is then used by the tree search strategy to balance
exploration and exploitation.
In our two-layered framework, hill-climbing optimization—whose
potential in falsification of hybrid systems has been established,
see e.g. [27]—is supervised by MCTS, with MCTS dictating which
region to sample from. By expanding new children, MCTS can
tell hill-climbing optimization to try an input region that has not
yet explored, or to exploit and dig deep in a direction that seems
promising. Such combination of MCTS and application-specific
lower-layer optimization seems to be a useful methodology that can
apply to problems other than hybrid system falsification. See §5 for
further discussion.
Our use of MCTS depends on our time-staged approach to falsification [? ], in which we synthesize K input segments one after
another. Our use of MCTS depends on incrementally synthesizing K
input segments one after another. Those input segments are for the
(K −1)T
time intervals [0, TK ), [ TK , 2T
K ), . . . , [ K ,T ], where T is the time
horizon. The Monte Carlo search tree will then be of depth K. See
Fig. 3. In this paper we restrict input signals to piecewise-constant
ones (this is a common assumption in falsification); an edge in the

Falsification of Hybrid Systems by Monte Carlo Tree Search
MCTS search tree from depth i − 1 to i (see Fig. 2) determines the
(i−1)T
input value ui for the interval [ K , iT
K ).
We have implemented our two-layered falsification framework in
MATLAB, building on Breach [11].3 Our experiments with falsification benchmarks from [23, 26] demonstrate the possible performance
improvements, especially in the ability of finding rare counterexamples.
Organization. In §2 we formulate the falsification problem. In §3
we present our main contribution, namely a two-layered optimization framework for falsification that combines MCTS and hill-climbing.
Our experimental results are in §4. In §5 we discuss related work,
locating the current work in the context of falsification and also of
other applications of MCTS and related machine learning methods.
In §6 we conclude with some directions of future research.
Notations. The set of (positive, nonnegative) real numbers is denoted by R (and R+ , R ≥0 , respectively). Closed and open intervals
are denoted such as [0, 2] and (2, 3); [0, 2) = {x ∈ R | 0 ≤ x < 2} is a
half-closed half-open interval. For a set X , |X | denotes its cardinality.

2

PROBLEM: HYBRID SYSTEM
FALSIFICATION

EMSOFT’18, September 2018, Torino, Italy
f : Rn → R, x 1 , . . . , x n ∈ Var, and I is a closed non-singular interval
in R ≥0 , i.e. I = [a, b] or [a, ∞) where a, b ∈ R and a < b.
We omit subscripts I for temporal operators if I = [0, ∞). Other
common connectives like ∨, →, >, I (always) and ^I (eventually),
are introduced as abbreviations: ^I φ ≡ > UI φ and I φ ≡ ¬^I ¬φ.
Atomic formulas like f (®
x) ≤ c, where c ∈ R is a constant, are also
accommodated by using negation and the function f 0 (®
x) := f (®
x) −c.
Definition 2.4 (robust semantics [12]). For an n-dimensional signal
w : R ≥0 → Rn and t ∈ R ≥0 , wt denotes the t-shift of w, that is,
wt (t 0 ) := w(t + t 0 ).
Let w : R ≥0 → RN be a signal (recall N = |Var|), and φ be an STL
formula. We define the
Jw, φK ∈ R ∪ {∞, −∞} as follows,
d robustness
Ã
by induction. Here and denote infimums and supremums of
real numbers, respectively. Their binary version u and t denote
minimum and maximum.

Jw, f (x 1 , · · · , x n ) > 0K := f w(0)(x 1 ), · · · , w(0)(x n )
Jw, ⊥K := −∞
Jw, ¬φK := −Jw, φK
Jw, φ 1 ∧ φ 2 K := Jw, φ 1 K u Jw, φ 2 K

d
Ã
0
Jw, φ 1 UI φ 2 K := t ∈I Jwt , φ 2 K u t 0 ∈[0,t ) Jwt , φ 1 K

Here are some intuitions and consequences of the definition. The
robustness Jw, f (®
x) > cK stands for the vertical margin f (®
x) − c for
We formulate the problem of hybrid system falsification. We also
the signal w at time 0. A negative robustness value indicates how
introduce robust semantics of temporal logics [12, 16] that allows
far the formula is from being true. The robustness for the eventually
Ã
us to reduce falsification to an optimization problem.
modality is computed by Jw, ^[a,b] (x > 0)K = t ∈[a,b] w(t)(x).
The original semantics of STL is Boolean, given by a binary relaDefinition 2.1 (time-bounded signal). Let T ∈ R+ be a positive
tion
|= between signals and formulas. The robust semantics refines
real. An m-dimensional signal with a time horizon T is a function
the Boolean one, in the sense that: Jw, φK > 0 implies w |= φ, and
w : [0,T ] → Rm .
Jw, φK < 0 implies w 6 |= φ, see [16, Prop. 16]. Optimization-based falLet w : [0,T ] → Rm and w 0 : [0,T 0 ] → Rm be m-dimensional
sification via robust semantics hinges on this refinement. Although
0
0
m
signals. Their concatenation w · w : [0,T + T ] → R is an mthe definitions so far are for time-unbounded signals only, we note
0
dimensional signal defined by (w · w )(t) := w(t) if t ∈ [0,T ], and
that the robust semantics Jw, φK, as well as the Boolean satisfaction
w 0 (t − T ) if t ∈ (T ,T + T 0 ].
LetT1 ,T2 ∈ (0,T ] such thatT1 < T2 . The restriction w|[T1,T2 ] : [0,T2 − w |= φ, allows straightforward adaptation to time-bounded signals
(Def. 2.1).
T1 ] → Rm of w : [0,T ] → Rm to the interval [T1 ,T2 ] is defined by
Finally, here is a formalization of the falsification problem. It
(w|[T1,T2 ] )(t) := w(T1 + t).
refines the description in §1. In particular, its use of real-valued
Definition 2.2 (system model M). A system model, with M-dimensional robust semantics enables use of hill-climbing optimization. See
input and N -dimensional output, is a function M that takes an input
Fig. 1.
signal u : [0,T ] → RM and returns a signal M(u) : [0,T ] → RN .
Definition 2.5 (falsifying input). Let M be a system model, and φ
Here the common time horizon T ∈ R+ is arbitrary.
be an STL formula. A signal u : [0,T ] → RM is a falsifying input if
Some recent works including [24] use sequences of time-stamped
JM(u), φK < 0 (that implies M(u) 6 |= φ).
values as basic objects in their problem formulation, in place of
continuous-time signals (as we do in the above). This difference is
3 TWO-LAYERED OPTIMIZATION
mostly presentational and not essential.
FRAMEWORK WITH MCTS
As a specification language we use signal temporal logic (STL) [32].
In this section we present our main contribution, namely a twoWe do so for simplicity of presentation; we can also use more exlayered optimization framework for hybrid system falsification. It
pressive logics such as the one in [2].
combines: Monte Carlo tree search (MCTS) [6, 28] (the upper layer)
In what follows Var is the set of variables, and we let N := |Var|.
for high-level planning; and hill-climbing optimization (such as SA,
Variables stand for physical quantities, control modes, etc. ≡ denotes
GNM and CMA-ES, the lower layer) for local input search (see Fig. 2
syntactic equality.
for a schematic overview). The upper layer steers the lower by the
UCT strategy [28], an established method in machine learning for
Definition 2.3 (syntax). In STL, atomic propositions and formulas

balancing exploration (i.e. coverage) and exploitation.
are defined as follows, respectively: α ::≡ f (x 1 , . . . , x n ) > 0 , and
We present two algorithms: the basic two-layered algorithm (Alφ ::≡ α | ⊥ | ¬φ | φ ∧ φ | φ UI φ. Here f is an n-ary function
gorithm 1), and the one enhanced with progressive widening (Al3 Code obtained at https://github.com/decyphir/breach.
gorithm 3). The auxiliary functions used therein are presented in

EMSOFT’18, September 2018, Torino, Italy

Zhenya Zhang, Ichiro Hasuo, Gidon Ernst, and Sean Sedwards

Figure 4: Our MCTS search tree, for a system model M with two input values (throttle and brake) whose ranges are [0, 100] and
[0, 325], respectively. We partition each interval to two (i.e. L 1 = L 2 = 2); thus the branching degree |A| is 2 × 2.

Figure 5: Playout by hill-climbing optimization
Algorithm 2. Our algorithms work on an MCTS search tree; its example is shown in Fig. 4.

3.1

The Basic Two-Layered Algorithm (Alg. 1)

We start with Algorithm 1, using the example in Fig. 4.
Time Staging. We search for a falsifying input signal, focusing on
piecewise-constant signals (Fig. 3, left). The interval [0,T ] is divided
into K intervals of the same size (here K is a tunable parameter). The
(K −1)T
time points 0, TK , 2T
—at which those intervals start—
K ,...,
K
are called control points. Our goal is therefore to find a sequence
u1 , . . . , uK , where each ui = (ui1 , . . . , ui M ) is an M-dimensional
real vector (M is the number of input for the model M), so that the
corresponding piecewise-constant signal is a falsifying one (Def. 2.5).
We assume intervals Ii = [uimin , uimax ] (i ∈ {1, . . . , M }) for the
ranges of input u 1 , . . . , u M of the model M.
The Search Tree. A search tree in MCTS has a branching degree
|A|, where the set A is called an action set in the MCTS literature. In
Go, for example, an action set A consists of possible moves.

We use, as the action set A, a partitioning of the input space
I 1 × · · · × I M . We partition the input space into L 1 × · · · × L M
hypercubes of the equal size, according to predetermined parameters
L 1 , . . . , L M . In Fig. 4 we present an example where M = 2 and
L 1 = L 2 = 2. There we have four actions in the set A, corresponding
to the four square regions in the figure.
An edge in our search tree represents a choice of an input region—
from which we choose the input value ui from—for a single control
(i−1)T
point K . The depth of the tree is K (the number of control
points). We follow the usual convention and specify a node of a
|A|-branching tree by a word w = a 1a 2 . . . a j over the alphabet A
(here j ≤ K). That is: the root is ε (the empty word), its child in the
direction a 1 ∈ A is a 1 , its children are a 1a 1 , a 1a 2 , . . . , and so on.
In general, a node in an MCTS search tree are decorated by two
values: reward R and visit count N . In our case a reward is given by
the estimate of the smallest (i.e. the best) robustness value.
Monte Carlo Tree Search Sampling. Much like usual MCTS, Algorithm 1 iteratively expands the search tree T . Initially the tree T is
root-only (Line 3), and in each iteration—called MCTS sampling—the

Falsification of Hybrid Systems by Monte Carlo Tree Search
Algorithm 1 Basic Two-Layered Algorithm
Require: a system model M, an STL formula φ, intervals Ii =
[uimin , uimax ] (i ∈ {1, . . . , M }) for the ranges of input u 1 , . . . , u M
of M, time horizon T ∈ R+ , and the following tunable parameters: the number K of control points, the number Li of partitions
of the input range [uimin , uimax ] for each i ∈ {1, . . . , M }, and the
scaler c in Line 2 of Algorithm 2
1: function MCTSPreprocess
2:
A ← {1, . . . , L 1 } × · · · × {1, . . . , L M } . the set of actions
3:
T ← {ε}
. the MCTS search tree, initially root-only
4:
N ← (ε 7→ 0) . visit count N initialized, defined only for ε
5:
R ← (ε 7→ ∞)
. reward function R initialized
→
−u ← null
6:
. place holder for a falsifying input
7:
R min ← ∞
. place holder for a minimum reward
→
−a
8:
. the most promising action sequence
min ← null
9:
while R(ε) ≥ 0 and within budget do
10:
MCTSSample(ε)
→
−
11:
if u , null then
. a falsifying input is found already in preprocessing
−u
12:
return →
13:
else
. return the most promising action sequence
−a
14:
return →
min

EMSOFT’18, September 2018, Torino, Italy
Algorithm 2 Auxiliary Functions for Algorithms 1 & 3
1:

2:

3:

4:

16:
17:
18:

19:
20:
21:
22:
23:

24:
25:

function MCTSSample(w)
. let w = a 1 . . . ad with ai ∈ A
N (w) ← N (w) + 1
if |w | < K then
if wa 0 ∈ T for all a 0 ∈ A then
. if all children have been expanded
a ← UCBSample(w)
. pick a child wa by UCB
MCTSSample(wa)
. recursive call
R(w) ← mina 0 ∈A R(wa 0 )
. back-propagation
else
randomly sample a ∈ A from {a | wa < T }
. expand a random unexpanded child wa
T ← T ∪ {wa}
u1 , . . . , uK
. playout by hill-climbing
JM(u1 . . . uK ), φK
←
arg minHillClimb
u1 ∈Reg(a 1 ), ...,ud ∈Reg(ad ),
ud +1 ∈Reg(a),
ud +2, ...,uK ∈I 1 ×···×I M

26:
27:
28:

29:
30:
31:

32:
33:
34:
35:
36:
37:

N (wa) ← 0;
R(wa) ← JM(u1 . . . uK ), φK
if R(wa) < 0 then
→
−u ← u . . . u
1
K
−u
. a falsifying input is found and stored in →
if R(wa) < R min then
→
−a
R min ← R(wa);
min ← a 1 . . . ad a
0
R(w) ← mina 0 ∈A R(wa )
. back-propagation
function Main
→
−x ← MCTSPreprocess
−u , an input signal then
−x = →
if →
. Line 11
−u
return →
−x = a a . . . a 0 ∈ A∗ with some K 0 ≤ K, Line 13
else . →
1 2
K
return
arg minHillClimb
JM(u1 . . . uK ), φK
u1 ∈Reg(a 1 ), ...,uK 0 ∈Reg(a K 0 ),
uK 0 +1, ...,uK ∈I 1 ×···×I M

s

2 ln N (w) ª
R(wa)
©
return arg max ­ 1 −
®
0) + c
0
max
R(w
N (wa)
w
∈T
a ∈A
«
¬
function Reg(a)
. The input region for an action a
. a ∈ A is of theh form (k 1 , . . . , k M ), see Line 2 of Algorithm 1
ÎM
return i=1
uimin + kLi −1
(uimax − uimin ) ,
i

uimin + Lkii (uimax − uimin )

Algorithm 3 Two-Layered Algorithm with Progressive Widening
Require: The same data as required in Algorithm 1, and additionally, constants C, α (used in Line 4)
The algorithm is the same as Algorithm 1, except that the function MCTSSample is replaced by the following one.
1:
2:
3:

15:

function UCBSample(w)

4:

5:
6:
7:
8:
9:

10:

function MCTSSample(w)
. let w = a 1 . . . ad with ai ∈ A
N (w) ← N (w) + 1
if |w | <
 K then

{a 0 ∈ A | wa 0 ∈ T } ≥ C · N (w)α
if
then
or wa 0 ∈ T for all a 0 ∈ A
. progressive widening: all or enough children expanded
a ← UCBSample(w)
. pick a child wa by UCB
MCTSSample(wa)
. recursive call
R(w) ← mina 0 ∈A R(wa 0 )
. back-propagation
else
Ð
S ← (a maximal convex subset of wa 0 <T Reg(a 0 ))
u1 , . . . , u K
. playout by hill-climbing
←
arg minHillClimb
JM(u1 . . . uK ), φK
u1 ∈Reg(a 1 ), ...,ud ∈Reg(ad ),
ud +1 ∈S,
ud +2, ...,uK ∈I 1 ×···×I M

11:
12:
13:
14:
15:
16:
17:
18:


a ← a ∈ A such that ud +1 ∈ Reg(a)
T ← T ∪ {wa}
N (wa) ← 0;
R(wa) ← JM(u1 . . . uK ), φK
if R(wa) < 0 then
→
−u ← u . . . u
1
K
if R(wa) < R min then
→
−a
R min ← R(wa);
min ← a 1 . . . ad a
0
R(w) ← mina 0 ∈A R(wa )
. back-propagation

invocation of the function MCTSSample on Line 10 adds one new
node to T . (In the MCTS literature, expanding a child means adding
the child to T .) We repeat MCTS sampling until a counterexample
is found, or the budget is used up (Line 9).
The exploration-exploitation trade-off in MCTS is in the choice
of the node to add. In each MCTS sampling, we start from the
root (Line 10), walk down in the tree T choosing already expanded
children (Lines 19–20), until we expand a child (Lines 23–24). Here,
growing a wider tree means exploration, while a deeper tree means
exploitation.

EMSOFT’18, September 2018, Torino, Italy

Zhenya Zhang, Ichiro Hasuo, Gidon Ernst, and Sean Sedwards

We use the UCT strategy [28], the most commonly used strategy in MCTS, to resolve the dilemma. UCT is based on the UCB
strategy for the multi-armed bandit problems; Line 2 of Algorithm 2
R(wa)
follows UCB, where the exploitation score 1 − max 0 R(w 0 ) and the
w ∈T
q
2 ln N (w )
exploration score
are superposed using a scaler c. Note
N (wa)
that our rewards R are given by robustness, and that falsification
favors smaller R. Note also that values of R can be greater than 1
R(wa)
in general. In the exploitation score 1 − max 0 R(w 0 ) , therefore,
w ∈T

we normalize rewardsq
to the interval [0, 1] and reverse their order.4
2 ln N (w )

The exploration score
is taken from UCB: the visit count
N (wa)
N (w) tells how many times the node w has been visited, that is, how
many offsprings the node w currently has in T . The scaler, for the
trade-off, is a tunable parameter, as usual in MCTS.
Playout and Back-Propagation. In MCTS, the reward of a newly
expanded node a 1a 2 . . . ad a (see e.g. Line 24) is computed by an
operation called playout. The result is then back-propagated, in a
suitable manner, to the ancestors: a 1 . . . ad , a 1 . . . ad −1 , . . . and
finally ε
In our MCTS algorithms for falsification we use hill-climbing optimization (such as SA, GNM and CMA-ES) for playout. See Line 25,
where input values u1 , u2 , . . . , uK are sampled by stochastic hillclimbing optimization, so that the resulting robustness value of the
specification φ becomes smaller. The regions to sample those values
from are dictated by the MCTS tree: u1 ∈ Reg(a 1 ), . . . , ud ∈ Reg(ad )
follow the actions a 1 , . . . , ad determined so far (here Reg is from
Algorithm 2); ud +1 ∈ Reg(a) follows the newly chosen action a
(Line 23); and the remaining values ud +2 , . . . , uK can be chosen
from the whole input range I 1 × · · · × I M .
See Fig. 5 for an example. Smaller gray squares represent actions,
and red dots represent input values (notice that they are chosen from
the gray regions). The values u1 , . . . , uK are sampled repeatedly so
that the robustness value JM(u1 . . . uK ), φK becomes smaller.
An intuition of this playout operation is that we sample the best
input signal u1 . . . uK , under the constraints imposed by the MCTS
search tree (namely, the input regions prescribed by the actions).
The least robustness value thus obtained is assigned to the newly
expanded node wa as its reward (Line 26). If R(wa) < 0 then this
means we have already succeeded in falsification (Line 28).
Back-propagation is an important operation in MCTS. Following the intuition is that the reward R(w) is the smallest robustness
achievable at the node w, we define the reward of an internal node
w by the minimum of its children’s rewards. See Lines 21 and 31.
Note that, via recursive calls of MCTSSample (Line 20), the result
of playout is propagated to all ancestors.
A Two-Layered Framework. In Algorithm 1, hill-climbing optimization occurs twice, in Lines 25 and 37. The first occurrence is in
playout of MCTS—this way we interleave MCTS optimization (by
growing a tree) and hill-climbing optimization. See Fig. 2. MCTS
optimization is considered to be a preprocessing phase in Algorithm 1
−a
(Line 33): its principal role is to find an action sequence →
min , i.e.

can assume that values of R are nonnegative, since otherwise we have already
obtained a falsifying input signal.

4 We

a sequence of input regions, that is most promising. In the remainder of the Main function, the second hill-climbing optimization is
−a
conducted for falsification, where we sample according to →
min .
The two occurrences of hill-climbing optimization (Lines 25 and 37)
therefore have different roles. Given also the fact that the first occurrence is repeated every time we expand a new child, in our
implementation we allocate a much smaller budget (timeout TOpo
in §4, 5–15 seconds) to the first occurrence than to the second (300
seconds).
−u is often found already in the preprocessing
A falsifying input →
−u (Line 35).
phase. In this case the Main function simply returns →

3.2

The Two-Layered Algorithm with
Progressive Widening (Alg. 3)

Our second algorithm (Algorithm 3) differs from the basic one (Algorithm 1) in the following two points.
Progressive Widening. Algorithm 3 uses progressive widening [9];
see Line 4. Unlike in the basic algorithm (Line 18 of Algorithm 1),
we do not always expand a new child even if there are unexpanded
ones; the threshold C · N (w)α is computed using the visit count
N (w) and tunable parameters C, α.
Progressive widening is a widely employed technique in MCTS for
coping with a large or infinite action set A—in such a case expanding
all children incurs a lot of computational cost. See e.g. [30]. In our
Algorithm 3 the action set A can be quite large, depending on the
numbers L 1 , . . . , Lm of input range partitions.
Hill-Climbing Optimization for Expanding Children.
In progressive widening, since we may
not expand all the
children, it makes
sense to be selecFigure 6: Lines 9–11 of Algorithm 3
tive about which child to expand. This is in contrast with random
sampling in Algorithm 1 (Line 23). See Line 10 of Algorithm 3,
where we first playout by hill-climbing optimization. The value
ud +1 thus obtained is then used to determine which child wa to
expand, in Line 11. In order to ensure that the new child wa is indeed previously unexpanded, the value ud +1 is sampled from the
Ð
set wa 0 <T Reg(a 0 )); in fact we restrict to its convex subset (Line 9)
because many hill-climbing optimization algorithms work best in a
convex domain. See Fig. 6 for illustration.

3.3

Discussion

Our algorithms interleave MCTS optimization and hill-climbing optimization: the latter is used in the playout operation of the former, for
sampling and estimating the reward of a high-level input-synthesis
strategy. This high-level strategy is concretely given by a sequence
a 1a 2 . . . ad of input regions. Via the UCT tree search strategy, we
ensure that our search in a search tree is driven not only by depth
but also by width. This way we enhance coverage in search-based
falsification, in the sense that different regions of the input space
are sampled in a structured and disciplined manner.

Falsification of Hybrid Systems by Monte Carlo Tree Search
In falsification of hybrid systems, it is often the case that simulation, i.e. running a model M under a given input signal, is computationally the most expensive operation. In our algorithm it happens
in Lines 25 and 37, since a hill-climbing optimization algorithm tries
many samples of u1 , . . . , uK . Simplifying Line 25, e.g. by decimating
the control points, can result in a useful variation of our algorithm.
Among the tunable parameters of the algorithm is the scaler c
used for the UCB sampling (Line 2 of Algorithm 2). Having this
parameter is unique to our falsification framework in comparison
to plain robustness guided optimization (with hill-climbing only).
Specifically, the parameter c endows our algorithm with flexibility
in the exploration-exploitation trade-off. Given the diversity of instances of the hybrid system falsification problem, it is unlikely that
there is a single value of c that is optimal for all falsification examples. An engineer can then use her/his expert domain knowledge
about the example to tune the parameter c.

4

EXPERIMENTAL EVALUATION

We have implemented our algorithms—the basic algorithm (Algorithm 1, henceforth called “basic”) and the variation with progressive
widening (Algorithm 3, henceforth called “P.W.”). The implementation is in MATLAB, using Breach [11] as a front-end for hill-climbing
optimization and for its implementation of the robust semantics.
The experiments have two goals. Firstly, in §4.2, we evaluate
the falsification performance of our proposal in comparison to the
state-of-the-art. Since our MCTS enhancement emphasizes coverage,
our interest is in the success rate in hard problem instances rather
than in execution time. Secondly, in §4.3, we evaluate the impact of
different choices of parameters for our algorithms (such as the UCB
scalar c in the Algorithm 2).

4.1

Experiment Setup

The experiments are based on the following benchmarks.
The automatic transmission (AT) model is a Simulink model that
was proposed as a benchmark for falsification in [23]. It has input
signals throttle ∈ [0, 100] and brake ∈ [0, 325], and computes the
car’s speed speed, the engine rotation rpm, and the selected gear gear.
We consider the following specifications, taken in part from [23].
S1 ≡ [0,30] (speed < 120) can be falsified easily by hill-climbing
with an input throttle = 100 and brake = 0 throughout.
S2 ≡ [0,30] (gear = 3 → speed ≥ 20) states that in gear three,
the speed should not get too low. A falsifying trace first has to speed
up to reach the required gear and then brake. The difficulty arises
from the lack of guidance by robustness as long as gear , 3: we
follow [23] and take gear = 1, . . . , gear = 4 as Boolean propositions,
instead of taking gear as a numeric variable. In contrast to [23] where
the speed threshold was 30, here we use a more difficult version
with a threshold of 20. This requires gear three to be reached early,
so that the vehicle can slow down sufficiently within the remaining
time horizon.
S3 ≡ ^[10,30] (speed < [53, 57]) states that it is not possible to
maintain a constant speed in the interval [53,57] after some initial
acceleration. A falsifying trace needs to be precise in the value of
the throttle to stay within these tight bounds. Moreover, the speed
range has to be hit at time 10.

EMSOFT’18, September 2018, Torino, Italy
S4 ≡ [0,10] (speed < 80) ∨ ^[0,30] (rpm > 4500) states that it is
not possible to reach speed 80 within 10 seconds with somewhat
limited rpm. To falsify, the throttle has to be used gently enough not
to exceed the rpm threshold of 4500.
S5 ≡ [0,29] (speed < 100) ∨ [29,30] (speed > 65) is a specification
designed to demonstrate the limitation of robustness-guided falsification by hill-climbing optimization only. Here, a falsifying trajectory
has to reach high speed before braking down again. Similarly to S2,
the speed 100 has to be reached much earlier than indicated time
bound of 29 to give sufficient time for deceleration. However, the
robustness computation shadows either of the disjuncts by using
the maximum as semantics for the ∨-connective.
S6 ≡ [0,30] (rpm < 4770 ∨ [0,1] (rpm > 600)) aims to prevent
systematic sudden drops from high rpm to low ones. It is falsified
if an rpm peak above 4770 is immediately followed by a drop to
rpm ≤ 600.
The second benchmark model is the Abstract Fuel Control (AFC)
model [26]. It takes two input signals, pedal angle and engine speed,
and outputs a critical signal called air-fuel ratio (AF), which influences fuel efficiency and performance of the car. The value is
expected to be close to a reference value AFref . The pedal angle varies in the range [0, 61.1] and the engine speed vary in the
range [900, 1100]. According to [26], this setting corresponds to
normal mode, where AFref = 14.7.
The basic requirement of the AFC is to keep the air-to-fuel ration
AF close to the reference AFref . However, changes to the pedal
angle cause brief spikes in the output signal AF before the controller
is able to regulate the engine. Falsification is used to discover amplitude and periods of such spikes. The formal specifications Sbasic is
[0,30] (¬(|AF − AFref | > 0.005 ∗ 14.7)). This specification is violated
when AF deviates from its AFref too much. Another specification
Sstable is ¬(^[6,26] [0,4] (|AF − AFref | > 0.01 ∗ 14.7)). The goal is
to find spikes where ratio is off by a fraction δ of the reference value
for at least t 0 seconds during the interval [6, 26].
The experiments ran Breach version 1.2.9 and MATLAB R2017b
on an Amazon EC2 c4.large instance (March 2018, 2.9 GHz Intel
Xeon E5-2666, 2 virtual CPU cores, 4 GB main memory).

4.2

Performance Evaluation

The results are shown in Table 1 and are grouped with respect
to the method: Breach as a baseline, our basic algorithm (“Basic,”
Algorithm 1) and its variation with progressive widening (“P.W.,”
Algorithm 3), as well as the underlying hill-climbing optimization
solver (CMA-ES, GNM and SA). Run times are shown in seconds.
Since the algorithms are stochastic, we give the success rate out of a
number of trials.
For all the experiments, an input signal is chosen to be piecewise
constant with K = 5 control points; and the number coincides with
the depth of the MCTS search tree. The timeout for Breach was
set to 900 seconds (which is well above all successful falsification
trials) with no upper limit on the number of simulations. For our
P.W. algorithm, we used the parameters C = 0.7 and α = 0.85 (Line 4
of Algorithm 3).
The choice of parameters for our two MCTS-based algorithms is
as follows: for each combination with the hill-climbing optimization
solvers, we present a set of parameters that gave good results over

EMSOFT’18, September 2018, Torino, Italy

Zhenya Zhang, Ichiro Hasuo, Gidon Ernst, and Sean Sedwards

Table 1: Comparison of Breach against Algorithms 1 (Basic) and Algorithm 3 (P.W.). For each specification, we show the success
rate out of 10 trials, and the average run time (in seconds) of those trials which were successful. The respective parameters are shown in the
leftmost columns: #sim is the maximum visit count for the root of the MCTS search tree (i.e. the maximum number of nodes of the tree); TOpo
(in seconds) is the timeout (wall-clock) for each individual MCTS playout by hill-climbing optimization. L is the partitioning of the input
space with respect to each dimension ((throttle, brake) for AT and (pedal, engine) for AFC); c is the scaler for the exploration-exploitation
trade-off in UCB (Algorithm 2). The number K of control points is 5 for all the specifications. For progressive widening (Algorithm 3) we use
the parameters C = 0.7 and α = 0.85. Timeout for the hill-climbing in the end (Line 37 of Algorithm 1) is 300 seconds.
Parameters

CMA-ES

c

Breach
Basic
P.W.

40
40

10/10
15 3 × 5 0.20 10/10
15 2 × 2 0.20 10/10

GNM

L

S1
succ. time

Breach
Basic
P.W.

20
20

10/10
5 3 × 5 0.20 10/10
5 3 × 5 0.05 10/10

SA

Algorithm #sim TOpo

The AT model

Breach
Basic
P.W.

20
40

The AFC model
S2
succ. time

S3
succ. time

S4
S5
succ. time succ. time

21.9 6/10 30.3 10/10 193.9 10/10
15.8 10/10 108.5 10/10 697.1 10/10
10.8 10/10 56.3 9/10 620.8 10/10

26.4
63.5
21.7

5.4 10/10 151.4 0/10
- 10/10 349.3
12.4 10/10 162.3 10/10 185.6 10/10 22.6
60.8 9/10 110.7 8/10 211.2 10/10 34.4

10/10 160.1 0/10
15 3 × 5 0.05 10/10 264.8 9/10 236.1
15 3 × 5 0.20 10/10 208.7 10/10 377.6

3/10 383.7 10/10 58.5
8/10 385.6 10/10 119.8
8/10 666.0 10/10 84.0

all the specifications. This is justified, because the performance is
quite dependent on these parameters, and one choice that works for
a given combination of a falsification algorithm and a hill-climbing
solver might just not work for another combination. However, note
that we do not change the settings across the specifications.
As we discussed at the end of §3.1, different budgets are allocated
to hill-climbing in playout (Line 25 of Algorithm 1) and to hillclimbing in the end (Line 37 of Algorithm 1). Specifically, the timeout
for the former is TOpo in Table 1 (5–15 seconds) while the timeout
for the latter is globally 300 seconds.
The results in Table 1 indicate, at a high-level, that for seemingly
hard problems, the benefit of the extra exploration done by the
MCTS layer significantly increases the falsification rate. This is most
evident in S5 and S6, where Breach (with any of CMA-ES, GNM or
SA) has at most 30–40% success rates. Our MCTS enhancements
succeed much more often.
For easy problems, the increased exploration typically increases
the falsification times somewhat, which is expected. One reason
is that falsification is in general a hard problem that can only be
tackled by heuristics. There is generally no single algorithm that
works on all instances equally well. For example, for S1, S4 and
Sbasic we observe that our algorithms can take longer than Breach.
We also note that the additional execution time is not prohibitively
large.
The choice of a hill-climbing optimization solver has a great influence on the outcome. CMA-ES has built-in support for some
exploration before the search converges in the most promising direction. Nevertheless we see that the upper-layer optimization by
MCTS can improve success rates (S5, S6, Sstable). The Nelder-Mead
variant GNM has very little support for exploration and furthermore,
Breach’s implementation is not stochastic (it uses deterministic lowdiscrepancy sequences as a source of quasi-randomness). For this
reason, the method quickly converges to non-falsifying minima that
are local and cannot be escaped without extra measures. Thus using

4/10 208.8
7/10 786.8
9/10 653.8

S6
succ. time

Sbasic
Sstable
succ. time succ. time

3/10 75.5 10/10
9/10 384.4 10/10
9/10 322.0 10/10

16.9
2.5
2.4

3/10 256.3
7/10 336.9
6/10 128.0

0/10
- 0/10
- 10/10
9.8
7/10 261.9 7/10 163.7 10/10 119.8
8/10 313.0 10/10 178.7 10/10 120.1

0/10
2/10 378.5
6/10 153.2

0/10
- 3/10 80.4 10/10
8/10 505.3 7/10 341.2 10/10
7/10 795.4 10/10 624.2 10/10

6/10 307.0
8/10 273.8
6/10 293.7

9.24
8.2
7.2

MCTS pays off especially with GNM; see for example S3 and S5.
Conversely, Simulated Annealing (SA) heavily relies on exploration
and keeps just a single good trace found so far, limiting it’s exploitation. In combination with MCTS, SA shows mixed performance. In
some cases falsification time becomes longer (S1, S3), whereas for
S5, MCTS is able to overcome this particular limitation, presumably
as it maintains several good prefixes.
The difference between the two variants, Algorithms 1 and 3 (the
latter with progressive widening), is not significant on most of the
examples. However, progressive widening has a positive effect on
the success rate and falsification time for S6 for GNM and SA.
In the experiments we set the maximum size of an MCTS search
tree (#sim) to be 20–40. Note that the number of all possible nodes
is way greater: it is (1 + |A| + |A| 2 + + |A| K ), which is 1365 when
L = 2 × 2 and 813616 when L = 3 × 5. The overall success rates seem
to suggest that, not only in computer Go but also in hybrid system
falsification, MCTS is very effective in searching in a vast space with
a limited budget.

4.3

Evaluation of Parameter Choices

We evaluate the effect of the parameters using the specification S5
for the AT model, where the success of falsification varies strongly.
For the experiments in this section we focus on Algorithm 1 (Basic).
Table 2 shows the results for the different optimization solvers
when varying the scaler c (for the UCB sampling, Line 2 of Algorithm 2). The first observation is a general trend that falsification
rate improves with increased focus on exploration. In particular, the
GNM algorithm benefits strongly from the added exploration. One
could also argue that since CMA-ES does already explore on its own,
too much focus on exploration in the MCTS layer is counterproductive (compare c = 0.5 to c = 1.0).
Table 3 shows the results for different partitioning of the input
space, where L = n × m means that the throttle range is partitioned
into n actions and the brake range into m actions (for the AT model;

Falsification of Hybrid Systems by Monte Carlo Tree Search
pedal and engine for the AFC model). We note that the different
choices have by far less influence than the scaler c. However, there
are some differences, for example GNM seems to cope badly with
the coarse partitioning 2 × 2 in the first column, which could be
attributed to its reliance on guidance by the MCTS layer.

5

RELATED WORK

Formal verification approaches to correctness of hybrid systems
employ a wide range of techniques from model checking, theorem
proving, rigorous numerics, nonstandard analysis, and so on [7, 14,
17, 18, 20, 22, 35]. Currently these are not very successful in dealing
with complex real-world systems, due to issues like scalability and
black-box components.
Optimization-based falsification of hybrid systems therefore attracts attention, as a testing technique that adaptively searches for
error input using algorithms from recent advances in machine learning. An overview is given in [27].
We now discuss the relationship between the current work and
existing works in the context of falsification.
Monte Carlo sampling is used in [33] for falsification. Our thesis is
that Monte Carlo tree search—an extension of Monte Carlo methods—
yields a powerful guiding method in optimization-based falsification.
The so-called multiple-shooting approach to falsification is studied
in [38]. It consists of: an upper layer that searches for an abstract
error trace given by a succession of cells; and a lower layer where an
abstract error trace is concretized to an actual error trace by picking
points from cells. This two-layered framework differs from ours: they
focus on safety specifications (avoiding an unsafe set); this restriction
allows search heuristics that relies on spacial metrics (such as A∗
search). In our current work, we allow arbitrary STL specifications,
and we use robustness values as guidance. Our framework can be
seen as an integration of multiple-shooting (the upper layer) and
single-shooting (the lower layer); they are interleaved in the same
way as search and sampling are interleaved in MCTS.
Besides MCTS, Gaussian process learning (GP learning) attracts attention in machine learning as a clean way of balancing exploitation
and exploration. The GP-UCB algorithm is a widely used strategy
there. Its use in hybrid system falsification is pursued e.g. in [3, 37].
The value of exploration/coverage has been recognized in the
falsification community [1, 10, 13, 29], not only for efficient search
for error inputs, but also for correctness guarantees in case no error
input is found. In this line, the closest to the current work is [1] in
which search is guided by a coverage metric on input spaces. The
biggest difference in the current work is that we structure the input
space by time, using time stages (see Fig. 3). We explore this staged
input space in the disciplined manner of MCTS. In [1] there is no
such staged structure in input spaces, and they use support vector
machines (SVM) for identifying promising regions.
Tree-based search is also used in [13] for falsification. They use
rapidly-exploring random trees (RRT), a technique widely used in
path planning in robotics. Their use of trees is geared largely towards exploration, using the coverage metric called star discrepancy
as guidance. In their algorithm, robustness-guided hill-climbing
optimization plays a supplementary role. This is in contrast to our
current framework, where we use MCTS and systematically integrate it with hill-climbing optimization.

EMSOFT’18, September 2018, Torino, Italy
Many works in coverage-guided falsification [13, 29] use coverage
metrics in the space of output or internal states, instead of the input
space. A challenge in such methods is that, in a complex model, the
correlation between input and output/state is hard to predict. It is
hard to steer the system’s output/state to a desired region.
There have been efforts to enhance expressiveness of MTL and
STL, so that engineers can express richer intentions—such as time
robustness and frequency—in specifications [2, 34]. This research
direction is orthogonal to ours; we shall investigate use of such
logics in the current framework. Other recent works with which
our current results could be combined include [24], which mines
parameter regions, and [15] that aims to exploit features of machine
learning components of system models for the sake of falsification.
We believe that the combination of MCTS and application-specific
lower-layer optimization—an instance of which is the proposed falsification framework—is a general methodology applicable to a variety
of applications. For example, for the MaxSAT problem, the work [21]
uses MCTS combined with hill-climbing local optimization.
Use of MCTS for search-based testing of hybrid systems is pursued
in [30]. We differ from [30] in the target systems: ours are deterministic, while [30] searches for random seeds for stochastic systems.
We also combine robustness-guided hill-climbing optimization.
Our use of time-ordered MCTS search trees can be seen as a form
of importance sampling, where we iteratively narrow down a search
space to more promising subspaces. Importance sampling is used
in [25] for rare events in statistical model checking.

6

CONCLUSIONS AND FUTURE WORK

In this work we have presented a two-layered optimization framework for hybrid system falsification. It combines Monte Carlo tree
search—a widely used method in machine learning for effective
stochastic search, balancing exploration and exploitation—and hillclimbing optimization—a local search method whose use in hybrid
system falsification is established in the community. Our experiments suggest its promising performance.
In §5 we already indicated some directions for future work. Further future directions are as follows.
In this work we demonstrated by experiments how coverage and
exploration can improve the chances of finding error input. Another
use of exploration, namely as the confidence measure about systems’
validity in case no error input is found (see [1, 13] and §5), should be
further investigated. Concretely, we are interested in computing a
quantitative coverage metric from the result of our MCTS algorithm.
Our choice of grid partitioning for actions in MCTS search trees
achieves good performance while simple. Other choices are possible,
using the extension of MCTS to continuous action sets [8, 9]. The
effect of taking those other choices shall be investigated.
An extension to stochastic hybrid systems does not seem hard,
following the MCTS approach in [30] that uses models with direct
access to randomness seeds (see §5).

ACKNOWLEDGMENTS
The authors are supported by ERATO HASUO Metamathematics for
Systems Design Project (No. JPMJER1603), JST; and Grants-in-Aid
No. 15KT0012, JSPS.

EMSOFT’18, September 2018, Torino, Italy

Zhenya Zhang, Ichiro Hasuo, Gidon Ernst, and Sean Sedwards

Table 2: Parameter Variation for Algorithm 1 (Basic): Exploration/Exploitation through scaler c. Success rate and average time (in
seconds, only successful trials). The other parameters are: input partitioning
L = 3 × 3, maximum tree size #sim = 40, playout timeout TOpo = 5 seconds.

Table 3: Parameter Variation for (Basic): Partitioning of the input space. Success rate and average time (in seconds, only successful trials). With
parameters c = 0.2, #sim = 40, TOpo = 5 seconds.

Solver

c = 0.02
c = 0.05
c = 0.2
c = 0.5
c = 1.0
succ. time succ. time succ. time succ. time succ. time

2×2
3×3
3×5
5×5
succ. time succ. time succ. time succ. time

CMA-ES
GNM
SA

4/10 343.14
0/10
3/10 376.89

8/10
3/10
5/10

6/10 298.08
0/10
7/10 340.15

8/10 333.46
8/10 289.16
5/10 321.60

8/10 362.07
6/10 358.33
7/10 425.70

6/10 348.47
9/10 350.63
9/10 392.08

REFERENCES
[1] Arvind S. Adimoolam, Thao Dang, Alexandre Donzé, James Kapinski, and Xiaoqing
Jin. 2017. Classification and Coverage-Based Falsification for Embedded Control
Systems. In Proc. CAV 2017 (Lecture Notes in Computer Science), Rupak Majumdar
and Viktor Kuncak (Eds.), Vol. 10426. Springer, 483–503.
[2] Takumi Akazaki and Ichiro Hasuo. 2015. Time Robustness in MTL and Expressivity
in Hybrid System Falsification. In Proc. CAV 2015 (Lecture Notes in Computer
Science), Daniel Kroening and Corina S. Pasareanu (Eds.), Vol. 9207. Springer,
356–374.
[3] Takumi Akazaki, Yoshihiro Kumazawa, and Ichiro Hasuo. 2017. Causality-Aided
Falsification. In Proc. FVAV@iFM 2017 (EPTCS), Lukas Bulwahn, Maryam Kamali,
and Sven Linker (Eds.), Vol. 257. 3–18.
[4] Yashwanth Annpureddy, Che Liu, Georgios Fainekos, and Sriram Sankaranarayanan. 2011. S-TaLiRo: A Tool for Temporal Logic Falsification for Hybrid
Systems. Springer Berlin Heidelberg, Berlin, Heidelberg, 254–257.
[5] Anne Auger and Nikolaus Hansen. 2005. A restart CMA evolution strategy with
increasing population size. In Proceedings of the IEEE Congress on Evolutionary
Computation, CEC 2005. IEEE, 1769–1776.
[6] Cameron Browne, Edward Jack Powley, Daniel Whitehouse, Simon M. Lucas,
Peter I. Cowling, Philipp Rohlfshagen, Stephen Tavener, Diego Perez Liebana,
Spyridon Samothrakis, and Simon Colton. 2012. A Survey of Monte Carlo Tree
Search Methods. IEEE Trans. Comput. Intellig. and AI in Games 4, 1 (2012), 1–43.
´
[7] Xin Chen, Erika Abrahám,
and Sriram Sankaranarayanan. 2013. Flow*: An
Analyzer for Non-linear Hybrid Systems. In Computer Aided Verification - 25th
International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013.
Proceedings (Lecture Notes in Computer Science), Natasha Sharygina and Helmut
Veith (Eds.), Vol. 8044. Springer, 258–263.
[8] Adrien Couëtoux, Jean-Baptiste Hoock, Nataliya Sokolovska, Olivier Teytaud,
and Nicolas Bonnard. 2011. Continuous Upper Confidence Trees. In Learning
and Intelligent Optimization - 5th International Conference, LION 5, Rome, Italy,
January 17-21, 2011. Selected Papers (Lecture Notes in Computer Science), Carlos
A. Coello Coello (Ed.), Vol. 6683. Springer, 433–445.
[9] Rémi Coulom. 2007. Computing ”Elo Ratings” of Move Patterns in the Game of
Go. ICGA Journal 30, 4 (2007), 198–208.
[10] Jyotirmoy V. Deshmukh, Xiaoqing Jin, James Kapinski, and Oded Maler. 2015. Stochastic Local Search for Falsification of Hybrid Systems. In Automated Technology
for Verification and Analysis - 13th International Symposium, ATVA 2015, Shanghai,
China, October 12-15, 2015, Proceedings (Lecture Notes in Computer Science), Bernd
Finkbeiner, Geguang Pu, and Lijun Zhang (Eds.), Vol. 9364. Springer, 500–517.
[11] Alexandre Donzé. 2010. Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems. In Computer Aided Verification, 22nd Int. Conf., CAV 2010
(LNCS), Tayssir Touili, Byron Cook, and Paul B. Jackson (Eds.), Vol. 6174. Springer,
167–170.
[12] Alexandre Donzé and Oded Maler. 2010. Robust Satisfaction of Temporal Logic
over Real-Valued Signals. In Proc. FORMATS 2010. , Krishnendu Chatterjee and
Thomas A. Henzinger (Eds.), Vol. 6246. Springer, 92–106.
[13] Tommaso Dreossi, Thao Dang, Alexandre Donzé, James Kapinski, Xiaoqing Jin,
and Jyotirmoy V. Deshmukh. 2015. Efficient Guiding Strategies for Testing of
Temporal Properties of Hybrid Systems. In NASA Formal Methods - 7th International Symposium, NFM 2015, Pasadena, CA, USA, April 27-29, 2015, Proceedings
(Lecture Notes in Computer Science), Klaus Havelund, Gerard J. Holzmann, and
Rajeev Joshi (Eds.), Vol. 9058. Springer, 127–142.
[14] Tommaso Dreossi, Thao Dang, and Carla Piazza. 2016. Parallelotope Bundles for
Polynomial Reachability. In Proceedings of the 19th International Conference on
Hybrid Systems: Computation and Control, HSCC 2016, Vienna, Austria, April 12-14,
2016, Alessandro Abate and Georgios E. Fainekos (Eds.). ACM, 297–306.
[15] Tommaso Dreossi, Alexandre Donzé, and Sanjit A. Seshia. 2017. Compositional
Falsification of Cyber-Physical Systems with Machine Learning Components.
In Proc. NFM 2017. , Clark Barrett, Misty Davies, and Temesghen Kahsai (Eds.),
Vol. 10227. 357–372.

337.46
347.09
405.54

8/10 333.46 8/10 344.77
8/10 289.16 10/10 335.09
5/10 321.60 8/10 416.39

7/10 369.87
8/10 331.65
6/10 381.85

[16] Georgios E. Fainekos and George J. Pappas. 2009. Robustness of temporal logic
specifications for continuous-time signals. Theor. Comput. Sci. 410, 42 (2009),
4262–4291.
[17] Chuchu Fan, Bolun Qi, Sayan Mitra, Mahesh Viswanathan, and Parasara Sridhar
Duggirala. 2016. Automatic Reachability Analysis for Nonlinear Hybrid Models
with C2E2. In Proc. CAV 2016. (Lecture Notes in Computer Science), Swarat
Chaudhuri and Azadeh Farzan (Eds.), Vol. 9779. Springer, 531–538.
[18] Goran Frehse, Colas Le Guernic, Alexandre Donzé, Scott Cotton, Rajarshi Ray,
Olivier Lebeltel, Rodolfo Ripado, Antoine Girard, Thao Dang, and Oded Maler. 2011.
SpaceEx: Scalable Verification of Hybrid Systems. In Computer Aided Verification
- 23rd International Conference, CAV 2011, Snowbird, UT, USA, July 14-20, 2011.
Proceedings (Lecture Notes in Computer Science), Ganesh Gopalakrishnan and Shaz
Qadeer (Eds.), Vol. 6806. Springer, 379–395.
[19] Goran Frehse and Sayan Mitra (Eds.). 2017. Proc. HSCC 2017. .
[20] Sicun Gao, Jeremy Avigad, and Edmund M. Clarke. 2012. δ -Complete Decision
Procedures for Satisfiability over the Reals. In Proc. IJCAR 2012. (Lecture Notes in
Computer Science), Bernhard Gramlich, Dale Miller, and Uli Sattler (Eds.), Vol. 7364.
Springer, 286–300.
[21] Jack Goffinet and Raghuram Ramanujan. 2016. Monte-Carlo Tree Search for the
Maximum Satisfiability Problem. In Proc. CP 2016. (Lecture Notes in Computer
Science), Michel Rueher (Ed.), Vol. 9892. Springer, 251–267.
[22] Ichiro Hasuo and Kohei Suenaga. 2012. Exercises in Nonstandard Static Analysis
of Hybrid Systems, See [31], 462–478.
[23] Bardh Hoxha, Houssam Abbas, and Georgios E. Fainekos. 2014. Benchmarks
for Temporal Logic Requirements for Automotive Systems. In 1st and 2nd International Workshop on Applied veRification for Continuous and Hybrid Systems,
ARCH@CPSWeek 2014, Berlin, Germany, April 14, 2014 / ARCH@CPSWeek 2015,
Seattle, WA, USA, April 13, 2015. (EPiC Series in Computing), Goran Frehse and
Matthias Althoff (Eds.), Vol. 34. EasyChair, 25–30.
[24] Bardh Hoxha, Adel Dokhanchi, and Georgios E. Fainekos. 2018. Mining parametric
temporal logic properties in model-based design for cyber-physical systems. STTT
20, 1 (2018), 79–93.
[25] Cyrille Jégourel, Axel Legay, and Sean Sedwards. 2012. Cross-Entropy Optimisation of Importance Sampling Parameters for Statistical Model Checking, See [31],
327–342.
[26] Xiaoqing Jin, Jyotirmoy V. Deshmukh, James Kapinski, Koichi Ueda, and Kenneth R. Butts. 2014. Powertrain control verification benchmark. In Proc. HSCC
2014. , Martin Fränzle and John Lygeros (Eds.). ACM, 253–262.
[27] J. Kapinski, J. V. Deshmukh, X. Jin, H. Ito, and K. Butts. 2016. Simulation-Based
Approaches for Verification of Embedded Control Systems: An Overview of
Traditional and Advanced Modeling, Testing, and Verification Techniques. IEEE
Control Systems 36, 6 (Dec 2016), 45–64.
[28] Levente Kocsis and Csaba Szepesvári. 2006. Bandit Based Monte-Carlo Planning. In Machine Learning: ECML 2006, 17th European Conference on Machine
Learning, Berlin, Germany, September 18-22, 2006, Proceedings (Lecture Notes in
Computer Science), Johannes Fürnkranz, Tobias Scheffer, and Myra Spiliopoulou
(Eds.), Vol. 4212. Springer, 282–293.
[29] Jan Kurátko and Stefan Ratschan. 2014. Combined Global and Local Search for
the Falsification of Hybrid Systems. In Proc. FORMATS 2014. (Lecture Notes
in Computer Science), Axel Legay and Marius Bozga (Eds.), Vol. 8711. Springer,
146–160.
[30] Ritchie Lee, Mykel J Kochenderfer, Ole J Mengshoel, Guillaume P Brat, and
Michael P Owen. 2015. Adaptive stress testing of airborne collision avoidance
systems. In Digital Avionics Systems Conference (DASC), 2015 IEEE/AIAA 34th.
IEEE, 6C2–1.
[31] P. Madhusudan and Sanjit A. Seshia (Eds.). 2012. Proc. CAV 2012. . Lecture Notes
in Computer Science, Vol. 7358. Springer.
[32] Oded Maler and Dejan Nickovic. 2004. Monitoring Temporal Properties of Continuous Signals. In Formal Techniques, Modelling and Analysis of Timed and FaultTolerant Systems, Joint Int. Confs. on Formal Modelling and Analysis of Timed
Systems, FORMATS 2004 and Formal Techniques in Real-Time and Fault-Tolerant

Falsification of Hybrid Systems by Monte Carlo Tree Search

[33]

[34]

[35]
[36]

[37]

[38]

Systems, FTRTFT 2004 (LNCS), Yassine Lakhnech and Sergio Yovine (Eds.), Vol. 3253.
Springer, 152–166.
Truong Nghiem, Sriram Sankaranarayanan, Georgios E. Fainekos, Franjo Ivancic,
Aarti Gupta, and George J. Pappas. 2010. Monte-carlo techniques for falsification
of temporal properties of non-linear hybrid systems. In Proceedings of the 13th
ACM International Conference on Hybrid Systems: Computation and Control, HSCC
2010, Stockholm, Sweden, April 12-15, 2010, Karl Henrik Johansson and Wang Yi
(Eds.). ACM, 211–220.
Luan Viet Nguyen, James Kapinski, Xiaoqing Jin, Jyotirmoy V. Deshmukh, Ken
Butts, and Taylor T. Johnson. 2017. Abnormal Data Classification Using TimeFrequency Temporal Logic, See [19], 237–242.
André Platzer. 2010. Logical Analysis of Hybrid Systems - Proving Theorems for
Complex Dynamics. Springer.
David Silver, Aja Huang, Chris J. Maddison, Arthur Guez, Laurent Sifre, George
van den Driessche, Julian Schrittwieser, Ioannis Antonoglou, Veda Panneershelvam, Marc Lanctot, Sander Dieleman, Dominik Grewe, John Nham, Nal Kalchbrenner, Ilya Sutskever, Timothy Lillicrap, Madeleine Leach, Koray Kavukcuoglu,
Thore Graepel, and Demis Hassabis. 2015. Mastering the game of Go with deep
neural networks and tree search. Nature 529 (2015), 484–489.
Simone Silvetti, Alberto Policriti, and Luca Bortolussi. 2017. An Active Learning
Approach to the Falsification of Black Box Cyber-Physical Systems. In Integrated
Formal Methods - 13th International Conference, IFM 2017, Turin, Italy, September
20-22, 2017, Proceedings (Lecture Notes in Computer Science), Nadia Polikarpova
and Steve Schneider (Eds.), Vol. 10510. Springer, 3–17.
Aditya Zutshi, Jyotirmoy V. Deshmukh, Sriram Sankaranarayanan, and James
Kapinski. 2014. Multiple shooting, CEGAR-based falsification for hybrid systems.
In 2014 International Conference on Embedded Software, EMSOFT 2014, New Delhi,
India, October 12-17, 2014, Tulika Mitra and Jan Reineke (Eds.). ACM, 5:1–5:10.

EMSOFT’18, September 2018, Torino, Italy

