Eﬀective Hybrid System Falsiﬁcation
Using Monte Carlo Tree Search Guided
by QB-Robustness
Zhenya Zhang1(B) , Deyun Lyu1 , Paolo Arcaini2 , Lei Ma1,3,4 ,Ichiro Hasuo2 , and Jianjun Zhao1
1
Kyushu University, Fukuoka, Japanzhang.zhenya.623@m.kyushu-u.ac.jp
2
National Institute of Informatics, Tokyo, Japan
3
University of Alberta, Edmonton, Canada
4
Alberta Machine Intelligence Institute, Edmonton, Canada

Abstract. Hybrid system falsiﬁcation is an important quality assurance
method for cyber-physical systems with the advantage of scalability andfeasibility in practice than exhaustive veriﬁcation. Falsiﬁcation, given adesired temporal speciﬁcation, tries to ﬁnd an input of violation insteadof a proof guarantee. The state-of-the-art falsiﬁcation approaches often
employ stochastic hill-climbing optimization that minimizes the degree ofsatisfaction of the temporal speciﬁcation, given by its quantitative robust
semantics. However, it has been shown that the performance of falsiﬁcation could be severely aﬀected by the so-called scale problem, related tothe diﬀerent scales of the signals used in the speciﬁcation (e.g., rpm andspeed): in the robustness computation, the contribution of a signal could
be masked by another one. In this paper, we propose a novel approachto tackle this problem. We ﬁrst introduce a new robustness deﬁnition,
called QB-Robustness, which combines classical Boolean satisfaction andquantitative robustness. We prove that QB-Robustness can be used tojudge the satisfaction of the speciﬁcation and avoid the scale problem
in its computation. QB-Robustness is exploited by a falsiﬁcation approach based on Monte Carlo Tree Search over the structure of the formal
speciﬁcation. First, tree traversal identiﬁes the sub-formulas for which itis needed to compute the quantitative robustness. Then, on the leaves,numerical hill-climbing optimization is performed, aiming to falsify such
sub-formulas. Our in-depth evaluation on multiple benchmarks demonstrates that our approach achieves better falsiﬁcation results than thestate-of-the-art falsiﬁcation approaches guided by the classical quantitative robustness, and it is largely not aﬀected by the scale problem.
Keywords: Falsiﬁcation · Signal temporal logic · Scale problem ·Monte carlo tree search · Robust semantics · QB-Robustness
This work is supported in part by JSPS KAKENHI Grant No. 20H04168, 19K24348,
19H04086, JST-Mirai Program Grant No. JPMJMI20B8, Japan. Lei Ma is also supported by Canada CIFAR AI Program and Natural Sciences and Engineering ResearchCouncil of Canada. Paolo Arcaini and Ichiro Hasuo are supported by ERATO HASUOMetamathematics for Systems Design Project (No. JPMJER1603), JST.
c The Author(s) 2021

A. Silva and K. R. M. Leino (Eds.) CAV 2021, LNCS 12759, pp. 595–618, 2021.
https://doi.org/10.1007/978-3-030-81685-8_29

596

Z. Zhang et al.

1

Introduction

Cyber-Physical Systems (CPS) are hybrid systems that combine physical systems(with continuous dynamics) and digital controllers (that are inherently discrete).
Being often safety-critical, their quality assurance is of great importance andwidely investigated by both academia and industry. The continuous dynamics
of hybrid systems leads to inﬁnite search spaces, making their veriﬁcation often
extremely diﬃcult.
Falsiﬁcation has been proposed as a more practically feasible approach thattackles the dual problem of veriﬁcation: instead of exhaustively proving a property, falsiﬁcation intends to uncover the existence of its violation with counterexamples. Formally, the problem is deﬁned as follows. Given a model M taking an
input signal u and outputting a signal M(u), and a speciﬁcation ϕ (a temporal
formula), the falsiﬁcation problem consists in ﬁnding a falsifying input, i.e., an
input signal u such that the corresponding output M(u) violates ϕ.
The most pursued and successful approach to the falsiﬁcation problem consists in turning it into an optimization problem; we call it optimization-based
falsiﬁcation. This is possible thanks to the quantitative robust semantics of temporal formulas [14,19]. Robust semantics extends the classical Boolean satisfaction relation v |= ϕ in the following way: it assigns a value w, ϕ ∈ R∪{∞, −∞}(i.e., robustness) that tells not only whether ϕ is satisﬁed or violated (by thesign), but also how robustly the formula is satisﬁed or violated.
Optimization-based falsiﬁcation approaches adopt hill-climbing stochastic
optimization strategies to generate inputs to decrease robustness, which terminate when they ﬁnd an input with negative robustness, i.e., a falsifying inputthat triggers the violation of the speciﬁcation ϕ. Diﬀerent optimization-based
falsiﬁcation algorithms have been proposed (see [26] for a survey), and mature
tools (e.g., Breach [13] and S-TaLiRo [4]) have also been developed.
The scale problem is a recognized issue in optimization-based falsiﬁcation [21,40], which could arise when multiple signals with diﬀerent scales are present in
the speciﬁcation. Namely, it is due to the computation of robust semantics ofBoolean connectives, i.e., the way in which the robustness values of diﬀerent
sub-formulas are compared and aggregated: such computation is problematic in
the presence of signals that take values having diﬀerent order of magnitudes.
Example 1. As very simple example, let us consider the formula ϕ ≡[0,30] (ϕ1 ∧ ϕ2 ), with ϕ1 ≡ gear < 6 and ϕ2 ≡ speed < 130. It is apparent
that ϕ1 is always satisﬁed (in any car model with 5 gears), and it has been
added in the speciﬁcation as redundant check.1 According to robust semantics, the Boolean connective ∧ is interpreted by minimum , and the “always”
operator [0,30] is interpreted by inﬁmum ; the robustness of an atomic
formula f (x) < c is given by the margin c − f (x). Therefore, the robustness of ϕ under the signal (gear , speed ), where gear , speed : [0, 30] → R, is1

Note that we built such a trivial example just to make the scale problem very easy
to understand. However, in general, the scale problem frequently occurs on muchless trivial speciﬁcations, as we will see in the experiments.

Eﬀective Falsiﬁcation Using MCTS Guided by QB-Robustness

597


 


130 − speed (t) . Note that the(gear , speed ), ϕ = t∈[0,30] 6 − gear (t)robustness of ϕ1 is always in the order of units, while the robustness of ϕ2 is,in general, in the order of tens. It is not diﬃcult to see that, if both ϕ1 andϕ2 are satisﬁed, the robustness of ϕ will only depend on ϕ1 (because of theminimum in the robust semantics of the logical connective). In this case, we saythat ϕ1 masks ϕ2 . In such a case, a falsiﬁcation approach relying on robustness
will be misled during the search. Note that, in this particular case, the only way
to falsify ϕ is to falsify ϕ2 , because ϕ1 is always satisﬁed; therefore, falsifying
this relatively simple formula could be extremely diﬃcult for state-of-the-art
optimization-based falsiﬁcation approaches (as we will show and have conﬁrmed
in the experiments).
In this paper, we propose a novel approach to tackle the scale problem in
optimization-based falsiﬁcation. Our intuition and insights are that we should
try to avoid the comparison of robustness values of diﬀerent sub-formulas, sothat one sub-formula does not mask the contribution of another one.
To achieve this, we ﬁrst propose a new way of computing the satisfactionof a formula that combines quantitative robust semantics and Boolean semantics. We name the new semantics as QB-Robustness. QB-Robustness, for eachtype of formula ϕ, requires selecting a sub-formula ϕk among its sub-formulas{ϕ1 , . . . , ϕK }. For ϕk , the quantitative robust semantics is computed, while forthe other sub-formulas the Boolean semantics is computed. Therefore, the computation of QB-Robustness requires identifying a path Σ along the parse tree ofthe formula ϕ, where visited sub-formulas are those for which the quantitativerobustness is computed. We prove that QB-Robustness, independently of theselected Σ, is equivalent (in terms of sign and satisfaction) to the quantitativerobust semantics (and also to the Boolean one).
In general QB-Robustness is a useful tool for avoiding the scale problem offalsiﬁcation. By deﬁnition, the quantitative robustness of diﬀerent sub-formulas
is never compared, so removing the main cause of the scale problem. It would
then make sense to use it for guiding the optimization-based falsiﬁcation process.
However, QB-Robustness requires to choose a particular sequence Σ of subformulas for which to compute the quantitative robustness. It is relatively easy toshow that some of them provide a better guidance than others to the falsiﬁcation
search. Considering the previous example, if Σ contains ϕ1 , we can encounter the
problem that the quantitative robustness of ϕ1 would not provide any guidance(i.e., no big variations in the robustness values would be observed). On the other
hand, if Σ contains ϕ2 , the quantitative robustness would have larger variations,providing more eﬀective guidance to the search.
Then, the key problem is how to select the best Σ, that enables the hillclimbing optimization used in falsiﬁcation to be more eﬀective. In general,
although it is often diﬃcult to know the best Σ in advance, it is still possible to learn it by observing sampling results using diﬀerent Σ. Based on thisintuition, we propose a novel falsiﬁcation approach that identiﬁes the sequencesΣ that is more likely to be eﬃcient, and uses them in the new falsiﬁcation
trials. Our approach could be seen as an instantiation of the classical Monte598

Z. Zhang et al.

Carlo Tree Search (MCTS) method [8,28], which is able to eﬃciently tackle theexploration-exploitation tradeoﬀ. In our context, exploration consists in incrementally constructing the tree that represents all the possible sequences, andexploitation consists in selecting the best Σ and running optimization-based
falsiﬁcation in which QB-Robustness with Σ is used.
Overall, the major Contributions of this paper are summarized as follows:– We propose a novel semantics (QB-Robustness) for STL formulas that combines quantitative robustness and Boolean satisfaction. We prove that QBRobustness can be used to show the satisﬁability of STL formulas;– We deﬁne a falsiﬁcation approach based on MCTS that exploits QBRobustness to address the scale problem;– We implement the approach in the tool ForeSee, based on which, we performed in-depth evaluation, demonstrating the eﬀectiveness and advantage
of our approach compared with the state of the art.
Paper Structure. In Sect. 2, we introduce the preliminaries of the optimizationbased falsiﬁcation. In Sect. 3, we introduce the novel STL semantics QBRobustness, and, in Sect. 4, we describe the MCTS-based falsiﬁcation approachthat uses QB-Robustness. In Sect. 5, we describe the experiments and evaluation
results. Finally, we discuss most relevant work to ours in Sect. 6, and conclude
the paper in Sect. 7.

2

Preliminaries

In this section, we brieﬂy review the falsiﬁcation framework based on robust
semantics of temporal logic [14].
Let T ∈ R+ be a positive real. An M -dimensional signal with a time horizon
T is a function w : [0, T ] → RM . We treat the system model as a black box, i.e.,
its behaviors are only observed from inputs and their corresponding outputs.
Formally, a system model, with M -dimensional input and N -dimensional output,
is a function M that takes an input signal u : [0, T ] → RM and returns a signal
M(u) : [0, T ] → RN . Here the common time horizon T ∈ R+ is arbitrary.
Definition 1 (STL Syntax). We ﬁx a set Var of variables. In Signal Temporal
Logic (STL), atomic propositions and formulas are deﬁned
 as follows, respectively: α ::≡ f (x1 , . . . , xN ) > 0, and ϕ ::≡ α | ⊥ | ¬ϕ | ϕ | ϕ | I ϕ | ♦I ϕ |ϕ UI ϕ Here f is an N -ary function f : RN → R, x1 , . . . , xN ∈ Var, and I is a
closed non-singular interval in R≥0 , i.e., I = [a, b] or [a, ∞), where a, b ∈ R anda < b. , ♦ and U are temporal operators, which are usually known as always,
eventually and until respectively. The always operator  and eventually operator ♦ can also be considered as special cases of the until operator U, where♦I ϕ ≡ UI ϕ and I ϕ ≡ ¬♦I ¬ϕ. Other common connectives such as →, areintroduced as syntactic sugar: ≡ ¬⊥, ϕ1 → ϕ2 ≡ ¬ϕ1 ∨ ϕ2 .
Definition 2 (Quantitative Robust Semantics). Let w : [0, T ] → RN be
an N -dimensional signal, and t ∈ [0, T ). The t-shift wt of w is the signal

Eﬀective Falsiﬁcation Using MCTS Guided by QB-Robustness599

wt : [0, T − t] → RN deﬁned by wt (t ) := w(t + t ). Let ϕ be an STL formula. We deﬁne the robustness w,
R ∪ {∞, −∞} as follows, by induction
 ϕ ∈ on the construction of formulas.
anddenote inﬁmums
and supremums ofreal numbers, respectively. , the binary version of , denotes minimum.
w, f (x1 , · · · , xN ) > 0 := f w(0)(x1 ), · · · , w(0)(xN )w, ⊥
w, ¬ϕ := −w, ϕ
 := −∞w, i ϕi  := i w, ϕi 
w, i ϕi  :=  i w, ϕi w, ♦I ϕ := t∈I∩[0,T ] wt , ϕw, I ϕ := t∈I∩[0,T ] wt , ϕ
 t




w, ϕ1 UI ϕ2  := t∈I∩[0,T ] w , ϕ2   t ∈[0,t) wt , ϕ1 
The original STL semantics is Boolean, given by a binary relation |= between
signals and formulas. The robust semantics reﬁnes the Boolean one in the following sense: w, ϕ > 0 implies w |= ϕ, and w, ϕ < 0 implies w |= ϕ, see [19,Prop. 16].
2.1

Hill Climbing-Guided Falsification

So far, the falsiﬁcation problem has received extensive industrial and academic attention. One possible approach direction by hill-climbing optimization
is an established ﬁeld, too: see [2–4,10,13–15,17,26,29,36–39,42] and the tools
Breach [13] and S-TaLiRo [4]. We formulate the problem and the methodology,
for later use in describing our falsiﬁcation approach.
Definition 3 (Falsifying Input). Let M be a system model, and ϕ be an STL
formula. A signal u : [0, T ] → R|Var| is a falsifying input if M(u), ϕ < 0; thelatter implies M(u) |= ϕ.
The use of quantitative robust semantics M(u), ϕ ∈ R∪{∞, −∞} in the above
problem enables the use of hill-climbing optimization.
Definition 4 (Hill Climbing-Guided Falsification). Assume the setting inDeﬁnition 3, for ﬁnding a falsifying input, the methodology of hill climbing-guided
falsiﬁcation is presented in Algorithm 1. Here, the function Hill-Climb makesa guess of an input signal u , aiming at minimizing the robustness M(u ), ϕ.
It does so, learning from the sampling history H that contains the previous
observations of input signals and their corresponding robustness values.
The Hill-Climb function can be designed based on various stochastic optimization algorithms. Typically, at the early phase of the optimization, the proposal of new input is usually based on random sampling; as the set of sampling
history grows larger, the algorithm takes various metaheuristic-based strategies to achieve the optimization goal eﬃciently. Examples of such algorithms
include Covariance Matrix Adaption Evolution Strategy (CMA-ES) [7] (used inour experiments), Simulated Annealing, Global Nelder Mead [32], etc.

600

Z. Zhang et al.

Algorithm 1. Hill climbing-guided falsiﬁcation
Require: a system model M, an STL formula ϕ, and a time budget
1: function Hill-Climb-Falsify(M, ϕ)2:initialize a placeholder u and rb ← ∞ the best input signal and robustness3:H←∅ sampling history of input signals and robustness
4:
while rb ≥ 0 and within the time budget do
5:u ← Hill-Climb(H) run hill climbing based on sampling history6:rb ← M(u ), ϕ compute robustness
7:
H ← H ∪ {(u , rb )} update sampling history8:
if rb < rb then9:rb ← rb , u ← u
 update the best input and robustnessuif rb < 010:
returnFailure otherwise, that is, no falsifying input found within the budget

3

QB-Robustness

The scale problem is a known important issue that negatively aﬀects the performance of falsiﬁcation, which arises when connective operators (i.e., conjunction
and disjunction) with operands that predicate on diﬀerent signals appear in the
STL formula under falsiﬁcation. According to the classic quantitative robust
semantics (see Deﬁnition 2), the robustness of those formulas is calculated basedon the comparison (minimum for conjunction, and maximum for disjunction)
between robustness values coming from the diﬀerent operand sub-formulas. However, since diﬀerent signals may diﬀer in magnitude, the comparison may bebiased, such that one signal w may always (or often) mask the contribution of
the others, and, therefore, the ﬁnal robustness may be dominated by this signal
w. Note that, although the scale problem aﬀects connective operators, it is not
only local to the place of their application, but it is always propagated to therobustness of the whole formula. The scale problem has been shown as a root
cause of the failure of many falsiﬁcation problems [21,40].
In this work, we propose a novel approach for solving the scale problem infalsiﬁcation. Our approach consists in introducing a new semantics for STL that
does not suﬀer from the scale problem. Such new semantics will be used in afalsiﬁcation approach based on Monte Carlo Tree Search. We describe details of
the new semantics in this section, and the new falsiﬁcation approach in Sect. 4.
The new proposed semantics, called QB-Robustness, combines quantitativerobustness and Boolean satisfaction. By construction, it never compares quantitative robustness values that come from diﬀerent sub-formulas, thus avoiding thescale problem. QB-Robustness is deﬁned for the whole STL formulas, except for
the “until” operator ϕ1 UI ϕ2 , when ϕ1 is an arbitrary formula. We still support
it as “eventually” and “always” operators2 , i.e., when ϕ1 = . Note that this is
not a major limitation, as QB-Robustness still supports the majority of speciﬁcations that are used in industry: indeed, in the experiments, we were able to2

Recall from Deﬁnition 1 that the “eventually” and “always” operators are deﬁned
in terms of the “until” operator.

Eﬀective Falsiﬁcation Using MCTS Guided by QB-Robustness

601

handle all the speciﬁcations used in falsiﬁcation competitions [18], which collectbenchmarks from industrial case studies.
To better explain the computation of QB-Robustness, we introduce somedeﬁnitions. Let us ﬁrst deﬁne the notion of immediate sub-formula for STL.
Definition 5 (Immediate Sub-Formulas). Let ϕ be an STL formula (seeDeﬁnition 1). We deﬁne the set ISForm(ϕ) of immediate sub-formulas of ϕ asfollows:
ISForm(α) := ∅ISForm(⊥) := ∅ϕi ) := {ϕ1 , . . . , ϕK }ISForm(i∈{1,...,K}

ISForm(I ϕ) := ISForm(ϕ)

ISForm(¬ϕ) := ISForm(ϕ)
ISForm(ϕi ) := {ϕ1 , . . . , ϕK }i∈{1,...,K}

ISForm(♦I ϕ) := ISForm(ϕ)

Intuitively, the immediate sub-formula set of a connective (conjunction or disjunction) contains all its operands. For the other unary operators (temporal
operators, negation, etc.), its immediate sub-formula set is given by the immediate sub-formula set of its argument.
The computation of QB-Robustness requires to select some nested immediate
sub-formulas. To this aim, we introduce the notion of sub-formula sequence.
Definition 6 (Sub-Formula Sequence). Let ϕ be an STL formula. A subformula sequence Σ = σ1 · . . . · σL w.r.t. ϕ is deﬁned as follows:
σ1 ∈ ISForm(ϕ)σl+1 ∈ ISForm(σl ) with l = 1, . . . , L − 1

where the · is the concatenation operator in the sequence. We use Σk to denotethe kth element of Σ. Moreover, we denote the ﬁrst element by Σhead , and thelast element by Σrear . We use Σhead to denote Σ without Σhead . We identify with εthe empty sequence; when ISForm(ϕ) = ∅, we use ε as its sub-formula sequence.
We identify with Σ ϕ the set of all the sub-formula sequences rooted in ϕ.
To be speciﬁc, in a sub-formula sequence Σ, each element is one of the subformulas of the previous element. This means that, for Boolean connectives, only
one of the operands is selected. Moreover, an atomic sub-formula predicatingover a single signal can only appear as the ﬁnal element of a sequence. We
exploit these characteristics of Σ to deﬁne QB-Robustness, which combines thequantitative robustness of the sub-formulas related to a given signal with the
Boolean satisfaction of the other sub-formulas. QB-Robustness, given a sequenceΣ, decides whether to compute the quantitative robust semantics or the Boolean
semantics of a sub-formula, by considering whether the sub-formula belongs to Σor not. This implies that, in the case of conjunction and disjunction, we evaluate
the quantitative robustness of the sub-formula in Σ and the Boolean satisfactionof the other sub-formulas. Based on such intuition, we deﬁne the semantics of
our proposed QB-Robustness in Deﬁnition 7, and demonstrate its usefulness in
Theorem 1.

602

Z. Zhang et al.

Definition 7 (Semantics of QB-Robustness). Let ϕ be an STL formula asdeﬁnedin Deﬁnition 1, and Σ be a sub-formula sequence w.r.t. ϕ. For ϕ ≡
ϕi | ϕi , let ϕk ∈ ISForm(ϕ) be the ﬁrst element Σhead of Σ, then we canrepresent these two cases as ϕ ≡ ϕk ∧ ϕk | ϕk ∨ ϕk , where ϕk is the conjunction(or disjunction, respectively) of the other formulas in ISForm(ϕ) \ {ϕk }. The
QB-Robustness QBRob(w, ϕ, Σ) of ϕ w.r.t. Σ is deﬁned as follows:
QBRob(w, α, ε) := w, αQBRob(w, ⊥, ε) := −∞QBRob(w, ¬ϕ, Σ) := −QBRob(w, ϕ, Σ)QBRob(w, ϕk , Σhead )if w |= ϕk
QBRob(w, ϕk ∧ ϕk , Σ) :=−∞otherwise
QBRob(w, ϕk , Σhead )if w |= ϕk
QBRob(w, ϕk ∨ ϕk , Σ) :=∞otherwise
QBRob(wt , ϕ, Σ)
QBRob(w, I ϕ, Σ) :=t∈I

QBRob(w, ♦I ϕ, Σ) :=

QBRob(wt , ϕ, Σ)t∈IWe now prove that the semantics of QB-Robustness is equivalent (in thesense of satisfaction) to the Boolean semantics, and so it can be used to show
violation of a speciﬁcation in a falsiﬁcation algorithm, as we do in this paper.
Theorem 1. Let ϕ be an STL formula. Given a signal w, for any Σ ∈ Σ ϕ , itholds that QBRob(w, ϕ, Σ) > 0 implies w |= ϕ. Similarly, for any Σ ∈ Σ ϕ , itholds that QBRob(w, ϕ, Σ) < 0 implies w |= ϕ.
Proof. We ﬁrst recall from [19, Prop. 16] that w, ϕ < 0 implies w |= ϕ, andthat w, ϕ > 0 implies w |= ϕ. We prove Theorem 1 by induction on the
structure of the formula.
– Case ϕ = α. By Deﬁnition 7, QBRob(w, α, ε) > 0 indicates that w, α > 0
and hence w |= α, and QBRob(w, α, ε) < 0 that w, α < 0 and hence w |= ϕ.
– For the following cases, let us assume that Theorem 1 holds for an arbitrary
formula ϕ and its sub-formula sequence Σ  that QBRob(w, ϕ , Σ  ) > 0 implies
w, ϕ  > 0, and that QBRob(w, ϕ , Σ  ) < 0 implies w, ϕ  < 0. We aim toprove that Theorem 1 also holds for ϕ, resulting from the application of theoperator in each of the following cases to ϕ , and Σ, the sub-formula sequenceof ϕ.
• Case ϕ = ϕ ∧ ψ, where ψ is an arbitrary formula. Let Σ = ϕ · Σ  , andlet us consider the two cases in which QBRob(w, ϕ, Σ) is negative andpositive separately:∗ If QBRob(w, ϕ, Σ) < 0, there are two sub-cases:· if QBRob(w, ϕ , Σ  ) < 0, then w, ϕ  < 0 (by assumption).
Then, by the robust semantics of conjunction, also w, ϕ < 0holds, and so it does w |= ϕ.

Eﬀective Falsiﬁcation Using MCTS Guided by QB-Robustness603· if QBRob(w, ϕ , Σ  ) > 0, then w, ϕ  > 0 (by assumption).
Then, it holds w |= ψ by Deﬁnition 7, and, therefore, it holds
w |= ϕ.
∗ If QBRob(w, ϕ, Σ) > 0, it means that QBRob(w, ϕ , Σ  ) > 0 and
w |= ψ (by Deﬁnition 7). By assumption, if QBRob(w, ϕ , Σ  ) > 0,then w, ϕ  > 0. Therefore, w |= ϕ.
• Case ϕ = I ϕ . Let Σ = Σ  , and let us consider the two cases in which
QBRob(w, ϕ, Σ) is negative and positive separately:∗ By Deﬁnition 7, QBRob(w, ϕ, Σ) < 0 indicates that there exists at ∈ I such that QBRob(wt , ϕ , Σ) < 0. By assumption, it holds thatwt |= ϕ . Then, by the semantics of the always operator , it holds
that w |= ϕ.
∗ By Deﬁnition 7, QBRob(w, ϕ, Σ) > 0 indicates that for all t ∈ I it
holds that QBRob(wt , ϕ , Σ) > 0. Then, by assumption, it holds thatfor all t ∈ I, wt |= ϕ . So, by the semantics of the always operator ,
it holds that w |= ϕ.
• Case ϕ = ¬ϕ . Let Σ = Σ  , and let us consider the two cases in which
QBRob(w, ϕ, Σ) is negative and positive separately:∗ By Deﬁnition 7, QBRob(w, ϕ, Σ) < 0 indicates that
QBRob(w, ϕ , Σ  ) > 0. By assumption, it holds that w |= ϕ , andtherefore, w |= ϕ.
∗ By Deﬁnition 7, QBRob(w, ϕ, Σ) > 0 indicates that
QBRob(w, ϕ , Σ  ) < 0. By assumption, it holds that w |= ϕ , and,
therefore, w |= ϕ.
• Proofs for the cases of ϕ = ϕ ∨ ψ and ϕ = ♦I ϕ follow similar proof
patterns, and so are left to the readers.
We use an example to illustrate how QB-Robustness is used for checking thesatisﬁability of an STL formula.
Example 2. Let w : [0, T ] → R2 be a 2-dimensional signal and ϕ = I (ϕ1 ∨ϕ2 )be an STL formula where ϕ1 and ϕ2 are two atomic formulas. Intuitively, tomake ϕ falsiﬁed, there must exist t ∈ I such that wt |= ϕ1 and wt |= ϕ2 . Let us
consider a non-trivial falsiﬁcation problem in which, for most of the signals w,
sets {t ∈ I | wt |= ϕ1 } and {t ∈ I | wt |= ϕ2 } are non-empty and disjoint.
By Deﬁnition 7, given the sub-formula sequenceΣ = ϕ1 of ϕ, the correspond
ing QB-Robustness is QBRob(w, ϕ, Σ) = t∈I QBRob(wt , ϕ1 ∨ ϕ2 , ϕ1 ), i.e., ittakes the inﬁmum of QBRob(wt , ϕ1 ∨ ϕ2 , ϕ1 ) over t ∈ I. Again, by Deﬁnition 7,
for any t ∈ I, QBRob(wt , ϕ1 ∨ ϕ2 , ϕ1 ) is computed as follows:




t
t
it
– if for a t ∈ I it holds
 w |= ϕ2 , then QBRob(w , ϕ1 ∨ ϕ2 , ϕ1 ) = ∞. Then,is impossible that t∈I QBRob(wt , ϕ1 ∨ ϕ2 , ϕ1 ) is given by QBRob(wt , ϕ1 ∨ϕ2 , ϕ1 );– if for a t ∈ I it holds wt |= ϕ2 , then QBRob(wt , ϕ1 ∨ ϕ2 , ϕ1 ) =QBRob(wt , ϕ1 , ε) = wt , ϕ1 . Inthis case, QBRob(wt , ϕ1 ∨ ϕ2 , ϕ1 ) has achance to determine the value of t∈I QBRob(wt , ϕ1 ∨ ϕ2 , ϕ1 ).

604

Z. Zhang et al.


Therefore, when Σ = ϕ1 , it holds that QBRob(w, ϕ, Σ) = t∈S wt , ϕ1 , wheret
S = {t ∈ I | w |= ϕ2 }, i.e., the inﬁmum of the quantitative robustness of ϕ1on the interval when ϕ2 is violated. Indeed, once this value is negative, it meansthat there exists a point t ∈ I when both ϕ1 and ϕ2 are violated; by the Boolean
semantics of always and disjunction, ϕ is violated.

4MCTS-Based Falsiﬁcation Guided by QB-Robustness

QB-Robustness never compares robustness values coming from signals with different magnitudes, and, therefore, it does not suﬀer from the scale problem. As
such, it could be used in falsiﬁcation approaches instead of the classical purequantitative robustness.
However, a sub-formula sequence Σ is required when calculating QBRobustness, and such sequence is not unique (see Deﬁnition 7). Note that the
selection of the sequence can aﬀect the performance of the numerical optimization algorithms used in falsiﬁcation. Let us consider ϕ ≡ ((gear < 6)∧(speed <130)) as an example. As explained in Sect.1, numerical optimization will performbetter if guided by the robustness values coming from speed rather than by thosecoming from gear . Therefore, in a falsiﬁcation approach using QB-Robustness,
it is important to select an appropriate sub-formula sequence Σ.
By using the QB-Robustness, the problem of falsifying an STL formula ϕconsists in ﬁnding both a signal w and a sub-formula sequence Σ such that
QBRob(w, ϕ, Σ) < 0. The selection of Σ is discrete, while the search for w isnumerical. In order to combine these processes that are diﬀerent in nature, we
propose to adapt Monte Carlo Tree Search (MCTS) [8,28]. In the following, we
ﬁrstly give a brief introduction to MCTS in Subsect. 4.1, and then present theapplication of MCTS to our falsiﬁcation problem in Subsect. 4.2.
4.1

MCTS Background

MCTS exempliﬁes the “trial and error” philosophy, and has achieved a great
success over the past decade, most notably in ﬁelds such as the computer Go
game [35]. MCTS explores the action space given by the possible actions of
the system; for example, in the Go game, these are the positions where to put
the next stone. The approach builds a tree of sequences of actions, and assigns
rewards to the diﬀerent branches. MCTS performs the search by iteratively taking the following four steps. See Fig. 1, where the general scheme is adapted toour current setting, for illustration.
– Selection. It selects a node to expand or to reason about. Initially, selection has
no other choice than the root. When a node has multiple expanded children,
selection will be done according to the UCB1 [6] algorithm.
– Expansion. Child expansion happens after selection if the selected node has
unexpanded children. A child will be added to the tree during expansion.
– Playout. After a node is just expanded or a leaf is reached, playout is performed for evaluating the node. The evaluation is given by a reward, whichEﬀective Falsiﬁcation Using MCTS Guided by QB-Robustness
Initialization

Expansion

Playout

Backpropagation

ϕ

ϕ

ϕ

ϕ

ϕ1
ϕ11

ϕ1

hill climbing guided
by QB-Robustness
Σ ← ϕ1 · ϕ11
rb ← QBRob(M(u), ϕ, Σ)Termination

selection by
UCB1 algorithm
visit : 1
rwd : 0.8

ϕ1
ϕ11

ϕ11

Selection

605

visit : 1
rwd : 0.8

visit : 1
rwd : 0.8

ϕ2

ϕ1
ϕ11

visit : 1
rwd : 0.8

visit : 1
rwd : 0.2

ϕ1
ϕ11

ϕ2
ϕ12

a falsifying input found!

Hill-Climb({u, rb})

Fig. 1. The workﬂow of MCTS-based falsiﬁcation guided by QB-Robustness. Let us
consider the falsiﬁcation of an STL formula ϕ = I (ϕ1 ∨ ϕ2 ), where ϕ1 = ϕ11 ∧ ϕ12 .
Initially, there is only the root in the tree, so the algorithm selects it for expansion.
Then, the algorithm keeps on randomly selecting a child of a non-fully expanded node,
until a leaf node is reached. By reaching a leaf, a sub-formula sequence Σ has been
constructed; the algorithm performs playout using Σ, by running hill-climbing optimization guided by the QB-Robustness with Σ, to estimate the reward of the path.
After playout, the algorithm backpropagates the reward and the number of visits fromthe leaf to the root. When all the children of a node are expanded, selection is done
based on the UCB1 algorithm. After many loops, the algorithm has explored all thepossible sub-formula sequences in Σ ϕ , and it starts allocating more resources to thosebranches where hill-climbing optimization progresses more smoothly. The algorithm
terminates either when a falsifying input is found, or when the budget is exhausted.

is a real number in [0, 1]. Reward can be interpreted diﬀerently in diﬀerent
contexts. For example, in the Go game, the reward of a position is measured
by the winning rate when a stone is positioned there; this is estimated byrandomly playing the game until the end for n times, and then taking theratio nnw of the number of winning as the winning rate.
– Backpropagation. Backpropagation updates the number of visits and thereward of the nodes along the path from the node of playout to the root.
These data are used in subsequent loops to decide the branches to explore.
At the end, the action space will be suﬃciently explored in an unbalanced manner, by focusing on the most promising sub-spaces giving the highest rewards.
4.2

Proposed QB-Robustness-Guided Falsification Approach

We here propose a falsiﬁcation framework based on MCTS in which, during tree
construction, we synthesize and select a sub-formula sequence that facilitates
the falsiﬁcation progress the most, and, at the bottom layer of the tree, we run
numerical optimization to search for a falsifying input and provide feedback (i.e.,
backpropagation) to guide the sequence selection.
We formalize our algorithm in Algorithm 2 and visualize its execution in
Fig. 1. In the following, we elaborate on our approach.

606

Z. Zhang et al.

Algorithm 2. MCTS-based falsiﬁcation guided by QB-Robustness
Require: a system model M, an STL formula ϕ, and the following tunable parameters: a scalar c for UCB1, an MCTS budget BM , and a playout budget BP .
1: function MCTS
 the root denoted as a sequence with ϕ only2:
Σ init ← ϕ the MCTS search tree, initially root only3:
T ← {Σ init } visit count N initialized, deﬁned only for root4:
N ← (Σ init → 0)
 reward function R initialized5:
R ← (Σ init → 0)
 the sampling history of hill climbing
6:
H ← (Σ init → ∅)7:
while ϕ not falsiﬁed and within the MCTS budget BM do
8:
MCTSSearch(Σ init )9: function MCTSSearch(Σ)
10:
if ISForm(Σrear ) = ∅ then
) then11:
if Σ · ϕk ∈ T for all ϕk∈ ISForm(Σrear
12:

ϕk ←

arg maxϕi ∈ISForm(Σrear )R(Σ · ϕi ) + c

2 ln N (Σ)
N (Σ · ϕi )

 the node has children
 all children expanded selection by UCB1

13:
14:
15:
16:
17:
18:
19:

else
 unexpanded children exist
randomly select ϕk from {ϕk ∈ ISForm(Σrear ) | Σ · ϕk ∈ T } expand a new childT ← T ∪ {Σ · ϕk }N (Σ · ϕk ) ← 0
H(Σ · ϕk ) ← ∅ recursive call
MCTSSearch(Σ · ϕk )R(Σ · ϕk )
 back propagation for rewardR(Σ) ←
max

20:
21:
22:
23:
24:
25:
26:
27:
28:

else
 a leaf node reachedwhile within playout budget BP do  playout by hill-climbing falsiﬁcationu ← Hill-Climb(H(Σ))
 hill-climbing
rb ← QBRob(M(u), ϕ, Σhead )if rb < 0 then falsifying input foundreturn (u, rb)
H(Σ) ← H(Σ) ∪ {(u, rb)} record sampling history
R(w) ← Rwd(rb, H(Σ))
N (Σ) ← N (Σ) + 1
 back propagation for visit countϕk ∈ISForm(Σrear )We construct the tree in this way: each node represents a sequence of formulas, and each edge of a node is a sub-formula of the last element of the sequence
represented by the node. The root is initialized with a sequence holding ϕ only(Lines 2–3) and some other properties including the number of visits to the diﬀerent nodes (Line 4), the reward (Line 5), and the history of hill-climbing sampling(Line 6). The main process of MCTS consists in calling the MCTSSearch function iteratively with the root as argument (Line 8), until the exhaustion of the
MCTS budget or a falsifying input is found (Line 7). The MCTSSearch function (Line 9) goes through the four phases, namely selection, expansion, playout
and backpropagation, of the original MCTS algorithm.

Eﬀective Falsiﬁcation Using MCTS Guided by QB-Robustness

607

Selection. Selection happens when a node has children (Line 10) and thesehave all been expanded (Line 11). It selects a child according to the UCB1 [6]algorithm (Line 12) to take a balance between exploration and exploitation. The
exploitation is embodied by the reward R(Σ · ϕi )—the higher the reward is,the more likely a falsifying input is found following that branch. Exploration,
N (Σ)
instead, is considered via 2Nln(Σ·ϕthat is negatively correlated to the numberi)of visits to a child—the more the child was visited before, the less chance it will
be visited again. The scalar c is a tunable parameter that balances the trade-oﬀ
between exploration and exploitation. After a child Σ · ϕk is selected, it will betaken as the argument of the next MCTSSearch loop (Line 18).

Expansion. If not all the children of a node have been expanded (Line 13), achild will be expanded. Expansion consists in randomly selecting a child fromthe unexpanded child list (Line 14), adding it to the tree (Line 15), initilizing
properties including the number of visits and history (Lines 16–17). After expansion, the newly expanded child will be taken as the argument of the recursive
call to MCTSSearch (Line 18).
Playout. If a leaf node that has no children to expand is reached, the playout
phase will start to devise a reward for evaluating the visited path. In our context,
we deﬁne the reward based on the best robustness value that can be obtainedwith the path; speciﬁcally, playout consists in running hill-climbing guided falsiﬁcation to search for a minimal robustness value (Line 22). Note that the sequenceΣ represented by a leaf node is actually the concatenation between ϕ and a subformula sequence of ϕ. We extract the suﬃx of Σ, i.e., the sub-formula sequence,
to compute the QB-Robustness as a guidance to the hill-climbing optimization(Line 23). If a negative QB-Robustness is found (Line 24), then the whole algorithm can be terminated and the input signal u that triggers the negative QBRobustness can be returned as the falsifying input (Line 25); otherwise, thesampling history of hill climbing will be saved (Line 26) so that the future playout at the same leaf can be restored from that context. After playout, the rewardof the leaf node will be updated based on the deﬁnition of the reward, which will
be introduced below. Reward Since our goal is to ﬁnd a sequence Σ with which
hill-climbing optimization can minimize QBRob(w, ϕ, Σ) smoothly, we connect
the reward with the hill-climbing progress. Formally, given a sampling history({rb }∪rbh ),H, our reward (Line 27) is deﬁned as Rwd(rb , H) := max rbh −minmax rbhwhere rbh is the history of robustness values in H.
Backpropagation. In MCTS, the playout result of a leaf is backpropagated tothe higher layer nodes along the path, so that the future selection on the highlayer is referred. Backpropagation updates two properties of each ancestor of theleaf till the root, the reward (Line 19) and the number of visits (Line 28).
Remark 1 (Approach Complexity). With respect to classical falsiﬁcation,
our approach introduces an exploration phase for searching the “best” subformula sequence to instantiate QB-Robustness. The number of these sequences
corresponds to the number of atomic sub-formulas (and so the leaves of the608

Z. Zhang et al.
Table 1. Benchmarks – STL speciﬁcations
Spec. ID Temporal speciﬁcation in STL
AT1
AT2
AT3
AT4
AT5
AT6
AT7

[0,30] (gear = 4 → speed > 35)
[0,30] (gear = 4 → ♦[0,5] (rpm < 4300))[0,30] (speed < 130 ∧ gear < 5)
[0,30] (speed < 135 ∧ rpm < 4780)
[0,30] (rpm < 600 → ♦[0,10] (gear > 1))
[0,30] (♦[0,5] (speed < 120 ∨ rpm > 3500))
[0,30] (rpm < 4750 ∧ gear < 5)

Spec. ID Temporal speciﬁcation in STL
AT8
AT9
AT10
AT11
AT12
AT13
AT14

[0,10] (speed < 50) ∨ ♦[0,30] (rpm > 2520)♦[10,30] (speed < 50 ∨ speed > 60 ∨ rpm < 1000)[0,30] (gear = 4 → (speed > 35 ∧ ♦[0,5] (rpm < 4000)))[0,30] (♦[0,8] (gear = 1 → (speed < 20 ∧ rpm < 600)))[0,30] (gear < 3) ∨ [0,30] (speed < 135 ∧ rpm < 4780)
[0,30] ((gear = 4 → ♦[0,5] (rpm < 4000)) ∧ gear < 5)
[0,30] (throttle = 0 ∨ brake = 0) → [0,30] (speed < 110)Spec. ID Temporal speciﬁcation in STL
AT15
AT16
AT17
AT18
AT19
AT20
AT21
AT22

[0,30] ((rpm < 4770 ∨ [0,1] (rpm > 1000)) ∧ ♦[0,5] (gear < 5))[0,30] (gear = 4 → ((♦[0,5] (rpm < 3000) ∧ (gear = 2 → speed < 20))))[0,5] (speed < 70 ∧ gear < 4) ∧ [10,20] (rpm < 4780) ∧ [25,30] (speed < 130)
[0,30] ((gear = 4 → ♦[0,5] (rpm < 4250)) ∧ (gear = 3 → ♦[0,5] (rpm < 4700)) ∧ (gear = 2 → ♦[0,5] (rpm < 4800)))[0,30] ((gear = 1 → speed < 80) ∧ (gear = 2 → speed < 90) ∧ (gear = 3 → speed > 20) ∧ (gear = 4 → speed > 30))
[0,29] (speed < 100) ∨ [29,30] (speed > 64) ∧ [0,30] (rpm < 4770 ∨ [0,1] (rpm > 700))[0,30] (throttle > 90 → ♦[0,10] (throttle < 30)) → [0,30] (gear = 4 → ♦[0,5] (rpm < 4000))[0,30] (throttle > 70 → ♦[0,10] (brake > 50)) → [0,30] (gear = 4 → speed > 35)
Spec. ID Temporal speciﬁcation in STL
AFC1
AFC2
AFC3
AFC4
AFC5
AFC6

[11,50] (mode = 1 → μ < 0.228)♦[0,50] (PedalAngle > 40) → [11,50] (μ < 0.225)♦[0,50] (EngineSpeed > 1000) → [11,50] (μ < 0.225)
[0,50] (EngineSpeed > 910 ∨ PedalAngle > 25) → [11,50] (μ < 0.225)♦[0,50] (PedalAngle > 40) → [11,50] (♦[0,8] (μ < 0.06))♦[0,50] (PedalAngle > 40 ∧ EngineSpeed > 1000) → [11,50] (♦[0,8] (μ < 0.06))

Spec. ID Temporal speciﬁcation in STL
FFR1
FFR2

[0,5] ((u1, u3 > 0 ∨ u1, u3 < 0) ∧ (u2, u4 > 0 ∨ u2, u4 < 0)) → [0,5] (¬(x1 > 3.9 ∧ x1 < 4.1) ∧ ¬(x3 > 3.9 ∧ x3 < 4.1))¬(♦[0,5] ([0,2] (x1 > 1.5 ∧ x1 < 1.7 ∧ x3 > 1.5 ∧ x3 < 1.7)))tree). Considering that most of the time is spent on playout, the complexity of
our approach grows linearly with the number of atomic sub-formulas.

5

Experimental Evaluation

In this section, we present the experiments we conducted to evaluate the eﬀectiveness of the proposed approach. We ﬁrst introduce the experiment setup
in Subsect. 5.1, and then we present the experimental evaluation results by
answering three research questions in Subsect. 5.2.
5.1

Experiment Setup

Simulink Models and Speciﬁcations As our benchmarks, we selected three
Simulink models frequently used in the falsiﬁcation community (i.e., in the falsiﬁcation competitions [18]), and 30 speciﬁcations deﬁned for them. All thesemodels are complicated hybrid systems with multiple input and output signals.
The speciﬁcations are STL formulas that formalize system requirements regarding safety, performance, etc. Since we are interested in assessing the inﬂuence ofthe scale problem to the performance of the compared falsiﬁcation approaches,

Eﬀective Falsiﬁcation Using MCTS Guided by QB-Robustness609

all the considered speciﬁcations predicate over, at least, two signals. Table 1
reports the 30 speciﬁcations under test. The IDs of the speciﬁcations identify
which models they belong to. A description of the three models and of their
speciﬁcations is as follows.
– Automatic Transmission (AT) [24] has two input signals, throttle ∈ [0, 100]and brake ∈ [0, 325], and three outputs signals including gear, speed andrpm. Most of the speciﬁcations we used formalize safety requirements of thesystem. For instance, AT2 requires that when gear is as high as 4, rpm
should not be larger than 4300; AT3 is an adaptation of the example we usedin Sect. 1; AT10-12 reason about the relationship among the three output
signals; AT17 speciﬁes three properties for three diﬀerent time intervals; AT18
speciﬁes diﬀerent properties for diﬀerent values of gear ; AT14, AT21 and
AT22 impose logical constraints on input signals, in addition to the property
under consideration.
– Abstract Fuel Control (AFC) [25] takes two input signals, PedalAngle ∈[8.8, 70] and EngineSpeed ∈ [900, 1100], and outputs a ratio μ reﬂecting thedeviation of air-fuel-ratio from its reference value. The basic safety requirement to this system is that μ should not be deviated from the reference value
too much (AFC1); in addition to that, our speciﬁcations also reason about
the resilience of the system (AFC5 and AFC6), and impose input constraints(AFC2-6).
– Free Floating Robot (FFR) [11] models robot moving in a 2-dimentional space.
It has four input signals u1 , u2 , u3 , u4 ∈ [−10, 10] that are boosters for a robot,
and four output signals that are the position in terms of coordinate values
x, y and their one-order derivatives ẋ, ẏ. The speciﬁcations regulate the kinetic
properties of the robot: FFR1 requires the robot to pass an area around thepoint (4, 4) under an input constraint, and FFR2 requires the robot to stayin an area for at least 2 s.
Baseline Approach and Our Proposed Approach. In our experiments, we compare
the performances of our proposed approach with the baseline Breach approach.
We implemented our approach in the tool ForeSee, which stands for FORmula
Exploitation by Sequence trEE for falsiﬁcation.
Breach is a state-of-the-art falsiﬁcation tool that implements the classic falsiﬁcation workﬂow we introduced in Sect. 2. The quantitative robustness calculation in Breach is based on the robust semantics given in Deﬁnition 2. Breachalso encapsulates several stochastic optimization algorithms, such as CMA-ES,
Simulated Annealing, etc. The implementation of our ForeSee approach uses
Breach only for interfacing with the Simulink model and for the calculationof quantitative robustness; instead, the calculation of QB-Robustness, and theimplementation of the MCTS algorithm are novel. Since CMA-ES has proved
to be the state-of-the-art stochastic algorithm [39], we select CMA-ES as ourbackend optimizer for the playout phase.3
3

ForeSee is available at https://github.com/choshina/ForeSee.

610

Z. Zhang et al.

We apply the two approaches, ForeSee and Breach, to each benchmark speciﬁcation reported in Table 1. Since both approaches are based on stochastic optimization, we repeat each experiment for 30 times, as suggested by a guideline for
conducting experiments with randomized algorithms [5]. For each experiment,
both approaches have been given a total timeout BM of 900 s (see Algorithm 2).
Evaluation Metrics. As ﬁrst evaluation metric, we compute the falsiﬁcation rate(FR) as the number of runs (out of 30) in which the approach returns a falsifying
input. Therefore, FR is an indicator of the eﬀectiveness of an approach, i.e., it
reﬂects the ability of an algorithm to falsify the speciﬁcation. As second evaluation metric, we compute the average time (seconds), as average execution timeof the successful falsiﬁcation runs. Therefore, the average time is an indicatorof the eﬃciency of the approach. We do not report the number of simulations
because these are consistent with the execution time.
Experiment Platform. In our experiments, we use Breach [13] (ver 1.2.13) with
CMA-ES (the state of the art). Breach accepts piece-wise constant signals as
input for the Simulink models; we use the same settings used in falsiﬁcationcompetitions [18]: we use piece-wise constant signals with ﬁve control points for
AT and AFC, and with four control points for FFR. As conﬁguration of MCTS
(see Algorithm 2), we set the UCB1 scalar c to 0.2, and the playout budget
BP to 10 generations. The experiments have been executed on an Amazon EC2c4.2xlarge instance (2.9 GHz Intel Xeon E5-2666 v3, 15 GB RAM).
5.2

Evaluation

We here analyze the experimental results using three research questions (RQs).
RQ1. Does the proposed approach perform better than state-of-the-art falsiﬁcation approaches?
In this RQ, we aim at assessing whether the proposed approach is indeed able
to tackle the scale problem in falsiﬁcation and performs better than state-of-theart approaches. Table 2 reports, for each speciﬁcation benchmark, the falsiﬁcation rate FR and the average execution time of our proposed approach ForeSee
and of the baseline Breach. The table further reports the diﬀerence of the two
metrics between the two approaches. We highlight in gray the best results inwhich ForeSee has an FR of 15 units higher than Breach. We observe thatfor 25 benchmarks out of 30, ForeSee has a better FR, and in 15 of these theimprovement is signiﬁcant (selected in gray). Note that there are notable cases,
such as AT3, AT13, AT16, and AT17, in which Breach only ﬁnds at most two
falsifying inputs, while ForeSee ﬁnds always at least 29 falsifying inputs. In fourcases, Breach has a better FR: while for AT8, AFC6, and FFR2 the diﬀerenceis minimal, it is quite large for AT14. We further inspected such speciﬁcationand its corresponding model (see Table 1); we noticed that all the sub-formulasin AT14 must be falsiﬁed to falsify the whole speciﬁcation4 , and they are all
4

Note that all binary connectivesof AT14 are disjunctions; indeed, A → B is thesyntactic sugar for ¬A B .

Eﬀective Falsiﬁcation Using MCTS Guided by QB-Robustness

611

Table 2. Falsiﬁcation performance comparison between Breach and ForeSee on benchmarks. Timeout: 900 s. FR in (/30), time in secs.
BreachFR timeAT1 12
AT2 18AT3 0
AT4 8
AT5 13
AT6 14
AT7 20
AT8 17
AT9 9
AT10 14
AT11 17

67.0
208.5
414.0
44.7
630.5
24.9
418.5
298.6
99.4
58.1

BreachFR time
AFC1 10
AFC2 12
AFC3 8ΔFR Δtime

29
30
29
30
30
20
30
13
29
30
30

+17
+12
+29
+12
+17
+6
+10
-4
+20
+16
+13

90.3
155.5
87.3
376.6
159.0
545.9
5.8
547.0
208.0
89.7
39.6

ForeSee
FR time532.2 12546.9 30
727.6 28

BreachFR timeFFR1 7

ForeSee
FR time132.1 7

ΔFR Δtime

458.0 +2
218.3 +18
232.5 +20

ForeSee
FR time

+23.3
-53.0
-37.4
+114.3-84.6-19.1+128.5
-90.6
-9.7
-18.5

-74.2
-328.6-495.1

ΔFR Δtime399.3 +0+267.2

BreachFR timeAT12 5
AT13 2
AT14 24
AT15 1
AT16 1
AT17 0AT18 18
AT19 15
AT20 1
AT21 10
AT22 13

379.2
75.2
184.9
66.1
13.0
160.0
81.8
97.7
239.0
72.0

BreachFR time
AFC4 7
AFC5 8
AFC6 10

ForeSee
FR timeΔFR Δtime

28
29
1
9
30
30
24
30
5
29
30

+23
+27
-23
+8
+29
+30
+6
+15
+4
+19
+17

381.4
98.3
601.5
331.8
6.7
208.8
234.3
154.3
286.2
425.5
113.3

ForeSee
FR time634.5 22576.9 9518.2 6

FFR2 30

38.0 27

ΔFR Δtime

500.3 +15322.0 +1
344.2 -4

BreachForeSee
FR time FR time

+2.2
+23.1
+416.6+265.7
-6.3
+74.3
+72.5
+188.5+186.5+41.3-134.2-254.9-174.0ΔFR Δtime

348.0 -3

+310.0diﬃcult to be falsiﬁed. In such a case, there is no best sub-formula sequence Σ:therefore, the time spent by ForeSee in exploring diﬀerent Σ does not provide
any improvement.
Regarding the time execution, there is no clear trend among the diﬀerent
results: sometimes ForeSee is faster, other times Breach is. However, even in
the cases in which ForeSee is slower, it is still below the timeout by which it
manages to ﬁnd a falsifying input (so, leading to better falsiﬁcation rates).
RQ2. Does the proposed approach solve the scale problem eﬀectively?
The benchmarks reported in Table 1 and experimented in RQ1, predicate
over signals having diﬀerent scales and so they suﬀer from the scale problem.
RQ1 showed that ForeSee is very eﬃcient in falsifying them. In this RQ, we wantto make a more systematic study of the eﬀects of the scale problem; indeed, thescale problem could manifest itself in diﬀerent ways, depending on the diﬀerenceof the order of magnitudes of the diﬀerent signals (e.g., speed [km/h] vs. rpm,
or speed [km/h] vs. rph). To assess this, we take six speciﬁcations from Table 1
and we artiﬁcially modify their outputs: namely, we multiply by 10k (with different k values depending on the speciﬁcation) the speed of AT1, AT3, AT4,

612

Z. Zhang et al.

Table 3. Falsiﬁcation performance under diﬀerent scales. Each rescaled signal isrescaled by 10k .
(a) AT1: speed × 10k(b) AT3: speed × 10k(c) AT4: speed × 10kk

BreachFR timeForeSee
FR timek

BreachFR timeForeSee
FR timek

BreachFR timeForeSee
FR time

-2
-1
0
1
2

30
25
12
9
9

26
29
29
28
30

77.5
107.9
90.3
81.8
94.2

-3
-2
-1
0
1

30
30
1
0
0

30
28
28
29
30

81.2
82.6
101.6
87.3
103.4

-2
-1
0
1
2

29
29
8
0
0

29
28
30
29
29

329.4
332.2
376.6
377.6
333.2

64.4 26131.9 30
96.4 28

77.5
107.9
90.3

min 0
max 30mean 12124.9 28
136.7 30132.5 29

81.2
103.4
91.2

min 0
max 29mean 13243.5 28414.0 30301.6 29

329.4
377.6
349.8

min 9
max 30mean 17

126.5
64.4
67.0
92.4
131.9

(d) AT9: speed × 10k

124.9
135.9
136.7
-

(e) AT15: rpm × 10k

247.2
243.5
414.0
-

(f) AFC3: EngineSpeed ×10kk

BreachFR timeForeSee
FR timek

BreachFR timeForeSee
FR timek

BreachFR timeForeSee
FR time

-1
0
1
2
3

11
9
10
28
30

28
29
29
29
29

259.8
208.0
221.2
248.9
209.6

-5
-4
-3
-2
0

20
13
4
0
1

6
10
5
9
9

222.3
258.8
313.6
268.6
331.8

0
-1
-2
-3
-4

8
18
29
30
29

28
29
29
29
30

232.5
284.1
211.5
230.1
236.2

162.6 28298.6 29207.3 29

208.0
259.8
229.5

min 0
max 20mean 1066.1 5158.1 10126.8 8

222.3
331.8
279.0

min 8
max 30mean 23198.2 28727.7 30423.2 29

211.5
284.1
238.9

min 9
max 30mean 18

202.6
298.6
197.4
175.4
162.6

138.3
158.1
144.6
66.1

727.6
574.2
401.2
215.0
198.2

and AT9; the rpm of AT15; and the EngineSpeed of AFC3. For each artiﬁcial
rescaling, both the Simulink model and the speciﬁcation have been changed.5
We run ForeSee and Breach on these rescaled benchmarks. Table 3 reports theexperimental results for each k. The table also reports the minimum, maximum,and mean results for FR and execution time. We observe that the performance ofBreach, in terms of FR, is very sensitive to the scale problem. Indeed, for all the
speciﬁcations, FR decreases with increasing or decreasing k; notable examples
are AT3 and AT4 in which Breach can (almost) always falsify with the minimum k, but never falsiﬁes with the maximum two k. This is the demonstrationof the eﬀects of the scale problem on falsiﬁcation approaches that only rely on
quantitative robust semantics where the robustness values of diﬀerent signals arecompared. By looking at the results of ForeSee, instead, we observe that it ismuch more robust and its FR performance is independent of the applied rescaling. This clearly shows that our falsiﬁcation approach guided by QB-Robustness
is successful in avoiding the scale problem.
5

Note that k = 0 corresponds to the experimental result in Table 2, and we report itagain for reference.

Eﬀective Falsiﬁcation Using MCTS Guided by QB-Robustness

613

Table 4. Falsiﬁcation performance under diﬀerent MCTS hyperparameters.

(a) Performance with varied cc

AT17
FR time023
0.02 26
0.2 300.5 301.0 30

177.8
196.7
208.8
297.0
311.7

AT19
FR timeAT21
FR time

30
30
30
29
30

30
28
29
30
24

224.6
278.5
154.3
227.3
240.2

463.4
501.3
425.5
509.0
497.0

(b) Performance with varied BP
BP

AT17
FR timeAT19
FR timeAT21
FR time

2
5
10
15
20

26
30
30
30
30

30
29
30
29
30

29
29
29
28
30

385.2
347.7
208.8
337.7
358.1

162.0
207.3
154.3
336.7
313.5

500.0
472.5
425.5
514.0
511.0

These results also allow us to show that the naive approach based on normalization for solving the scale problem does not work, as also reported in [41].
Indeed, one may think that a solution for tackling the scale problem could beto rescale the signals in a way to make them have the same order of magnitude. This is not a good approach. Let us consider the results in Table 3c for
AT4 ([0,30] (speed < 135 ∧ rpm < 4780)). In this case, speed is multiplied by
10k . We may think that the best falsiﬁcation result should occur when speed ismultiplied by 102 , because this would make the two signals both in the order of
thousands. However, this rescaling is the one giving the worst result. The best
result is actually given by the rescaling making speed even smaller (i.e., k = −2
and k = −1). This means that the correct way for handling the scale problem
cannot be identiﬁed in advance, but we need an approach as ours that learns
during falsiﬁcation the best strategy.
RQ3. How do the hyperparameters of MCTS inﬂuence the performance of the
proposed approach?
Our proposed approach is an instantiation of the Monte Carlo Tree Search(MCTS) method [8,28] that can be conﬁgured with some hyperparameters,
namely the scalar c used by UCB1 (Line 12 in Algorithm 2), and the playout
budget BP (Line 21 in Algorithm 2), both used for balancing between exploration and exploitation. Therefore, the performance of MCTS could be aﬀectedby the values used for these hyperparameters. In this RQ, we try to assess
this. We selected three benchmarks speciﬁcations (AT17, AT19, and AT21) andvaried one hyperparameter while keeping the other ﬁxed. Namely, we experimented with c ∈ {0, 0.02, 0.2, 0.5, 1} and budget BP = 10 (see Table 4a), andwith BP ∈ {2, 5, 10, 15, 20} and budget c = 0.2 (see Table 4b). Looking at theresults of Table 4a for AT17 and AT21, there seems to be some inﬂuence by
the scalar c. In AT17, the worst result in terms of FR is obtained when c is 0,
meaning that MCTS only focuses on exploitation. AT17 is a speciﬁcation thatsuﬀers from the scale problem, as shown by the very bad performance of Breachin Table 2; for such a speciﬁcation, we need to perform some exploration to ﬁnd
the best Σ: this explain the low performance of MCTS with c = 0. On the other614

Z. Zhang et al.

hand, the worst FR performance of AT21 is given by the highest value c = 1
that requires MCTS to spend a lot of time in exploration. Since AT21 is not an
extremely diﬃcult speciﬁcation (indeed Breach has FR of 10 in Table 2), suchvery conservative approach does not pay oﬀ, while more greedy approaches (i.e.,with lower c) have better performance.
Looking at the results of Table 4b related to BP , it seems that there is no
too much inﬂuence. The only diﬀerence is given in AT17 with BP = 2 where
the FR is slightly lower than the other cases. This means that, provided that a
suﬃciently large value for BP is given, ForeSee is not too sensitive to it.

6

Related Work

Quality assurance of CPS has been actively studied, due to its great signiﬁcance. Diﬀerent approaches, including but not limited to model checking, theorem proving, rigorous numerics, and nonstandard analysis [9,16,20,22,23,31,33],
have been proposed to solve the problem. However, due to the scalability issue
and existence of black-box components, those approaches are not widely appliedin the real-world systems.
The optimization-based falsiﬁcation approach inherits the search-based testing methodology, and is much more scalable than pure veriﬁcation-based
approaches. The key issue of search-based testing is the exploration-exploitation
trade-oﬀ. This issue has been discussed for the veriﬁcation of quantitative properties (e.g., [34]). In the falsiﬁcation community, there have also been a lotof works focusing on that, and these works tackle the problem from diﬀerent
perspectives. Metaheuristics refers to high-level heuristic strategies that utilize
heuristics to improve the search eﬃciency. Several metaheuristic strategies havebeen applied in falsiﬁcation, such as Simulated Annealing [1], tabu search [10],and so on. Coverage-guided falsiﬁcation [2,10,15,29] aims to guide the searchusing some coverage metrics, so that the search space is suﬃciently explored.
Recently, machine learning techniques have also been applied to falsiﬁcation toenhance the search ability. For instance, Bayesian optimization [3,11,36] utilizes
an acquisition function to balance exploration and exploitation; Reinforcement
learning [27,37] naturally emphasizes on exploration.
The scale problem is a recognized issue [12,21,40] that is known to severely
aﬀect the performance of falsiﬁcation. In [40], we proposed a multi-armed bandit
approach to solve the problem in a speciﬁc setting, that is, safety properties with
Boolean connectives: I (ϕ1 ∧ ϕ2 ) and I (ϕ1 ∨ ϕ2 ). The approach is not applicable to formulas having more nested sub-formulas, or even connectives having
more operands; therefore many of the benchmarks we used in Subsect.5.2 fall outof the scope of [40]. The techniques introduced in [12,21] rely on explicit declaration of input vacuity and output robustness. Compared to their approaches, ourmethod does not need that, but we learn the signiﬁcance of each signal throughtree exploration and reward computation.
MCTS, as an eﬀective search framework, has been applied in testing hybrid
systems. In [30], the authors applied an adaption of MCTS in testing, namely,

Eﬀective Falsiﬁcation Using MCTS Guided by QB-Robustness

615

adaptive press testing, to detect the potential dangerous cases of airborne collision. A recent study of MCTS on hybrid system falsiﬁcation is [39]. There,
the authors discretized the search space to construct the search tree, and thenapplied MCTS to explore diﬀerent sub-spaces. Compared to their approach, ourwork aims to tackle the scale problem and so we exploit the structure of speciﬁcation formulas to construct the tree search framework.

7

Conclusion and Future Work

Optimization-based falsiﬁcation is a widely used approach for quality assuranceof CPS, that tries to ﬁnd an input violating a Signal Temporal Logic (STL)
speciﬁcation. It does this by exploiting the quantitative robust semantics of thespeciﬁcation, trying to minimize its robustness. The performance of falsiﬁcation
is aﬀected by the scale problem in the presence of the comparison of robustness values of sub-formulas predicating over signals having diﬀerent scales. In
this paper, we propose QB-Robustness, a new STL semantics that does not
suﬀer from the scale problem, because it avoids such comparison. The computation of QB-Robustness requires to specify a sub-formula sequence telling forwhich sub-formulas the quantitative robustness must be computed. We thenpropose a Monte Carlo Tree Search (MCTS)-based falsiﬁcation approach thatsynthesizes a sub-formula sequence for QB-Robustness, and uses this for guiding
numerical optimization. Experimental results show that the proposed approachachieves better falsiﬁcation results than a state-of-the-art falsiﬁcation tool thatuses standard quantitative robust semantics.
In the analysis of RQ1, we observed that, when the speciﬁcations have a particular structure, our approach has no advantage and, actually, it could decrease
the performance by trying to ﬁnd a best sub-formula sequence that does notexist for the current initial sampling. As future work, we plan to devise someheuristics that could handle these cases: for example, we could perform a better
initial sampling (see Subsect. 2.1) that could provide a better initial guidance.

References
1. Abbas, H., Fainekos, G.: Convergence proofs for simulated annealing falsiﬁcationof safety properties. In: 50th Annual Allerton Conference on Communication, Control, and Computing, pp. 1594–1601. IEEE (2012)
2. Adimoolam, A., Dang, T., Donzé, A., Kapinski, J., Jin, X.: Classiﬁcation andcoverage-based falsiﬁcation for embedded control systems. In: Majumdar, R.,
Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 483–503. Springer, Cham(2017). https://doi.org/10.1007/978-3-319-63387-9 24
3. Akazaki, T., Kumazawa, Y., Hasuo, I.: Causality-aided falsiﬁcation. In: Proceedings First Workshop on Formal Veriﬁcation of Autonomous Vehicles, FVAV@iFM
2017, Turin, Italy, 19th September 2017. EPTCS, vol. 257, pp. 3–18 (2017)
4. Annpureddy, Y., Liu, C., Fainekos, G., Sankaranarayanan, S.: S-TaLiRo: a tool
for temporal logic falsiﬁcation for hybrid systems. In: Abdulla, P.A., Leino, K.R.M.
(eds.) TACAS 2011. LNCS, vol. 6605, pp. 254–257. Springer, Heidelberg (2011).
https://doi.org/10.1007/978-3-642-19835-9 21

616

Z. Zhang et al.

5. Arcuri, A., Briand, L.: A practical guide for using statistical tests to assess randomized algorithms in software engineering. In: Proceedings of the 33rd International
Conference on Software Engineering, ICSE 2011, pp. 1–10. ACM New York (2011)
6. Auer, P.: Using conﬁdence bounds for exploitation-exploration trade-oﬀs. J. Mach.
Learn. Res. 3, 397–422 (2002)
7. Auger, A., Hansen, N.: A restart CMA evolution strategy with increasing population size. In: Proceedings of the IEEE Congress on Evolutionary Computation,
CEC 2005, pp. 1769–1776. IEEE (2005)
8. Browne, C., et al.: A survey of monte carlo tree search methods. IEEE Trans.
Comput. Intellig. AI Games 4(1), 1–43 (2012)
9. Chen, X., Ábrahám, E., Sankaranarayanan, S.: Flow*: an analyzer for non-linear
hybrid systems. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp.
258–263. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-397998 18
10. Deshmukh, J., Jin, X., Kapinski, J., Maler, O.: Stochastic local search for falsiﬁcation of hybrid systems. In: Finkbeiner, B., Pu, G., Zhang, L. (eds.) ATVA 2015.
LNCS, vol. 9364, pp. 500–517. Springer, Cham (2015). https://doi.org/10.1007/
978-3-319-24953-7 35
11. Deshmukh, J.V., Horvat, M., Jin, X., Majumdar, R., Prabhu, V.S.: Testing cyberphysical systems through bayesian optimization. ACM Trans. Embedded Comput.
Syst. 16(5), 170:1–170:18 (2017)12. Dokhanchi, A., Yaghoubi, S., Hoxha, B., Fainekos, G.E.: Vacuity aware falsiﬁcation
for MTL request-response speciﬁcations. In: 13th IEEE Conference on Automation
Science and Engineering, CASE 2017, Xi’an, China, 20–23 August 2017, pp. 1332–
1337. IEEE (2017)13. Donzé, A.: Breach, a toolbox for veriﬁcation and parameter synthesis of hybrid
systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp.
167–170. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-142956 17
14. Donzé, A., Maler, O.: Robust satisfaction of temporal logic over real-valued signals.
In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp.
92–106. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15297-9 9
15. Dreossi, T., Dang, T., Donzé, A., Kapinski, J., Jin, X., Deshmukh, J.V.: Eﬃcient guiding strategies for testing of temporal properties of hybrid systems. In:
Havelund, K., Holzmann, G., Joshi, R. (eds.) NFM 2015. LNCS, vol. 9058, pp.
127–142. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-17524-9 10
16. Dreossi, T., Dang, T., Piazza, C.: Parallelotope bundles for polynomial reachability. In: Proceedings of the 19th International Conference on Hybrid Systems:
Computation and Control, HSCC 2016 pp. 297–306. ACM, New York (2016)17. Dreossi, T., Donzé, A., Seshia, S.A.: Compositional falsiﬁcation of cyber-physicalsystems with machine learning components. In: Barrett, C., Davies, M., Kahsai, T.
(eds.) NFM 2017. LNCS, vol. 10227, pp. 357–372. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-57288-8 26
18. Ernst, G., et al.: ARCH-COMP 2020 category report: Falsiﬁcation. In: ARCH20.
7th International Workshop on Applied Veriﬁcation of Continuous and Hybrid
Systems (ARCH20). EPiC Series in Computing, vol. 74, pp. 140–152. EasyChair(2020)
19. Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic speciﬁcations forcontinuous-time signals. Theor. Comput. Sci. 410(42), 4262–4291 (2009)

Eﬀective Falsiﬁcation Using MCTS Guided by QB-Robustness

617

20. Fan, C., Qi, B., Mitra, S., Viswanathan, M., Duggirala, P.S.: Automatic reachability analysis for nonlinear hybrid models with C2E2. In: Chaudhuri, S., Farzan, A.
(eds.) CAV 2016. LNCS, vol. 9779, pp. 531–538. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41528-4 29
21. Ferrère, T., Nickovic, D., Donzé, A., Ito, H., Kapinski, J.: Interface-aware signal
temporal logic. In: Proceedings of the 22nd ACM International Conference on
Hybrid Systems: Computation and Control, HSCC 2019, Montreal, QC, Canada,
16–18 April 2019, pp. 57–66 (2019)22. Frehse, G., et al.: SpaceEx: scalable veriﬁcation of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379–395. Springer,
Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1 30
23. Hasuo, I., Suenaga, K.: Exercises in nonstandard static analysis of hybrid systems.
In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 462–478.
Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31424-7 34
24. Hoxha, B., Abbas, H., Fainekos, G.E.: Benchmarks for temporal logic requirements
for automotive systems. In: 1st and 2nd International Workshop on Applied veRiﬁcation for Continuous and Hybrid Systems, ARCH@CPSWeek 2014, Berlin, Germany, 14 April 2014/ARCH@CPSWeek 2015, Seattle, USA, 13 April 2015. EPiC
Series in Computing, vol. 34, pp. 25–30. EasyChair (2014)
25. Jin, X., Deshmukh, J.V., Kapinski, J., Ueda, K., Butts, K.: Powertrain control
veriﬁcation benchmark. In: Proceedings of the 17th Int. Conf. on Hybrid Systems:
Computation and Control, HSCC 2014, pp. 253–262. ACM, NY, USA (2014)
26. Kapinski, J., Deshmukh, J.V., Jin, X., Ito, H., Butts, K.: Simulation-based
approaches for veriﬁcation of embedded control systems: an overview of traditional
and advanced modeling, testing, and veriﬁcation techniques. IEEE Control Syst.
36(6), 45–64 (2016)
27. Kato, K., Ishikawa, F.: Learning-based falsiﬁcation for model families of cyberphysical systems. In: 2019 IEEE 24th Paciﬁc Rim International Symposium on
Dependable Computing (PRDC), pp. 236–245 (December 2019)
28. Kocsis, L., Szepesvári, C.: Bandit based monte-carlo planning. In: Fürnkranz, J.,
Scheﬀer, T., Spiliopoulou, M. (eds.) ECML 2006. LNCS (LNAI), vol. 4212, pp.
282–293. Springer, Heidelberg (2006). https://doi.org/10.1007/11871842 29
29. Kuřátko, J., Ratschan, S.: Combined global and local search for the falsiﬁcation of
hybrid systems. In: Legay, A., Bozga, M. (eds.) FORMATS 2014. LNCS, vol. 8711,
pp. 146–160. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-105123 11
30. Lee, R., Kochenderfer, M.J., Mengshoel, O.J., Brat, G.P., Owen, M.P.: Adaptive
stress testing of airborne collision avoidance systems. In: Digital Avionics Systems
Conference, 2015 IEEE/AIAA 34th, pp. 6C2-1. IEEE (2015)
31. Liebrenz, T., Herber, P., Glesner, S.: Deductive veriﬁcation of hybrid control systems modeled in Simulink with KeYmaera X. In: Sun, J., Sun, M. (eds.) ICFEM
2018. LNCS, vol. 11232, pp. 89–105. Springer, Cham (2018). https://doi.org/10.
1007/978-3-030-02450-5 6
32. Luersen, M.A., Le Riche, R.: Globalized Nelder-mead method for engineering optimization. Comput. Struct. 82(23), 2251–2260 (2004)
33. Platzer, A.: Logical Foundations of Cyber-Physical Systems. Springer, Cham(2018) https://doi.org/10.1007/978-3-319-63588-0
34. Seshia, S.A., Rakhlin, A.: Quantitative analysis of systems using game-theoretic
learning. ACM Trans. Embed. Comput. Syst. 11(S2), 55:1–55:27 (2012)
35. Silver, D., et al.: Mastering the game of Go with deep neural networks and tree
search. Nature 529, 484–489 (2015)

618

Z. Zhang et al.

36. Silvetti, S., Policriti, A., Bortolussi, L.: An active learning approach to the falsiﬁcation of black box cyber-physical systems. In: Polikarpova, N., Schneider, S.
(eds.) IFM 2017. LNCS, vol. 10510, pp. 3–17. Springer, Cham (2017). https://doi.
org/10.1007/978-3-319-66845-1 1
37. Akazaki, T., Liu, S., Yamagata, Y., Duan, Y., Hao, J.: Falsiﬁcation of cyberphysical systems using deep reinforcement learning. In: Havelund, K., Peleska, J.,
Roscoe, B., de Vink, E. (eds.) FM 2018. LNCS, vol. 10951, pp. 456–465. Springer,
Cham (2018). https://doi.org/10.1007/978-3-319-95582-7 27
38. Zhang, Z., Arcaini, P., Hasuo, I.: Hybrid system falsiﬁcation under (in)equality
constraints via search space transformation. IEEE Trans. Comput. Aided Des.
Integr. Circ. Syst. 39(11), 3674–3685 (2020)
39. Zhang, Z., Ernst, G., Sedwards, S., Arcaini, P., Hasuo, I.: Two-layered falsiﬁcationof hybrid systems guided by monte carlo tree search. IEEE Trans. Comput. Aided
Des. Integr. Circuits Syst. 37(11), 2894–2905 (2018)
40. Zhang, Z., Hasuo, I., Arcaini, P.: Multi-armed bandits for Boolean connectives inhybrid system falsiﬁcation. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol.
11561, pp. 401–420. Springer, Cham (2019). https://doi.org/10.1007/978-3-03025540-4 23
41. Zhang, Z., Lyu, D., Arcaini, P., Ma, L., Hasuo, I., Zhao, J.: On the eﬀectivenessof signal rescaling in hybrid system falsiﬁcation. In: Dutle, A., Moscato, M.M.,
Titolo, L., Muñoz, C.A., Perez, I. (eds.) NFM 2021. LNCS, vol. 12673, pp. 392–
399. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-76384-8 24
42. Zutshi, A., Deshmukh, J.V., Sankaranarayanan, S., Kapinski, J.: Multiple shooting,cegar-based falsiﬁcation for hybrid systems. In: 2014 International Conference on
Embedded Software, EMSOFT 2014, New Delhi, India, 12–17 October 2014, pp.
5:1–5:10. ACM (2014)

Open Access This chapter is licensed under the terms of the Creative Commons
Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/),
which permits use, sharing, adaptation, distribution and reproduction in any medium
or format, as long as you give appropriate credit to the original author(s) and thesource, provide a link to the Creative Commons license and indicate if changes were
made.
The images or other third party material in this chapter are included in thechapter’s Creative Commons license, unless indicated otherwise in a credit line to thematerial. If material is not included in the chapter’s Creative Commons license andyour intended use is not permitted by statutory regulation or exceeds the permitteduse, you will need to obtain permission directly from the copyright holder.