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

Multi-Armed Bandits for Boolean Connectives inHybrid System Falsification
Zhenya Zhang, Ichiro Hasuo, Paolo Arcaini
Hybrid system falsification is an actively studied topic, as a scalable quality assurance methodology for real-world cyberphysical systems. In falsification, one employs stochastic hill-climbing optimization to quickly find a counterexample input
to a black-box system model. Quantitative robust semantics is the technical key that enables use of such optimization. In
this paper, we tackle the so-called scale problem regarding Boolean connectives that is widely recognized in the community:
quantities of different scales (such as speed [km/h] vs. rpm, or worse, rph) can mask each other’s contribution to robustness.
Our solution consists of integration of the multi-armed bandit algorithms in hill climbing-guided falsification frameworks,
with a technical novelty of a new reward notion that we call hill-climbing gain. Our experiments show our approach’srobustness under the change of scales, and that it outperforms a state-of-the-art falsification tool.

The falsification problem

1 Introduction• Given: a model M (that takes an input signal u andHybrid System Falsification

yields an output signal M(u)), and a specification

Quality assurance of cyber-physical systems (CPS) is

φ (a temporal formula)attracting growing attention from both academia and in-• Find: a falsifying input, that is, an input signal u

dustry, not only because it is challenging and scientif-

such that the corresponding output M(u) violates

ically interesting, but also due to the safety-critical na-

φture of many CPS. The combination of physical systems

u

/ M

M(u)
̸|=φ ?

/(with continuous dynamics) and digital controllers (thatIn optimization-based falsification, the above prob-

are inherently discrete) is referred to as hybrid systems,

lem is turned into an optimization problem. It is ro-capturing an important aspect of CPS. To verify hybridbust semantics of temporal formulas [12, 17] that makes

systems is intrinsically hard, because the continuous dy-

it possible. Instead of the Boolean satisfaction relation

namics therein leads to infinite search spaces.

v |= φ, robust semantics assigns a quantity Jv, φK ∈More researchers and practitioners are therefore turn-R ∪ {∞, −∞} that tells us, not only whether φ is true

ing to optimization-based falsification as a quality assur-

or not (by the sign), but also how robustly the formula

ance measure for CPS. The problem is formalized as fol-is true or false. This allows one to employ hill-climbinglows.

optimization: we iteratively generate input signals, in the
direction of decreasing robustness, hoping that eventually
we hit negative robustness.
An illustration of robust semantics is in Table 1. We

This work was originally published at 31st International Conference on Computer-Aided Verification.
Zhenya Zhang, Ichiro Hasuo, Paolo Arcaini, 国立情報学研究
所, National Institute of Informatics.

use signal temporal logic (STL) [12], a temporal logic
that is commonly used in hybrid system specification.

表 1: Boolean satisfaction w |= φ, and quantitative robustness values Jw, φK, of three signals of speed for the STL

formula φ ≡ 2[0,30] (speed < 120)

90

60

60

70

110

90

80

60

96

00

w |= φJw, φK

0
10

20

30

130

120

30

30
0

SPEED

SPEED

90

120

120

SPEED

120

120

signal w

150

150

150

100

110120

90
60
30

00

10

20

0

30

0
0

10

20

TIME

TIME

TIME

True
30

True
10

False
−10

30

The specification says the speed must always be below

sition120 during the time interval [0, 30]. In the search of

In the field of hybrid falsification—and more generally

an input signal u (e.g. of throttle and brake) whose cor-in search-based testing—the following problem is widely

responding output M(u) violates the specification, therecognized. We shall call the problem the scale problem

quantitative robustness JM(u), φK gives much more in-(in Boolean superposition).

formation than the Boolean satisfaction M(u) |= φ. In-

Consider an STL specification φ ≡ 2[0,30] (¬(rpm >deed, in Table 1, while Boolean satisfaction fails to dis-4000) ∨ (speed > 20)) for a car; it is equivalent tocriminate the first two signals, the quantitative robustness

2[0,30] ((rpm > 4000) → (speed > 20)) and says thatindicates a tendency that the second signal is closer to vi-

the speed should not be too small whenever the rpm isolation of the specification.

over 4000. According to the usual definition in the litera-In the falsification literature, stochastic algorithms

ture [11, 17], the Boolean connectives ¬ and ∨ are inter-are used for hill-climbing optimization. Examples include simulated annealing (SA), globalized Nelder-Meadpreted by − and the supremum ⊔, respectively; and the⊔“always” operator 2[0,30] is by infimum . Therefore(GNM [30]) and covariance matrix adaptation evolution

the robust semantics of φ under the signal (rpm, speed ),strategy (CMA-ES [6]). Note that the system model M

where rpm, speed : [0, 30] → R, is given as follows.

can be black-box: we have only to observe the correspondence between input u and output M(u). Observing an

J(rpm, speed), φK =

d

((

) (
))
4000 − rpm(t) ⊔ speed(t) − 20t∈[0,30](1)error M(u′ ) for some input u′ is sufficient evidence for asystem designer to know that the system needs improve-

A problem is that, in the supremum of two real values

ment. Besides these practical advantages, optimization-in (1), one component can totally mask the contribution

based falsification is an interesting scientific topic: itof the other. In this specific example, the former (rpm)combines two different worlds of formal reasoning andcomponent can have values as big as thousands, while thestochastic optimization.

latter (speed ) component will be in the order of tens. This

Optimization-based falsification started in [17] and hasmeans that in hill-climbing optimization it is hard to use

been developed vigorously [1,3–5,9,11–13,15,27,28,34,

the information of both signals, as one will be masked.

36,38]. See [26] for a survey. There are mature tools such

Another related problem is that the efficiency of a fal-as Breach [11] and S-Taliro [5]; they work with industry-sification algorithm would depend on the choice of units

standard Simulink models.

of measure. Imagine replacing rpm with rph in (1), which

Challenge: The Scale Problem in Boolean Superpo-

makes the constant 4000 into 240000, and make the situation even worse.

These problems—that we call the scale problem—

2I (φ1 ∧ φ2 ) and 2I (φ1 ∨ φ2 ); we call them (con-occur in many falsification examples, specifically whenjunctive/disjunctive) safety properties. We identify ana specification involves Boolean connectives. We do

instance of the MAB problem in the choice of the for-need Boolean connectives in specifications: for exam-

mula (out of φ1 , φ2 ) to try to falsify by hill climbing.

ple, many real-world specifications in industry are of the

See Fig. 1. We combine MAB algorithms (such as ε-form 2I (φ1 → φ2 ), requiring that an event φ1 triggers

greedy and UCB1, see §3. 2) with hill-climbing optimiza-a countermeasure φ2 all the time.

tion, for the purpose of coping with the scale problem in

One could use different operators for interpreting

Boolean superposition. This combination is made possi-

Boolean connectives. For example, in [21], ∨ and ∧ areble by introducing a novel reward notion for MAB, calledinterpreted by + and × over R, respectively. However,hill-climbing gain, that is tailored for this purpose.

these choices do not resolve the scale problem, either. In
general, it does not seem easy to come up with a fixed set

We have implemented our MAB-based falsification
framework in MATLAB, building on Breach [11].†1 Ourof operators over R that interpret Boolean connectives

experiments with benchmarks from [7, 24, 25] demon-and are free from the scale problem.

strate that our MAB-based approach is a viable one
against the scale problem. In particular, our approach isobserved to be (almost totally) robust under the change ofscaling (i.e. changing units of measure, such as from rpm
to rph that we discussed after the formula (1)). Moreover,

φ1

φ2

図 1: A multi-armed bandit for falsifying 2I (φ1 ∧ φ1 )for the benchmarks taken from the previous works—they
do not suffer much from the scale problem—our algorithm performs better than the state-of-the-art falsification tool Breach [11].

Contribution: Integrating Multi-Armed Bandits

Related Work

into Optimization-Based Falsification

Besides those we mentioned, we shall discuss some re-As a solution to the scale problem in Boolean super-

lated works.

position that we just described, we introduce a new ap-

Formal verification approaches to correctness of hy-

proach that does not superpose robustness values. In-

brid systems employ a wide range of techniques, includ-

stead, we integrate multi-armed bandits (MAB) in the ex-ing model checking, theorem proving, rigorous numerics,

isting framework of falsification guided by hill-climbing

nonstandard analysis, and so on [8, 14, 18, 20, 22, 23, 29,

optimization.

32]. These are currently not very successful in dealing

The MAB problem is a prototypical reinforcement
learning problem: a gambler sits in front of a row of slotwith complex real-world systems, due to issues like scalability and black-box components.

machines; their performance (i.e. average reward) is not

Our use of MAB in falsification exemplifies the role

known; the gambler plays a machine in each round and heof the exploration-exploitation trade-off, the core prob-

continues with many rounds; and the goal is to optimize

lem in reinforcement learning. The trade-off has been al-

cumulative rewards. The gambler needs to play different

ready discussed for the verification of quantitative prop-

machines and figure out their performance, at the cost oferties (e.g., [33]) and also in some works on falsification.

the loss of opportunities in the form of playing subopti-

A recent example is [36], where they use Monte Carlomal machines.
In this paper, we focus on specifications of the form

†1 Code obtained at https://github.com/decyphir/breach.

tree search to force systematic exploration of the space

Let w : [0, T ] → RM and w′ : [0, T ′ ] → RM be M -of input signals. Besides MCTS, Gaussian process learn-

dimensional signals. Their concatenation w·w′ : [0, T +ing (GP learning) has also attracted attention in machine

T ′ ] → RM is the M -dimensional signal defined bylearning as a clean way of balancing exploitation and ex-(w · w′ )(t) = w(t) if t ∈ [0, T ], and (w · w′ )(t) =ploration. The GP-UCB algorithm is a widely used strat-w′ (t − T ) if t ∈ (T, T + T ′ ].

egy there. Its use in hybrid system falsification is pursued

Let 0

<

T1

<

T2

≤

w|[T1 ,T2 ] : [0, T2 − T1 ] → R

e.g. in [3, 34].
More generally, coverage-guided falsification [1, 9,

M

T.

The restrictionof w : [0, T ] → RM

to the interval [T1 , T2 ] is defined by (w|[T1 ,T2 ] )(t) =13, 28] aims at coping with the exploration-exploitationw(T1 + t).

trade-off. One can set the current work in this context—

One main advantage of optimization-based falsification

the difference is that we force systematic exploration onis that a system model can be a black box—observing thethe specification side, not in the input space.

correspondence between input and output suffices. We

There have been efforts to enhance expressiveness oftherefore define a system model simply as a function.

MTL and STL, so that engineers can express richer

Definition 2 (system model M) A system model, withintentions—such as time robustness and frequency—in

M -dimensional input and N -dim. output, is a function

specifications [2, 31]. This research direction is orthogo-

M that takes an input signal u : [0, T ] → RM and re-nal to ours; we plan to investigate the use of such logics

turns a signal M(u) : [0, T ] → RN . Here the com-in our current framework.

mon time horizon T ∈ R+ is arbitrary.

Further-

A similar masking problem around Boolean connec-

more, we impose the following causality condition ontives is discussed in [10, 19]. Compared to those ap-

M: for any time-bounded signals u : [0, T ] → RM andproaches, our technique does not need the explicit decla-u′ : [0, T ′ ] → RM , we require that M(u · u′ ) [0,T ] =ration of input vacuity and output robustness, but it reliesM(u).

on the “hill-climbing gain” reward to learn the signifi-

Definition 3 (STL syntax) We fix a set Var of vari-cance of each signal.

ables. In STL, atomic propositions and formulas are de-Finally, the interest in the use of deep neural networks

fined as follows, respectively: α ::≡ f (x1 , . . . , xN ) >is rising in the field of falsification (as well as in many0, and φ ::≡ α | ⊥ | ¬φ | φ ∧ φ | φ ∨ φ | φ UI φ.

other fields). See e.g. [4, 27].

Here f is an N -ary function f : RN → R, x1 , . . . , xN ∈Var, and I is a closed non-singular interval in R≥0 , i.e.

2 Preliminaries: Hill Climbing-Guided Falsification

I = [a, b] or [a, ∞) where a, b ∈ R and a < b.
We omit subscripts I for temporal operators if I =We review a well-adopted methodology for hybrid sys-

[0, ∞). Other common connectives such as →, ⊤, 2I

tem falsification, namely the one guided by hill-climbing(always) and 3I (eventually), are introduced as abbrevi-

optimization. It makes essential use of quantitative robust

ations: 3I φ ≡ ⊤ UI φ and 2I φ ≡ ¬3I ¬φ. An atomic

semantics of temporal formulas, which we review too.

formula f (⃗x) ≤ c, where c ∈ R, is accommodated using¬ and the function f ′ (⃗x) := f (⃗x) − c.

2. 1 Robust Semantics for STL

Definition 4 (robust semantics [12]) Let w : [0, T ] →Our definitions here are taken from [12, 17].

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

Definition 1 ((time-bounded) signal) Let T ∈ R+ be at-shift of w, denoted by wt , is the time-bounded signal

positive real. An M -dimensional signal with a time hori-

wt : [0, T − t] → RN defined by wt (t′ ) := w(t + t′ ).

zon T is a function w : [0, T ] → R .
MLet w : [0, T ] → R|Var| be a signal, and φ be an

STL formula. We define the robustness Jw, φK ∈ R ∪model, and φ be an STL formula. A signal u : [0, T ] →{∞, −∞} as follows, by induction on the constructiond⊔of formulas. Here and denote infimums and supre-

R|Var| is a falsifying input if JM(u), φK < 0; the lattermums of real numbers, respectively. Their binary version

The use of quantitative robust semantics JM(u), φK ∈⊓ and ⊔ denote minimum and maximum.

R ∪ {∞, −∞} in the above problem enables the use of()
Jw, f (x1 , · · · , xn ) > 0K := f w(0)(x1 ), · · · , w(0)(xn )Jw, ⊥K := −∞Jw, ¬φK := −Jw, φK
Jw, φ1 ∧ φ2 K := Jw, φ1 K ⊓ Jw, φ2 K
(2)Jw, φ1 ∨ φ2 K := Jw, φ1 K ⊔ Jw, φ2 K
(3)
⊔ (
l
)
′
Jw, φ1 UI φ2 K :=Jwt , φ2 K ⊓Jwt , φ1 K

hill-climbing optimization.

t∈I∩[0,T ]t′ ∈[0,t)

For atomic formulas, Jw, f (⃗x) > cK stands for the vertical margin f (⃗x) − c for the signal w at time 0. A
negative robustness value indicates how far the formula
is from being true. It follows from the definition that

implies M(u) ̸|= φ.

Definition 6 (hill climbing-guided falsification) Assume
the setting in Def. 5. For finding a falsifying input, themethodology of hill climbing-guided falsification is presented in Algorithm 1.
Here the function H ILL -C LIMB makes a guess of an
input signal uk , aiming at minimizing the robustness
JM(uk ), φK. It does so, learning from the previous ob()
servations ul , JM(ul ), φK l∈[1,k−1] of input signals

the robustness for the eventually modality is given by⊔
Jw, 3[a,b] (x > 0)K = t∈[a,b]∩[0,T ] w(t)(x).

u1 , . . . , uk−1 and their corresponding robustness values

The above robustness notion taken from [12] is there-

The H ILL -C LIMB function can be implemented byfore spatial. Other robustness notions take temporal as-

various stochastic optimization algorithms. Examples

pects into account, too, such as “how long before theare CMA-ES [6] (used in our experiments), SA, anddeadline the required event occurs.” See e.g. [2, 12]. Our

GNM [30].

(cf. Table 1).

choice of spatial robustness in this paper is for the sakeof simplicity, and is thus not essential.
The original semantics of STL is Boolean, given as
usual by a binary relation |= between signals and formulas. The robust semantics refines the Boolean one
in the following sense: Jw, φK > 0 implies w |= φ,and Jw, φK < 0 implies w ̸|= φ, see [17, Prop. 16].
Optimization-based falsification via robust semantics
hinges on this refinement.

2. 2 Hill Climbing-Guided Falsification

Algorithm 1 Hill climbing-guided falsification
Require: a system model M, an STL formula φ, and a budgetK
1: function H ILL -C LIMB -FALSIFY(M, φ, K)
2:
rb ← ∞ ; k ← 0
3:while rb ≥ 0 and k ≤ K do
4:k ←k+1(())
5:
uk ← H ILL -C LIMB
ul , JM(ul ), φK l∈[1,k−1]
6:
rbk ← JM(uk ), φK
7:
if rbk < rb then8:rb ← rbk{
uk
if rb < 0, i.e., rbk = JM(uk ), φK < 09:u←
Failure otherwise
10:
return u

As we discussed in the introduction, the falsification
problem attracts growing industrial and academic attention. Its solution methodology by hill-climbing optimization is an established field, too: see [1, 3, 5, 9, 11–

3 Our Multi-Armed Bandit-Based Falsification Algorithm

13, 15, 26, 28, 34, 38] and the tools Breach [11] and S-

In this section, we present our contribution, namely a

TaLiRo [5]. We formulate the problem and the method-

falsification algorithm that addresses the scale problem

ology, for later use in describing our multi-armed bandit-

in Boolean superposition (see §1). The main novelties inbased algorithm.

the algorithm are as follows.

Definition 5 (falsifying input) Let M be a system

1. (Use of MAB algorithms) For binary Boolean con-

nectives, unlike most works in the field, we do notIn §3. 3–3. 4, we present two falsification algorithms,

superpose the robustness values of the constituent

for conjunctive and disjunctive safety properties respec-

formulas φ1 and φ2 using a fixed operator (such as

tively. For the reason we just discussed, we expect the⊓ and ⊔ in (2)). Instead, we view the situation as an

disjunctive algorithm should be more important in real-

instance of the multi-armed bandit problem (MAB):

world application scenarios. In fact, the disjunctive al-

we use an algorithm for MAB to choose one formula

gorithm turns out to be more complicated, and it is best

φi to focus on (here i ∈ {1, 2}); and then we apply

introduced as an extension of the conjunctive algorithm.

hill climbing-guided falsification to the chosen for-We define the restriction of robust semantics to amula φi .
2. (Hill-climbing gain as rewards in MAB) For our(sub)set of time instants. Note that we do not requireS ⊆ [0, T ] to be a single interval.

integration of MAB and hill-climbing optimization,

Definition 8 (Jw, ψKS , robustness restricted to S ⊆ [0, T ] )the technical challenge is find a suitable notion of

Let w : [0, T ] → R|Var| be a signal, ψ be an STL for-reward for MAB. We introduce a novel notion that

mula, and S ⊆ [0, T ] be a subset. We define the robust-

we call hill-climbing gain: it formulates the (downward) robustness gain that we would obtain by ap-

ness of w under ψ restricted to S bydJw, ψKS := t∈S Jwt , ψK .

plying hill-climbing optimization, suitably normal-

Obviously, Jw, ψKS < 0 implies that there exists t ∈ Sized using the scale of previous robustness values.

such that Jwt , ψKS < 0. We derive the following easy

(4)

Later, in §4, we demonstrate that combining those twolemma; it is used later in our algorithm.

features gives rise to falsification algorithms that success-Lemma 9 In the setting of Def. 8, consider a disjunctive

fully cope with the scale problem in Boolean superposi-

safety property φ ≡ 2I (φ1 ∨ φ2 ), and let S := {t ∈tion.

I ∩ [0, T ] | Jwt , φ1 K < 0}. Then Jw, φ2 KS < 0 implies

Our algorithms focus on a fragment of STL as target

Jw, 2I (φ1 ∨ φ2 )K < 0.

specifications. They are called (disjunctive and conjunctive) safety properties. In §3. 1 we describe this fragment

3. 2 The Multi-Armed Bandit (MAB) Problem

of STL, and introduce necessary adaptation of the se-

The multi-armed bandit (MAB) problem describes a

mantics. After reviewing the MAB problem in §3. 2, we

situation where,

present our algorithms in §3. 3–3. 4.

• a gambler sits in front of a row A1 , . . . , An of slot
machines;

3. 1 Conjunctive and Disjunctive Safety Properties• each slot machine Ai gives, when its arm is played(i.e. in each attempt), a reward according to a pre-Definition 7 (conjunctive/disjunctive safety property)

scribed (but unknown) probability distribution µi ;An STL formula of the form 2I (φ1 ∧ φ2 ) is called a• and the goal is to maximize the cumulative reward

conjunctive safety property; an STL formula of the form

after a number of attempts, playing a suitable arm in

2I (φ1 ∨ φ2 ) is called a disjunctive safety property.

each attempt.

It is known that, in industry practice, a majority of

The best strategy of course is to keep playing the best

specifications is of the form 2I (φ1 → φ2 ), wherearm Amax , i.e. the one whose average reward avg(µmax )φ1 describes a trigger and φ2 describes a countermea-

is the greatest. This best strategy is infeasible, however,sure that should follow. This property is equivalent tosince the distributions µ1 , . . . , µn are initially unknown.

2I (¬φ1 ∨ φ2 ), and is therefore a disjunctive safety prop-

Therefore the gambler must learn about µ1 , . . . , µnerty.

through attempts.

The MAB problem exemplifies the “learning by try-rew1 rew2 . . . rewk ) is given by the number of occur-ing” paradigm of reinforcement learning, and is thus

rences of Aj in Ai1 Ai2 . . . Aik . Its empirical average re-heavily studied. The greatest challenge is to balance
between exploration and exploitation. A greedy (i.e.

ward R(j, Ai1 Ai2 . . . Aik , rew1 rew2 . . . rewk ) is given∑by l∈{l∈[1,k]|il =j} rewl , i.e. the average return of the

exploitation-only) strategy will play the arm whose em-

arm Aj in the history. When the history is obvious frompirical average reward is the maximum. However, since

the context, we simply write N (j, k) and R(j, k).

the rewards are random, this way the gambler can miss3. 2. 1 MAB Algorithms

another arm whose real performance is even better but

There have been a number of algorithms proposed forwhich is yet to be found so. Therefore one needs to mix

the MAB problem; each of them gives a strategy (also

exploration, too, occasionally trying empirically non-called a policy) that tells which arm to play, based on

optimal arms, in order to identity their true performance.

the previous attempts and their rewards. The focus here

The relevance of MAB to our current problem is as fol-is how to resolve the exploration-exploitation trade-off.

lows. Falsifying a conjunctive safety property 2I (φ1 ∧Here we review two well-known algorithms.

φ2 ) amounts to finding a time instant t ∈ I at which ei-

3. 2. 1. 1 The ε-Greedy Algorithm

ther φ1 or φ2 is falsified. We can see the two subformulasThis is a simple algorithm that spares a small fraction ε(φ1 and φ2 ) as two arms, and this constitutes an instanceof chances for empirically non-optimal arms. The sparedof the MAB problem. In particular, playing an arm trans-

probability ε is uniformly distributed. See Algorithm 2.

lates to a falsification attempt by hill climbing, and collecting rewards translates to spending time to minimize
the robustness. We show in §3. 3–3. 4 that this basic idea
extends to disjunctive safety properties 2I (φ1 ∨φ2 ), too.
A rigorous formulation of the MAB problem is presented for the record.
Definition 10 (the multi-armed bandit problem) The
multi-armed bandit (MAB) problem is formulated as follows.

Algorithm 2 The ε-greedy algorithm for MAB
Require: the setting of Def. 10, and a constant ε > 0 (typicallyvery small)At the k-th attempt, choose the arm Aik as follows
1: jemp-opt ← arg max R(j, k − 1)
▷ the arm that isj∈[1,n]empirically optimal
2: Sample
ik ∈ [1, n] from the distribution[]εjemp-opt 7−→ (1 − ε) + nε
j 7−→ nfor each j ∈ [1, n] \ {jemp-opt }3: return ik

Input: arms (A1 , . . . , An ), the associated probability
distributions µ1 , . . . , µn over R, and a time horizon H ∈3. 2. 1. 2 The UCB1 Algorithm
The UCB1 (upper confidence bound) algorithm is

N ∪ {∞}.
Goal: synthesize a sequence Ai1 Ai2 . . . AiH , so that the∑
cumulative reward H
k=1 rewk is maximized. Here themore complex; it comes with a theoretical upper boundreward rewk of the k-th attempt is sampled from the dis-

tive reward and the optimal (but infeasible) cumulative

tribution µik associated with the arm Aik played at the

reward (i.e. the result of keep playing the optimal arm

k-th attempt.
LetAmax ). It is known that the UCB1 algorithm’s regret√
is at most O( nH log H) after H attempts, improving(Ai1 . . . Aik , rew1 . . . rewk ) be a history, i.e. the se-

the naive random strategy (which has the expected regret

quence of arms played so far (here i1 , . . . , ik ∈ [1, n]),O(H)).

We introduce some notations for later use.

and the sequence of rewards obtained by those attempts(rewl is sampled from µil ).
For an arm Aj , its visit count N (j, Ai1 Ai2 . . . Aik ,for regrets, i.e. the gap between the expected cumula-

See Alg. 3. The algorithm is deterministic, and picks
the arm that maximizes the value shown in Line 1. The
first term R(j, k − 1) is the exploitation factor, reflecting

the arm’s empirical performance. The second term is the

Algorithm 5 Our MAB-guided algorithm II: disjunctive

exploration factor. Note that it is bigger if the arm Aj

safety properties

has been played less frequently. Note also that the explo-

Require: a system model M, an STL formula φ ≡ 2I (φ1 ∨φ2 ), and a budget K
1: function MAB-FALSIFY-D ISJ -S AFETY(M, φ, K)
The same as Algorithm 4, except that Line 7 is replaced by
the following Line 7’.
{7’:
rbk ← JM(uk ), φik KSk
where Sk =t ∈}t
I ∩ [0, T ] JM(uk ), φi K < 0k▷ here φi denotes the other formula than φik , amongk
φ1 , φ2

ration factor eventually decays over time: the denominator grows roughly with O(k), while the numerator grows
with O(ln k).
Algorithm 3 The UCB1 algorithm for MAB
Require: the setting of Def. 10, and a constant c > 0
At the k-th attempt,
Aik as follows( choose the arm√)
1: ik ← arg max R(j, k − 1) + c
j∈[1,n]2 ln(k−1)
N (j,k−1)

The algorithm is in Algorithm 4. Some remarks are in

2: return ik

order.
3. 3 Our MAB-Guided Algorithm I: Conjunctive
Safety Properties
Our first algorithm targets at conjunctive safety properties. It is based on our identification of MAB in a
Boolean conjunction in falsification—this is as we discussed just above Def. 10. The technical novelty lies in
the way we combine MAB algorithms and hill-climbing
optimization; specifically, we introduce the notion of hillclimbing gain as a reward notion in MAB (Def. 11). This
first algorithm paves the way to the one for disjunctive

Algorithm 4 aims to falsify a conjunctive safety property φ ≡ 2I (φ1 ∧ φ2 ). Its overall structure is to interleave two sequences of falsification attempts, both ofwhich are hill climbing-guided. These two sequencesof attempts aim to falsify 2I φ1 and 2I φ2 , respectively.
Note that JM(u), φK ≤ JM(u), 2I φ1 K, therefore falsification of 2I φ1 implies falsification of φ; the same
holds for 2I φ2 , too.
In Line 5 we run an MAB algorithm to decide whichof 2I φ1 and 2I φ2 to target at in the k-th attempt. The
function MAB takes the following as its arguments: 1)

safety properties, too (§3. 4).

the list of arms, given by the formulas φ1 , φ2 ; 2) their
Algorithm 4 Our MAB-guided algorithm I: conjunctive

rewards R(φ1 ), R(φ2 ); 3) the history φi1 . . . φik−1 ofsafety properties

previously played arms (il ∈ {1, 2}); and 4) the history

Require: a system model M, an STL formula φ ≡ 2I (φ1 ∧φ2 ), and a budget K
1: function MAB-FALSIFY-C ONJ -S AFETY(M, φ, K)
2:
rb ← ∞ ; k ← 0

rew1 . . . rewk−1 of previously observed rewards. This

3:
4:
5:

while rb ≥ 0 and k ≤ K dok ←k+1 (()
ik ← MAB (φ1 , φ2 ), R(φ1 ), R(φ2 ) ,6:

φi1 . . . φik−1 , rew1 . . . rewk−1(())
uk ← H ILL -C LIMB
(ul , rbl )where l ∈ [1, k − 1] such that il = ik

7:
8:
9:
10:
11:

rbk ← JM(uk ), 2I φik K
if rbk < rb thenrb ← rbk{
uk
if rb < 0u←
Failure otherwise
return uway, the type of the MAB function in Line 5 matches theformat in Def. 10, and thus the function can be instantiated with any MAB algorithm such as Algorithms 2–3.
The only missing piece is the definition of the rewards)

R(φ1 ), R(φ2 ). We introduce the following notion, tailored for combining MAB and hill climbing.
Definition 11 (hill-climbing gain) In Algorithm 4, inLine 5, the reward R(φi ) of the arm φi (where i ∈{1, 2}) is defined by

R(φi ) = max-rb(i,k−1)−last-rb(i,k−1)
max-rb(i,k−1)0

if φi was played

otherwise
Here max-rb(i, k − 1) := max{rbl | l ∈ [1, k −1], il = i} (i.e. the greatest rbl so far, in those attempts

lieve this problem setting is even more important than thewhere φi was played), and last-rb(i, k − 1) := rbllast

conjunctive case, since it encompasses conditional safetywith llast being the greatest l ∈ [1, k − 1] such that il = iproperties (i.e. of the form 2I (φ1 → φ2 )). See §3. 1 for(i.e. the last rbl for φi ).

discussions.

Since we try to minimize the robustness values rbl

In the disjunctive setting, the challenge is that falsifi-

through falsification attempts, we can expect that rbl for acation of 2I φi (with i ∈ {1, 2}) does not necessarily

fixed arm φi decreases over time. (In the case of the hill-

imply falsification of 2I (φ1 ∨ φ2 ). This is unlike theclimbing algorithm CMA-ES that we use, this is in fact

conjunctive setting. Therefore we need some adaptation

guaranteed). Therefore the value max-rb(i, k − 1) in theof Algorithm 4, so that the two interleaved sequences ofdefinition of R(φi ) is the first observed robustness value.

falsification attempts for φ1 and φ2 are not totally inde-

The numerator max-rb(i, k − 1) − last-rb(i, k − 1) thenpendent of each other. Our solution consists of restricting

represents how much robustness we have reduced so far

time instants to those where φ2 is false, in a falsification

by hill climbing—hence the name “hill-climbing gain.”attempt for φ1 (and vice versa), in the way described in

The denominator max-rb(i, k − 1) is there for normal-

Def. 8.
Algorithm 5 shows our MAB-guided algorithm for fal-ization.
In Algorithm 4, the value rbk is given by the robust-sifying a disjunctive safety property 2I (φ1 ∨ φ2 ). The

ness JM(uk ), 2I φik K. Therefore the MAB choice in

only visible difference is that Line 7 in Algorithm 4 isLine 5 essentially picks ik for which hill climbing yields

replaced with Line 7’. The new Line 7’ measures thegreater effect (but also taking exploration into account—quality of the suggested input signal uk in the way re-see §3. 2).

stricted to the region Sk in which the other formula is al-

In Line 6 we conduct hill-climbing optimization—

ready falsified. Lem. 9 guarantees that, if rbk < 0, thensee §2. 2. The function H ILL -C LIMB learns from the pre-indeed the input signal uk falsifies the original specifica-

vious attempts ul1 , . . . , ulm regarding the same formulation 2I (φ1 ∨ φ2 ).

φik , and their resulting robustness values rbl1 , . . . , rblm .

The assumption that makes Alg. 5 sensible is that, al-Then it suggests the next input signal uk that is likely tothough it can be hard to find a time instant at which

minimize the (unknown) function that underlies the cor[]
respondences ulj 7→ rblj j∈[1,m] .

both φ1 and φ2 are false (this is required in falsifying
2I (φ1 ∨ φ2 )), falsifying φ1 (or φ2 ) individually is not

Lines 6–8 read as follows: the hill-climbing algorithm

hard. Without this assumption, the region Sk in Line 7’

suggests a single input uk , which is then selected or re-would be empty most of the time. Our experiments in §4

jected (Line 8) based on the robustness value it yields

demonstrate that this assumption is valid in many prob-(Line 7). We note that this is a simplified picture: inlem instances, and that Alg. 5 is effective.

our implementation that uses CMA-ES (it is an evolutionary algorithm), we maintain a population of some ten

4 Experimental Evaluation

particles, and each of them is moved multiple times (ourWe name MAB-UCB and MAB-ϵ-greedy the two ver-choice is three times) before the best one is chosen as uk .

sions of MAB algorithm using strategies ε-Greedy (seeAlg. 2) and UCB1 (see Alg. 3). We compared the pro-

3. 4 Our MAB-Guided Algorithm II: Disjunctive
Safety Properties
The other main algorithm of ours aims to falsify a disjunctive safety property φ ≡ 2I (φ1 ∨ φ2 ). We be-posed approach (both versions MAB-UCB and MAB-ϵ-greedy) with a state-of-the-art falsification framework, namely Breach [11].

Breach encapsulates

several hill-climbing optimization algorithms, including

CMA-ES (covariance matrix adaptation evolution strat-

tain specifications of different complexity, we artificiallyegy) [6], SA (simulated annealing), GNM (global Nelder-modified a constant (turned into a parameter named τ if

Mead) [30], etc. According to our experience, CMA-ES

it is contained in a time interval, named ρ otherwise) ofoutperforms other hill-climbing solvers in Breach, so

the specification: for each specification S, we generated

the experiments for both Breach and our approach rely

m different versions, named as Si with i ∈ {1, . . . , m};on the CMA-ES solver.
Experiments have been executed using Breach 1.2.13

the complexity of the specification (in terms of difficulty
to falsify it) increases with increasing i.†2 In total, weon an Amazon EC2 c4.large instance, 2.9 GHz Intel Xeon

produced 60 specifications. Column parameter in the ta-

E5-2666, 2 virtual CPU cores, 4 GB RAM.

ble shows which concrete values we used for the param-

Benchmarks

eters ρ and τ . Note that all the specifications but one are

We selected three benchmark models from the lit-

disjunctive safety properties (i.e., 2I (φ1 ∨ φ2 )), as theyerature, each one having different specifications. The

are the most difficult case and they are the main target offirst one is the Automatic Transmission (AT) model [16,our approach; we just add AT5 as example of conjunctive

24].

It has two input signals, throttle∈[0, 100] andsafety property (i.e., 2I (φ1 ∧ φ2 )).

brake∈[0, 325], and computes the car’s speed , engine

Our approach has been proposed with the aim of tack-rotation in rounds per minute rpm, and the automati-ling the scale problem. Therefore, to better show how ourcally selected gear . The specifications concern the re-approach mitigates this problem, we generated a second

lation between the three output signals to check whether

benchmark set Sbench as follows. We selected 15 spec-

the car is subject to some unexpected or unsafe behav-

ifications from Bbench (with concrete values for the pa-

iors. The second benchmark is the Abstract Fuel Control

rameters) and, for each specification S, we changed the(AFC) model [16, 25]. It takes two input signals, pedal

corresponding Simulink model by multiplying one of its

angle∈[8.8, 90] and engine speed∈[900, 1100], and out-

outputs by a factor 10k , with k ∈ {−2, 0, 1, 2, 3} (noteputs the critical signal air-fuel ratio (AF ), which influ-

that we also include the original one using scale factor

ences fuel efficiency and car performance. The value100 ); the specification has been modified accordingly, by

is expected to be close to a reference value AFref ;multiplying with the scale factor the constants that are

mu≡|AF −AFref |/AFrefis the deviation of AF fromcompared with the scaled output. We name a specifica-

The specifications check whether this prop-

tion S scaled with factor 10k as S k . Table 2b reports theerty holds under both normal mode and power enrich-

IDs of the original specifications, the output that has been

ment mode. The third benchmark is a model of a mag-scaled, and the used scaled factors; in total, the bench-

netic levitation system with a NARMA-L2 neurocontroller

mark set Sbench contains 60 specifications .

(NN) [7,16]. It takes one input signal, Ref ∈[1, 3], which

Experiment In our context, an experiment consists in theis the reference for the output signal Pos, the position of

execution of an approach A (either Breach, MAB-ϵ--a magnet suspended above an electromagnet. The spec-

greedy, or MAB-UCB) over a specification S for 30 tri-

ifications say that the position should approach the ref-als, using different initial seeds. For each experiment, we

erence signal in a few seconds when these two are notrecord the success SR as the number of trials in whichclose.

a falsifying input was found, and average execution time

AFref .

We built the benchmark set Bbench, as shown in Ta-of the trials. Complete experimental results are reported

ble 2a that reports the name of the model and its specifications (ID and formula). In total, we found 11 specifications. In order to increase the benchmark set and ob-†2 Note that we performed this classification based on thefalsification results of Breach.

表 2: Benchmark sets Bbench and Sbench(b) Sbench(a) Bbench (here δt′ (w) represents wt (t′ ) − wt (0)).
Spec ID scaled

Bench

AT

AFC

Specification

Parameter

ID

FormulaAT1

2[0,30] ((gear = 3) → (speed > ρ))ρ ∈ {20.6, 20.4, 20.2, 20, 19.8}

AT12

AT2

2[0,30] ((gear = 4) → (speed > ρ))ρ ∈ {43, 41, 39, 37, 35}

AT13ρ ∈ {700, 800, 900, 1000, 1100}

AT14

AT11

AT3

2[0,30] ((gear = 4) → (rpm > ρ))AT4

2[0,30−τ ] ((δ10 (rpm) > 2000) → (δτ (gear ) > 0)) τ ∈ {15, 16, 17, 18, 19}

AT15

AT5

2[0,30] ((speed < ρ) ∧ (RP M < 4780))

ρ ∈ {130, 131, 132, 133, 134, 135, 136, 137}

AT54

AT6

2[0,26] ((δ4 (speed ) > ρ) → (δ4 (gear ) > 0))ρ ∈ {20, 25, 30, 35, 40}

AT55

AT7

2[0,30−τ ] ((δτ (speed ) > 30) → (δτ (gear ) > 0))τ ∈ {2, 3, 4, 5, 6, 7, 8}

AT56

AFC1 2[11,50] ((controller mode = 0) → (mu < ρ))ρ ∈ {0.16, 0.17, 0.18, 0.19, 0.2}

AT57

AFC2 2[11,50] ((controller mode = 1) → (mu < ρ))ρ ∈ {0.222, 0.224, 0.226, 0.228, 0.23}

close ≡ |P os − Ref | <= ρ + α ∗ |Ref |speed k ∈{-2,0,1,3}

speed k ∈{-2,0,1,3}

AT58
AFC11

reach ≡ 3[0,2] (2[0,1] (close))NNfactor 10k

outputAFC12

NN1 2[0,18] (¬close → reach), α = 0.04

ρ ∈ {0.001, 0.002, 0.003, 0.004, 0.005}

AFC13

NN1 2[0,18] (¬close → reach), α = 0.03

ρ ∈ {0.001, 0.002, 0.003, 0.004, 0.005}

AFC14

mu

k ∈{0,1,2,3}

AFC15

in Appendix A in the extended version [37]†3 . We re-significance†5 [35]; the null hypothesis is that there is noport aggregated results in Table 3. For benchmark set

difference in applying A1 A2 in terms of the compared

Bbench, it reports aggregated results for each group of

measure (SR or time).

specifications obtained from S (i.e., all the different versions Si obtained by changing the value of the parame-

4. 1 Evaluationter); for benchmark set Sbench, instead, results are ag-

We evaluate the proposed approach with some researchkgregated for each scaled specification S (considering thequestions.

versions Sik obtained by changing the parameter value).
We report minimum, maximum and average number of

RQ1 Which is the best MAB algorithm for our purpose?

successes SR, and time in seconds. For MAB-ϵ-greedy

In § 3. 2, we described that the proposed approach canand MAB-UCB, both for SR and time, we also report the
average percentage difference†4 (∆) w.r.t. to the corre-

be executed using two different strategies for choosing

sponding value of Breach.
Comparison In the following, we compare two

the arm in the MAB problem, namely MAB-ϵ-greedy
and MAB-UCB. We here assess which one is better interms of SR and time. From the results in Table 3,

approaches A1 , A2 ∈ {Breach, MAB-ϵ-greedy,

it seems that MAB-UCB provides slightly better perfor-

MAB-UCB } by comparing the number of their suc-mance in terms of SR; this has been confirmed by thecesses SR and average execution time using the nonparametric Wilcoxon signed-rank test with 5% level of

Wilcoxon test applied over all the experiments (i.e., on
the non-aggregated data reported in Appendix A in theextended version [37]): the null hypothesis that using†3 The code, models, and specifications are available online
at https://github.com/ERATOMMSD/FalStar-MAB.
†4 ∆=((m−b)∗100)/(0.5∗(m+b)) where m is the result of
MAB and b the one of Breach.

anyone of the two strategies has no impact on SR is†5 We checked that the distributions are not normal with thenon-parametric Shapiro-Wilk test.

表 3: Aggregated results for benchmark sets Bbench and Sbench (SR: # successes out 30 trials. Time in secs. ∆:percentage difference w.r.t. Breach). Outperformance cases are highlighted, indicated by positive ∆ of SR, andnegative ∆ of time.
Spec.
ID

BreachSR (/30)

MAB-ϵ-greedy

time (sec.)

MAB-UCB

SR (/30)

time (sec.)

SR (/30)

time (sec.)

Min Max Avg Min Max Avg Min Max Avg∆ Min Max Avg∆ Min Max Avg∆ Min Max Avg

∆
−97.1

AT1

14

25 20.2

125 361.2 223.1

24

30 28.6

35.7 62.7 213.4 106.4

−73.4

28

30 29.2

37.8 45.1 146.8 77.4

AT2

11

30 20.2

14 390.6 209.8

30

30

30

43.9 11.9 126.3 54.5

−96.9

27

30 29.4

42.2 17.7 92.5 36.8 −112.1

AT3

29

30 29.4

2.3 22.2 14.2

30

30

30

2

2.5

3.5

−82.9

30

30

30

2

AT4

18

30 25.8 19.5 265.3 109.6

29

30 29.816

7.8 45.1 24.4

−105

30

30

30

16.6

AT5

6

23 14.1 203.1 525.9 366.2

26

30 28.5

149 93.7 −120.6

26

30 28.2

71.4 37.7 154.1 99.2 −116.8

AT65

29 22.8 30.1 509.5

157

21

30

27

28

2.3

300 95.1

−98.3

22

30

27

27.7

2.9 247.3 86.1

−99.4

AT7

15

30 26.6 12.2

314 81.520

30 28.6

8.4

2.9 283.9 49.9

−92

23

30

29

10.3

5.5 223.3 42.9

−88.3

AFC1

6

30 14.4 124.8 565.6 413.5

4

28

12 −28.4

171 568.4

446

10.8

5

30 16.4

9.7 98.7 559.8 389.9

−9.3

AFC2

2

30

18 80.7 582.3 343.4

5

30

20

23.8 43.2 547.8 301.9

−23.8

5

30

20

22.9 59.4 568.4 320.5

−11.1

NN1

17

25 20.8 212.9 384.7 292.9

14

27 20.2 −4.5 189.5 422.8 320.3

6.2

17

28 22.6

7.3 148.2 403.3 272.3

−11.8

NN2

27

28 27.2 55.5 93.4 73.1

30

30

30

11 39.3 26.3

−97.8

30

30

9.8 14.6 38.2 27.4

−92.3

AT1−2

30

30

28

30

29 −3.4 75.6 178.3 118.7

68.7

28

30 29.4 −2.1 54.3 136.3 80.3

33.3

30 42.5 97.4 56.9

72.1 35.2

9.8

7

30

2.5

3.6

3

−88.6

6.2 36.2 22.2 −113.5

0

AT1

14

25 20.2

125 361.2 223.1

24

30 28.6

35.7 62.7 213.4 106.4

−73.4

28

30 29.2

37.8 45.1 146.8 77.4

AT11

4

21 15.4 204.5 527.6 310.2

25

30

68.4

49 234.7 102.1

−108

27

29 28.2

64.5 77.5 128.7 105.1

−93

AT13

8

24 19.829

30 29.8

44.6 67.5 170.6 101.9

−77.3

29

30 29.4

43.4 55.4 104.8 80.6

−93.6

AT5−2

29

30 29.6 61.1 163.7

102

25

30 27.8 −6.4 76.9 139.5 111.9

12.6

28

30 29.4 −0.7 48.5 131.9 85.7

−17

AT50

6

18 11.2 291.1 525.9 423.1

28

30 28.4

90.5 80.2 151.3 107.4 −117.7

26

30

AT51

0

2 0.4 566.4

600 593.3

27

30 28.4 194.8 70.7 184.5 110.3 −138.525

30 27.6 194.1 83.1

AT53

0

1 0.2 586.4

600 597.3

27

30 28.6 197.2 66.8 163.3 102.5 −142.3

27

29

AFC10

6

30 14.4 124.8 565.6 413.5

4

29 16.4

8.5 115.1 559.9 411.1

−2.8

5

30 16.4

9.7 98.7 559.8 389.9

−9.3

AFC11

7

30 16.6

3

29 10.8 −60.9 198.1 587.6 465.8

24.6

7

29 17.8

10.3 105.7 527.3 354.3

−10.3

AFC12

0

12 5.2 434.4

600 535.8

3

28 11.6

96.2 180.8 577.6

463

−20.7

4

30

17

127 73.7 556.3 374.5

−47.3

AFC13

1

12 4.8 425.7 587.4 532.6

3

30 14.4

109

138 585.5 436.5

−28

7

30

15

113 77.1 553.4 403.7−39.9

164 471.7 240.1

99 548.2 393.3

29

28

−97.1

89.4 68.3 154.1 114.9 −114.5
150 123.7 −131.2

28 197.2 80.4 160.9 111.9 −137.4

rejected with p-value equal to 0.005089, and the alter-for each specification S, all its scaled versions are re-native hypothesis that SR is better is accepted with p-

ported in increasing order of the scaling factor. We ob-value=0.9975; in a similar way, the null hypothesis thatserve that changing the scaling factor affects (sometimes

there is no difference in terms of time is rejected withgreatly) the number of successes SR of Breach; for ex-

p-value equal to 3.495e-06, and the alternative hypothe-

ample, for AT55 and AT57 it goes from 30 to 0. For

sis that is MAB-UCB is faster is accepted with p-value=1.

MAB-UCB, instead, SR is similar across the scaled ver-Therefore, in the following RQs, we compare Breachsions of each specification: this shows that the approachwith only the MAB-UCB version of our approach.

is robust w.r.t. to the scale problem as the “hill-climbing

RQ2 Does the proposed approach effectively solve thegain” reward in Def. 11 eliminates the impact of scal-

scale problem?

ing and UCB1 algorithm balances the exploration and ex-

We here assess if our approach is effective in tackling
the scale problem. Table 4 reports the complete experimental results over Sbench for Breach and MAB-UCB;

ploitation of two sub-formulas. The observation is confirmed by the Wilcoxon test over SR: the null hypothesis
is rejected with p-value=1.808e-09, and the alternative表 4: Experimental results – Sbench (SR: # successes out of 30 trials. Time in secs)
Spec.

Breach

MAB-UCBSpec.

Breach

MAB-UCBSpec.

Breach

ID

SR

time

SR

time

ID

SR

time

SR

time

ID

SR

time

SR

time

(/30)

(sec.)(/30)(sec.)(/30)(sec.)(/30)(sec.)(/30)(sec.)(/30)(sec.)

AT1−2
1

30

51.3

30

54.3

AT5−2
4

30

61.1

30

48.5

AFC10
1

30

124.8

30

98.7

AT10
1

25

125

29

75

AT50
4

18

291.1

28

94.5

AFC11
1

30

99

29

105.7

AT11
1

20

221.1

28

107.9

AT51
4

2

566.4

25

150

AFC12
1

12

434.4

30

73.7

AT53
4
AT5−2
5
AT50
5
AT51
5
AT53
5
AT5−2
6
AT50
6
AT51
6
AT53
6
AT5−2
7
AT50
7
AT51
7
AT53
7
AT5−2
8
AT50
8
AT51
8
AT53
8

1

586.4

28

96.2

AFC13
1

12

425.7

30

77.1

30

71.3

29

67.8

AFC10
2

16

421.5

23

346.8

15

369.1

27

114

AFC11
2

25

345.9

27

227.9

0

600

29

83.1

AFC12
2

8

497.2

25

320.5

0

600

27

113.8

AFC13
2

5

518.1

21

364

29

110.2

28

103.3

AFC10
3

11

457.7

15

442

10

438.2

30

68.3

AFC11
3

13

479.2

14

455.5

0

600

27

126.7

AFC12
3

2

590.7

15

453.2

0

600

29

80.4

AFC13
3

5

545.6

8

510.6

30

103.6

30

77.3

AFC10
4

9

498.2

9

502.1

7

491.4

26

154.1

AFC11
4

8

494

12

455

0

600

27

134.3

AFC12
4

4

556.8

11

468.7

0

600

29

108

AFC13
4

1

587.4

9

513.4

29

163.7

30

131.9

AFC10
5

6

565.6

5

559.8

6

525.9

29

143.6

AFC11
5

7

548.2

7

527.3

0

600

30

124.2

AFC12
5

0

600

4

556.3

0

600

27

160.9

AFC13
5

1

586

7

553.4

AT13
1
AT1−2
2
AT10
2
AT11
2
AT13
2
AT1−2
3
AT10
3
AT11
3
AT13
3
AT1−2
4
AT10
4
AT11
4
AT13
4
AT1−2
5
AT10
5
AT11
5
AT13
5

23

170

29

55.4

30

49

29

67.5

22

187.5

30

45.1

21

204.5

29

77.5

24

164

30

61

30

42.5

30

62.4

19

239.5

29

62.5

16

296.2

27

128.7

21

209.8

30

93.4

30

44.5

30

80.8

21

202.2

30

57.4

16

301.7

28

119.5

23

185.1

29

88.3

30

97.4

28

136.3

14

361.2

28

146.8

4

527.6

29

91.9

8

471.7

29

104.8

MAB-UCBhypothesis accepted with p-value=1. Instead, the null hy-

used with any kind of specification.

pothesis that there is no difference in terms of time cannot

RQ4 Is the proposed approach more effective than an

be rejected with p-value=0.3294.

approach based on rescaling?

RQ3 How does the proposed process behave with notscaled benchmarks?

A naı̈ve solution to the scale problem could be torescale the signals used in specification at the same scale.

In RQ2, we checked whether the proposed approach

Thanks to the results of RQ2, we can compare to this pos-is able to tackle the scale problem for which it has beensible baseline approach, using the scaled benchmark set

designed. Here, instead, we are interested in investigat-

Sbench. For example, AT5 suffers from the scale prob-

ing how it behaves on specifications that have not been

lem as speed is one order of magnitude less than rpm.

artificially scaled (i.e., those in Bbench). From Table 3

However, from Table 3, we observe that the scaling that(upper part), we observe that MAB-UCB is always bet-

would be done by the baseline approach (i.e., runningter than Breach both in terms of SR and time, which

Breach over AT51 ) is not effective, as SR is 0.4/30, thatis shown by the highlighted cases. This is confirmed byis much lower than the original SR 14.1/30 of the un-

Wilcoxon test over SR and time: null hypotheses are re-scaled approach using Breach. Our approach, instead,

jected with p-values equal to, respectively, 6.02e-08 andraises SR to 28.4/30 and to 27.6/30 using the two pro-

1.41e-08, and the alternative hypotheses that MAB-UCB

posed versions. By monitoring Breach execution, we

is better are both accepted with p-value=1. This means

notice that the naı̈ve approach fails because it tries to fal-that the proposed approach can also handle specifications

sify rpm<4780, which, however, is not falsifiable; ourthat do not suffer from the scale problem, and so it can beapproach, instead, understands that it must try to falsify

speed <ρ. More details are given in the extended version [37].

5 Conclusion and Future work
In this paper, we propose a solution to the scale problem that affects falsification of specifications containing
Boolean connectives.

The approach combines multi-

armed bandit algorithms with hill climbing-guided falsification. Experiments show that the approach is robust
under the change of scales, and it outperforms a state-ofthe-art falsification tool. The approach currently handles
binary specifications. As future work, we plan to generalize it to complex specifications having more than two
Boolean connectives.
謝辞 The authors are supported by ERATO HASUOMetamathematics for Systems Design Project (No. JPMJER1603), JST.
参考文献
[ 1 ] Adimoolam, A., Dang, T., Donzé, A., Kapinski, J., andJin, X.: Classification and Coverage-Based Falsification for
Embedded Control Systems, Computer Aided Verification,
Cham, Springer International Publishing, 2017, pp. 483–
503.
[ 2 ] Akazaki, T. and Hasuo, I.: Time Robustness in MTL
and Expressivity in Hybrid System Falsification, Computer
Aided Verification, Cham, Springer International Publishing, 2015, pp. 356–374.
[ 3 ] Akazaki, T., Kumazawa, Y., and Hasuo, I.: CausalityAided Falsification, Proceedings First Workshop on Formal Verification of Autonomous Vehicles, FVAV@iFM 2017,
Turin, Italy, 19th September 2017., EPTCS, Vol. 257, 2017,
pp. 3–18.
[ 4 ] Akazaki, T., Liu, S., Yamagata, Y., Duan, Y., and Hao,
J.: Falsification of Cyber-Physical Systems Using Deep
Reinforcement Learning, Formal Methods - 22nd International Symposium, FM 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 1517, 2018, Proceedings, Havelund, K., Peleska, J., Roscoe,B., and de Vink, E. P.(eds.), Lecture Notes in Computer Science, Vol. 10951, Springer, 2018, pp. 456–465.
[ 5 ] Annpureddy, Y., Liu, C., Fainekos, G., and Sankaranarayanan, S.: S-TaLiRo: A Tool for Temporal Logic Falsification for Hybrid Systems, Springer, 2011, pp. 254–257.
[ 6 ] Auger, A. and Hansen, N.: A restart CMA evolution
strategy with increasing population size, Proceedings of theIEEE Congress on Evolutionary Computation, CEC 2005,
IEEE, 2005, pp. 1769–1776.
[ 7 ] Beale, M. H., Hagan, M. T., and Demuth, H. B.: Neu-ral Network ToolboxTM User’s Guide, The Mathworks Inc,
(1992).
[ 8 ] Chen, X., Ábrahám, E., and Sankaranarayanan, S.:
Flow*: An Analyzer for Non-linear Hybrid Systems,
Computer Aided Verification, Berlin, Heidelberg, Springer
Berlin Heidelberg, 2013, pp. 258–263.
[ 9 ] Deshmukh, J., Jin, X., Kapinski, J., and Maler, O.:
Stochastic Local Search for Falsification of Hybrid Systems, Automated Technology for Verification and Analysis,
Cham, Springer International Publishing, 2015, pp. 500–517.
[10] Dokhanchi, A., Yaghoubi, S., Hoxha, B., and Fainekos,
G. E.: Vacuity aware falsification for MTL request-response
specifications, 13th IEEE Conference on Automation Science and Engineering, CASE 2017, Xi’an, China, August
20-23, 2017, IEEE, 2017, pp. 1332–1337.
[11] Donzé, A.: Breach, A Toolbox for Verification and Parameter Synthesis of Hybrid Systems, Computer Aided Verification, 22nd Int. Conf., CAV 2010, LNCS, Vol. 6174,
Springer, 2010, pp. 167–170.
[12] Donzé, A. and Maler, O.: Robust Satisfaction of Temporal Logic over Real-Valued Signals, Formal Modeling andAnalysis of Timed Systems - 8th Int. Conf., FORMATS 2010,
LNCS, Vol. 6246, Springer, 2010, pp. 92–106.
[13] Dreossi, T., Dang, T., Donzé, A., Kapinski, J., Jin,X., and Deshmukh, J. V.: Efficient Guiding Strategies for
Testing of Temporal Properties of Hybrid Systems, NASA
Formal Methods, Cham, Springer International Publishing,
2015, pp. 127–142.
[14] Dreossi, T., Dang, T., and Piazza, C.: Parallelotope Bundles for Polynomial Reachability, Proc. of the 19th International Conference on Hybrid Systems: Computation andControl, HSCC ’16, New York, NY, USA, ACM, 2016,
pp. 297–306.
[15] Dreossi, T., Donzé, A., and Seshia, S. A.: Compositional Falsification of Cyber-Physical Systems with
Machine Learning Components, NASA Formal Methods,
Cham, Springer International Publishing, 2017, pp. 357–
372.
[16] Ernst, G., Arcaini, P., Donzé, A., Fainekos, G., Mathesen, L., Pedrielli, G., Yaghoubi, S., Yamagata, Y., andZhang, Z.: ARCH-COMP 2019 Category Report: Falsification, ARCH19. 6th International Workshop on Applied
Verification of Continuous and Hybrid Systems, Frehse, G.
and Althoff, M.(eds.), EPiC Series in Computing, Vol. 61,
EasyChair, 2019, pp. 129–140.
[17] Fainekos, G. E. and Pappas, G. J.: Robustness of temporal logic specifications for continuous-time signals, Theor.
Comput. Sci., Vol. 410, No. 42(2009), pp. 4262–4291.
[18] Fan, C., Qi, B., Mitra, S., Viswanathan, M., and Duggirala, P. S.: Automatic Reachability Analysis for Nonlinear
Hybrid Models with C2E2, Computer Aided Verification,
Cham, Springer International Publishing, 2016, pp. 531–
538.
[19] Ferrère, T., Nickovic, D., Donzé, A., Ito, H., and Kapinski, 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., Ozay, N. and Prabhakar,
P.(eds.), ACM, 2019, pp. 57–66.
[20] Frehse, G., Le Guernic, C., Donzé, A., Cotton, S.,
Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T.,
and Maler, O.: SpaceEx: Scalable Verification of Hybrid
Systems, Computer Aided Verification, Berlin, Heidelberg,
Springer, 2011, pp. 379–395.
[21] Fu, Z. and Su, Z.: XSat: A Fast Floating-Point Satisfiability Solver, Computer Aided Verification - 28th International Conference, CAV 2016, Toronto, ON, Canada,
July 17-23, 2016, Proceedings, Part II, Chaudhuri, S.
and Farzan, A.(eds.), Lecture Notes in Computer Science,Vol. 9780, Springer, 2016, pp. 187–209.
[22] Gao, S., Avigad, J., and Clarke, E. M.: δ-Complete
Decision Procedures for Satisfiability over the Reals, Automated Reasoning, Berlin, Heidelberg, Springer, 2012,
pp. 286–300.
[23] Hasuo, I. and Suenaga, K.: Exercises in Nonstandard
Static Analysis of Hybrid Systems, Computer Aided Verification, 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 veRification for Continuous and Hybrid Systems, ARCH@CPSWeek2014, Berlin, Germany, April 14, 2014 / ARCH@CPSWeek2015, Seattle, USA, April 13, 2015., Frehse, G. and Althoff,M.(eds.), EPiC Series in Computing, Vol. 34, EasyChair,
2014, pp. 25–30.
[25] Jin, X., Deshmukh, J. V., Kapinski, J., Ueda, K., andButts, K.: Powertrain Control Verification 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 Verification of Embedded Control Systems: An Overview of Traditional andAdvanced Modeling, Testing, and Verification Techniques,IEEE Control Systems, Vol. 36, No. 6(2016), pp. 45–64.
[27] Kato, K., Ishikawa, F., and Honiden, S.: Falsificationof Cyber-Physical Systems with Reinforcement Learning,
3rd Workshop on Monitoring and Testing of Cyber-Physical
Systems, MT@CPSWeek 2018, Porto, Portugal, April 10,
2018, IEEE, 2018, pp. 5–6.
[28] Kuřátko, J. and Ratschan, S.: Combined Global and Local Search for the Falsification of Hybrid Systems, Formal

Modeling and Analysis of Timed Systems, Cham, Springer
International Publishing, 2014, pp. 146–160.
[29] Liebrenz, T., Herber, P., and Glesner, S.: Deductive Verification 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, Sun, J. and Sun,
M.(eds.), Lecture Notes in Computer Science, Vol. 11232,
Springer, 2018, pp. 89–105.
[30] Luersen, M. A. and Le Riche, R.: Globalized Nelder–
Mead method for engineering optimization, Computers &Structures, Vol. 82, No. 23(2004), pp. 2251–2260.
[31] Nguyen, L. V., Kapinski, J., Jin, X., Deshmukh, J. V.,
Butts, K., and Johnson, T. T.: Abnormal Data Classification
Using Time-Frequency Temporal Logic, Proc. of the 20th
International Conference on Hybrid Systems: Computation
and Control, HSCC ’17, New York, NY, USA, ACM, 2017,
pp. 237–242.
[32] Platzer, A.: Logical Foundations of Cyber-Physical Systems, Springer, 2018.
[33] 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.
[34] Silvetti, S., Policriti, A., and Bortolussi, L.: An
Active Learning Approach to the Falsification of BlackBox Cyber-Physical Systems, Integrated Formal Methods,
Cham, Springer International Publishing, 2017, pp. 3–17.
[35] Wohlin, C., Runeson, P., Hst, M., Ohlsson, M. C., Regnell, B., and Wessln, A.: Experimentation in Software Engineering, Springer Publishing Company, Incorporated, 2012.
[36] Zhang, Z., Ernst, G., Sedwards, S., Arcaini, P., andHasuo, I.: Two-Layered Falsification 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.
[37] Zhang, Z., Hasuo, I., and Arcaini, P.: Multi-Armed Bandits for Boolean Connectives in Hybrid System Falsification(Extended Version), CoRR, Vol. abs/1905.07549(2019).
[38] Zutshi, A., Deshmukh, J. V., Sankaranarayanan, S., andKapinski, J.: Multiple shooting, CEGAR-based falsification
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.