日本ソフトウェア科学会第 38 回大会 (2021 年度) 講演論文集

Eﬀective Hybrid System Falsiﬁcation Using Monte Carlo
Tree Search Guided by QB-Robustness
Zhenya Zhang, Deyun Lyu, Paolo Arcaini, Lei Ma, Ichiro Hasuo, Jianjun Zhao
Hybrid system falsiﬁcation is an important quality assurance method for cyber-physical systems with theadvantage of scalability and feasibility in practice than exhaustive veriﬁcation. Falsiﬁcation, given a desired
temporal speciﬁcation, tries to ﬁnd an input of violation instead of a proof guarantee. The state-of-theart 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 beenshown that the performance of falsiﬁcation could be severely aﬀected by the so-called scale problem, related
to the diﬀerent scales of the signals used in the speciﬁcation (e.g., rpm and speed): in the robustness computation, the contribution of a signal could be masked by another one. In this paper, we propose a novel
approach to tackle this problem. We ﬁrst introduce a new robustness deﬁnition, called QB-Robustness,
which combines classical Boolean satisfaction and quantitative robustness. We prove that QB-Robustness
can be used to judge 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 structureof the formal speciﬁcation. First, tree traversal identiﬁes the sub-formulas for which it is needed to computethe 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 the state-of-the-art falsiﬁcation approaches guided by theclassical quantitative robustness, and it is largely not aﬀected by the scale problem.

ﬁnite search spaces, making their veriﬁcation often

1 Introduction

extremely diﬃcult.

Cyber-Physical Systems (CPS) are hybrid sys-

Falsiﬁcation has been proposed as a more practi-

tems that combine physical systems (with continu-

cally feasible approach that tackles the dual prob-

ous dynamics) and digital controllers (that are in-lem of veriﬁcation: instead of exhaustively proving

herently discrete). Being often safety-critical, theira property, falsiﬁcation intends to uncover the ex-

quality assurance is of great importance and widely

istence of its violation with counterexamples. For-

investigated by both academia and industry. The

mally, the problem is deﬁned as follows. Given a

continuous dynamics of hybrid systems leads to in-model M taking an input signal u and outputtingThis work was originally published at 33rd International Conference on Computer-Aided Veriﬁcation. [41]Zhenya Zhang, Deyun Lyu, Jianjun Zhao, 九州大学
大 学 院 シ ス テ ム 情 報 科 学 研 究 院, Graduate Schoolof Information Science and Electrical Engineering,
Kyushu University.
Paolo Arcaini, Ichiro Hasuo, 国立情報学研究所, National Institute of Informatics.
Lei Ma, University of Alberta, Canada.

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 suchthat the corresponding output M(u) violates φ.
The most pursued and successful approach tothe falsiﬁcation problem consists in turning it into
an optimization problem; we call it optimizationbased falsiﬁcation. This is possible thanks to thequantitative robust semantics of temporal formu-bustness of an atomic formula f (⃗x) < c is givenlas [14, 19]. Robust semantics extends the classicalby the margin c − f (⃗x).

Boolean satisfaction relation v |= φ in the following

ness of φ under the signal (gear , speed ), where

way: it assigns a value Jw, φK ∈ R ∪ {∞, −∞} (i.e.,
robustness) that tells not only whether φ is satis-gear , speed : [0, 30] → R, is J(gear , speed ), φK =
((
) (
))
d
6 − gear (t) ⊔ 130 − speed (t) . Notet∈[0,30]

ﬁed or violated (by the sign), but also how robustly

that the robustness of φ1 is always in the order ofthe formula is satisﬁed or violated.

units, while the robustness of φ2 is, in general, in

Therefore, the robust-

Optimization-based falsiﬁcation approaches adopt

the order of tens. It is not diﬃcult to see that, if

hill-climbing stochastic optimization strategies toboth φ1 and φ2 are satisﬁed, the robustness of φgenerate inputs to decrease robustness, which

will only depend on φ1 (because of the minimum interminate when they ﬁnd an input with nega-

the robust semantics of the logical connective). In

tive robustness, i.e., a falsifying input that trig-

this case, we say that φ1 masks φ2 . In such a case,gers the violation of the speciﬁcation φ. Diﬀer-

a falsiﬁcation approach relying on robustness willent optimization-based falsiﬁcation algorithms havebe misled during the search. Note that, in this par-been proposed (see [26] for a survey), and mature

ticular case, the only way to falsify φ is to falsify

tools (e.g., Breach [13] and S-TaLiRo [4]) have also

φ2 , because φ1 is always satisﬁed; therefore, falsify-

been developed.

ing this relatively simple formula could be extremely

The scale problem is a recognized issue in
optimization-based falsiﬁcation [21, 40],

which

could arise when multiple signals with diﬀerentdiﬃcult for state-of-the-art optimization-based falsiﬁcation approaches (as we will show and have conﬁrmed in the experiments).

scales are present in the speciﬁcation. Namely, it

In this paper, we propose a novel approach tois due to the computation of robust semantics oftackle the scale problem in optimization-based fal-

Boolean connectives, i.e., the way in which the ro-

siﬁcation. Our intuition and insights are that webustness values of diﬀerent sub-formulas are com-

should try to avoid the comparison of robustness

pared and aggregated: such computation is prob-

values of diﬀerent sub-formulas, so that one sub-lematic in the presence of signals that take values

formula does not mask the contribution of another

having diﬀerent order of magnitudes.

one.

Example 1 As very simple example, let us con-

To achieve this, we ﬁrst propose a new way ofsider the formula φ ≡ 2[0,30] (φ1 ∧ φ2 ), with φ1 ≡computing the satisfaction of a formula that com-

gear < 6 and φ2 ≡ speed < 130. It is appar-bines quantitative robust semantics and Boolean

ent that φ1 is always satisﬁed (in any car model

semantics. We name the new semantics as QB-

with 5 gears), and it has been added in the speciﬁcation as redundant check.†1 According to ro-

Robustness. QB-Robustness, for each type of for-bust semantics, the Boolean connective ∧ is in-its sub-formulas {φ1 , . . . , φK }. For φk , the quan-

terpreted by minimum ⊓, and the “always” operd
ator 2[0,30] is interpreted by inﬁmum ; the ro-titative robust semantics is computed, while for†1 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 much less trivial speciﬁcations, as we
will see in the experiments.

mula φ, requires selecting a sub-formula φk among

the other sub-formulas the Boolean semantics is
computed.

Therefore, the computation of QB-

Robustness requires identifying a path Σ along
the parse tree of the formula φ, where visited
sub-formulas are those for which the quantita-

tive robustness is computed. We prove that QB-

best Σ and running optimization-based falsiﬁcation

Robustness, independently of the selected Σ, isin which QB-Robustness with Σ is used.

equivalent (in terms of sign and satisfaction) to

Overall, the major Contributions of this paper

the quantitative robust semantics (and also to theare summarized as follows:

Boolean one).

• We propose a novel semantics (QB-Robustness)

In general QB-Robustness is a useful tool for

for STL formulas that combines quantitative

avoiding the scale problem of falsiﬁcation. By deﬁ-robustness and Boolean satisfaction. We prove

nition, the quantitative robustness of diﬀerent sub-that QB-Robustness can be used to show theformulas is never compared, so removing the main

satisﬁability of STL formulas;cause of the scale problem. It would then make• We deﬁne a falsiﬁcation approach based on

sense to use it for guiding the optimization-based

MCTS that exploits QB-Robustness to address

falsiﬁcation process. However, QB-Robustness re-the scale problem;

quires to choose a particular sequence Σ of sub-• We implement the approach in the tool

formulas for which to compute the quantitative ro-

ForeSee, based on which, we performed in-bustness. It is relatively easy to show that some ofdepth evaluation, demonstrating the eﬀective-

them provide a better guidance than others to theness and advantage of our approach comparedfalsiﬁcation search. Considering the previous exam-with the state of the art.

ple, if Σ contains φ1 , we can encounter the prob-

Paper structure In §2, we introduce the preliminar-

lem that the quantitative robustness of φ1 would

ies of the optimization-based falsiﬁcation. In §3, we

not provide any guidance (i.e., no big variations

introduce the novel STL semantics QB-Robustness,in the robustness values would be observed). On

and, in §4, we describe the MCTS-based falsiﬁ-

the other hand, if Σ contains φ2 , the quantitative

cation approach that uses QB-Robustness. In §5,

robustness would have larger variations, providing

we describe the experiments and evaluation results.

more eﬀective guidance to the search.

Finally, we discuss most relevant work to ours in §6,Then, the key problem is how to select the bestand conclude the paper in §7.

Σ, that enables the hill-climbing optimization usedin falsiﬁcation to be more eﬀective. In general, al-

2 Preliminaries

though it is often diﬃcult to know the best Σ in

In this section, we brieﬂy review the falsiﬁcation

advance, it is still possible to learn it by observing

framework based on robust semantics of temporal

sampling results using diﬀerent Σ. Based on thislogic [14].

intuition, we propose a novel falsiﬁcation approach

Let T∈ R+ be a positive real.

An M -

that identiﬁes the sequences Σ that is more likely

dimensional signal with a time horizon T is a func-

to be eﬃcient, and uses them in the new falsiﬁca-

tion w : [0, T ] → RM . We treat the system modeltion trials. Our approach could be seen as an in-

as a black box, i.e., its behaviors are only observed

stantiation of the classical Monte Carlo Tree Searchfrom inputs and their corresponding outputs. For-(MCTS) method [8, 28], which is able to eﬃciently

mally, a system model, with M -dimensional input

tackle the exploration-exploitation tradeoﬀ. In ourand N -dimensional output, is a function M that

context, exploration consists in incrementally con-takes an input signal u : [0, T ] → RM and returns astructing the tree that represents all the possible

signal M(u) : [0, T ] → RN . Here the common time

sequences, and exploitation consists in selecting thehorizon T ∈ R+ is arbitrary.

2. 1 Hill Climbing-Guided Falsiﬁcation

Deﬁnition 2 (STL Syntax) We ﬁx a set Var of

So far, the falsiﬁcation problem has received ex-

variables. In Signal Temporal Logic (STL), atomic

tensive industrial and academic attention.

propositions and formulas are deﬁned as follows,

possible approach direction by hill-climbing opti-

respectively: α ::≡ f (x1 , . . . , xN ) > 0, and φ ::≡∧∨α | ⊥ | ¬φ | φ | φ | 2I φ | 3I φ | φUI φ Here f ismization is an established ﬁeld, too: see [2–4, 10,

an N -ary function f : R

One

13–15,17,26,29,36–39,43] and the tools Breach [13]→ R, x1 , . . . , xN ∈ Var,and S-TaLiRo [4]. We formulate the problem andand I is a closed non-singular interval in R≥0 , i.e.,the methodology, for later use in describing our fal-

I = [a, b] or [a, ∞), where a, b ∈ R and a < b.

siﬁcation approach.

2, 3 and U are temporal operators, which are usu-

Deﬁnition 4 (Falsifying Input) Let M be aally known as always, eventually and until respec-

system model, and φ be an STL formula. A sig-

tively. The always operator 2 and eventually oper-

nal u : [0, T ] → R|Var| is a falsifying input if

ator 3 can also be considered as special cases of

JM(u), φK < 0; the latter implies M(u) ̸|= φ.

the until operator U, where 3I φ ≡ ⊤ UI φ and

The use of quantitative robust semantics JM(u), φK ∈2I φ ≡ ¬3I ¬φ. Other common connectives such as

R ∪ {∞, −∞} in the above problem enables the use→, ⊤ are introduced as syntactic sugar: ⊤ ≡ ¬⊥,of hill-climbing optimization.

φ1 → φ2 ≡ ¬φ1 ∨ φ2 .

Deﬁnition 5 (Hill Climbing-Guided Falsiﬁcation)N

Deﬁnition 3 (Quantitative Robust Semantics) Assume the setting in Def. 4, for ﬁnding a falsifyLet w : [0, T ] → RN be an N -dimensional signal,

ing input, the methodology of hill climbing-guided

and t ∈ [0, T ). The t-shift w of w is the signal

falsiﬁcation is presented in Algo. 1.

tw : [0, T − t] → R
t

N

t

′

′

deﬁned by w (t ) := w(t + t ).
Algorithm 1 Hill climbing-guided falsiﬁcation

Let φ be an STL formula. We deﬁne the robustnessJw, φK ∈ R ∪ {∞, −∞} as follows, by induction ond⊔the construction of formulas.
anddenote inﬁmums and supremums of real numbers, respectively.
d⊓, the binary version of , denotes minimum.
()
Jw, f (x1 , · · · , xn ) > 0K := f w(0)(x1 ), · · · , w(0)(xn )Jw, ⊥K := −∞Jw, ¬φK := −Jw, φK∧l
Jw,
φi K :=Jw, φi K
i
i
∨
⊔
Jw,
φi K :=Jw, φi KiilJw, 2I φK :=Jwt , φK⊔t∈I∩[0,T ]Jw, 3I φK :=Jwt , φKt∈I∩[0,T ]Jw, φ1 UI φ2 K :=⊔t∈I∩[0,T ](Jwt , φ2 K ul′

Jwt , φ1 K

t′ ∈[0,t))Require: a system model M, an STL formula φ, anda time budget
1: function Hill-Climb-Falsify(M, φ)2:initialize a placeholder u and rb ← ∞▷ thebest input signal and robustness3:
H ← ∅ ▷ sampling history of input signals androbustness
4:
while rb ≥ 0 and within the time budget do
5:u′ ← Hill-Climb(H)▷ run hill climbing
based on sampling history6:rb′ ← JM(u′ ), φK▷ compute robustness
7:
H ← H ∪ {(u′ , rb′ )}▷ update sampling
history8:
if rb′ < rb then9:rb ← rb′ , u ← u′
▷ update the best
input and robustness{uif rb < 010:
returnFailure otherwise

The original STL semantics is Boolean, given bya binary relation |= between signals and formulas.
The robust semantics reﬁnes the Boolean one in
the following sense: Jw, φK > 0 implies w |= φ, andJw, φK < 0 implies w ̸|= φ, see [19, Prop. 16].

Here, the function Hill-Climb makes a guess ofan input signal u′ , aiming at minimizing the robustness JM(u′ ), φK. It does so, learning from thesampling history H that contains the previous ob-

proach consists in introducing a new semantics forservations of input signals and their corresponding

STL that does not suﬀer from the scale problem.

robustness values.

Such new semantics will be used in a falsiﬁcation

The Hill-Climb function can be designed based

approach based on Monte Carlo Tree Search. We

on various stochastic optimization algorithms.

describe details of the new semantics in this section,

Typically, at the early phase of the optimization,and the new falsiﬁcation approach in §4.

the proposal of new input is usually based on ran-

The new proposed semantics,

called QB-

dom sampling; as the set of sampling history grows

Robustness, combines quantitative robustness andlarger, the algorithm takes various metaheuristic-

Boolean satisfaction.

based strategies to achieve the optimization goalcompares quantitative robustness values that comeeﬃciently.

Examples of such algorithms include

from diﬀerent sub-formulas, thus avoiding the scale

Covariance Matrix Adaption Evolution Strategy

problem. QB-Robustness is deﬁned for the whole(CMA-ES) [7] (used in our experiments), Simulated

STL formulas, except for the “until” operator φ1 UI

Annealing, Global Nelder Mead [32], etc.

φ2 , when φ1 is an arbitrary formula. We still support it as “eventually” and “always” operators†2 ,By construction, it never

3 QB-Robustnessi.e., when φ1 = ⊤. Note that this is not a ma-

The scale problem is a known important issue

jor limitation, as QB-Robustness still supports thethat negatively aﬀects the performance of falsi-

majority of speciﬁcations that are used in industry:ﬁcation, which arises when connective operators

indeed, in the experiments, we were able to handle(i.e., conjunction and disjunction) with operands

all the speciﬁcations used in falsiﬁcation competi-that predicate on diﬀerent signals appear in thetions [18], which collect benchmarks from industrial

STL formula under falsiﬁcation. According to thecase studies.

classic quantitative robust semantics (see Def. 3),

To better explain the computation of QB-

the robustness of those formulas is calculated

Robustness, we introduce some deﬁnitions. Let us

based on the comparison (minimum for conjunc-

ﬁrst deﬁne the notion of immediate sub-formula fortion, and maximum for disjunction) between ro-

STL.

bustness values coming from the diﬀerent operandDeﬁnition 6 (Immediate Sub-Formulas) Let φ

sub-formulas. However, since diﬀerent signals may

be an STL formula (see Def. 2). We deﬁne the set

diﬀer in magnitude, the comparison may be biased,

ISForm(φ) of immediate sub-formulas of φ as fol-such that one signal w may always (or often) masklows:

the contribution of the others, and, therefore, theISForm(α) := ∅ﬁnal robustness may be dominated by this signal w.

ISForm(¬φ) := ISForm(φ)∧
ISForm(φi ) := {φ1 , . . . , φK }Note that, although the scale problem aﬀects con-i∈{1,...,K}

nective operators, it is not only local to the place of
their application, but it is always propagated to the

ISForm(⊥) := ∅ISForm(∨φi ) := {φ1 , . . . , φK }i∈{1,...,K}

robustness of the whole formula. The scale prob-

ISForm(2I φ) := ISForm(φ)

lem has been shown as a root cause of the failure

ISForm(3I φ) := ISForm(φ)

of many falsiﬁcation problems [21, 40].
In this work, we propose a novel approach forsolving the scale problem in falsiﬁcation. Our ap-†2 Recall from Def. 2 that the “eventually” and “always” operators are deﬁned in terms of the “until”
operator.

Intuitively, the immediate sub-formula set of a con-in Σ and the Boolean satisfaction of the other sub-nective (conjunction or disjunction) contains all its

formulas. Based on such intuition, we deﬁne the se-operands. For the other unary operators (tempo-

mantics of our proposed QB-Robustness in Def. 8,

ral operators, negation, etc.), its immediate sub-and demonstrate its usefulness in Thm. 9.

formula set is given by the immediate sub-formulaDeﬁnition 8 (Semantics of QB-Robustness)

set of its argument.

Let φ be an STL formula as deﬁned in Def. 2,

Toand Σ be a sub-formula sequence w.r.t. φ. For∧∨φ ≡ φi | φi , let φk ∈ ISForm(φ) be the ﬁrst el-

this aim, we introduce the notion of sub-formula

ement Σhead of Σ, then we can represent these twosequence.

cases as φ ≡ φk ∧φk | φk ∨φk , where φk is the con-Deﬁnition 7 (Sub-Formula Sequence) Let φjunction (or disjunction, respectively) of the otherbe an STL formula. A sub-formula sequence Σ =formulas in ISForm(φ) \ {φk }. The QB-Robustness

σ1 · . . . · σL w.r.t. φ is deﬁned as follows:

QBRob(w, φ, Σ) of φ w.r.t. Σ is deﬁned as Fig. 1:

The computation of QB-Robustness requires toselect some nested immediate sub-formulas.

σ1 ∈ ISForm(φ)σl+1 ∈ ISForm(σl )with l = 1, . . . , L − 1

We now prove that the semantics of QB-

where the · is the concatenation operator in the se-

Robustness is equivalent (in the sense of satisfac-

quence. We use Σk to denote the kth element oftion) to the Boolean semantics, and so it can be

Σ. Moreover, we denote the ﬁrst element by Σhead ,used to show violation of a speciﬁcation in a falsi-

and the last element by Σrear . We use Σhead to de-ﬁcation algorithm, as we do in this paper.

note Σ without Σhead . We identify with ε the empty

Theorem 9 Let φ be an STL formula.

sequence; when ISForm(φ) = ∅, we use ε as its sub-a signal w, for any Σ ∈ Σφ , it holds that

formula sequence. We identify with Σφ the set of

QBRob(w, φ, Σ) > 0 implies w |= φ. Similarly,

all the sub-formula sequences rooted in φ.
To be speciﬁc, in a sub-formula sequence Σ, each

Given

for any Σ ∈ Σφ , it holds that QBRob(w, φ, Σ) < 0
implies w ̸|= φ.

element is one of the sub-formulas of the previous

Proof 10 We ﬁrst recall from [19, Prop. 16] thatelement. This means that, for Boolean connectives,Jw, φK < 0 implies w ̸|= φ, and that Jw, φK > 0

only one of the operands is selected. Moreover, an

implies w |= φ. We prove Thm. 9 by induction on

atomic sub-formula predicating over a single sig-

the structure of the formula.

nal can only appear as the ﬁnal element of a se-• Case φ = α. By Def. 8, QBRob(w, α, ε) > 0

quence. We exploit these characteristics of Σ toindicates that Jw, αK > 0 and hence w |= α,deﬁne QB-Robustness, which combines the quanti-

and QBRob(w, α, ε) < 0 that Jw, αK < 0 andtative robustness of the sub-formulas related to ahence w ̸|= φ.

given signal with the Boolean satisfaction of the• For the following cases,

let us assume

other sub-formulas. QB-Robustness, given a se-that Thm. 9 holds for an arbitrary for-quence Σ, decides whether to compute the quan-mula φ′ and its sub-formula sequence Σ′ thattitative robust semantics or the Boolean semantics

QBRob(w, φ′ , Σ′ ) > 0 implies Jw, φ′ K > 0, andof a sub-formula, by considering whether the sub-that QBRob(w, φ′ , Σ′ ) < 0 implies Jw, φ′ K < 0.

formula belongs to Σ or not. This implies that, in

We aim to prove that Thm. 9 also holds for φ,

the case of conjunction and disjunction, we evalu-

resulting from the application of the operator

ate the quantitative robustness of the sub-formulain each of the following cases to φ′ , and Σ, theQBRob(w, α, ε) := Jw, αK

QBRob(w, ⊥, ε) := −∞QBRob(w, ¬φ, Σ) := −QBRob(w, φ, Σ) QBRob(w, φ , Σ )if w |= φkk
headQBRob(w, φk ∧ φk , Σ) := −∞otherwise QBRob(w, φ , Σ )if w ̸|= φkk
headQBRob(w, φk ∨ φk , Σ) := ∞otherwisel⊔t
QBRob(w, 2I φ, Σ) :=QBRob(w , φ, Σ)
QBRob(w, 3I φ, Σ) :=QBRob(wt , φ, Σ)
t∈I

t∈I

図 1: QB-Robustness

the semantics of the always operator

sub-formula sequence of φ.
– Case φ = φ′ ∧ ψ, where ψ is an ar′′2, it holds that w ̸|= φ.

Let Σ = φ · Σ , and∗ By Def. 8, QBRob(w, φ, Σ) > 0 indi-

let us consider the two cases in whichcates that for all t ∈ I it holds that

QBRob(w, φ, Σ) is negative and positive

QBRob(wt , φ′ , Σ) > 0. Then, by as-

separately:

sumption, it holds that for all t ∈ I,

∗ If QBRob(w, φ, Σ) < 0, there are two

wt |= φ′ .

bitrary formula.

So, by the semantics ofthe always operator 2, it holds that

sub-cases:′′· if QBRob(w, φ , Σ ) < 0, then′Jw, φ K < 0 (by assumption).

w |= φ.
– Case φ = ¬φ′ .

Let Σ = Σ′ , andThen, by the robust semantics

let us consider the two cases in whichof conjunction, also Jw, φK < 0

QBRob(w, φ, Σ) is negative and positive

holds, and so it does w ̸|= φ.

separately:′′· if QBRob(w, φ , Σ ) > 0, then′

∗ By Def. 8, QBRob(w, φ, Σ) < 0 indi-

Jw, φ K > 0 (by assumption).

cates that QBRob(w, φ′ , Σ′ ) > 0. By

Then, it holds w ̸|= ψ by Def. 8,

assumption, it holds that w |= φ′ , andand, therefore, it holds w ̸|= φ.

therefore, w ̸|= φ.

∗ If QBRob(w, φ, Σ) > 0, it means∗ By Def. 8, QBRob(w, φ, Σ) > 0 indi-that QBRob(w, φ′ , Σ′ ) > 0 and w |=cates that QBRob(w, φ′ , Σ′ ) < 0. By

ψ (by Def. 8).

assumption, it holds that w ̸|= φ′ , and,By assumption, if

QBRob(w, φ′ , Σ′ ) > 0, then Jw, φ′ K >– Proofs for the cases of φ = φ′ ∨ ψ and

0. Therefore, w |= φ.
′– Case φ = 2I φ .

therefore, w |= φ.

′Let Σ = Σ , andlet us consider the two cases in which
QBRob(w, φ, Σ) is negative and positive

φ = 3I φ′ follow similar proof patterns,
and so are left to the readers.
We use an example to illustrate how QB-

separately:

Robustness is used for checking the satisﬁability of∗ By Def. 8, QBRob(w, φ, Σ) < 0 indi-an STL formula.

cates that there exists a t ∈ I such that

Example 11 Let w : [0, T ]QBRob(wt , φ′ , Σ) < 0. By assump-dimensional signal and φ = 2I (φ1 ∨ φ2 ) be an STL′tion, it holds that w ̸|= φ . Then, byt→

R2 be a 2-

formula where φ1 and φ2 are two atomic formu-

las. Intuitively, to make φ falsiﬁed, there must exist

lection of the sequence can aﬀect the performancet ∈ I such that w ̸|= φ1 and w ̸|= φ2 . Let us con-of the numerical optimization algorithms used insider a non-trivial falsiﬁcation problem in which,falsiﬁcation.

for most of the signals w, sets {t ∈ I | w ̸|= φ1 }6) ∧ (speed < 130)) as an example. As explainedand {t ∈ I | w ̸|= φ2 } are non-empty and disjoint.

in §1, numerical optimization will perform better if

By Def. 8, given the sub-formula sequence Σ =guided by the robustness values coming from speed

φ1 of φ, the corresponding QB-Robustness isdt
QBRob(w, φ, Σ) =t∈I QBRob(w , φ1 ∨ φ2 , φ1 ),rather than by those coming from gear . Therefore,i.e., it takes the inﬁmum of QBRob(w , φ1 ∨φ2 , φ1 )is important to select an appropriate sub-formula

t

t

t

t

t

′

over t ∈ I. Again, by Def. 8, for any t ∈ I,t′

QBRob(w , φ1 ∨ φ2 , φ1 ) is computed as follows:• if for a t′∈ I it holds wt′

Let us consider φ ≡ 2((gear <in a falsiﬁcation approach using QB-Robustness, itsequence Σ.
By using the QB-Robustness, the problem of fal-|= φ2 , thensifying an STL formula φ consists in ﬁnding both a

QBRob(wt , φ1 ∨ φ2 , φ1 ) = ∞. Then, it isd
impossible that t∈I QBRob(wt , φ1 ∨ φ2 , φ1 ) issignal w and a sub-formula sequence Σ such that′t′given by QBRob(w , φ1 ∨ φ2 , φ1 );• if for a t′∈ I it holds w

t′

crete, while the search for w is numerical. In or-

̸|= φ2 , thent′t′

QBRob(w , φ1 ∨φ2 , φ1 ) = QBRob(w , φ1 , ε) =′QBRob(w, φ, Σ) < 0. The selection of Σ is dis-′der to combine these processes that are diﬀerent
in nature, we propose to adapt Monte Carlo TreeIn this case, QBRob(wt , φ1 ∨Search (MCTS) [8, 28]. In the following, we ﬁrstly

φ2 , φ1 ) has a chance to determine the value ofdtt∈I QBRob(w , φ1 ∨ φ2 , φ1 ).

give a brief introduction to MCTS in §4. 1, and thenJwt , φ1 K.

Therefore,

when

QBRob(w, φ, Σ) =

Σ
d

φ1 ,

=

it

holds

that

present the application of MCTS to our falsiﬁcation
problem in §4. 2.

t∈S Jw , φ1 K, where S = {t ∈tI | w ̸|= φ2 }, i.e., the inﬁmum of the quantitative

4. 1 MCTS Backgroundrobustness of φ1 on the interval when φ2 is vio-

MCTS exempliﬁes the “trial and error” philoso-

lated. Indeed, once this value is negative, it means

phy, and has achieved a great success over the pastthat there exists a point t ∈ I when both φ1 and φ2

decade, most notably in ﬁelds such as the com-are violated; by the Boolean semantics of always

puter Go game [35]. MCTS explores the action

and disjunction, φ is violated.

space given by the possible actions of the system;t

for example, in the Go game, these are the positions

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

where to put the next stone. The approach builds atree of sequences of actions, and assigns rewards to

QB-Robustness never compares robustness val-

the diﬀerent branches. MCTS performs the searchues coming from signals with diﬀerent magnitudes,

by iteratively taking the following four steps. Seeand, therefore, it does not suﬀer from the scaleFig. 2, where the general scheme is adapted to our

problem. As such, it could be used in falsiﬁcation

current setting, for illustration.

approaches instead of the classical pure quantita-• Selection. It selects a node to expand or totive robustness.

reason about. Initially, selection has no other

However, a sub-formula sequence Σ is required

choice than the root. When a node has mul-when calculating QB-Robustness, and such se-tiple expanded children, selection will be done

quence is not unique (see Def. 8). Note that the se-according to the UCB1 [6] algorithm.

• Expansion. Child expansion happens after se-of a node is a sub-formula of the last element oflection if the selected node has unexpanded

the sequence represented by the node. The root ischildren. A child will be added to the tree dur-

initialized with a sequence holding φ only (Lines 2-

ing expansion.

3) and some other properties including the num-

• Playout. After a node is just expanded or a leaf

ber of visits to the diﬀerent nodes (Line 4), theis reached, playout is performed for evaluating

reward (Line 5), and the history of hill-climbing

the node. The evaluation is given by a reward,

sampling (Line 6). The main process of MCTS

which is a real number in [0, 1]. Reward canconsists in calling the MCTSSearch function it-

be interpreted diﬀerently in diﬀerent contexts.

eratively with the root as argument (Line 8), until

For example, in the Go game, the reward of athe exhaustion of the MCTS budget or a falsifying

position is measured by the winning rate when

input is found (Line 7). The MCTSSearch func-

a stone is positioned there; this is estimatedtion (Line 9) goes through the four phases, namely

by randomly playing the game until the end

selection, expansion, playout and backpropagation,

for n times, and then taking the ratio

nw
n

of

the number of winning as the winning rate.
• Backpropagation.

of the original MCTS algorithm.
4. 2. 0. 1 Selection

Backpropagation updates

Selection happens when a node has children

the number of visits and the reward of the(Line 10) and these have all been expanded

nodes along the path from the node of playout(Line 11).

to the root. These data are used in subsequent

UCB1 [6] algorithm (Line 12) to take a balance be-loops to decide the branches to explore.

tween exploration and exploitation. The exploita-

At the end, the action space will be suﬃciently ex-tion is embodied by the reward R(Σ · φi )—theplored in an unbalanced manner, by focusing on

higher the reward is, the more likely a falsifying in-

the most promising sub-spaces giving the highest

put is found following that branch. Exploration, in√N (Σ)
stead, is considered via 2Nln(Σ·φthat is negatively
i)rewards.

It selects a child according to thecorrelated to the number of visits to a child—the
4. 2 Proposed QB-Robustness-Guided Falsiﬁcation Approach

more the child was visited before, the less chance
it will be visited again. The scalar c is a tunable

We here propose a falsiﬁcation framework based

parameter that balances the trade-oﬀ between ex-

on MCTS in which, during tree construction, weploration and exploitation. After a child Σ · φk issynthesize and select a sub-formula sequence that

selected, it will be taken as the argument of the

facilitates the falsiﬁcation progress the most, and,next MCTSSearch loop (Line 18).

at the bottom layer of the tree, we run numerical

4. 2. 0. 2 Expansion

optimization to search for a falsifying input and

If not all the children of a node have been ex-

provide feedback (i.e., backpropagation) to guide

panded (Line 13), a child will be expanded. Ex-

the sequence selection.

pansion consists in randomly selecting a child from

We formalize our algorithm in Algo. 2 and visualize its execution in Fig. 2.

In the following, weelaborate on our approach.

the unexpanded child list (Line 14), adding it to
the tree (Line 15), initilizing properties including
the number of visits and history (Lines 16-17).

We construct the tree in this way: each node

After expansion, the newly expanded child will

represents a sequence of formulas, and each edge

be taken as the argument of the recursive call to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
2:
Σinit ← φ
▷ the root denoted as a sequence with φ only3:
T ← {Σinit }▷ the MCTS search tree, initially root only4:N ← (Σinit 7→ 0)▷ visit count N initialized, deﬁned only for root5:
R ← (Σinit 7→ 0)▷ reward function R initialized6:
H ← (Σinit 7→ ∅)▷ the sampling history of hill climbing
7:
while φ not falsiﬁed and within the MCTS budget BM do
8:
MCTSSearch(Σinit )9: function MCTSSearch(Σ)
10:
if ISForm(Σrear ) 6= ∅ then11:
if Σ · φk ∈ T for all φk ∈then)
( ISForm(Σrear )√2 ln N (Σ)
12:φk ←arg maxR(Σ · φi ) + c
N (Σ · φi )φi ∈ISForm(Σrear )
13:
14:
15:
16:
17:

else
randomly select φk from {φk ∈ ISForm(Σrear ) | Σ · φk 6∈ T }T ← T ∪ {Σ · φk }N (Σ · φk ) ← 0
H(Σ · φk ) ← ∅

18:
19:

MCTSSearch(Σ · φk )R(Σ) ←max
R(Σ · φk )

20:
21:
22:
23:
24:
25:

else
while within playout budget BP dou ← Hill-Climb(H(Σ))
rb ← QBRob(M(u), φ, Σhead )if rb < 0 thenreturn (u, rb)

26:
27:
28:

φk ∈ISForm(Σrear )H(Σ) ← H(Σ) ∪ {(u, rb)}

▷ the node has children▷ all children expanded▷ selection by UCB1
▷ unexpanded children exist▷ expand a new child▷ recursive call▷ back propagation for reward▷ a leaf node reached▷ playout by hill-climbing falsiﬁcation▷ hill-climbing▷ falsifying input found▷ record sampling history

R(w) ← Rwd(rb, H(Σ))
N (Σ) ← N (Σ) + 1▷ back propagation for visit count

MCTSSearch (Line 18).

quence, to compute the QB-Robustness as a guid-4. 2. 0. 3 Playoutance to the hill-climbing optimization (Line 23).

If a leaf node that has no children to expand

If a negative QB-Robustness is found (Line 24),is reached, the playout phase will start to devise

then the whole algorithm can be terminated anda reward for evaluating the visited path. In our

the input signal u that triggers the negative QB-

context, we deﬁne the reward based on the best

Robustness can be returned as the falsifying in-robustness value that can be obtained with theput (Line 25); otherwise, the sampling history of

path; speciﬁcally, playout consists in running hill-

hill climbing will be saved (Line 26) so that the

climbing guided falsiﬁcation to search for a minimal

future playout at the same leaf can be restored

robustness value (Line 22). Note that the sequence

from that context. After playout, the reward ofΣ represented by a leaf node is actually the concate-

the leaf node will be updated based on the deﬁ-nation between φ and a sub-formula sequence of φ.

nition of the reward, which will be introduced be-

We extract the suﬃx of Σ, i.e., the sub-formula se-low. Reward Since our goal is to ﬁnd a sequence ΣInitialization

Expansion

Playout

Backpropagation

'

'

'

'

'1

'11

'11

'11
hill climbing guided
by QB-Robustness⌃rb'1 · '11

Termination

selection by
UCB1 algorithm
visit : 1
rwd : 0.8

'1

'1

Selection

visit : 1
rwd : 0.8

'2

'1

'11

visit : 1
rwd : 0.8

visit : 1
rwd : 0.8

visit : 1
rwd : 0.2

'1

'11

'2

'12

a falsifying input found!

QBRob(M(u), ', ⌃)Hill-Climb({u, rb})

図 2: The workﬂow of MCTS-based falsiﬁcation guided by QB-Robustness. Let us consider the falsiﬁca-

tion of an STL formula φ = 2I (φ1 ∨ φ2 ), where φ1 = φ11 ∧ φ12 . Initially, there is only the root in thetree, so the algorithm selects it for expansion. Then, the algorithm keeps on randomly selecting a childof 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 from the 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 the possible 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.
with which hill-climbing optimization can minimize

sponds to the number of atomic sub-formulas (andQBRob(w, φ, Σ) smoothly, we connect the reward

so the leaves of the tree). Considering that most ofwith the hill-climbing progress. Formally, given a

the time is spent on playout, the complexity of oursampling history H, our reward (Line 27) is deﬁned

approach grows linearly with the number of atomic′

as Rwd(rb , H):=

max rbh −min ({rb′ }∪rbh ),max rbhwhere

sub-formulas.

rbh is the history of robustness values in H.
4. 2. 0. 4 Backpropagation

5 Experimental Evaluation

In MCTS, the playout result of a leaf is backprop-

In this section, we present the experiments weagated to the higher layer nodes along the path, so

conducted to evaluate the eﬀectiveness of the pro-that the future selection on the high layer is re-posed approach. We ﬁrst introduce the experiment

ferred. Backpropagation updates two properties ofsetup in §5. 1, and then we present the experimen-

each ancestor of the leaf till the root, the reward

tal evaluation results by answering three research(Line 19) and the number of visits (Line 28).

questions in §5. 2.

Remark 12 (Approach Complexity) With respect to classical falsiﬁcation, our approach introduces an exploration phase for searching the“best” sub-formula sequence to instantiate QBRobustness. The number of these sequences corre-5. 1 Experiment Setup

quirement to this system is that µ should not

5. 1. 0. 1 Simulink Models and Speciﬁca-

be deviated from the reference value too much
(AFC1); in addition to that, our speciﬁcations

tions
As our benchmarks, we selected three Simulink

also reason about the resilience of the systemmodels frequently used in the falsiﬁcation commu-(AFC5 and AFC6), and impose input con-nity (i.e., in the falsiﬁcation competitions [18]), andstraints (AFC2-6).

30 speciﬁcations deﬁned for them. All these mod-

• Free Floating Robot (FFR) [11] models robot

els are complicated hybrid systems with multiple

moving in a 2-dimentional space. It has four

input and output signals. The speciﬁcations are

input signals u1 , u2 , u3 , u4 ∈ [−10, 10] that are

STL formulas that formalize system requirements

boosters for a robot, and four output signals

regarding safety, performance, etc. Since we are in-that are the position in terms of coordinate

terested in assessing the inﬂuence of the scale prob-

values x, y and their one-order derivatives ẋ, ẏ.

lem to the performance of the compared falsiﬁca-

The speciﬁcations regulate the kinetic proper-

tion approaches, all the considered speciﬁcations

ties of the robot: FFR1 requires the robot topredicate over, at least, two signals. Table 1 re-pass an area around the point (4, 4) under anports the 30 speciﬁcations under test. The IDs of

input constraint, and FFR2 requires the robot

the speciﬁcations identify which models they belong to. A description of the three models and of

to stay in an area for at least 2 seconds.
5. 1. 0. 2 Baseline approach and our proposed approach

their speciﬁcations is as follows.
• Automatic Transmission (AT) [24] has two in-

In our experiments, we compare the perfor-

put signals, throttle ∈ [0, 100] and brake ∈mances of our proposed approach with the baseline[0, 325], and three outputs signals including

Breach approach. We implemented our approach

gear, speed and rpm. Most of the speciﬁca-

in the tool ForeSee, which stands for FORmula

tions we used formalize safety requirements of

Exploitation by Sequence trEE for falsiﬁcation.

the system. For instance, AT2 requires that

Breach is a state-of-the-art falsiﬁcation tool thatwhen gear is as high as 4, rpm should not be

implements the classic falsiﬁcation workﬂow we in-larger than 4300; AT3 is an adaptation of thetroduced in §2. The quantitative robustness calcu-

example we used in §1; AT10-12 reason about

lation in Breach is based on the robust semantics

the relationship among the three output sig-

given in Def. 3. Breach also encapsulates several

nals; AT17 speciﬁes three properties for threestochastic optimization algorithms, such as CMA-

diﬀerent time intervals; AT18 speciﬁes diﬀerent

ES, Simulated Annealing, etc. The implementation

properties for diﬀerent values of gear ; AT14,

of our ForeSee approach uses Breach only for inter-

AT21 and AT22 impose logical constraints on

facing with the Simulink model and for the calcula-

input signals, in addition to the property undertion of quantitative robustness; instead, the calcu-

consideration.

lation of QB-Robustness, and the implementation• Abstract Fuel Control (AFC) [25] takes twoof the MCTS algorithm are novel. Since CMA-ES∈ [8.8, 70] andhas proved to be the state-of-the-art stochastic al-EngineSpeed ∈ [900, 1100], and outputs a ra-

gorithm [39], we select CMA-ES as our backend

tio µ reﬂecting the deviation of air-fuel-ratio

optimizer for the playout phase.

input signals, PedalAngle

from its reference value. The basic safety re-

We apply the two approaches, ForeSee and表 1: Benchmarks – STL speciﬁcations
Spec. ID

Temporal speciﬁcation in STL

Spec. ID

Temporal speciﬁcation in STL

AT1

2[0,30] (gear = 4 → speed > 35)

AT82[0,10] (speed < 50) ∨ 3[0,30] (rpm > 2520)

AT2

2[0,30] (gear = 4 → 3[0,5] (rpm < 4300))AT9

3[10,30] (speed < 50 ∨ speed > 60 ∨ rpm < 1000)AT3

2[0,30] (speed < 130 ∧ gear < 5)AT10

2[0,30] (gear = 4 → (speed > 35 ∧ 3[0,5] (rpm < 4000)))

AT4

2[0,30] (speed < 135 ∧ rpm < 4780)

AT112[0,30] (3[0,8] (gear = 1 → (speed < 20 ∧ rpm < 600)))AT5

2[0,30] (rpm < 600 → 3[0,10] (gear > 1))

AT12

2[0,30] (gear < 3) ∨ 2[0,30] (speed < 135 ∧ rpm < 4780)

AT62[0,30] (3[0,5] (speed < 120 ∨ rpm > 3500))AT132[0,30] ((gear = 4 → 3[0,5] (rpm < 4000)) ∧ gear < 5)AT7

2[0,30] (rpm < 4750 ∧ gear < 5)AT14

2[0,30] (throttle = 0 ∨ brake = 0) → 2[0,30] (speed < 110)Spec. ID

Temporal speciﬁcation in STL

AT15

2[0,30] ((rpm < 4770 ∨ 2[0,1] (rpm > 1000)) ∧ 3[0,5] (gear < 5))AT16

2[0,30] (gear = 4 → ((3[0,5] (rpm < 3000) ∧ (gear = 2 → speed < 20))))AT172[0,5] (speed < 70 ∧ gear < 4) ∧ 2[10,20] (rpm < 4780) ∧ 2[25,30] (speed < 130)AT18

2[0,30] ((gear = 4 → 3[0,5] (rpm < 4250)) ∧ (gear = 3 → 3[0,5] (rpm < 4700)) ∧ (gear = 2 → 3[0,5] (rpm < 4800)))AT19

2[0,30] ((gear = 1 → speed < 80) ∧ (gear = 2 → speed < 90) ∧ (gear = 3 → speed > 20) ∧ (gear = 4 → speed > 30))AT20

2[0,29] (speed < 100) ∨ 2[29,30] (speed > 64) ∧ 2[0,30] (rpm < 4770 ∨ 2[0,1] (rpm > 700))AT212[0,30] (throttle > 90 → 3[0,10] (throttle < 30)) → 2[0,30] (gear = 4 → 3[0,5] (rpm < 4000))
2[0,30] (throttle > 70 → 3[0,10] (brake > 50)) → 2[0,30] (gear = 4 → speed > 35)

AT22
Spec. ID

Temporal speciﬁcation in STL

AFC1

2[11,50] (mode = 1 → µ < 0.228)

AFC2

3[0,50] (PedalAngle > 40) → 2[11,50] (µ < 0.225)

AFC3

3[0,50] (EngineSpeed > 1000) → 2[11,50] (µ < 0.225)

AFC4

2[0,50] (EngineSpeed > 910 ∨ PedalAngle > 25) → 2[11,50] (µ < 0.225)

AFC5

3[0,50] (PedalAngle > 40) → 2[11,50] (3[0,8] (µ < 0.06))

AFC6

3[0,50] (PedalAngle > 40 ∧ EngineSpeed > 1000) → 2[11,50] (3[0,8] (µ < 0.06))

Spec. ID

Temporal speciﬁcation in STL

FFR1

2[0,5] ((u1, u3 > 0 ∨ u1, u3 < 0) ∧ (u2, u4 > 0 ∨ u2, u4 < 0)) → 2[0,5] (¬(x1 > 3.9 ∧ x1 < 4.1) ∧ ¬(x3 > 3.9 ∧ x3 < 4.1))

FFR2¬(3[0,5] (2[0,2] (x1 > 1.5 ∧ x1 < 1.7 ∧ x3 > 1.5 ∧ x3 < 1.7)))

Breach, to each benchmark speciﬁcation reportedof an approach, i.e., it reﬂects the ability of an al-

in Table 1. Since both approaches are based on

gorithm to falsify the speciﬁcation. As second eval-stochastic optimization, we repeat each experi-

uation metric, we compute the average time (sec-ment for 30 times, as suggested by a guidelineonds), as average execution time of the successful

for conducting experiments with randomized algo-falsiﬁcation runs. Therefore, the average time is anrithms [5]. For each experiment, both approaches

indicator of the eﬃciency of the approach. We dohave been given a total timeout BM of 900 seconds

not report the number of simulations because these(see Alg. 2).

are consistent with the execution time.

5. 1. 0. 3 Evaluation Metrics

5. 1. 0. 4 Experiment Platform

As ﬁrst evaluation metric, we compute the falsiﬁ-

In our experiments, we use Breach [13] (vercation rate (FR) as the number of runs (out of 30)

1.2.13) with CMA-ES (the state of the art). Breachin which the approach returns a falsifying input.

accepts piece-wise constant signals as input for the

Therefore, FR is an indicator of the eﬀectiveness

Simulink models; we use the same settings used

in falsiﬁcation competitions [18]: we use piece-wise

be falsiﬁed. In such a case, there is no best sub-constant signals with ﬁve control points for AT andformula sequence Σ: therefore, the time spent by

AFC, and with four control points for FFR. As con-ForeSee in exploring diﬀerent Σ does not provide

ﬁguration of MCTS (see Alg. 2), we set the UCB1

any improvement.

scalar c to 0.2, and the playout budget BP to 10

Regarding the time execution, there is no clear

generations. The experiments have been executed

trend among the diﬀerent results:

sometimes

on an Amazon EC2 c4.2xlarge instance (2.9 GHz

ForeSee is faster, other times Breach is. However,Intel Xeon E5-2666 v3, 15 GB RAM).

even in the cases in which ForeSee is slower, it isstill below the timeout by which it manages to ﬁnd

5. 2 Evaluation

a falsifying input (so, leading to better falsiﬁcation

We here analyze the experimental results using

rates).

three research questions (RQs).

RQ2 Does the proposed approach solve the scale

RQ1 Does the proposed approach perform better

problem eﬀectively?

than state-of-the-art falsiﬁcation approaches?

The benchmarks reported in Table 1 and exper-

In this RQ, we aim at assessing whether the pro-imented in RQ1, predicate over signals having dif-

posed approach is indeed able to tackle the scale

ferent scales and so they suﬀer from the scale prob-

problem in falsiﬁcation and performs better thanlem. RQ1 showed that ForeSee is very eﬃcient instate-of-the-art approaches. Table 2 reports, forfalsifying them. In this RQ, we want to make aeach speciﬁcation benchmark, the falsiﬁcation rate

more systematic study of the eﬀects of the scale

FR and the average execution time of our proposed

problem; indeed, the scale problem could manifest

approach ForeSee and of the baseline Breach. The

itself in diﬀerent ways, depending on the diﬀerencetable further reports the diﬀerence of the two met-of the order of magnitudes of the diﬀerent signals

rics between the two approaches. We highlight in(e.g., speed [km/h] vs. rpm, or speed [km/h] vs.

gray the best results in which ForeSee has an FRrph). To assess this, we take six speciﬁcations fromof 15 units higher than Breach. We observe that

Table 1 and we artiﬁcially modify their outputs:

for 25 benchmarks out of 30, ForeSee has a betternamely, we multiply by 10k (with diﬀerent k values

FR, and in 15 of these the improvement is signif-

depending on the speciﬁcation) the speed of AT1,

icant (selected in gray). Note that there are no-

AT3, AT4, and AT9; the rpm of AT15; and thetable cases, such as AT3, AT13, AT16, and AT17,

EngineSpeed of AFC3. For each artiﬁcial rescaling,in which Breach only ﬁnds at most two falsifying
inputs, while ForeSee ﬁnds always at least 29 fal-

both the Simulink model and the speciﬁcation havebeen changed.†4 We run ForeSee and Breach on

sifying inputs. In four cases, Breach has a better

these rescaled benchmarks. Table 3 reports the ex-

FR: while for AT8, AFC6, and FFR2 the diﬀerence

perimental results for each k. The table also reports

is minimal, it is quite large for AT14. We further

the minimum, maximum, and mean results for FR

inspected such speciﬁcation and its corresponding

and execution time. We observe that the perfor-

model (see Table 1); we noticed that all the subformulas in AT14 must be falsiﬁed to falsify thewhole speciﬁcation†3 , and they are all diﬃcult to†3 Note that all binary connectives of AT14 are dis-junctions; indeed, A → B is the syntactic sugarfor ¬A ∨ B.
†4 Note that k = 0 corresponds to the experimental result in Table 2, and we report it again forreference.

表 2: Falsiﬁcation performance comparison between Breach and ForeSee on benchmarks. Timeout: 900

secs. FR in (/30), time in secs.
BreachFR

time

BreachForeSee
FR

time

∆FR

∆time

ForeSee

FR

time

FR

time

∆FR

∆time
+2.2

AT1

12

67.0

29

90.3

+17

+23.3

AT12

5

379.2

28

381.4

+23

AT2

18

208.5

30

155.5

+12

-53.0

AT13

2

75.2

29

98.3

+27

+23.1

AT3

0

-

29

87.3

+29

-

AT14

24

184.9

1

601.5

-23

+416.6

AT4

8

414.0

30

376.6

+12

-37.4

AT15

1

66.1

9

331.8

+8

+265.7

AT5

13

44.7

30

159.0

+17

+114.3

AT16

1

13.0

30

6.7

+29

-6.3

AT6

14

630.5

20

545.9

+6

-84.6

AT17

0

-

30

208.8

+30

-

AT7

20

24.9

30

5.8

+10

-19.1

AT18

18

160.0

24

234.3

+6

+74.3

AT8

17

418.5

13

547.0

-4

+128.5

AT19

15

81.8

30

154.3

+15

+72.5

AT9

9

298.6

29

208.0

+20

-90.6

AT20

1

97.7

5

286.2

+4

+188.5

AT10

14

99.4

30

89.7

+16

-9.7

AT21

10

239.0

29

425.5

+19

+186.5

AT11

17

58.1

30

39.6

+13

-18.5

AT22

13

72.0

30

113.3

+17

+41.3

∆FR

∆time

BreachForeSee

Breach

FR

time

FR

time

AFC1

10

532.2

12

458.0

+2

-74.2

AFC2

12

546.9

30

218.3

+18

-328.6

AFC3

8

727.6

28

232.5

+20

-495.1

AFC6

Breach

FFR1

∆FR

∆time

FR

time

FR

AFC4

7

634.5

22

500.3

+15

-134.2

AFC5

8

576.9

9

322.0

+1

-254.9

10

518.2

6

344.2

-4

-174.0

BreachForeSee

FR

time

FR

time

∆FR

∆time

7

132.1

7

399.3

+0

+267.2

ForeSee

FFR2

time

ForeSee

FR

time

FR

time

∆FR

∆time

30

38.0

27

348.0

-3

+310.0mance of Breach, in terms of FR, is very sensitive

These results also allow us to show that theto the scale problem. Indeed, for all the speciﬁca-

naive approach based on normalization for solving

tions, FR decreases with increasing or decreasing

the scale problem does not work, as also reported

k; notable examples are AT3 and AT4 in whichin [42]. Indeed, one may think that a solution for

Breach can (almost) always falsify with the mini-tackling the scale problem could be to rescale themum k, but never falsiﬁes with the maximum two

signals in a way to make them have the same or-k. This is the demonstration of the eﬀects of the

der of magnitude. This is not a good approach.

scale problem on falsiﬁcation approaches that only

Let us consider the results in Table 3c for AT4

rely on quantitative robust semantics where the ro-(2[0,30] (speed < 135 ∧ rpm < 4780)). In this case,bustness values of diﬀerent signals are compared.

speed is multiplied by 10k . We may think that the

By looking at the results of ForeSee, instead, webest falsiﬁcation result should occur when speed isobserve that it is much more robust and its FR per-multiplied by 102 , because this would make the twoformance is independent of the applied rescaling.

signals both in the order of thousands. However,This clearly shows that our falsiﬁcation approach

this rescaling is the one giving the worst result. The

guided by QB-Robustness is successful in avoiding

best result is actually given by the rescaling mak-the scale problem.

ing speed even smaller (i.e., k = −2 and k = −1).

表 3: Falsiﬁcation performance under diﬀerent scales. Each rescaled signal is rescaled by 10k .
(a) AT1: speed × 10k

Breach(b) AT3: speed × 10k

ForeSee

Breach(c) AT4: speed × 10k

ForeSee

BreachForeSee

k

FR

time

FR

time

k

FR

time

FR

time

k

FR

time

FR

time

-2

30

126.5

26

77.5

-3

30

124.9

30

81.2

-2

29

247.2

29

329.4

-1

25

64.4

29

107.9

-2

30

135.9

28

82.6

-1

29

243.5

28

332.2

0

12

67.0

29

90.3

-1

1

136.7

28

101.6

0

8

414.0

30

376.6

1

9

92.4

28

81.8

0

0

-

29

87.3

1

0

-

29

377.6

2

9

131.9

30

94.2

1

0

-

30

103.4

2

0

-

29

333.2

min

9

64.4

26

77.5

min

0

124.9

28

81.2

min

0

243.5

28

329.4

max

30

131.9

30

107.9

max

30

136.7

30

103.4

max

29

414.0

30

377.6

17

96.4

28

90.3

mean

12

132.5

29

91.2

mean

13

301.6

29

349.8

mean

(d) AT9: speed × 10k

Breach(e) AT15: rpm × 10k

ForeSee

Breach(f) AFC3: EngineSpeed ×10k

ForeSee

BreachForeSee

k

FR

time

FR

time

k

FR

time

FR

time

k

FR

time

FR

time

-1

11

202.6

28

259.8

-5

20

138.3

6

222.3

0

8

727.6

28

232.5

0

9

298.6

29

208.0

-4

13

158.1

10

258.8

-1

18

574.2

29

284.1

1

10

197.4

29

221.2

-3

4

144.6

5

313.6

-2

29

401.2

29

211.5

2

28

175.4

29

248.9

-2

0

-

9

268.6

-3

30

215.0

29

230.1

3

30

162.6

29

209.6

0

1

66.1

9

331.8

-4

29

198.2

30

236.2

min

9

162.6

28

208.0

min

0

66.1

5

222.3

min

8

198.2

28

211.5

max

30

298.6

29

259.8

max

20

158.1

10

331.8

max

30

727.7

30

284.1

mean

18

207.3

29

229.5

mean

10

126.8

8

279.0

mean

23

423.2

29

238.9

This means that the correct way for handling theues used for these hyperparameters. In this RQ,

scale problem cannot be identiﬁed in advance, but

we try to assess this. We selected three bench-

we need an approach as ours that learns duringmarks speciﬁcations (AT17, AT19, and AT21)

falsiﬁcation the best strategy.

and varied one hyperparameter while keeping theRQ3 How do the hyperparameters of MCTS in-other ﬁxed. Namely, we experimented with c ∈ﬂuence the performance of the proposed approach?

{0, 0.02, 0.2, 0.5, 1} and budget BP = 10 (see Ta-

Our proposed approach is an instantiation of theMonte 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 Alg. 2), and the playout budget BP (Line 21
in Alg. 2), both used for balancing between exploration and exploitation.

Therefore, the per-formance of MCTS could be aﬀected by the val-

ble 4a), and with BP ∈ {2, 5, 10, 15, 20} and budget c = 0.2 (see Table 4b). Looking at the resultsof Table 4a for AT17 and AT21, there seems tobe some inﬂuence by the scalar c. In AT17, theworst result in terms of FR is obtained when c is 0,
meaning that MCTS only focuses on exploitation.
AT17 is a speciﬁcation that suﬀers from the scale
problem, as shown by the very bad performance of表 4:

Falsiﬁcation performance under diﬀerent

MCTS hyperparameters.

6 Related Work
Quality assurance of CPS has been actively stud-(a) Performance with varied c

AT17

AT19

ied, due to its great signiﬁcance.
AT21

Diﬀerent ap-

proaches, including but not limited to model checking, theorem proving, rigorous numerics, and non-

c

FR

time

FR

time

FR

time

0

23

177.8

30

224.6

30

463.4

0.02

26

196.7

30

278.5

28

501.3

0.2

30

208.8

30

154.3

29

425.5

scalability issue and existence of black-box compo-

0.5

30

297.0

29

227.3

30

509.0

nents, those approaches are not widely applied in

1.0

30

311.7

30

240.2

24

497.0

the real-world systems.

(b) Performance with varied BP

AT17

AT19

standard analysis [9, 16, 20, 22, 23, 31, 33], have been
proposed to solve the problem. However, due to the

The optimization-based falsiﬁcation approach inAT21

herits the search-based testing methodology, andis much more scalable than pure veriﬁcation-based

BP

FR

time

FR

time

FR

time

2

26

385.2

30

162.0

29

500.0

5

30

347.7

29

207.3

29

472.5

is the exploration-exploitation trade-oﬀ. This is-

10

30

208.8

30

154.3

29

425.5

sue has been discussed for the veriﬁcation of quan-

15

30

337.7

29

336.7

28

514.0

titative properties (e.g., [34]). In the falsiﬁcation

20

30

358.1

30

313.5

30

511.0

community, there have also been a lot of works fo-

approaches. The key issue of search-based testing

cusing on that, and these works tackle the probMetaheuristics

Breach in Table 2; for such a speciﬁcation, we needlem from diﬀerent perspectives.

to perform some exploration to ﬁnd the best Σ: thisrefers to high-level heuristic strategies that utilize

explain the low performance of MCTS with c = 0.

heuristics to improve the search eﬃciency. Several

On the other hand, the worst FR performance of

metaheuristic strategies have been applied in fal-

AT21 is given by the highest value c = 1 that re-

siﬁcation, such as Simulated Annealing [1], tabu

quires MCTS to spend a lot of time in exploration.

search [10], and so on. Coverage-guided falsiﬁca-

Since AT21 is not an extremely diﬃcult speciﬁca-

tion [2, 10, 15, 29] aims to guide the search using

tion (indeed Breach has FR of 10 in Table 2), suchsome coverage metrics, so that the search space isvery conservative approach does not pay oﬀ, while

suﬃciently explored. Recently, machine learning

more greedy approaches (i.e., with lower c) havetechniques have also been applied to falsiﬁcation tobetter performance.

enhance the search ability. For instance, Bayesian

Looking at the results of Table 4b related to BP ,optimization [3, 11, 36] utilizes an acquisition func-

it seems that there is no too much inﬂuence. Thetion to balance exploration and exploitation; Rein-

only diﬀerence is given in AT17 with BP = 2 whereforcement learning [27,37] naturally emphasizes on

the FR is slightly lower than the other cases. This

exploration.

means that, provided that a suﬃciently large value

The scale problem is a recognized issue [12,21,40]

for BP is given, ForeSee is not too sensitive to it.

that is known to severely aﬀect the performance offalsiﬁ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 con-

nectives: 2I (φ1 ∧ φ2 ) and 2I (φ1 ∨ φ2 ). The ap-

tative robustness must be computed. We then pro-proach is not applicable to formulas having morepose a Monte Carlo Tree Search (MCTS)-based fal-

nested sub-formulas, or even connectives having

siﬁcation approach that synthesizes a sub-formulamore operands; therefore many of the benchmarks

sequence for QB-Robustness, and uses this for guid-

we used in §5. 2 fall out of the scope of [40]. The

ing numerical optimization. Experimental results

techniques introduced in [12, 21] rely on explicit

show that the proposed approach achieves better

declaration of input vacuity and output robustness.

falsiﬁcation results than a state-of-the-art falsiﬁca-

Compared to their approaches, our method doestion tool that uses standard quantitative robust se-

not need that, but we learn the signiﬁcance of eachmantics.

signal through tree exploration and reward compu-

In the analysis of RQ1, we observed that, when
the speciﬁcations have a particular structure, ourtation.
MCTS, as an eﬀective search framework, hasapproach has no advantage and, actually, it could

been applied in testing hybrid systems. In [30], thedecrease the performance by trying to ﬁnd a best

authors applied an adaption of MCTS in testing,sub-formula sequence that does not exist for thenamely, adaptive press testing, to detect the po-

current initial sampling. As future work, we plan

tential dangerous cases of airborne collision. A re-to devise some heuristics that could handle thesecent study of MCTS on hybrid system falsiﬁcation

cases: for example, we could perform a better ini-

is [39]. There, the authors discretized the search

tial sampling (see §2. 1) that could provide a better

space to construct the search tree, and then ap-

initial guidance.

plied MCTS to explore diﬀerent sub-spaces. Com-謝 辞 This work is supported in part bypared to their approach, our work aims to tackle

JSPS KAKENHI Grant No.20H04168, 19K24348,

the scale problem and so we exploit the structure of

19H04086, JST-Mirai Program Grant No.JPMJMI20B8,

speciﬁcation formulas to construct the tree search

Japan. Lei Ma is also supported by Canada CIFAR

framework.

AI Program and Natural Sciences and Engineering

7 Conclusion and Future Work

Research Council of Canada. Paolo Arcaini and

Optimization-based falsiﬁcation is a widely used

Ichiro Hasuo are supported by ERATO HASUO

approach for quality assurance of CPS, that tries

Metamathematics for Systems Design Project (No.

to ﬁnd an input violating a Signal Temporal Logic

JPMJER1603), JST.

(STL) speciﬁcation. It does this by exploiting thequantitative robust semantics of the speciﬁcation,

参 考 文 献trying to minimize its robustness.

[ 1 ] Abbas, H. and Fainekos, G.: Convergence proofs
for simulated annealing falsiﬁcation of safety properties, 50th Annual Allerton Conference on Communication, Control, and Computing, IEEE, 2012,
pp. 1594–1601.
[ 2 ] Adimoolam, A., Dang, T., Donzé, A., Kapinski,J., and Jin, X.: Classiﬁcation and Coverage-Based
Falsiﬁcation for Embedded Control Systems, Computer Aided Veriﬁcation, Cham, Springer, 2017,
pp. 483–503.
[ 3 ] Akazaki, T., Kumazawa, Y., and Hasuo, I.:
Causality-Aided Falsiﬁcation, Proceedings First
Workshop on Formal Veriﬁcation of Autonomous
Vehicles, FVAV@iFM 2017, Turin, Italy, 19th

The perfor-

mance 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-formulasequence telling for which sub-formulas the quanti-

September 2017., EPTCS, Vol. 257, 2017, pp. 3–
18.
[ 4 ] Annpureddy, Y., Liu, C., Fainekos, G., andSankaranarayanan, S.: S-TaLiRo: A Tool for Temporal Logic Falsiﬁcation for Hybrid Systems, Tools
and Algorithms for the Construction and Analysis
of Systems, Berlin, Heidelberg, Springer Berlin Heidelberg, 2011, pp. 254–257.
[ 5 ] Arcuri, A. and Briand, L.: A Practical Guide
for Using Statistical Tests to Assess Randomized
Algorithms in Software Engineering, Proceedings ofthe 33rd International Conference on Software Engineering, ICSE ’11, New York, NY, USA, ACM,
2011, pp. 1–10.
[ 6 ] Auer, P.:
Using conﬁdence bounds for
exploitation-exploration trade-oﬀs, Journal of Machine Learning Research, Vol. 3, No. Nov(2002),
pp. 397–422.
[ 7 ] Auger, A. and Hansen, N.: A restart CMA
evolution strategy with increasing population size,
Proceedings of the IEEE Congress on Evolutionary
Computation, CEC 2005, IEEE, 2005, pp. 1769–
1776.
[ 8 ] Browne, C., Powley, E. J., Whitehouse, D., Lucas, S. M., Cowling, P. I., Rohlfshagen, P., Tavener,
S., Liebana, D. P., Samothrakis, S., and Colton,
S.: A Survey of Monte Carlo Tree Search Methods,
IEEE Trans. Comput. Intellig. and AI in Games,
Vol. 4, No. 1(2012), pp. 1–43.
[ 9 ] Chen, X., Ábrahám, E., and Sankaranarayanan,S.: Flow*: An Analyzer for Non-linear Hybrid Systems, Computer Aided Veriﬁcation, Berlin, Heidelberg, Springer Berlin Heidelberg, 2013, pp. 258–
263.
[10] Deshmukh, J., Jin, X., Kapinski, J., and Maler,O.: Stochastic Local Search for Falsiﬁcation of Hybrid Systems, Automated Technology for Veriﬁcation and Analysis, Cham, Springer, 2015, pp. 500–517.
[11] Deshmukh, J. V., Horvat, M., Jin, X., Majumdar, R., and Prabhu, V. S.: Testing CyberPhysical Systems through Bayesian Optimization,
ACM Trans. Embedded Comput. Syst., Vol. 16,
No. 5(2017), pp. 170:1–170:18.
[12] Dokhanchi, A., Yaghoubi, S., Hoxha, B., andFainekos, G. E.: Vacuity aware falsiﬁcation for MTL
request-response speciﬁcations, 13th IEEE Conference on Automation Science and Engineering,
CASE 2017, Xi’an, China, August 20-23, 2017,
IEEE, 2017, pp. 1332–1337.
[13] Donzé, A.: Breach, A Toolbox for Veriﬁcation
and Parameter Synthesis of Hybrid Systems, Computer Aided Veriﬁcation, 22nd Int. Conf., CAV
2010, LNCS, Vol. 6174, Springer, 2010, pp. 167–
170.
[14] Donzé, A. and Maler, O.: Robust Satisfaction of
Temporal Logic over Real-Valued Signals, Formal
Modeling and Analysis of Timed Systems - 8th Int.

Conf., LNCS, Vol. 6246, Springer, 2010, pp. 92–
106.
[15] Dreossi, T., Dang, T., Donzé, A., Kapinski, J.,
Jin, X., and Deshmukh, J. V.: Eﬃcient Guiding
Strategies for Testing of Temporal Properties ofHybrid Systems, NASA Formal Methods, Springer,
2015, pp. 127–142.
[16] Dreossi, T., Dang, T., and Piazza, C.: Parallelotope Bundles for Polynomial Reachability, Proc. of
the 19th International Conference on Hybrid Systems: Computation and Control, HSCC ’16, New
York, NY, USA, ACM, 2016, pp. 297–306.
[17] Dreossi, T., Donzé, A., and Seshia, S. A.: Compositional Falsiﬁcation of Cyber-Physical Systems
with Machine Learning Components, NASA Formal
Methods, Cham, Springer, 2017, pp. 357–372.
[18] Ernst, G., Arcaini, P., Bennani, I., Donzé, A.,
Fainekos, G., Frehse, G., Mathesen, L., Menghi,
C., Pedrielli, G., Pouzet, M., Yaghoubi, S., Yamagata, Y., and Zhang, Z.: ARCH-COMP 2020 Category Report: Falsiﬁcation, ARCH20. 7th International Workshop on Applied Veriﬁcation of Continuous and Hybrid Systems (ARCH20), EPiC Series
in Computing, Vol. 74, EasyChair, 2020, pp. 140–
152.
[19] Fainekos, G. E. and Pappas, G. J.: Robustnessof Temporal Logic Speciﬁcations for ContinuousTime Signals, Theor. Comput. Sci., Vol. 410,
No. 42(2009), pp. 4262–4291.
[20] Fan, C., Qi, B., Mitra, S., Viswanathan, M., andDuggirala, P. S.: Automatic Reachability Analysis
for Nonlinear Hybrid Models with C2E2, Computer
Aided Veriﬁcation, Cham, Springer, 2016, pp. 531–
538.
[21] Ferrère, T., Nickovic, D., Donzé, A., Ito, H., andKapinski, J.: Interface-aware signal temporal logic,
Proceedings of the 22nd ACM International Conference on Hybrid Systems: Computation and Control,
HSCC 2019, Montreal, QC, Canada, April 16-18,
2019., 2019, pp. 57–66.
[22] Frehse, G., Le Guernic, C., Donzé, A., Cotton,
S., Ray, R., Lebeltel, O., Ripado, R., Girard, A.,
Dang, T., and Maler, O.: SpaceEx: Scalable Veriﬁcation of Hybrid Systems, Computer Aided Veriﬁcation, Berlin, Heidelberg, Springer, 2011, pp. 379–395.
[23] Hasuo, I. and Suenaga, K.: Exercises in
Nonstandard Static Analysis of Hybrid Systems,
Computer Aided Veriﬁcation, Berlin, Heidelberg,
Springer, 2012, pp. 462–478.
[24] Hoxha, B., Abbas, H., and Fainekos, G. E.:
Benchmarks for Temporal Logic Requirements
for Automotive Systems, 1st and 2nd International Workshop on Applied veRiﬁcation for Continuous and Hybrid Systems, ARCH@CPSWeek2014, Berlin, Germany, April 14, 2014 /ARCH@CPSWeek 2015, Seattle, USA, April 13,
2015., EPiC Series in Computing, Vol. 34, Easy-Chair, 2014, pp. 25–30.
[25] Jin, X., Deshmukh, J. V., Kapinski, J., Ueda,
K., and Butts, K.: Powertrain Control Veriﬁcation
Benchmark, Proc. of the 17th Int. Conf. on Hybrid Systems: Computation and Control, HSCC ’14,
NY, USA, ACM, 2014, pp. 253–262.
[26] Kapinski, J., Deshmukh, J. V., Jin, X., Ito,
H., and 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
Systems, Vol. 36, No. 6(2016), pp. 45–64.
[27] Kato, K. and Ishikawa, F.: Learning-Based Falsiﬁcation for Model Families of Cyber-Physical Systems, 2019 IEEE 24th Paciﬁc Rim International
Symposium on Dependable Computing (PRDC),
Dec 2019, pp. 236–245.
[28] Kocsis, L. and Szepesvári, C.: Bandit Based
Monte-Carlo Planning, Machine Learning: ECML
2006, Berlin, Heidelberg, Springer, 2006, pp. 282–
293.
[29] Kuřátko, J. and Ratschan, S.: Combined Global
and Local Search for the Falsiﬁcation of Hybrid Systems, Formal Modeling and Analysis of Timed Systems, Cham, Springer, 2014, pp. 146–160.
[30] Lee, R., Kochenderfer, M. J., Mengshoel, O. J.,
Brat, G. P., and Owen, M. P.: Adaptive stress testing of airborne collision avoidance systems, Digital
Avionics Systems Conference, 2015 IEEE/AIAA
34th, IEEE, 2015, pp. 6C2–1.
[31] Liebrenz, T., Herber, P., and Glesner, S.: Deductive Veriﬁcation of Hybrid Control Systems
Modeled in Simulink with KeYmaera X, Formal
Methods and Software Engineering - 20th International Conference on Formal Engineering Methods, ICFEM 2018, Gold Coast, QLD, Australia,
November 12-16, 2018, Proceedings, Lecture Notes
in Computer Science, Vol. 11232, Springer, 2018,
pp. 89–105.
[32] Luersen, M. A. and Le Riche, R.: Globalized
Nelder–Mead method for engineering optimization,
Computers & Structures, Vol. 82, No. 23(2004),
pp. 2251–2260.
[33] Platzer, A.: Logical Foundations of CyberPhysical Systems, Springer, 2018.
[34] Seshia, S. A. and Rakhlin, A.: Quantitative
Analysis of Systems Using Game-Theoretic Learning, ACM Trans. Embed. Comput. Syst., Vol. 11,
No. S2(2012), pp. 55:1–55:27.
[35] Silver, D., Huang, A., Maddison, C. J., Guez,

A., Sifre, L., van den Driessche, G., Schrittwieser,J., Antonoglou, I., Panneershelvam, V., Lanctot,
M., Dieleman, S., Grewe, D., Nham, J., Kalchbrenner, N., Sutskever, I., Lillicrap, T., Leach,M., Kavukcuoglu, K., Graepel, T., and Hassabis,D.: Mastering the game of Go with deep neuralnetworks and tree search, Nature, Vol. 529(2015),
pp. 484–489.
[36] Silvetti, S., Policriti, A., and Bortolussi, L.: An
Active Learning Approach to the Falsiﬁcation ofBlack Box Cyber-Physical Systems, Integrated Formal Methods, Cham, Springer, 2017, pp. 3–17.
[37] Yamagata, Y., Liu, S., Akazaki, T., Duan, Y.,
and Hao, J.: Falsiﬁcation of cyber-physical systems
using deep reinforcement learning, IEEE Transactions on Software Engineering, (2020).
[38] Zhang, Z., Arcaini, P., and Hasuo, I.: Hybrid
System Falsiﬁcation under (In)equality Constraints
via Search Space Transformation, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 39, No. 11(2020), pp. 3674–
3685.
[39] Zhang, Z., Ernst, G., Sedwards, S., Arcaini, P.,
and Hasuo, I.: Two-Layered Falsiﬁcation of Hybrid
Systems Guided by Monte Carlo Tree Search, IEEE
Transactions on Computer-Aided Design of Integrated Circuits and Systems, Vol. 37, No. 11(2018),
pp. 2894–2905.
[40] Zhang, Z., Hasuo, I., and Arcaini, P.: Multiarmed Bandits for Boolean Connectives in Hybrid System Falsiﬁcation, Computer Aided Veriﬁcation, Cham, Springer International Publishing,
2019, pp. 401–420.
[41] Zhang, Z., Lyu, D., Arcaini, P., Ma, L., Hasuo,I., and Zhao, J.: Eﬀective Hybrid System Falsiﬁcation Using Monte Carlo Tree Search Guided by QBRobustness, Computer Aided Veriﬁcation, Silva, A.
and Leino, K. R. M.(eds.), Cham, Springer International Publishing, 2021, pp. 595–618.
[42] Zhang, Z., Lyu, D., Arcaini, P., Ma, L., Hasuo, I., and Zhao, J.: On the Eﬀectiveness of
Signal Rescaling in Hybrid System Falsiﬁcation,
NASA Formal Methods, Cham, Springer International Publishing, 2021, pp. 392–399.
[43] Zutshi, A., Deshmukh, J. V., Sankaranarayanan,S., and Kapinski, J.: Multiple shooting, CEGARbased falsiﬁcation for hybrid systems, 2014 International Conference on Embedded Software, EMSOFT 2014, New Delhi, India, October 12-17,
2014, ACM, 2014, pp. 5:1–5:10.