On the Eﬀectiveness of Signal Rescalingin Hybrid System Falsiﬁcation
Zhenya Zhang1(B) , Deyun Lyu1 , Paolo Arcaini2 , Lei Ma1 ,Ichiro Hasuo2 , and Jianjun Zhao1
1

Kyushu University, Fukuoka, Japanzhang.zhenya.623@m.kyushu-u.ac.jp
2
National Institute of Informatics, Tokyo, Japan

Abstract. Hybrid system falsiﬁcation employs stochastic optimization
to search for counterexamples to a system speciﬁcation in Signal Temporal Logic (STL), guided by quantitative STL robustness. The scale
problem could arise when the STL formula is composed of sub-formulas
concerning signals having diﬀerent scales (e.g., speed [km/h] and rpm):
the performance of falsiﬁcation could be negatively aﬀected because different scales can mask each other’s contribution to robustness. A natural
solution consists in rescaling the signals to the same order of magnitude.
In this paper, we investigate whether this “basic” approach is always
eﬀective, or better rescaling strategies could be devised. Experimental
results show that basic rescaling is not always the best strategy, andsometimes “unbalanced” rescalings work better. We investigate the reasons of this, and we identify future research directions based on thisobservation.
Keywords: Falsiﬁcation · Signal temporal logic · Scale problem ·Rescaling

1

Introduction

Automated formal veriﬁcation of hybrid systems is almost infeasible due to theinﬁnite search spaces given by the physical components. Falsification has been
proposed as a more practical approach that, rather than attempting to prove
the system speciﬁcation, tries to violate it: given a model M that takes an input
signal u and outputs a signal M(u), and a temporal logic specification ϕ (usuallyin Signal Temporal Logic (STL) [5]), the falsiﬁcation problem consists in ﬁnding
an input signal u such that the corresponding output M(u) violates ϕ.

This work is supported in part by JSPS KAKENHI Grant No. 20H04168, 19K24348,
19H04086, and JST-Mirai Program Grant No. JPMJMI18BB, Japan. Paolo Arcaini
and Ichiro Hasuo are supported by ERATO HASUO Metamathematics for Systems
Design Project (No. JPMJER1603), JST.
c Springer Nature Switzerland AG 2021

A. Dutle et al. (Eds.): NFM 2021, LNCS 12673, pp. 392–399, 2021.
https://doi.org/10.1007/978-3-030-76384-8_24

On the Eﬀectiveness of Signal Rescaling in Hybrid System Falsiﬁcation

393

Falsiﬁcation is usually turned into an optimization problem by exploiting
the robust semantics of temporal logic formulas [3,5]: instead of the classical Boolean satisfaction relation v |= ϕ, robust semantics assigns a value
v, ϕ ∈ R ∪ {∞, −∞} (i.e., robustness) that tells not only whether ϕ is satisﬁed or violated (by the sign), but also assesses how robustly it is satisﬁed orviolated. Since negative robustness indicates that the speciﬁcation is violated,
the goal of falsiﬁcation is to minimize the robustness to obtain a negative value.
Diﬀerent optimization-based falsiﬁcation algorithms have been proposed [7], that
employ stochastic optimization approaches, such as hill-climbing: they generate
inputs with the aim of decreasing robustness, and terminate when they ﬁnd an
input with negative robustness (i.e., a falsifying input). Also falsiﬁcation tools,
as Breach [2] and S-TaLiRo [1], are available.
The scale problem is a recognized issue in falsiﬁcation [6,8]. It is due to thecomputation of robust semantics, namely the way in which the robustness valuesof diﬀerent sub-formulas are compared: such computation is problematic in thepresence of signals that take values having diﬀerent order of magnitudes. As asimple example, let’s consider the formula ϕ ≡ ϕ1 ∨ ϕ2 , with ϕ1 ≡ gear < 3
to the robust semantics,
the robustnessof ϕ1 ,and ϕ2 ≡ speed > 35. Accordingat a given moment t, is 3 − gear (t) , and of ϕ2 is speed (t) − 35 ; the Boolean
connective ∨, instead, is interpreted by supremum . Note that the robustnessof ϕ1 is always in the order of units, while the robustness of ϕ2 is, in general,in the order of tens. Because of this, whenever ϕ2 is satisﬁed, it will almost
always mask the contribution of ϕ1 to the ﬁnal robustness of ϕ. The situation
is even more frequent if complete formulas with temporal operators (the ones
we consider) and their semantics are taken into account. Such a masking eﬀect
could be problematic for falsiﬁcation. Indeed, if the contribution of a signal s1 to
the global robustness is masked by another signal s2 , the falsiﬁcation algorithm
has no guidance, because it does not know how s1 should be modiﬁed to falsify
the whole formula.
A naı̈ve solution to the scale problem consists in rescaling the signals usedin the speciﬁcation at the same scale; we name such approach as basic rescaling.
In this paper, we are interested in assessing to what extent such approach is
eﬀective, i.e., if applying the basic rescaling leads to optimal falsiﬁcation results.
We perform an empirical evaluation using 2 benchmarks and 12 speciﬁcations,
showing that the basic rescaling is not always the best strategy; indeed, in somecases, scaling the signals in other ways (e.g., making their orders of magnitude
even more diﬀerent) leads to better falsiﬁcation results. We do a further analysisof these cases, explaining why this is the case; we then describe how such ﬁndings
can be used to pave new research directions in falsiﬁcation.
Paper structure. Sect. 2 provides some necessary background. Sect. 3 introduces the scale problem, and the basic rescaling approach to tackle it. Sect.
refsec:experiments presents the experiments we conducted to assess the eﬀectiveness of the basic rescaling, and to discover whether other rescaling strategies
are more eﬀective. Finally, Sect. 5 concludes the paper.

394

2

Z. Zhang et al.

Preliminary

In this section, we review the falsiﬁcation framework based on robust semantics
of temporal logic [3]. Let T ∈ R+ be a positive real. An M -dimensional signal(M ∈ N) with a time horizon T is a function w : [0, T ] → RM . We treat thesystem model as a black box, i.e., its behaviors are only observed from inputs
and their corresponding outputs. Formally, a system model, with M -dimensional
input and N -dimensional output, is a function M that takes an input signal
u : [0, T ] → RM and returns a signal M(u) : [0, T ] → RN . Here the common
time horizon T ∈ R+ is arbitrary.
Definition 1 (STL syntax). We ﬁx a set Var of variables. In Signal Temporal
Logic (STL), atomic propositions and formulas are deﬁned as follows, respectively: α ::≡ f (x1 , . . . , xN ) > 0, and ϕ ::≡ α | ⊥ | ¬ϕ | ϕ ∧ ϕ | ϕ ∨ ϕ | ϕ UI ϕ.
Here f is an N -ary function f : RN → R, x1 , . . . , xN ∈ Var, and I is a closed
non-singular interval in R≥0 , i.e. I = [a, b] or [a, ∞) where a, b ∈ R and a < b.
Other common connectives such as →, , 2I (always) and 3I (eventually), areintroduced as abbreviations: 3I ϕ ≡ UI ϕ and 2I ϕ ≡ ¬3I ¬ϕ.
Definition 2 (Robust semantics). Let w : [0, T ] → RN be an N -dimensionalsignal, and t ∈ [0, T ). The t-shift wt of w is the signal wt : [0, T − t] → RN
deﬁned by wt (t ) := w(t + t ). Let w : [0, T ] → R|Var| be a signal, and ϕ be
an STL formula. We deﬁne the robustness w,ϕ ∈ R∪ {∞, −∞} as follows,by induction on the construction of formulas.
anddenote inﬁmums andsupremums of real numbers, respectively. Their binary version and  denote
minimum and maximum.
w, f (x1 , · · · , xN ) > 0 := f w(0)(x1 ), · · · , w(0)(xN )w, ⊥ := −∞w, ¬ϕ := −w, ϕ
ϕ
w, ϕ1 ∨ ϕ2  :=w, ϕ1 ∧ ϕ2  := w, ϕ1  w,
 t2
 w, ϕ1   w, ϕ2 tw, ϕ1 UI ϕ2  := t∈I∩[0,T ] w , ϕ2 t ∈[0,t) w , ϕ1 
The original STL semantics is Boolean, given by a binary relation |= between
signals and formulas. The robust semantics reﬁnes the Boolean one in the following sense: w, ϕ > 0 implies w |= ϕ, and w, ϕ < 0 implies w |= ϕ, see [5,Prop. 16].
Optimization-Guided Falsification. Falsiﬁcation can be transformed into an
optimization problem by taking the robustness as objective function. The goal of
optimization is to minimize the robustness value by varying input signals—once
a negative robustness is found, it indicates the existence of a counterexample
violating the system speciﬁcation. To solve the optimization problem, diﬀerent metaheuristic-based optimization techniques can be used (e.g., CMA-ES,
Simulated Annealing), and these have been implemented in state-of-the-art falsiﬁcation tools such as Breach [2].

On the Eﬀectiveness of Signal Rescaling in Hybrid System Falsiﬁcation

3395

A Rescaling Approach for Tackling the Scale Problem

The scale problem [6,8] is known to aﬀect the falsiﬁcation performance. We here
shed a light on this problem and present a straightforward solution based on
signal rescaling.
Scale Problem. An STL formula is commonly composed of multiple subformulas concerning diﬀerent signals. These signals are likely to have diﬀerent
magnitudes. First of all, diﬀerent signals can range diﬀerently (e.g., speed ranges
over [0, 150] while gear is an integer less than 5). Moreover, the magnitude ofa signal may also depend to the use of diﬀerent measurement units (e.g., speed
may be measured in km/h, m/s, mph, etc.). The scale problem arises when therobustness of such a formula is computed: the process requires the comparison
between robustness values coming from diﬀerent sub-formulas (see the deﬁnition of robust semantics in Deﬁnition 2), and so the global robustness may be
dominated by only one of the involved signals. As the optimization process infalsiﬁcation is guided by robustness, the scale problem can pose an inﬂuence on
the performance of falsiﬁcation. We show the harmfulness of this issue via an
example.
Example 3. Consider an automatic transmission system that outputs gear ∈{1, 2, 3, 4} and speed ∈ [0, 150]. A safety property concerning the system is asfollows: ϕ ≡ 2I (gear = 4 → speed > 35). ϕ is equivalent to 2I (ϕ1 ∨ ϕ2 ) whereϕ1 ≡ ¬(gear = 4), ϕ2 ≡ speed > 35. Given a signal w consisting of speed
and gear , the calculation of its robustness consists in computing the inﬁmum of{wt , ϕ1 ∨ ϕ2  | t ∈ I}. This process is unfolded as follows: (i) for each t ∈ I,
compute wt , ϕ1  and wt , ϕ2 , and take their maximum as wt , ϕ1 ∨ ϕ2 ; (ii)obtain {wt , ϕ1 ∨ ϕ2  | t ∈ I}, and take its inﬁmum as w, ϕ.
In case T = {wt , ϕ1 ∨ ϕ2  | t ∈ I} contains values both from wt , ϕ1  andtw , ϕ2 , the inﬁmum of T will almost always be dominated by wt , ϕ1  due tothe scale issue of the two signals. This scenario is actually common, especiallywhen ϕ is not falsiﬁed. Hence, the contribution of ϕ2 to the ﬁnal robustness of
ϕ is almost always masked by ϕ1 . Even worse, wt , ϕ1  changes discretely due
to the nature of gear , and so does the ﬁnal robustness w, ϕ; this means thata small variation of the system input may not result in a change of the ﬁnal
robustness. Such flat robustness is problematic for optimization (that has no
guidance), and so falsiﬁcation will likely fail.
Rescaling Approach. Since the scale problem arises because of signals having
diﬀerent magnitudes, a straightforward solution could be to rescale the signals tothe same magnitude. We call this approach as basic rescaling. For this approach,domain knowledge regarding the ranges [l, u] of each signal is needed for computing the rescaling factor δ. Namely, given an STL formula concerning two signals
ranging over [l1 , u1 ] and [l2 , u2 ], respectively, the basic approach for deciding the2
rescaling factor δ w.r.t. the former signal is δ = uu21 −l
−l1 .

396

Z. Zhang et al.

Note that, in our experiments, we will also investigate the use of “unbalanced” scaling factors that rescale the signal in a diﬀerent way from the basic
rescaling (i.e., not at the same order of magnitude), and we will compare theirperformance.
In our experiments, we use Simulink for the system models. In order toimplement the rescaling approach in Simulink, we perform these two steps: (i)we amplify/diminish a selected signal w by δ times, by adding a gain block
to w with a parameter δ; (ii) we modify the constants of the STL formula inaccordance with the rescaled signals.

4

Experimental Evaluation

We selected two Simulink models used in falsiﬁcation competitions [4], namely,
Automatic Transmission (AT) and Abstract Fuel Control (AFC). Our domain
knowledge on the signal ranges of the models is as follows: AT takes throttleth ∈ [0, 100] and brake br ∈ [0, 325] as input signals, and gives gear ∈ {1, 2, 3, 4},
speed ∈ [0, 150], and rpm ∈ [0, 4500] as output signals; AFC takes pedal anglepa ∈ [8.8, 70] and engine speed es ∈ [900, 1100] as input signals, and gives
controller mode cm ∈ {0, 1, 2} and a scalar μ ∈ [0, 0.25] (the performance ofthe system) as output signals. Note that the ranges for input signals are set byusers and thus precise, but the ranges for output signals are reported empiricallyby sampling. In total, we evaluate 9 speciﬁcations for AT and 3 for AFC (seeTable 1).
Experiments were conducted using Breach 1.2.13 (with CMA-ES as solver)
on an Amazon EC2 c4.large, 2.9 GHz Intel Xeon E5-2666, 2 virtual CPU cores,
4 GB RAM.
Table 1. STL speciﬁcations (Δt (w) = wt − w)
Spec. ID Temporal specification in STL

Spec. ID Temporal specification in STL

AT1

2[0,30] (Δ1 (speed) < 30 ∧ Δ1 (rpm) < 3500) AT7

AT2

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

AT3

2[0,30] (3[0,10] (rpm < 600) → gear = 1)AT92[0,30] (th = 0 ∨ br = 0) → 2[0,30] (speed < 110)AT4

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

AFC1

2[11,50] (cm = 1 → μ < 0.228)

AT5

2[0,30] (3[0,8] (speed < 130 ∧ rpm < 4750)) AFC2

3[0,50] (pa > 40) → 2[11,50] (μ < 0.225)

AT6

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

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

On the Eﬀectiveness of Signal Rescaling in Hybrid System Falsiﬁcation

397

Table 2. Experimental results with diﬀerent rescaling strategiesδ
no-rescaling
basic
rpm × 10−3rpm × 10−2rpm × 10−1rpm × 101

SR
2
8
26
12
3
4

AT1
time
#sim
57.4
44
152.2 109.1
103.8 81.7
138.9 105.7
114.7 82.3
54.7
41

SR
23
30
30
17
19
18

AT2
time
190.9
126.5
121.5
203.0
182.3
175.8

#sim
144.3
86.1
96.7
155.2
123.4
130.2

SR
9
30
18
14
13
17

AT3
time #sim
7.9
6.1
3.1
2.3
6.8
5.4
8.2
6.4
8.1
6
8.0
6.1

no-rescaling
basic

SR
10
28

AT7
time
#sim
137.0 102.7
112.7 84.9

SR
11
0

AT8
time #sim
320.5 236.8
-

SR
22
23

AT9
time #sim
268.2 209192.2 137.5

speed × 10−2
speed × 10−1
speed × 101
speed × 102

29
23
10
8

152.9
136.6
82.9
139.9

29
29
0
0

326.1
296.4
-

1
0
13
2

592.4
388.8
139.1

δ

122.7
108.0
62.3
94.1

256.7
229.1
-

461
256.2
101.5

SR
7
10
5
3
8
8

AT4
time
49.7
24.2
14.8
19.2
31.7
26.6

#sim
38.3
17.8
12
15
23.4
20.1

SR
30
18
10
11
30
30

AT5
time
166.4
196.2
69.5
154.3
1.3
149.2

#sim
130.1
140.5
55.2
114.7
1
109.5

SR
7
13
2
13
13
5

AT6
time
377.5
375.6
452.0
389.2
372.4
348.4

#sim
280.3
269.2
349
273.8
266
244.6

no-rescaling
basic

SR
4
11

AFC1
time #sim
320.1 234.8
381.7 271.6

SR
2
30

AFC2
time #sim
487.5 334.5
312.8 225.9

SR
4
0

AFC3
time #sim
354.6 245.8-

μ × 101
μ × 102
μ × 103μ × 104

11
6
8
8

363.4
387.5
405.7
467.7

9
30
29
28

408.0
240.3
198.7
265.9

11
4
1
2

303.1
307.8
117.9
320.6

δ

254
266.2
283.9
295.9

259.4
176.3
147.1
170.5

215.5
197
78
228.5

Evaluation. An experiment consists in the execution of falsiﬁcation using agiven rescaling strategy (no-rescaling, basic rescaling as described in Sect. 3,
or a diﬀerent rescaling), over a speciﬁcation for 30 trials, using diﬀerent seeds.
For each experiment, we collect the success rate (SR) as the number of trials inwhich a falsifying input was found, the average execution time of the successful
trials, and the average number of simulations. Table 2 reports all experimental
results1 . We analyze them using 3 research questions.
RQ1 Does the basic rescaling approach always solve the scale problem?
First, we want to assess the eﬀectiveness of the basic rescaling approach. From
Table 2, we observe that in 7 out of 12 cases (AT1, AT2, AT3, AT6, AT7, AFC1,
AFC2), the approach does improve the success rate w.r.t. the no-rescaling approach in which the signals are kept in their original order of magnitudes; thisis particular evident in AT3. On the other hand, we observe that in some cases
there is almost no improvement given by the basic rescaling (as AT4and AT9)and, in few cases, the basic rescaling approach even diminishes the success rate,as AT5and AT8: this is an indication that only considering the theoretical rangesof the signals may be not a good strategy, as the concrete robustness values associated to these signals usually have diﬀerent order of magnitudes.
RQ2 How does the rescaling factor inﬂuence the falsiﬁcation performance?
In the previous RQ, we observed that the basic rescaling is not always eﬀective.
In this RQ, we investigate whether other types of rescaling (i.e., not at the sameorder of magnitude) can lead to better falsiﬁcation results. From Table 2, weobserve that this is the case. In 3 out of 12 cases (AT1, AT5, and AT8), thebest falsiﬁcation result is obtained by an “unbalanced” rescaling strategy. This
conﬁrms that the best rescaling is the one that aﬀects the robustness landscapein a way that the falsiﬁcation algorithm is facilitated. The next RQ provides
further analyses that explain such phenomenon.

1

The source code is available at https://github.com/choshina/FalSTAR-NFM.

398

Z. Zhang et al.
50

120

100

80

60

40

20

0

robustness value

4000

robustness value

robustness value

140

3500

3000

2500

2000

1500

1000

500

100

200

300

400

500

600

700

800

simulations(a) No rescaling

900

1000

40
35
30
25
20
15
10
5
0

0

0

45

0

100

200

300

400

500

600

700

800

900

1000

0

50

(b) Basic rescaling

100

150

200

250

300

simulations

simulations(c) Best rescaling

Fig. 1. Comparison of rescaling strategies for AT8

RQ3 Why do “unbalanced” rescalings sometimes improve the performance?
In order to answer this question, we investigate AT8, for which the basic rescaling
does not work at all, while two other unbalanced rescalings work very well. AT8is2[0,30] (ϕ1 ∧ ϕ2 ), where ϕ1 ≡ speed < 135 and ϕ2 ≡ rpm < 4780. We run thefalsiﬁcation algorithm using no-rescaling, basic rescaling, and the best rescaling
strategy (i.e., with speed with 10−1 ), each taking 1000 simulations as timeout.
For each simulation, we calculate values robspeed and robrpm from the output
signals w, as follows:(i) we obtain {wt , ϕ1 ∧ ϕ2  | t ∈ [0, 30]};(ii) for each t ∈ [0, 30], we identify whether wt , ϕ1 ∧ ϕ2  is given by valuet, ϕ1  in Sϕ1 or wt , ϕ2  in Sϕ2 ,wt , ϕ1  or wt , ϕ2 , and we record w
accordingly. Then, we assign robspeed as Sϕ1 and robrpm as Sϕ2 ; if Sϕ1(or Sϕ2 ) is empty, then robspeed (or robrpm ) is omitted.
In this way, we know, for each sample, which is the signal that contributed
to the ﬁnal robustness. Figure 1 shows, for the three approaches, robspeed androbrpm of each sample. Note that the ﬁnal robustness of each sample is given by
the minimum between robspeed and robrpm . In Fig. 1a, we see that rpm always
determines the ﬁnal value, and no falsifying input is found: this shows that, in thiscase, falsiﬁcation driven by rpm is not eﬃcient. This is against the assumption of
the basic rescaling that the signals having larger ranges lead to higher robustness
values; indeed, we see from Fig. 1b that the basic rescaling actually worsens thesituation, having the eﬀect of increasing the robustness related to speed . From
Fig. 1c, we see that the best rescaling is an unbalanced one, in which the speed
is decreased of one order of magnitude: in this case, the falsiﬁcation algorithm
is very eﬀective, and ﬁnds a falsifying input after 172 simulations.

5

Conclusion and Future Work

We have shown that having signals of diﬀerent scales in a speciﬁcation can aﬀect
the falsiﬁcation eﬀectiveness, because, due to the robust semantics, one signal
can mask the other. We have also shown that the naı̈ve approach that rescales
the signals to the same order of magnitude does not always solve the problem.
Sometimes, “unbalanced” rescalings are better. Future research direction consists

On the Eﬀectiveness of Signal Rescaling in Hybrid System Falsiﬁcation399

in devising falsiﬁcation approaches that can automatically ﬁnd such rescalings,
either before or during the search.

References
1. Annpureddy, Y., Liu, C., Fainekos, G., Sankaranarayanan, S.: S-TaLiRo: a tool
for temporal logic falsiﬁcation for hybrid systems. In: Abdulla, P.A., Leino, K.R.M.
(eds.) TACAS 2011. LNCS, vol. 6605, pp. 254–257. Springer, Heidelberg (2011).
https://doi.org/10.1007/978-3-642-19835-9 21
2. Donzé, A.: Breach, a toolbox for veriﬁcation and parameter synthesis of hybrid systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp.
167–170. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-142956 17
3. Donzé, A., Maler, O.: Robust satisfaction of temporal logic over real-valued signals.
In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp.
92–106. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15297-9 9
4. Ernst, G., et al.: ARCH-COMP 2020 category report: falsiﬁcation. In: ARCH20. 7thInternational Workshop on Applied Veriﬁcation of Continuous and Hybrid Systems(ARCH20). EPiC Series in Computing, vol. 74, pp. 140–152. EasyChair (2020).
10.29007/trr1
5. Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic speciﬁcations forcontinuous-time signals. Theor. Comput. Sci. 410(42), 4262–4291 (2009)
6. Ferrère, T., Nickovic, D., Donzé, A., Ito, H., Kapinski, J.: Interface-aware signal temporal logic. In: Proceedings of the 22nd ACM International Conference on Hybrid
Systems: Computation and Control, HSCC 2019, Montreal, QC, Canada, April 16–
18, 2019, pp. 57–66 (2019)7. Kapinski, J., Deshmukh, J.V., Jin, X., Ito, H., Butts, K.: Simulation-based
approaches for veriﬁcation of embedded control systems: An overview of traditional
and advanced modeling, testing, and veriﬁcation techniques. IEEE Control Syst.
36(6), 45–64 (2016)
8. Zhang, Z., Hasuo, I., Arcaini, P.: Multi-armed bandits for boolean connectives inhybrid system falsiﬁcation. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol.
11561, pp. 401–420. Springer, Cham (2019). https://doi.org/10.1007/978-3-03025540-4 23