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

Gaussian Process-Based Conﬁdence Estimationfor Hybrid System Falsiﬁcation
張 振亜

パオロ アルカイニ

Cyber-Physical Systems (CPSs) are widely adopted in safety-critical domains, raising great demands ontheir quality assurance. However, the application of formal veriﬁcation is limited due to the continuous
dynamics of CPSs. Instead, simulation-based falsiﬁcation, which aims at ﬁnding a counterexample to refutethe system speciﬁcation, is a more feasible and hence actively pursued approach. Falsiﬁcation adopts an
optimization approach, treating robustness, given by the quantitative semantics of the speciﬁcation language(usually Signal Temporal Logic (STL)), as the objective function. However, similarly to traditional testing,in the absence of found counterexamples, falsiﬁcation does not give any guarantee on the system safety. To
ﬁll this gap, in this paper, we propose a conﬁdence measure that estimates the probability that a formal
speciﬁcation is indeed not falsiﬁable, by relying on the information encapsulated in the simulation data collected during falsiﬁcation. Methodologically, we approximate the robustness domain by feeding simulation
data into a Gaussian Process (GP) Regression process; we then do a minimization sampling on the trained
GP, and then estimate the probability that all the robustness values inferred from these sampled points
are positive; we take this probability as the conﬁdence measure. We experimentally study the propertiesof monotonicity and soundness of the proposed conﬁdence measure. We also apply the measure to several
state-of-the-art falsiﬁcation algorithms to assess the maximum conﬁdence they provide when they do notﬁnd a falsifying input, and the stability of such conﬁdence across diﬀerent repetitions.

Reprinted by permission from Springer Nature Cus-

1 Introduction

tomer Service Centre GmbH.

Cyber-Physical Systems (CPS) are characterized
Journal publisher: Springer, Cham.

by the combination of physical systems having conJournal name:Formal Methods.

November 20-26,

tinuous dynamics, and discrete digital controllers;
2021, Proceedings.

for this, they are also called hybrid systems. CPSs
Reference citation:

Gaussian Process-Based Conﬁ-

are often employed in safety-critical domains, makdence Estimation for Hybrid System Falsiﬁcation.

ing their quality assurance of paramount imporZhang, Z., Arcaini, P.

tance. However, the continuous dynamics of hyCopyright: ©2021 Springer Nature Switzerland AG

brid systems makes their automated formal veriﬁadvance online publication, 10 November 2021 (doi:cation extremely diﬃcult, if not impossible. Therehttps://doi.org/10.1007/978-3-030-90870-6 18).

fore, academia and industry have been pursuing themore feasible approach of falsiﬁcation [13, 22, 29,This work was originally published at 24th International Symposium on Formal Methods [35].
Zhenya Zhang, 九州大学システム情報科学研究院, Facultyof Information Science and Electrical Engineering,
Kyushu University.
Paolo Arcaini, 国立情報学研究所, National Institute ofInformatics.

30, 33, 37, 38] that, instead of trying to prove a formal speciﬁcation, attempts to ﬁnd a counterexample showing its violation. Speciﬁcally, given a model
M taking input signal u and producing output signal M(u), and a formal speciﬁcation φ (a temporalformula), the falsiﬁcation problem consists in ﬁnd-sifying input exists in the unexplored search space.

ing a falsifying input, i.e., an input signal u such

The construction of the conﬁdence measure is asthat M(u) violates φ.

follows. We ﬁrst train, using Gaussian Process Re-

The common approach to solve the falsiﬁcation

gression [31], a Gaussian Process (GP) from the

problem is to turn it into an optimization problem

falsiﬁcation data, acting as a surrogate model of(also called optimization-based falsiﬁcation), by ex-

the real robustness function, i.e., it provides an es-

ploiting the quantitative robust semantics of tem-timation of the robustness. Then, we sample inporal formulas [14, 19]. Robust semantics extends

the GP the points that have the minimum values,

the classical Boolean satisfaction relation w |= φas these are the points that have the higher prob-

by assigning a value Jw, φK ∈ R ∪ {∞, −∞} (i.e.,ability to identify negative robustness. We thenrobustness) that tells not only whether φ is satisﬁed

compute the cumulative probability that these sur-or violated (by the sign), but also how robustly therogate sampled data are all positive, i.e., that theformula is satisﬁed or violated. Optimization-based

approximated robustness is always positive, and so

falsiﬁcation algorithms iteratively generate inputs

the speciﬁcation is not falsiﬁed. We take this prob-with the aim of ﬁnding an input with negative ro-ability as the conﬁdence value estimating how likely

bustness. Several optimization-based falsiﬁcation

it is that the speciﬁcation holds.

algorithms have been developed [1, 3, 10, 13, 18, 29,
33, 36–39].
Given a speciﬁcation φ, a falsiﬁcation algorithm

We performed a series of experiments to assess towhat extent the proposed conﬁdence measure guarantees some desired properties:

either returns an input signal falsifying φ, or it re-• monotonicity: the conﬁdence measure should

ports that the search was unsuccessful if no suchnot decrease as new falsiﬁcation data (i.e., in-input was found. As usual in testing (falsiﬁcation isputs with corresponding robustness values) area particular type of search-based testing approach),being added. A monotonically increasing mea-in the latter case, we do not know whether the spec-

sure does not prematurely assess high conﬁ-

iﬁcation φ is really not falsiﬁable, or the algorithm

dence, and so it can be reliably used to decide

did not explore the search space enough. In suchwhether enough falsiﬁcation search has beena case, a practitioner would like to have some esti-

performed; it can also be used as a stopping cri-mate of the real absence of a falsifying input (andterion during the falsiﬁcation search itself. In

so of the satisfaction of φ).

classical coverage criteria for software testing,

To this aim, in this paper, we propose a conﬁ-

increasing monotonicity is implicitly guaran-

dence measure for hybrid system falsiﬁcation. The

teed, because the test requirements are known

deﬁnition of the measure starts from the observa-

in advance, and so any new test input cantion that, as output, a falsiﬁcation algorithm also

only increase the coverage (when an uncovered

provides the set of input signals that have been

test requirement is covered) or at most leavesampled during the search, together with their cor-

it unchanged. For our conﬁdence measure, in-

responding robustness values. Starting from thesedata†1 , we try to estimate the likelihood that no fal-creasing monotonicity cannot be guaranteed,†1 Note that we assume that the conﬁdence measure is computed starting from non-falsifying inputs only. The measure does not make sense if at

least one falsifying input is used for its computation; in that case, there is no need of the conﬁdence measure, as we know that the speciﬁcation
is falsiﬁable.

as it is always possible to ﬁnd a new input signal that drastically changes the derived Gaus-

2 Backgroundsian Process and so the computed conﬁdence.

We here review the basic concepts and ap-

However, we will experimentally show that theproaches of hybrid system falsiﬁcation.

measure can eﬃciently account for the unex-

System Model. Let T ∈ R≥0 be a positive real.

plored search space and that monotonicity is
guaranteed to some extent.
• soundness: intuitively, the conﬁdence should
also depend on “how robustly” a speciﬁcation holds. Given two speciﬁcations that areboth non-falsiﬁable, the one that is more ro-

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 abust should lead to higher conﬁdence than thefunction M that takes an input signal u : [0, T ] →less robust one. Take the example of a car sys-

RM and returns a signal M(u) : [0, T ] → RN . Heretem, and two speciﬁcations requiring that thethe common time horizon T ∈ R≥0 is arbitrary.

“speed is always less than 120” and “speed isalways less than 150”; intuitively, in the absence of a falsifying input, the conﬁdence of the

The process of obtaining a system output signal
M(u), given an input signal u, is called simulation.

latter speciﬁcation should not be lower thanIn this work, we adopt Signalthat of the former one (given that a falsiﬁca-

Speciﬁcations.

tion approach has been run for both with the

Temporal Logic (STL) as our speciﬁcation language

same budget).

to formalize properties that should be satisﬁed by

In the experiments, we will also use the conﬁ-

the system. We introduce the syntax and semantics

dence measure to assess the performance of exist-

in the following.

ing falsiﬁcation algorithms, which implement dif-Deﬁnition 1 (STL syntax) We ﬁx a set Var offerent search strategies.

Namely, we will checkvariables. In Signal Temporal Logic (STL), atomic

the conﬁdence provided by three falsiﬁcation algo-

propositions and formulas are deﬁned as follows,

rithms (Random search, CMAES, and MCTS) executed

respectively: α ::≡ f (x1 , . . . , xN ) > 0, and φ ::≡with the same budget; moreover, we will also checkα | ⊥ | ¬φ | φ ∧ φ | φ UI φ. Here f is an N -ary

their stability, i.e., how much the conﬁdence mea-function f : RN → R, x1 , . . . , xN ∈ Var, and I is asure changes in repeated runs.

closed non-singular interval in R≥0 , i.e. I = [a, b]
or [a, ∞) where a, b ∈ R and a < b. Other com-

§2 provides the neces-mon connectives such as →, ⊤, □I (always) andsary background. §3 introduces the problem and♢I (eventually), are introduced as abbreviations:overviews the approach to compute the proposed♢I φ ≡ ⊤ UI φ and □I φ ≡ ¬♢I ¬φ.

conﬁdence measure, whose phases are described in

Deﬁnition 2 (Robust semantics) Let w : [0, T ] →§4. §5 presents the experiments done to assess the

RN be an N -dimensional signal, and t ∈ [0, T ).

measure. Finally, §6 reviews related work, and §7

The t-shift wt of w is the signal wt : [0, T − t] →concludes the paper.

RN deﬁned by wt (t′ ) := w(t + t′ ). Let w : [0, T ] →Paper Structure.

R|Var| be a signal, and φ be an STL formula. We
deﬁne the robustness Jw, φK ∈ R∪{∞, −∞} as fol-

lows, by induction on the construction of formulas.
d⊔anddenote inﬁmums and supremums of realmore eﬃcient but greedy algorithm is by exploit-

numbers, respectively. Their binary version ⊓ andtion into an optimization problem that minimizes

ing the STL robust semantics and turning falsiﬁca-⊔ denote minimum and maximum.
the() robustness JM(u), φK; the process stops whenJw, f (x1 , · · · , xN ) > 0K := f w(0)(x1 ), · · · , w(0)(xN )a negative robustness result JM(u), φK is observed
Jw, ⊥K := −∞(i.e., a falsifying input u has been found), or theJw, ¬φK := −Jw, φK
search budget (in terms of number of simulations)Jw, φ1 ∧ φ2 K := Jw, φ1 K ⊓ Jw, φ2 K
expires.
⊔ ( t
l
)
′
Jw, φ1 UI φ2 K :=Jw , φ2 K ⊓Jwt , φ1 K
In order to solve the optimization problem,t′ ∈[0,t)t∈I∩[0,T ]The original STL semantics is Boolean, given bystochastic optimization algorithms, such as hilla binary relation |= between signals and formulas.

climbing, are employed, because they work eﬃ-

The robust semantics reﬁnes the Boolean one as

ciently with black box objective functions, likefollows: Jw, φK > 0 implies w |= φ, and Jw, φK < 0

JM(u), φK in our case.

implies w ̸|= φ, see [19, Prop. 16].

various metaheuristic strategies so that they can

These algorithms adopt

In the following, given a ﬁxed speciﬁcation φ, weeﬃciently explore the search space and achieve op-

denote as Ru the robustness of an input signal u to

timal solutions. For instance, CMAES [23] is an

the speciﬁcation φ, i.e., Ru = JM(u), φK.

evolutionary search-based method that focuses on

Falsiﬁcation Approaches.

Falsiﬁcation con-sists in synthesizing input signals to ﬁnd one that
violates the system speciﬁcation. The targets offalsiﬁcation, i.e., input signals u : [0, T ] → RM ,are time-variant continuous functions. In practice,synthesizing such continuous signals is infeasible.
Hence, practitioners employ parametrized representations to characterize the signals [13, 16, 26];
a commonly used representation is piecewise constant. A piecewise constant signal u : [0, T ] → RM
has a hyperparameter c, such that during each interval [ (i−1)T, iT] (i ∈ 1, . . . , c), u(t) is a constant.
ccIn this way, a ﬁnite number c · M of parameters isused to identify a signal u. We will identify with Ω
the (c · M )-dimensional hyperrectangle identifying
the input space (also search space) used for falsiﬁcation.
Various approaches have been proposed to solve
the falsiﬁcation problem. The naive one is by uniformly random sampling input signals u in the input space Ω, and check if the corresponding output signal M(u) violates the speciﬁcation φ. A

exploitation. A more recent work MCTS [37] employs Monte-Carlo Tree Search to achieve a balance
between exploration and exploitation of the search
space. We refer readers to [8] for a more comprehensive survey of diﬀerent optimization-based falsiﬁcation algorithms. Also mature tools, such as
Breach [13] and S-TaLiRo [3], have been developed.

3 Problem Deﬁnition and Overview of
the Proposed Approach
In this work, we tackle the problem of characterizing the likelihood that a formal speciﬁcation isindeed non-falsiﬁable, given that a falsiﬁcation algorithm has tried to falsify it using a given set of
input signals, all giving positive robustness.
Deﬁnition 3 (Conﬁdence Estimation Problem)
The conﬁdence estimation problem is formally deﬁned as follows:• Given: a ﬁnite set T = {⟨u∗1 , Ru∗1 ⟩, . . . , ⟨u∗N , Ru∗N ⟩}of pairs, where each u∗i ∈ Ω is a point in the
input space Ω, and Ru∗i ∈ R≥0 is the robustness(a positive real) of u∗i .
• Return: the likelihood that, for all points u′ ∈Process RegressionΩ, it holds Ru′ > 0.
This problem is in general undecidable: ﬁrst, theIn this section, we explain all the phases of therobustness computation R(u) = JM(u), φK relies

process shown in Fig. 1. In §4. 1, we ﬁrst explain

on a black box model M, in which the robustness

how we derive a Gaussian Process (GP) from thevalues of unexplored points are not predictable (i.e.,

falsiﬁcation data. Then, in §4. 2, we describe how

R is unknown); moreover, there are inﬁnitely many

we sample from the obtained GP, and derive a con-unexplored points in the search space Ω, regardlessﬁdence measure from the sampled data.

of the size of T , since Ω is a continuous domain.
Overview of the Proposed Approach forConﬁdence Estimation.

We provide an

overview of the proposed approach in Fig. 1. We

4. 1 Building a surrogate model of the robustness function via Gaussian Process Regression

assume that a falsiﬁcation algorithm has been run

A Gaussian Process (GP) is a generalization offor some time with the aim of falsifying a given

Gaussian distribution (a.k.a. normal distribution)

speciﬁcation for a given system, without successfrom single/multiple variables to continuous do-(i.e., no falsifying input has been found). The pro-mains [31]. While a Gaussian distribution char-posed approach takes as input the produced falsiﬁ-

acterizes the probability distribution of a ﬁnite set

cation data T , consisting of a set of system inputsof variables, a GP models the distribution of in-u∗ and their robustness values Ru∗ , as deﬁned inﬁnite variables in a continuous domain, i.e., sam-Def. 3. These data, after being normalized, are fedpling from a GP derives a function instance in theinto a Gaussian Process (GP) Regression process

domain.

to train a GP as a surrogate of robustness function

main Ω is deﬁned as a collection of random vari-

R. Using the obtained GP, we want to estimate

ables Xt indexed by t ∈ Ω, such that any ﬁnite

the probability that there exists no point having

set X = {Xt | t ∈ Ω} of those variables compose

negative robustness. First, we need to identify thea multivariate Gaussian distribution X ∼ N (µ, Σ),points with lower values in the GP (so approxi-

where µ and Σ are the mean vector and the covari-mating lower robustness values), as these are thoseance matrix of the distribution, respectively. The

that can actually reduce the probability; to do this,correlation between two variables Xti , Xtj ∈ X is

we perform a global sampling method to collect areﬂected by their covariance Σi,j —the larger |Σi,j |set of points that have low values, and then per-is, the more highly Xti and Xtj are correlated. In aform a local search starting from these points with

GP, the covariance between two variables Xti andthe aim of ﬁnding points with even lower values.

Xtj is dependent on the (Euclidean) distance ofFormally, a GP over a continuous do-

Starting from the found points, we apply an estab-their indices ti and tj —the closer ti and tj are, thelished method [6] to compute the probability thatlarger the covariance is. This is implemented by the

all these points still approximate positive robust-

covariance function (a.k.a. kernel ) K : Ω × Ω → R

ness values. The approach outputs a conﬁdenceof GP, whose complicated deﬁnition will be elabo-

value conf ∈ [0, 1] that indicates how likely the sys-

rated later.

tem satisﬁes the system speciﬁcation.

GP regression consists in deciding the covariancefunction of a GP, by learning from the observed

4 Conﬁdence Estimation via Gaussiandata, so that the distributions of unknown vari-data

Falsification Data

Cumulative Probability Calculation

GP Posterior

Multivariate Gaussian Distribution

Gaussian Process
Regression

A

B

Confidence

Hybrid System
Falsification

sample possibly negative points A, B

SystemSpecification

GP Prior

Input

Minimization Sampling

Workflow

Output

図 1: The proposed GP regression-based conﬁdence estimation approach for hybrid system falsiﬁcation

ables can be predicted, based on Bayes’ rules [31,parametrized function templates, and then ﬁt the§2.1].

Unlike other regression frameworks (e.g.,parameters based on training data. Convention-

deep learning), the prediction for an unknown point

ally, the mean function m can simply be a con-made by the GP provides a Gaussian distribution,

stant; here we use 0. The selection of the covariancei.e., a mean and a variance, rather than a single

function K is more sophisticated, as it is required

value, so we can exploit this information to derive

to guarantee Assumption 4. Widely-used choices

our conﬁdence measure.

for K include squared exponential kernel, Matérn

The prerequisite of GP regression is that thekernel and so on (see a discussion in [31, §4.2]). In

function that we want to approximate guarantees

this work, we follow a typical selection, namely, thethe following assumption [31].

closer in the input space have also closer output

squared exponential kernel, shown)( as follows:|ui − uj |2
K(ui , uj | θf , θl ) = θf exp −2θl2
where θf , θl ∈ R are tunable hyperparameters. Ini-

values.

tially (the left part of Fig. 2), these parameters have

Assumption 4 Two points that are geometrically

In general, the assumption is reasonable for any

arbitrary values θf0 and θl0 and identify a function

robustness function, as a small tuning of input sig-

K0 ; by this function, we obtain an initial GP priornals usually leads to a small change of the system

R ∼ GP 0 (m, K0 ).

outputs and so of the robustness value; such assumption is common in diﬀerent works on testingof CPSs [2, 9, 32]. So, we can apply GP regression
for approximating the robustness function. Fig. 2
shows the GP regression we apply to learn a surrogate model for the robustness function R from thefalsiﬁcation data T = {⟨u∗1 , Ru∗1 ⟩, . . . , ⟨u∗N , Ru∗N ⟩}Training.

at ﬁnding the optimal values θfopt , θlopt for θf , θl ,such that, under θfopt and θlopt , the likelihood of theoccurrence of the falsiﬁcation data T (in Def. 3) ismaximized. This method is referred to as maximum
likelihood estimation (MLE),
shown as follows:)
(
opt
opt
∗
θf , θl = arg max P Ru1 , . . . , Ru∗N | θf , θlθf ,θlin Def. 3. The process is elaborated in the following.

The parameter tuning process aims

(1)
where Pis the probability density function

mean function m and a covariance function K, de-of the multivariate Gaussian distribution of[]Ru∗1 . . . Ru∗N (see [31, §2.2 and §5] for more

noted as R ∼ GP(m, K). To determine m and K,

details).

a commonly-used approach is to ﬁrst specify twomerical optimization solver, such as Quasi-Newton

GP Prior.

A GP is uniquely identiﬁed by aThis problem can be solved by a nu-

GP priorRu

Falsification datau

R ⇠ GP 0 (m, K0 )
m=0✓

K0 (ui , uj ) = ✓f0 exp

Training(MLE)|ui uj |2(✓l0 )2◆
2

GP posterior
Ru

95% lower
confidence boundR ⇠ GP(m, K)
m=0
K(ui , uj ) = ✓fopt expu|ui uj |22(✓lopt )2!

図 2: Gaussian Process Regression for the Approximation of the Robustness Function

The problem in Def. 5 asks for the tail probability

method [7].
GP Posterior.

Given the decision of hyperpa-

rameters θf and θl , we can ﬁx our GP posterior forthe robustness function R (the right part of Fig. 2)
as R ∼ GP(m, K). By this, the posterior distribution of any unknown point u ∈ Ω is inferred as follows, according to Bayes’ rules [31, §2.2 and §A.2]:
Ru ∼N (µ, σ 2 )µ = Σu Σ−1u∗ Ru∗
[

σ

2

(2)

T
= K(u, u) − Σu Σ−1uu∗ Σ]where Σu = K(u, u∗1 ) . . . K(u, u∗N ) ,[ K(u∗1 ,u∗1 ) ... K(u∗1 ,u∗N ) ]
..
..
,
Σu∗ =
.
.
∗
∗
K(uN[,u∗K(u∗1)
N ,uN )]
and Ru∗ = Ru∗1 . . . Ru∗ . Ru identiﬁes theNinferred distribution for the robustness of u.

of a given GP; the exact answer of the problem ishard in general, and is still actively pursued in the
GP community [24, 27, 28]. Since our work mainly
aims at giving a hint of how likely it is that there
exists no counterexample in the falsiﬁcation search
space, an approximation of the tail probability isenough. In this section, we introduce a samplingbased approach to approximate the likelihood (i.e.,the conﬁdence measure) as deﬁned in Def. 5.
The process of conﬁdence estimation is shown in
Alg. 1. It requires the GP posterior GP obtainedin §4. 1 with its input space Ω, and two natural
numbers H, h ∈ N+ such that h ≪ H. The algorithm consists in a minimization sampling phase,and a cumulative probability calculation phase; at

4. 2 Conﬁdence Estimation
In this section, we describe how we derive a conﬁdence measure on the result of falsiﬁcation, basedon the surrogate GP posterior we obtained in §4. 1.

the end, it returns a conﬁdence value conf ∈ [0, 1]that indicates how likely it is that there exists nocounterexample in Ω. In the following, we elaborate on the process.

Accordingly, the problem introduced in Def. 3 isMinimization Sampling.

reformulated in terms of GP as follows:

Def. 5 is decided by its dual problem, i.e., the like-Deﬁnition 5 (GP-Based Conﬁdence) The GP-

lihood that there exists u ∈ Ω whose Ru is neg-based conﬁdence estimation problem is formalized

ative. To answer this problem, we need to col-as follows:lect the points in Ω, whose inferred robustness val-

• Given: the GP posterior R ∼ GP(m, K);ues have a considerable probability to be negative,• Return: the likelihood that any inferred distri-and then calculate their cumulative probability dis-bution Ru (for all u ∈ Ω) is positive.

The likelihood in

tribution. Since Ω is continuous, there could ex-

Algorithm 1 Conﬁdence estimation
Require: The R ∼ GP(m, K) obtained in §4. 1 and its input space ΩRequire: H: the number of points to randomly sample from GP
Require: h: the number of top-h sampled points to use for local search, s.t. h ≪ H
Ensure: conf: the conﬁdence value that the speciﬁcation holds

1: function EstimateConfidence(GP, Ω, H, h)2:collect a set U of u ∈ Ω by randomly sampling H points in Ω

3:

sort all u ∈ U ascendingly by lowBound(u) and take the ﬁrst h ones {u1 , . . . , uh }4:for i ∈ {1, . . . , h} do

5:u′i ← arg min lowBound(u) starting from uiu∈Ωµ ← Σu Σ−1∗
u∗ RuRu′1 , . . . , Ru′h ∼ N (µ, Σ) s.t.,TΣ ← K(u, u) − Σu Σ−1
∗ Σu
) u
(
return conf ← MvnCdf ⟨Ru′1 , . . . , Ru′h ⟩, [0, ∞)6:
7:▷ local search▷ see Eq. 2

ist inﬁnitely many such points, and hence it is(Line 3). Namely, we take each of the h sampledimpossible to involve all of them. However, ourpoints as a starting point to perform a local search,work mainly aims at giving an approximation ofaiming at ﬁnding new points that have even lower

the likelihood, so it suﬃces to select a ﬁnite set of

conﬁdence bound (Line 5); we use these points

points from Ω as representatives for that class of

to construct a multivariate Gaussian distribution,

points. To this aim, we construct a new function

based on the deﬁnition of GP (Line 6).

lowBound(u) = µ(u) − 1.96σ(u), that is, the 95%
lower conﬁdence bound of the posterior distribution of Ru in Eq. 2 (see an illustration in the GP
posterior in Fig. 2). Intuitively, if lowBound(u) islower than 0, there is still a considerable probability that Ru is negative; otherwise, we consider that
Ru is unlikely to be negative.
Therefore, this phase consists of an optimization process, taking lowBound(u) as the objectivefunction to be minimized. In order to derive comprehensive and precise estimation, we adopt a hybrid optimization approach that combines global
search and local search. First, in the global search,
we perform a comprehensive random sampling inΩ (Line 2) and sort the H points ascendingly
according to their 95% lower conﬁdence boundlowBound(u) (Line 3); we select the ﬁrst h sampled
points to perform a further minimization process

Cumulative Probability Calculation.

Given

the constructed multivariate Gaussian distribution
Ru′1 , . . . , Ru′k ∼ N (µ, Σ) in Line 6, we can apply
existing methods to calculate the probability thatRu′1 , . . . , Ru′k are all positive. There have been aline of works doing this; in our work, we adopt thestate-of-the-art, that is, a minimax tilting-based
approach [6] to calculate the probability. The function MvnCdf in Line 7 shows the interface of [6]:it takes as input the multivariate Gaussian distribution, i.e., its mean and covariance matrix, andthe range in which the distribution is expected tolocate; it returns a value conf, that indicates how
likely the multivariate Gaussian distribution distributes in the given range.

(AFC1) of the system is that µ shouldn’t devi-

5 Experimental Evaluation

ate too much from the reference value.

We here describe the experiments we conducted

Speciﬁcations are parameterized by a parameterto evaluate the proposed conﬁdence measure. We

ωi ; we set it to ﬁve diﬀerent values to have speciﬁ-

ﬁrst present the experiments settings in §5. 1; then,cations of diﬀerent complexity for the experiments.

in §5. 2, we analyze experimental results using aseries of research questions.

Software and Hardware Speciﬁcations. Our
experiments rely on Breach [13] to interface
Simulink and compute STL robustness. The ex-

5. 1 Experiment Settings

periments have been executed on an AWS EC2As benchmarks, we selected three Simulink models and seven STL speciﬁcations deﬁned for them,that are commonly used, in particular in falsiﬁcation competitions [11, 16, 17]. Table 1 reports thec4.2xlarge instance (2.9 GHz Intel Xeon E5-2666
v3, 15 GB RAM). The code and all the experimental results are available online at https://github.
com/choshina/GPConfidence.

benchmarks and the corresponding speciﬁcations.
The speciﬁcation ID identiﬁes the corresponding
model. A description of the models and of their
speciﬁcations is as follows.
• Automatic Transmission (AT) [25] models an

5. 2 Evaluation
We assess the viability of the proposed conﬁdence
measure using three research questions, describedas follows.

automotive system that has two input signals,
throttle ∈ [0, 100] and brake ∈ [0, 325], andthree outputs signals, gear , speed , and rpm.
The speciﬁcations consider system safety: requirements on speed (AT1, AT3), on rpm(AT4), or their relation (AT2).
• Free Floating Robot (FFR) [9] models a robot
operating in a 2D space.

It has four input

signals u1 , u2 , u3 , u4 ∈ [−10, 10] representing
the boosters, and four output signals that represent the coordinates x, y of the robot position, and their one-order derivatives ẋ, ẏ. The
speciﬁcations specify kinetic properties for the
robot: FFR1 requires the robot to pass an areaaround the point (4, 4) under an input constraint, and FFR2 requires the robot to stayin a given area for at least 2 seconds.
• Abstract Fuel Control (AFC) [26] takes two
input signals, Pedal Angle ∈ [8.8, 70] andEngine Speed ∈ [900, 1100], and outputs aratio µ reﬂecting the deviation of air-fuelratio from its reference value. A requirement

RQ1 Does the conﬁdence measure monotonicallyincrease?
As explained in §1, a conﬁdence measure, in order
to be reliable, should be monotonically increasing,i.e., it should not decrease as new falsiﬁcation datais considered. As previously explained, this cannot
be theoretically guaranteed by the proposed metric,
as it is always possible to ﬁnd a new input that drastically changes the learned GP. Therefore, we here
want to assess to what extent the proposed metric ismonotonically increasing. For each benchmark (using the default value ωd ), we have randomly sampled an increasing number of points in Ω; then, foreach set of sampled points T , we have computed theminimum robustness and the conﬁdence measure.
Fig. 3 shows, for each benchmark, how the minimum robustness value (right axis and red plot) andthe conﬁdence measure (left axis and blue plot)change by increasing the size of T .†2 The plots†2 Since computing the conﬁdence measure can takeup to 30 seconds, we have computed it only forsome sizes of |T |.

表 1: Speciﬁcations. For each one, we list a set of parameters ω1 , . . . , ω5 for RQ2; the default parameterused in RQ1 and RQ3 is indicated by ωdωi (i = 1, . . . , 5)

ωd

AT1

□[0,30] (speed < ωi ){135, 140, 145, 150, 155}

ω3

AT2

□[0,10] (speed < 50) ∨ ♢[0,30] (rpm > ωi )

{500, 750, 1000, 1250, 1500} ω4□[0,29] (speed < 100) ∨ □[29,30] (speed > ωi ){57, 59, 61, 63, 65}

ω2□[0,30] (rpm < 4770 ∨ □[0,1] (rpm > ωi )){200, 300, 400, 500, 600}

ω1

FFR1

¬ ♢[0,5] x, y ∈ [3.9 + ωi , 4.1 − ωi ] ∧ ẋ, ẏ ∈ [−0.5, 0.5] {0.01, 0.03, 0.05, 0.07, 0.09}

FFR2¬♢[0,5] □[0,2] (x, y ∈ [1.5 + ωi , 1.7 − ωi ]){0, 0.02, 0.04, 0.06, 0.08}

ω2

AFC1

□[11,50] (controller mode = 1 → µ < ωi ){0.25, 0.3, 0.35, 0.4, 0.45}

ω2

15

0.6
10
0.4
5

0.2

0
500

1000

250

0.8

200

0.6

150

0.4

100

0.2

50

0
900

0
2000

1500

1

950

(a) AT1

1

0.8

0.8

0.6

0.6

0.4

0.4

100

0.2

0.2

0

0

0.6
300
0.4
200
0.2

6000

7000

200

400

number of simulations

600

Minimum robustness
Confidence

400

Minimum robustness
Confidence

Confidence

0.8

5000

6

0.4

4

0.2

2

1400

0.8

0.2

0.6

0.15

0.4

0.1

0.2

0.05

500

Confidence

0.8

0.8

0.6

0.6

0.4

0.4

0.2

0.2

1000

1200

1500

0
2000

(f) FFR2
1

800

1000

number of simulations(e) FFR1

600

0
2000

0.25

0

0
800 1000 1200 1400 1600 1800

1

0
400

1800

1

number of simulations(d) AT4

1600(c) AT3

1

500

4000

0.6

number of simulations

600

3000

8

(b) AT2

1

2000

0.8

0
1200

0
1100

1050

10

number of simulations

number of simulations

0
1000

1000

1

1400

1600

Minimum robustness

Confidence

0.8

Minimum robustness
Confidence

20

ω1

Minimum robustness

1

Minimum robustness
Confidence

AT3
AT4

Minimum robustness

Spec. ID STL formula0
1800

number of simulations(g) AFC1

図 3: RQ1 – Experimental results on monotonicity

show the intervals of sizes of T in which the con-tions for lower number of simulations (e.g., FFR2);

ﬁdence measure changes signiﬁcantly, before stabi-these initial oscillations are expected, because thelizing to a given value. We observe that, in most of

precision of the GP depends on the number of ele-

the cases (i.e., AT1, AT2, AT3, FFR1, and FFR2),

ments of the training data. For some cases, instead,the measure is quite monotonic, with few oscilla-

the conﬁdence measure remains high for some timeat the beginning (i.e., AT4 and AFC1) and thenmum robustness and the conﬁdence measure overstabilizes at a lower value. For AFC1, the reason

the simulations. Then, for each speciﬁcation type,

is that the minimum robustness is always very low;

we have selected the minimum number of simula-so, with more observations, the GP learns such low

tions for which, in at least one instantiation of ωi ,robustness, and so the conﬁdence on the absence

the conﬁdence measure reaches 100% (or we selectof a falsifying input decreases. For AT4, the main

the maximum number 2000 if none of them reaches

decrease in conﬁdence occurs due to big drops in100%), and we take this number of simulations tominimum robustness. A way to increase the conﬁ-

compare the results of the speciﬁcation type: indence also in the presence of low robustness would

this way, we can observe whether there are actu-

be to add more training data, so that the GP canally diﬀerences, and we avoid the saturation eﬀect

get a better estimation; this is not applicable inthat may be obtained by using a lot of simulations

our context, because we rely only on the falsiﬁca-

in which the results converge to the same value.

tion data. However, in the next research question,

Table 2 reports, for each speciﬁcation type, re-we show that the conﬁdence metric is still reliable.

sults of the diﬀerent instantiations, in terms of

Answer to RQ1: Most of the time, the con-minimum robustness (minRob), conﬁdence measureﬁdence measure is reliable, as it does not de-(conf), and conﬁdence computation time (in secs);

crease (signiﬁcantly) with increasing number

results are sorted increasingly by minRob. We noteof simulations. However, in some cases, thethat, overall, the metric is sound because, given ameasure is ﬂuctuating for a lower number of

speciﬁcation type, lower conﬁdence values are ob-

simulations, due to big changes in minimum

tained for lower robustness. Usually, large change

robustness.

in conﬁdence occurs when there is a big percentage change in robustness, such as AT2, where the

RQ2 Is the conﬁdence measure sound?

maximum value of minRob is 21.3% bigger than theminimum value, and the diﬀerence in conﬁdence is

We claim that a conﬁdence measure is sound if it
is related to the diﬃculty of falsifying a speciﬁcation, which can be assessed by the minimum robustness that is achieved by a falsiﬁcation algorithm.
Therefore, we expect that the lower the minimum
robustness is, the lower the conﬁdence should be.

88.92 perc. points. In some cases, the variance ofconf across the instantiations is not too high, as in
AT3, AT4, and FFR1 (diﬀerences of 14.93, 35.4,
and 9.11 perc. points); we notice that, in thesecases, the percentage change of robustness is small(0.99%, 0.36%, and 2.04%).

To assess to what extent the proposed conﬁdence
measure is sound, we compare the conﬁdence results for the diﬀerent instantiations of a speciﬁcation type in Table 1; indeed, these represent similar
problems that, however, can have diﬀerent valuesof minimum robustness (as the speciﬁcation is moreor less demanding). Concretely, for each speciﬁca-

Answer to RQ2: Overall, the conﬁdence
measure is sound as it is related to the difﬁculty of the speciﬁcation, measured by theminimum robustness.
RQ3 What is the conﬁdence provided by diﬀerenttion type and for each of the diﬀerent values of thefalsiﬁcation algorithms?
We are here interested in investigating what isparameter ωi , we have run random sampling forthe conﬁdence provided by diﬀerent falsiﬁcation al-

2000 simulations, and we have collected the mini-

gorithms (i.e., implementing diﬀerent search strate-表 2: RQ2 – Experimental results on soundness. conf is in %; time is in secs.
AT1
ωi

AT2

AT3

minRob

conf

time

ωi

minRob

conf

ω1

5.12

39.23

22.8

ω5

33.42

ω2

10.06

97.77

26.3

ω4

34.55

ω3

13.6

49.93

24.2

ω3

43.72

ω4

18.1

100

23.43

ω2

250

ω5

22.41

100

26.6

ω1

500

88.92

time

ωi

minRob

conf

time

ωi

minRob

conf

time

0

30

ω5

4.82

82.52

22.4

ω3

355.44

56.59

29.9

0.01

33.4

ω3

5.56

93.89

19.6

ω4

445.41

87.62

30.9

0

27.9

ω4

6.24

89.67

21.4

ω5

466.57

85.86

26.6

26.33

29.3

ω2

7.13

93.34

22.5

ω2

473.54

90.79

30.6

29.7

ω1

9.6

97.45

23.4

ω1

608.4

91.99

28.5

FFR1
ωi

minRob

conf

ω5

0.21

ω3

0.49

AT4

FFR2
time

ωi

minRob

99.28

20

ω3

99.95

20.3

ω1

AFC1

conf

time

ωi

minRob

conf

time

0.01

1.27

23.2

ω1

0.02

11.17

21.2

ω2

0.03

1.84

0.3

0.08

10.48

0.3

ω2

0.5

90.84

21.5

ω2

0.03

2.53

20.2

ω3

0.13

99.95

0.2

ω1

0.58

98.88

24.2

ω4

0.07

47.23

16.8

ω4

0.18

100

0.3

ω4

0.64

92.37

23.1

ω5

0.08

0.91

21.1

ω5

0.23

100

0.3

gies) when they are not able to falsify. We tookgarding the variance of the results, we observe thatthree representative algorithms:

Random search

CMAES is the one with the highest variance, as diﬀer-

that performs pure exploration, CMAES [23] that is

ent search trials can lead to diﬀerent search paths

a greedy approach that favours exploitation, andand so diﬀerent conﬁdence values; also Random has

MCTS [37] that provides a balance between explo-

some variance across the results, but not as muchration and exploitation. We have applied the three

as CMAES. MCTS is the more stable approach, as thealgorithms (for 2000 simulations) to three bench-balance between exploration and exploitation leads

mark speciﬁcations (AT3, FFR1, and AFC1 instan-most of the times to the same search paths, and so

tiated with ωd as reported in Table 1); we repeatedto the same conﬁdence values.

the experiments 10 times.

Answer to RQ3: Falsiﬁcation approaches

Fig. 4 reports how the conﬁdence measurethat provide enough exploration lead to higher

changes across the 10 repetitions. We observe that

conﬁdence. MCTS is the more stable algorithm.

higher conﬁdence is usually obtained by Random:
since it explores more, it can provide more distributed data for GP learning, so obtaining a better
GP (with less uncertainty). On the contrary, CMAES
obtains low conﬁdence as it does not explore enoughand so the GP learning does not have training data
for large parts of the search space in which the uncertainty of the GP will be high. MCTS can obtain
good results when it explores enough (as in FFR1
and AFC1), but sometimes it can be too greedy(as in AT3) and so it obtains low conﬁdence. Re-

6 Related Work
Gaussian processes and Gaussian process regression are widely applied in diﬀerent contexts. In
statistics, GP regression, usually referred to as
Kriging methods, is used to build surrogate models for measuring the probability of rare events,
e.g., [5, 21, 34]. These works usually develop new
sampling techniques to derive rare events probability using limited numbers of observations, andhave been widely applied in engineering domains.
Theoretical explorations in tail probability of GPs

図 4: Conﬁdence comparison between diﬀerent falsiﬁcation algorithms

have been heavily conducted in the statistics com-

result.

munity [24, 27, 28]. In general, this is a hard prob-

Our conﬁdence measure has similarities with cov-

lem and research eﬀorts are still on-going; achieve-

erage criteria used in testing, as they both aim at

ments so far usually limit GP to certain types, e.g.,

giving a conﬁdence on the absence of faults. The

Brownian motion.

main diﬀerence is that coverage criteria ﬁx a set

In falsiﬁcation, GP regression has been mainlyof test requirements that need to be covered, andused for guiding the search process, and not forthe coverage level acts as a conﬁdence value; inconﬁdence estimation as done in this paper. Desh-our case, the conﬁdence measure does not specify

mukh et al. [9] apply Bayesian optimization, an op-

what needs to be covered, but implicitly considers

timization approach derived from GP regression, tothe coverage of the input space. Coverage crite-

falsiﬁcation, and investigates a dimension reduction

ria have been proposed for falsiﬁcation. Dokhanchi

technique. Akazaki [2] uses it for the falsiﬁcation

et al. [12] deﬁne coverage based on the blocks ofof conditional properties □I φcond → φsafe in which

Simulink models, and integrate the coverage level

the antecedent φcond must be satisﬁed in order to be

as part of the objective function of the falsiﬁcation

able to violate the property; GP regression is usedproblem. Dreossi et al. [15] use “star discrepancy”

to guide the search towards input satisfying φcond .

as a measure of input space coverage, and use it to

Silvetti et al. [32] use GP regression to approximate

guide the falsiﬁcation search. Adimoolam et al. [1]the STL semantics and so identify the inputs thatclassify inputs according to their robustness values,

have higher probability to have lower robustness.

and deﬁne coverage based on the clustered inputs.

Apart from falsiﬁcation, also in the more general

All these works use coverage as a means for guid-

context of search-based testing (SBT), the usage ofing the search, but they do not explicitly use it as a

GP regression has been recently advocated [20] forconﬁdence measure. Although our conﬁdence mea-

speeding up the search. However, to the best ofsure is not a coverage criterion, it has some good

our knowledge, no work in falsiﬁcation or SBT uses

properties as monotonicity that would allow to also

GP regression for conﬁdence estimation on the ﬁnal

use it as stopping criterion for falsiﬁcation; this us-

age of the measure is part of our future work.
In the veriﬁcation community, other approaches
provide some type of conﬁdence on the veriﬁcation

try to properly characterize the systems in which
the assumption holds, and so the conﬁdence measure is more trustworthy.

results. For example, in probabilistic model check-

謝辞 Paolo Arcaini is supported by ERATO HA-

ing [4, Chapter 10], the probability that a given

SUO Metamathematics for Systems Design Projectproperty holds can be estimated; the approach is,(No.

however, much diﬀerent from ours, as it operates

AI Techniques for Practical Applications of High-on much simpler models as Markov chains.

Quality Machine Learning-based Systems Project

JPMJER1603), JST; and by Engineerable(Grant Number JPMJMI20B8), JST-Mirai.

7 Conclusion
In this paper, we have proposed a conﬁdence
measure that, in case a falsiﬁcation algorithm has
terminated without returning any falsifying input,
estimates the probability that the speciﬁcation isindeed non-falsiﬁable. The measure is computed
by ﬁrst performing a Gaussian Process (GP) Regression process that learns the robustness function from the falsiﬁcation data, and by then deriving from it the probability that no falsifying input
exists.
In this work, we have considered one particularkernel function for GP; as future work, we plan
to investigate whether other kernel functions provide better results. The proposed approach works
better if the ﬁtness landscape is smooth (see Assumption 4); however, in some cases, the ﬁtness
landscape of the robustness could be quite complicated, in particular when output signals of diﬀerent
magnitudes are used in the speciﬁcation (called thescale problem in [38–40]); as future work, we plan
to devise techniques that mitigate the scale problem, and so make it easier to learn the robustness
function.
The approach is applicable to hybrid systems inwhich Assumption 4 holds, i.e., those for which
the Gaussian approximation is suitable. While thisusually holds for continuous dynamics, it may nothold when discrete modes (e.g., states of a hybrid
automaton) are involved. As future work, we planto perform a much larger empirical evaluation to参 考 文 献[ 1 ] 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 International Publishing, 2017, pp. 483–503.
[ 2 ] Akazaki, T.: Falsiﬁcation of Conditional Safety
Properties for Cyber-Physical Systems with Gaussian Process Regression, Runtime Veriﬁcation,
Cham, Springer International Publishing, 2016,
pp. 439–446.
[ 3 ] Annpureddy, Y., Liu, C., Fainekos, G., andSankaranarayanan, S.: S-TaLiRo: A Tool for
Temporal Logic Falsiﬁcation for Hybrid Systems,
Springer, 2011, pp. 254–257.
[ 4 ] Baier, C. and Katoen, J.-P.: Principles of Model
Checking (Representation and Mind Series), The
MIT Press, 2008.
[ 5 ] Balesdent, M., Morio, J., and Marzat, J.:
Kriging-based adaptive importance sampling algorithms for rare event estimation, Structural Safety,
Vol. 44(2013), pp. 1–10.
[ 6 ] Botev, Z.: The normal law under linear restrictions: simulation and estimation via minimax tilting, Journal of the Royal Statistical Society: Series
B (Statistical Methodology), Vol. 1, No. 79(2017),
pp. 125–148.
[ 7 ] Broyden, C. G.: A class of methods for solving
nonlinear simultaneous equations, Mathematics ofcomputation, Vol. 19, No. 92(1965), pp. 577–593.
[ 8 ] Corso, A., Moss, R. J., Koren, M., Lee, R.,
and Kochenderfer, M. J.: A survey of algorithms
for black-box safety validation, arXiv preprint
arXiv:2005.02979, (2020).
[ 9 ] Deshmukh, J., Horvat, M., Jin, X., Majumdar,R., and Prabhu, V. S.: Testing Cyber-Physical Systems through Bayesian Optimization, ACM Trans.
Embed. Comput. Syst., Vol. 16, No. 5s(2017).
[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] Dokhanchi, A., Yaghoubi, S., Hoxha, B.,
Fainekos, G., Ernst, G., Zhang, Z., Arcaini, P., Hasuo, I., and Sedwards, S.: ARCH-COMP18 Category Report: Results on the Falsiﬁcation Benchmarks, ARCH18. 5th International Workshop on
Applied Veriﬁcation of Continuous and Hybrid Systems, EPiC Series in Computing, Vol. 54, EasyChair, 2018, pp. 104–109.
[12] Dokhanchi, A., Zutshi, A., Sriniva, R. T.,
Sankaranarayanan, S., and Fainekos, G.: Requirements Driven Falsiﬁcation with Coverage Metrics,
Proceedings of the 12th International Conferenceon Embedded Software, EMSOFT ’15, IEEE Press,
2015, pp. 31–40.
[13] Donzé, A.: Breach, a Toolbox for Veriﬁcation
and Parameter Synthesis of Hybrid Systems, Proceedings of the 22nd International Conference on
Computer Aided Veriﬁcation, CAV’10, Berlin, Heidelberg, Springer-Verlag, 2010, pp. 167–170.
[14] Donzé, A. and Maler, O.: Robust Satisfactionof Temporal Logic over Real-Valued Signals, Proceedings of the 8th International Conference on
Formal Modeling and Analysis of Timed Systems,
FORMATS’10, Berlin, Heidelberg, Springer-Verlag,
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
of Hybrid Systems, NASA Formal Methods - 7thInternational Symposium, NFM 2015, Pasadena,
CA, USA, April 27-29, 2015, Proceedings, 2015,
pp. 127–142.
[16] 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.
[17] Ernst, G., Arcaini, P., Donzé, A., Fainekos, G.,
Mathesen, L., Pedrielli, G., Yaghoubi, S., Yamagata, Y., and Zhang, Z.: ARCH-COMP 2019 Category Report: Falsiﬁcation, ARCH19. 6th International Workshop on Applied Veriﬁcation of Continuous and Hybrid Systems, EPiC Series in Computing, Vol. 61, EasyChair, 2019, pp. 129–140.
[18] Ernst, G., Sedwards, S., Zhang, Z., and Hasuo,
I.: Fast Falsiﬁcation of Hybrid Systems Using Probabilistically Adaptive Input, Quantitative Evaluation of Systems, Cham, Springer, 2019, pp. 165–181.
[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] Feldt, R. and Poulding, S.: Broadening the

Search in Search-Based Software Testing: It Need
Not Be Evolutionary, Proceedings of the EighthInternational Workshop on Search-Based Software
Testing, SBST ’15, IEEE Press, 2015, pp. 1–7.
[21] Giordano, S., Gubinelli, M., and Pagano, M.:
Rare events of Gaussian processes: a performancecomparison between bridge Monte-Carlo and importance sampling, International Conference on Next
Generation Wired/Wireless Networking, Springer,
2007, pp. 269–280.
[22] Gladisch, C., Heinz, T., Heinzemann, C.,
Oehlerking, J., von Vietinghoﬀ, A., and Pﬁtzer, T.:
Experience Paper: Search-Based Testing in Automated Driving Control Applications, Proceedings ofthe 34th IEEE/ACM International Conference on
Automated Software Engineering, ASE ’19, IEEE
Press, 2019, pp. 26–37.
[23] Hansen, N., Müller, S. D., and Koumoutsakos,
P.: Reducing the time complexity of the derandomized evolution strategy with covariance matrix
adaptation (CMA-ES), Evolutionary computation,
Vol. 11, No. 1(2003), pp. 1–18.
[24] Harper, A. J.: Bounds on the suprema of Gaussian processes, and omega results for the sum of arandom multiplicative function, The Annals of Applied Probability, Vol. 23, No. 2(2013), pp. 584 –
616.
[25] 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, EasyChair, 2014, pp. 25–30.
[26] 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.
[27] Li, W. V., Shao, Q.-M., et al.: Lower tail probabilities for Gaussian processes, The Annals of Probability, Vol. 32, No. 1A(2004), pp. 216–242.
[28] Marcus, M. B., Shepp, L. A., et al.: Sample
behavior of Gaussian processes, Proceedings of the
Sixth Berkeley Symposium on Mathematical Statistics and Probability, Volume 2: Probability Theory,
The Regents of the University of California, 1972.
[29] Menghi, C., Nejati, S., Briand, L., andParache, Y. I.: Approximation-Reﬁnement Testingof Compute-Intensive Cyber-Physical Models: An
Approach Based on System Identiﬁcation, Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering, ICSE ’20, New York,NY, USA, Association for Computing Machinery,
2020, pp. 372–384.
[30] Nejati, S., Gaaloul, K., Menghi, C., Briand,L. C., Foster, S., and Wolfe, D.: Evaluating Model
Testing and Model Checking for Finding Requirements Violations in Simulink Models, Proceedingsof the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering,
ESEC/FSE 2019, New York, NY, USA, Association
for Computing Machinery, 2019, pp. 1015–1025.
[31] Rasmussen, C. E., Williams, C. K., and Bach,F.: Gaussian Processes for Machine Learning, MIT
Press, 2006.
[32] 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.
[33] 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).
[34] Zanette, A., Zhang, J., and Kochenderfer, M. J.:
Robust super-level set estimation using gaussian
processes, Joint European Conference on Machine
Learning and Knowledge Discovery in Databases,
Springer, 2018, pp. 276–291.
[35] Zhang, Z. and Arcaini, P.: Gaussian ProcessBased Conﬁdence Estimation for Hybrid System
Falsiﬁcation, International Symposium on Formal
Methods, Springer, 2021, pp. 330–348.
[36] 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.
[37] 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.
[38] Zhang, Z., Hasuo, I., and Arcaini, P.: Multiarmed Bandits for Boolean Connectives in Hybrid
System Falsiﬁcation, Computer Aided Veriﬁcation,
Dillig, I. and Tasiran, S.(eds.), Cham, Springer International Publishing, 2019, pp. 401–420.
[39] 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.
[40] 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, Dutle, A., Moscato, M. M.,
Titolo, L., Muñoz, C. A., and Perez, I.(eds.), Cham,
Springer International Publishing, 2021, pp. 392–
399.