Time-Staging Enhancement ofHybrid System Falsification
Gidon Ernst

Ichiro Hasuo

Zhenya Zhang

Sean Sedwards

National Institute of Informatics, Tokyo, Japan

University of Waterloo, Waterloo, Canada{gidon,hasuo,zhangzy}@nii.ac.jp

sean.sedwards@uwaterloo.ca

Optimization-based falsification employs stochastic optimization algorithms to search for error inputof hybrid systems. In this paper we introduce a simple idea to enhance falsification, namely timestaging, that allows the time-causal structure of time-dependent signals to be exploited by the optimizers. Time staging consists of running a falsification solver multiple times, from one interval
to another, incrementally constructing an input signal candidate. Our experiments show that timestaging can dramatically increase performance in some realistic examples. We also present theoretical results that suggest the kinds of models and specifications for which time staging is likely to beeffective.

1

Introduction

Hybrid Systems Quality assurance of cyber-physical systems (CPS) has been recognized as an important challenge, where many CPS are hybrid systems that combine the discrete dynamics of computers
and the continuous dynamics of physical components. Unfortunately, analysis of hybrid systems poses
unique challenges, such as the limited applicability of formal verification. In formal verification one aims
to give a mathematical proof for a system’s correctness. This is much harder for hybrid systems than forcomputer software/hardware, where the presence of continuous dynamics makes many problems more
complex or even undecidable (e.g. reachability in hybrid automata).
Optimization-Based Falsification Bemore robustly
This way to??
cause of these difficulties, an increasclimb down :)true
ing number of researchers are turning true
input
input
to optimization-based falsification as aless soquality assurance measure. It is a testing false
quantitative
method rather than that of formal verifiBoolean semantics
robust semantics
cation; the problem is formalized as folFigure 1: From Boolean to robust semantics
lows.
• Given: a model M (that takes an input signal u and yields
an output signal M (u)), and a specification ϕ (a temporal
M (u)
u /
formula)/M
6|= ϕ ?
• Answer: error input, that is, an input signal u such that thecorresponding output M (u) violates ϕIn the optimization-based falsification approach, the above falsification problem is turned into an optimization problem. This is possible thanks to robust semantics of temporal formulas [14]. Instead of theBoolean satisfaction relation v |= ϕ, robust semantics assigns a quantity Jv, ϕK ∈ R ∪ {∞, −∞} that tells
To appear in EPTCS.

2

Time-Staging Enhancement of Hybrid System Falsificationus, not only whether ϕ is true or not (by the sign), but also how robustly the formula is true or false. This
allows one to employ hill-climbing optimization (see Fig. 1): we iteratively generate input signals, in the
direction of decreasing robustness, hoping that eventually we hit negative robustness.
Optimization-based falsification is a subclass of search-based testing: it adaptively chooses test cases(input signals u) based on previous observations. One can use stochastic algorithms for optimization(such as simulated annealing), which turn out to be much more scalable than many model checking
algorithms that rely on exhaustive search. Note also that the system model M can be black box: it isenough to know the correspondence between input u and output M (u). An error input u is concrete
evidence for the system’s need for improvement, and thus has great appeal to practitioners.
The approach of optimization-based falsification was initiated in [14] and has been actively pursued
ever since [3, 5, 7, 8, 10, 11, 20]. There are now mature tools, such as Breach [8] and S-Taliro [5], which
work with industry-standard Simulink models.
Contribution We introduce a simple idea of time staging for enhancement of optimization-based falsification. Time staging consists of running a falsification solver repeatedly, from one input segment toanother, incrementally constructing an input signal.
In general, in solving a concrete problem C by a metaheuristic H (such as stochastic optimization,
evolutionary computation, etc.), a key to success is to communicate as much information as possible in
the translation from C to H —that is, to let H exploit structures unique to C . Our idea of time staging
follows this philosophy. More specifically, via time staging we communicate the time-causal structureof time-dependent signals—a structure that is present in some instances of the falsification problem but
not in optimization problems in general—to stochastic optimization solvers.
Our implementation of time-staged falsification is based on Breach [8]. We show that this simple
idea can dramatically enhance its performance in some examples. We also present some theoreticalconsiderations on the kinds of problem instances where time staging is likely to work, and some resultsthat aid implementation of time staging.
Structure of the Paper In §2 we informally outline optimization-based falsification and illustrate theidea of time staging. We then turn to formal developments: in §3 we review existing falsification works
and in §4 we present our algorithm, augmented by some theoretical results that aid its implementation.
§5 is devoted to the theoretical consideration of two specific settings in which time staging is guaranteed
to work well. These settings will serve as useful “rules of thumb” for practical applications. In §6 we
discuss our implementation and experimental results. We conclude in §8.

2

Schematic Overview: Falsification and Time Staging

We illustrate falsification and time staging, informally with an example.
Example Setting We take as a system model M a simple automotive powertrain whose input signal
is 1-dimensional (the throttle u) and whose output signal is the vehicle speed v. We assume that M
exhibits the following
natural behavior: the larger u is, the quicker v grows. Let our specification be
ϕ ≡ 2(v ≤ 120) , where ≡ denotes the syntactic equality. To falsify ϕ the vehicle speed v must exceed
120. From the assumption about M ’s behavior, we expect u to be large in a falsifying input signal. Notethat this is a simplified version of one of our experiments in §6.

G. Ernst, I. Hasuo, Z. Zhang & S. Sedwards

3(i + 1)-th samplingi-th sampling
throttle

throttle
(i)

(i+1)

u4

(i+1)

u1

u2

(i+1)

(i)

(i+1)

u3
(i)

u2

(i)

u4

time

· · · −→

Choosing
(i+1)
(i+1)
, . . . , uK
u1
by optimization−−−−−−−−−−−−−−−→

vehicle speed
120

u3

u1

time

−→ · · ·vehicle speed120v(i+1)
v(i)

time

time

Figure 2: Conventional optimization-based falsification (without time staging).
first stage

second stage

throttle

throttle

(1)

u1

...

time

(1)

u2

time
vehicle speed
(n )

v1 1
(2)

v1
(1)
v1

(n )

v1 1

optimization

(n )

..
.

(2)

u2

..
.

v2 2
(1)

v2

−→ · · ·optimization

vehicle speed
120

Choosing
the best
prefix(n )u 1−−1−−−−−−→

optimization

(2)

u1

(n )

u2 2

optimization

...

(n )

u1 1

(n )

u1 1

time

time

Figure 3: Falsification with time staging

⇒

⇒

ng

bi
m

cli
llhi

robustness JM(u), ϕK···u(2) u(1) u(i)u(i+1) ?

⇒ ··· ⇒
input signal u

Figure 5: Nelder-Mead optimization. Here the inFigure 4: Hill-climbing optimization in falsification put space is the two-dimensional square, and the(unknown) score function is depicted by contour
lines. Figures are from Wikipedia

4Time-Staging Enhancement of Hybrid System Falsification

Optimization-Based Falsification Fig. 2 illustrates how a conventional optimization-based falsification procedure works. In the i-th sampling one tries an input signal u(i) . Following the falsification litera(i)(i)
ture we focus on piecewise constant signals. Thus a signal u(i) is represented by a sequence (u1 , . . . , uK )of real numbers. See the top left of Fig. 2. The corresponding output signal v(i) = M (u(i) ) is shown
below it.
Since v(i) does not reach the threshold 120, we move on to the (i + 1)-th sampling and try a new
(i+1)
(i+1)
input signal u(i+1) = (u1 , . . . , uK ). The choice of u(i+1) is made by an optimization algorithm.
Specifically, the optimization algorithm observes the results of the previously sampled input signals
u(1) , . . . , u(i) —especially the robustness
value JM (u(i) ), ϕK that each input u(i) achieves. In the currentsetting where ϕ ≡ 2(v ≤ 120) , the robustness value is simply the difference between 120 and the peakvehicle speed. The optimization algorithm tries to derive some general tendency, which it then uses toincrease the probability that the next input signal u(i+1) will make the robustness smaller (i.e. the peakvehicle speed higher).
Hill climbing is a prototype of such optimization algorithms. Its use in falsification is illustrated
in Fig. 4, where u = (u1 , . . . , uK ) is depicted as one-dimensional for clarity. The actual curve for therobustness value JM (u), ϕK (gray and dashed) is unknown. Still the previous observations under inputu(1) , . . . , u(i) suggest that to the right is the climbing down direction. The next candidate u(i+1) is pickedaccordingly, towards negative robustness. Another well-known optimization algorithm is the NelderMead algorithm. See Fig. 5, where the input space is two-dimensional and the (unknown) robustness
function is depicted by contour lines.
(i+1)
(i+1)
We see in the right of Fig. 2 that the new input signal u(i+1) = (u1 , . . . , uK ) leads to a corresponding output signal v(i+1) that reduces the robustness value by achieving a higher peak speed. We
continue this way, u(i+2) , u(i+3) , . . . , hoping to eventually reach a falsifying input signal.
Absence of the Time-Causal Information A closer look at Fig. 2 reveals room for improvement. In
Fig. 2, the new input signal u(i+1) indeed achieves a smaller overall robustness JM (u), ϕK than u(i) .
(i+1)
(i)
However, its initial segment u1
is smaller than u1 ; consequently the vehicle speed v(i+1) is smaller(i)than v(i) in the first few seconds. Keeping the initial segment u1 would have achieved an even greaterpeak speed.
The problem here is that the time-causal structure inherent in the problem is not explicitly communicated to the optimization algorithm. The relevant structure is more specifically time monotonicity: an
input prefix that achieves smaller robustness (i.e. a greater peak speed) is more likely to extend to a fullfalsifying input signal. Although it is possible that a stochastic optimization algorithm somehow “learns”
time monotonicity, it is not guaranteed, because the structure of input spaces (the horizontal axis in Fig. 4
and the squares in Fig. 5) does not explicitly reflect time-causal structures.
While the time monotonicity is not shared by all instances of the falsification problems, we find many
realistic instances that approximately satisfy the property. We discuss time monotonicity in §5, as wellas in the context of our experiments in §6.
Falsification with Time Staging Our proposal of time staging consists of incrementally synthesizing acandidate input signal. We illustrate this in Fig. 3. In the first stage (left), we run a falsification algorithm
and try to find an initial input segment that achieves low robustness (i.e. high peak speed). This first stagecomprises running n1 samplings, as illustrated in Fig. 2. This process will gradually improve candidates
for the initial input segment, in the way the arrows ↑ on the left in Fig. 3 designate. Let us assume that(n )the last candidate u1 1 is the (tentative) best, achieving the smallest robustness.

G. Ernst, I. Hasuo, Z. Zhang & S. Sedwards

5(n )In the second stage (on the right in Fig. 3) we continue u1 1 and synthesize the second input segment.
This is again by running a falsification algorithm, as depicted. Note that, in each stage (a box in Fig. 3),
the whole iterated process in Fig. 2 is conducted. In this way we continue to the K-th stage, always
starting with the input segment that performed the best in the previous stage, thus exploiting the timecausal structure.
While time staging is not difficult to implement, there is a challenge in using it effectively. An immediate question is whether choosing the single best input segment in each stage is the optimal approach.
Our current strategy favors exploitation over exploration: it might miss a falsifying signal whose robustness must decrease slowly in the earlier segments and only quickly in the latter segments. Indeed weare working on an evolutionary variant of the above time-staged algorithm, where multiple segments
are passed over from one stage to another, in order to maintain diversity and conduct exploration. Thatsaid, even under the current simple strategy of picking the best one, we observe significant performanceenhancement in some falsification problems. See §6.
We can summarize this trade-off in terms of the size of search spaces. Let U be the set of candidates
for input segments, and K be the number of stages. Then the size of the set of whole input signals is|U|K , choosing one input segment for each stage. In our staged algorithm, in contrast, the search spacefor each stage is U and overall our search space is K · |U|. This reduction comes with the risk of missing
some falsifying input signals. The experimental results in §6 suggest this risk is worth taking. Moreover,in §5 we present some theoretical conditions for the absence of such risk. They help users decide inpractical applications when time staging will be effective.

3

Optimization-Based Falsification

From this section on we turn to the formal description and analysis of our algorithm. This section presents
a review of existing works on optimization-based falsification.
System Models Let us formalize our system models.
Definition 3.1 (time-bounded signal). Let T ∈ R>0 be a positive real. A (time-bounded) m-dimensionalsignal with a time horizon T is a function w : [0, T ] → Rm .
Let w : [0, T ] → Rm and w0 : [0, T 0 ] → Rm be (time-bounded) signals. Their concatenation w ·w0 : [0, T + T 0 ] → Rm is defined by (w · w0 )(t) := w(t) if t ∈ [0, T ], and w0 (t − T ) if t ∈ (T, T + T 0 ].
Let T1 , T2 ∈ (0, T ] such that T1 < T2 . The restriction w|[T1 ,T2 ] : [0, T2 − T1 ] → Rm of w : [0, T ] → Rm to
the interval [T1 , T2 ] is defined by (w|[T1 ,T2 ] )(t) := w(T1 + t).
Definition 3.2 (system model M ). A system model, with M-dimensional input, is a function M thattakes an input signal u : [0, T ] → RM and returns M (u) : [0, T ] → RN . Here the common time horizon
T ∈ R>0 is arbitrary.
Furthermore, we impose the following causality condition on M . For any time-bounded signals
u : [0, T ] → RM and u0 , we require that M (u · u0 ) [0,T ] = M (u).
Note that M (u · u0 ) = M (u) · M (u0 ) does not hold in general: feeding u can change the internal
state of M . This motivates the following definition.
Definition 3.3 (continuation Mu ). Let M be a system model and u : [0, T ] → RM be a signal. The
continuation of M after u, denoted by Mu , is defined as follows. For an input signal u0 : [0, T 0 ] → RM :Mu (u0 )(t) := M (u · u0 )(T + t).

6Time-Staging Enhancement of Hybrid System Falsification

Signal Temporal Logic and Robust Semantics We review signal temporal logic (STL) [21] and its
robust semantics [10, 14]. Var is the set of variables, and let N := |Var|. Variables stand for physicalquantities, control modes, etc. ≡ denotes syntactic equality.
Definition 3.4 (syntax). In STL, atomic propositions and formulas are defined 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 anda < b.
We omit subscripts I for temporal operators if I = [0, ∞). Other common connectives like ∨, →, >,2I (always) and 3I (eventually), are introduced as abbreviations: 3I ϕ ≡ > UI ϕ and 2I ϕ ≡ ¬3I ¬ϕ.
Atomic formulas like f (~x) ≤ c, where c ∈ R is a constant, are also accommodated by using negation andthe function f 0 (~x) := f (~x) − c.

Definition 3.5 (robust semantics [9, 10]). For an unbounded n-dimensional signal w : R≥0 → Rn andt ∈ R≥0 , wt denotes the t-shift of w, that is, wt (t 0 ) := w(t + t 0 ).
Let w : R≥0 → RN be a signal (recall N = |Var|), and ϕ be an STL formula. We define the robustnessJw, ϕK ∈ R ∪ {∞, −∞} as follows, by induction. Here u and t denote infimums and supremums of real
numbers, respectively.
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 u Jw, ϕ2 K
dF
0
Jw, ϕ1 UI ϕ2 K := t∈I Jwt , ϕ2 K u t 0 ∈[0,t) Jwt , ϕ1 K

Here are some intuitions and consequences. The robustness Jw, f (~x) > cK stands for the verticalmargin f (~x) − c for the signal w at time 0. A negative robustness value indicates how far the formula
is from being true. The robustness for the eventually modality is computed by Jw, 3[a,b] (x > 0)K =Ft∈[a,b] w(t)(x).
The original semantics of STL is Boolean, given by a binary relation |= between signals and formulas. The robust semantics refines the Boolean one, in the sense that: Jw, ϕK > 0 implies w |= ϕ, andJw, ϕK < 0 implies w 6|= ϕ. Optimization-based falsification via robust semantics [14] hinges on thisrefinement. See [10].
Although the definitions so far are for unbounded signals only, we note that the robust semantics
Jw, ϕK, as well as the Boolean satisfaction w |= ϕ, allows straightforward adaptation to time-boundedsignals (Def. 3.1). See Appendix A.
Falsification Solvers In the next definition, a prototype of a score function ρ is given by the robustness
ρϕ of a given STL specification ϕ. The generality of allowing other ρ is needed later in §4.
ρϕ (v) := Jv, ϕK(1)

Definition 3.6 (falsification solver). A falsification solver is a stochastic algorithm Falsify that takes, as
input: 1) a system model M (Def. 3.2) with M-dimensional input; 2) a score function ρ that takes an
output signal v of M and returns a score ρ(v) ∈ R ∪ {−∞, ∞}; and 3) a time horizon T ∈ R>0 . The
algorithm Falsify returns an M-dimensional signal u : [0, T ] → RM .
Each invocation Falsify(M , ρ, T ) of the solver is called a falsification trial. It is successful if the
returned signal u satisfies ρ(M (u)) < 0. Note that the returned signal u can differ in every trial, since
Falsify is a stochastic algorithm.

G. Ernst, I. Hasuo, Z. Zhang & S. Sedwards

7

Algorithm 1 Internal Structure of a Falsification Solver Falsify(M , ρ, T )Require: a system model M , a score function ρ, and T ∈ R>0
1: U ← (). the list U collects all the candidates u : [0, T ] → RM
2: while ¬InitialSamplingDone(T, U) do3:u ← InitialSampling(T ). u : [0, T ] → RM is sampled following some recipe
4:
U ← cons(U, u)
5: while ¬OptimizationSamplingDone(M , ρ, T, U) do
6:u ← OptimizationSampling(M , ρ, T, U)
7:. u is sampled, so that ρ(M (u)) becomes small, based on previous samples in U
8:
U ← cons(U, u)
9: u ← arg minu∈U ρ(M (u))
10: return u. a trial is successful if ρ(M (u)) < 0
We further assume the internal structure of the solver Falsify follows the scheme in Algorithm 1. It
consists of two phases. The first initial sampling phase collects some candidates for u : [0, T ] → RM
regardless of the system model M or the score function ρ. In the second optimization sampling phase,a stochastic optimization algorithm is employed to sample a candidate u that is likely to make the score
ρ(M (u)) small.
Implementation of Falsification Solvers Both Breach [8] and S-Taliro [5] take industry-standard
Simulink models as system models. For input signal candidates the tools focus on piecewise constantsignals; they are represented by sequences (u1 , . . . , uK ) of real numbers, much like in §2. Here K is thenumber of control points; in our staged algorithm we use the same K for the number of stages.
The tools offer multiple stochastic optimization algorithms for the optimization sampling phase,including CMA-ES [6], global Nelder-Mead and simulated annealing. The initial sampling phase ismostly by random sampling. Additionally, in Breach with global Nelder-Mead, so-called corner samples
are added to the list U. The number of corner samples grows exponentially as K grows, i.e. as we havemore control points.

4

Time Staging in Optimization-Based Falsification

Definition 4.1 (time-staged deployment of falsification solver). Let M be a system model, ϕ be an STL
formula, and T ∈ R>0 be a time horizon. Let K ∈ N be a parameter; it is the number of time stages. The
time-staged deployment of a falsification solver Falsify is the procedure in Algorithm 2. On the line 3,
the model Mu is the continuation of M after u (Def. 3.3); the score function ∂v ρϕ is defined by(1)(∂v ρϕ )(v0 ) := ρϕ (v · v0 ) = Jv · v0 , ϕK .

(2)

The whole procedure is stochastic (since Falsify is); an invocation is called a time-staged falsification
trial. It is successful if the returned signal u satisfies JM (u), ϕK < 0.

A falsification trial (i.e. an invocation of Algorithm 1) is an iterative process: the more we sample, themore likely we obtain a falsifying input signal. Since we run multiple falsification trials in Algorithm 2(one trial for each of the K stages), an important question is how we distribute available time to different
stages.

8Time-Staging Enhancement of Hybrid System Falsification

Algorithm 2 Time-Staged Deployment of a Falsification Solver
Require: a falsification solver Falsify, a system model M , an STL formula ϕ, T ∈ R>0 and K ∈ N
1: u ← (). the input prefix obtained so far. We start with the empty signal ()2: for j ∈ {1, . . . , K} do
3:. synthesizing the j-th input segmentu0 ← Falsify(Mu , ∂M (u) ρϕ , KT )4:u ← u · u0
. concatenate u0 , after which the length of u is jTK
5: return u. a time-staged falsification trial is successful if JM (u), ϕK < 0
A simple strategy is to fix the number of samples in each phase of Algorithm 1. Then the predicates
init andInitialSamplingDone(T, U) and OptimizationSamplingDone(M , ρ, T, U) are given by |U| > Nmax
opt
opt
init
|U| > Nmax , where Nmax , Nmax are constants.
An adaptive strategy, that we also implemented for the optimization sampling phase, is to continue
stuck , and we stop after N stuck consampling until we stop seeing progress. Here we fix a parameter Nmax
max
secutive samplings without reducing robustness. A similar strategy of adaptively choosing the numberof samples can be introduced for random sampling in the initial sampling phase (the lines 2–4 of Algorithm 1).

4.1

Towards Efficient Implementation

A key to speedup of Algorithm 2 is in the line 3; more specifically, how we handle the previous input
prefix u. Here we discuss two directions, one on the model Mu and the other on the score function∂v ρϕ . (We note that the suggested enhancements are not currently used in our implementation, becauseof performance reasons. See below.)

Continuation of Models Optimization-based falsification has a very wide application domain. Since
it only requires a black-box model M , the concrete form of M can vary from a program to a Simulink
model and even a system with hardware components (HILS). These models can be very big, and usually
the bottleneck in falsification lies in simulation, that is, to compute M (u) given an input signal u.
In the line 3 of Algorithm 2, therefore, using the definition M (u · u0 )(T +t) in Def. 3.3 is in principle
not a good strategy: it requires simulation of M for the whole prefix u·u0 , which can be avoided if we candirectly simulate the continuation Mu . In Simulink this is possible by saving the snapshot of the model
after a simulation, via the SaveFinalState model configuration parameter. In our implementation we
do not do so, though, because the overhead of saving and loading snapshots is currently greater thanthe cost of simulating. This balance can become different, if we figure out a less expensive way to use
snapshots, or if we study more complex models.

Derivative of Formulas The situation is similar with the score function ∂M (u) ρϕ in the line 3 of Algorithm 2. Using the presentation ρϕ (M (u) · v0 ) in (2) requires scanning the same prefix M (u) repeatedly.
Desired here is a syntactic presentation of ∂M (u) ρϕ , that will be given as an STL formula ∂M (u) ϕ suchthat ∂M (u) ρϕ = ρ(∂M (u) ϕ) . This would allow one to utilize available algorithms for computing robustness
values Jv, ∂M (u) ϕK.
Definition 4.2 (derivative of flat STL formulas). Let T ∈ R>0 , and v : [0, T ] → RN be a signal. Givenan STL formula ϕ that is flat in the sense that it does not have nested temporal operators, the derivativeG. Ernst, I. Hasuo, Z. Zhang & S. Sedwards

9∂v ϕ by v is defined inductively as follows.
∂v f (~x) > 0 :≡ cJv, f (~x)>0K∂v ⊥ :≡ ⊥∂v (¬ϕ) :≡ ¬∂v ϕ∂v (ϕ1 ∧ ϕ2 ) :≡ (∂v ϕ1 ) ∧ (∂v ϕ2 )
∂v (ϕ1 UI ϕ2 ) :≡ cJv,ϕ1 UI ϕ2 K ∨ (cJv,2ϕ1 K ∧ ϕ1 ) UI−T ϕ2
Here the interval I − T is obtained by shifting endpoints, such as [a, b] − T = [a − T, b − T ]. For eachr ∈ R, the notation cr abbreviates the atomic formula r > 0, where r is thought of as a constant function.
We use the fact that Jw, cr K = r.

Until formulas ϕ1 UI ϕ2 are split into the evaluation on the signal prefix v (first disjunct), and acontinuation (second disjunct). The constant cJv,2ϕ1 K injects the robustness of ϕ1 seen so far into theresidual formula (recall
 that both of 2 and ∧ take the infimum). It follows that ∂v 2I ϕ ≡ cJv,2ϕK ∧2I−T ϕ and ∂v 3 ϕ ≡ cJv,3ϕK ∨ 3I−T ϕ.
Proposition 4.3. Let T ∈ R>0 , v : [0, T ] → RN be a signal, and ϕ be a flat STL formula. We have, forany v0 : [0, T 0 ] → RN , Jv0 , ∂v ϕK = Jv · v0 , ϕK.

A proof is in Appendix B. Use of derivatives for timed specifications is also found e.g. in [22].
The settings are different, though: Boolean semantics in [22] while our semantics is quantitative. Our
restriction to flat formulas comes mainly from this difference, and lifting the flatness restriction seems
hard.

5

Sufficient Conditions for Time Staging

We present some theoretical analyses of the performance of time staging that indicate to which classof systems the time-staged approach can apply. We give some sufficient conditions under which theapproach is guaranteed to work. However, it should be noted that it is not necessary that a concrete
system satisfies these conditions strictly as these are rather restrictive. Nevertheless, we believe that users
with expert domain knowledge can judge whether their models satisfy these conditions approximately.
This way our results provide those users with “rules of thumb.”
As we discussed in the last paragraph of §2, the potential performance advantage by time staging
comes from the reduction of search spaces from |U|K to K · |U|. Here U is the set of potential input
segments for each stage, and K is the number of stages. This advantage comes at the risk of missingout some error input signals. The following basic condition (3), that we call incremental falsification,
ensures that there is no such risk. More precisely, we can decompose the “best” input signal u into a firststage u1 and its remainder u2 such that the entire falsification problem (left hand side) is solved by greedy
optimization of the initial segment (inner arg minu1 ), and subsequent optimization of the continuation(outer minu2 ). For all choices of T1 , T2 with ranges u : [0, T1 + T2 ] → Rm and ui : [0, Ti ] → Rm :
 z
r 

minJM (u), ϕK = min M arg minJM (u1 ), ϕK · u2 , ϕ
u

u2

(3)

u1

Algorithm 2 repeatedly unfolds (3) by picking constant T1 = T /K where T is the time horizon and K is
the number of stages. The rest of this section is devoted to the search for concrete sufficient conditionsfor (3).

10

Time-Staging Enhancement of Hybrid System Falsification

Monotone Systems and Ceiling Specifications We formalize the time monotonicity property in §2.
That it implies incremental falsification (3) can be easily proved.
Definition 5.1 (time-monotone falsification problem). A system model M and an STL formula ϕ aresaid to constitute a time-monotone falsification problem if, for any input signals u1 , u01 : [0, T1 ] → Rm andu2 : [0, T2 ] → Rm , JM (u1 ), ϕK ≤ JM (u01 ), ϕK implies JM (u1 · u2 ), ϕK ≤ JM (u01 · u2 ), ϕK.
We investigate yet more concrete conditions that ensures time monotonicity. The following condition
on system models is assumed in the example of §2.

Definition 5.2 (monotone system, ceiling specification). Let x be a variable (for output). A system model
M is said to be monotone in x if, for each u1 , u01 : [0, T1 ] → RM and u2 : [0, T2 ] → RM , M (u1 )(T1 )(x) ≤M (u01 )(T1 )(x) implies M (u1 · u2 )(T1 + T2 )(x) ≤ M (u01 · u2 )(T1 + T2 )(x).
An STL formula of the form 2(x < c), where x is a variable and c ∈ R is a constant, is called aceiling formula.
One can speculate that a monotone system and a ceiling specification 2(x < c), like those in §2,
constitute a time-monotone falsification problem. The speculation is not true, unfortunately; a counterexample is easily constructed using a model M whose output signal is not increasing. We can instead
show the following weaker property.
Definition 5.3 (truncated time monotonicity). A system model M and an STL formula ϕ constitute a
truncated time-monotone falsification problem if, for any input u1 , u01 : [0, T1 ] → Rm and u2 : [0, T2 ] →Rm , JM (u1 ), ϕK ≤ JM (u01 ), ϕK implies existence of T ∈ (0, T1 ] such that JM ((u1 |[0,T ] ) · u2 ), ϕK ≤JM ((u01 |[0,T ] ) · u2 ), ϕK .
Proposition 5.4. Let M be a model monotone in x, and ϕ ≡ 2(x < c) . Then M and ϕ constitute a
truncated time-monotone falsification problem.
The proof, in Appendix C.1, constructs a concrete choice of T in Def. 5.3. Specifically it is theinstant T ∈ [0, T1 ] in which the robustness JM (u1 |[0,T ] ), ϕK is minimum. In the scenario of §2 this is theinstant that the vehicle speed is in its peak. Note that truncated time monotonicity does not guarantee(K−1)T
incremental falsification as per (3), but it implies that the current rigid time staging at 0, KT , 2T
K ,...,
K
is not optimal. These theoretical considerations suggest potential improvement of the staged procedurein Def. 4.1 with adaptive choice of stages, which is left for future work.
Stateless Systems and Reachability Specifications Here is another sufficient condition.
Definition 5.5 (stateless system, reachability formula). A system model M is said to be stateless if,
for any input signals u1 , u01 : [0, T1 ] → Rm and u2 : [0, T2 ] → Rm , we have M (u1 · u2 )|(T1 ,T2 ] = M (u01 ·u2 )|(T1 ,T2 ] .
An STL formula 3ψ, where ψ is modality-free, is called a reachability formula.
Note that being stateless is a sufficient but not necessary condition for M (u1 · u2 ) = M (u1 ) · M (u2 ).
Statelessness requires insensitivity to previous input prefixes, but a stateless system can still be sensitive
to time.
Proposition 5.6. Let M be a stateless system and ϕ be a reachability specification ϕ ≡ (3ψ). Then M
and ϕ satisfy the incremental falsification property (3).
A proof is easy. A typical situation in which we would appeal to Prop. 5.6 is when: the specification is3(x < c1 ∨ x > c2 ) (which can be hard to falsify if c1 < c2 are close); and the system is already in its
stable state (so that its behavior does not depend much on what happened during the transient phase). Our
experiments in §6 demonstrate that time staging can drastically improve performance in such settings.

G. Ernst, I. Hasuo, Z. Zhang & S. Sedwards

11

Table 1:
Experimental results. Each column shows how many falsification trials succeeded(out of 20), and the average runtime. S1: 2[0,30] (v < 120). S2: 2[0,30] (g = 3 → v ≥ 30).
S3: 3[10,30] (v ≤ vmin ∨ v ≥ vmax ), where: vmin = 50, vmax = 60 (easy); vmin = 53, vmax = 57 (hard).
S4: 2[0,10] (v < v) ∨ 3[0,30] (ω > ωmax ), where: vmin = 80, ωmax = 4500 (easy); vmin = 50, ωmax = 2700
(mid); vmin = 50, ωmax = 2520 (hard). The specification S for the Abstract Fuel Control model is¬(3[t1 ,t2 ] [0,t 0 ] (AF − AF ref > δ ∗ 14.7)), where: t1 = 0, t2 = 6, t 0 = 3, δ = 0.07 (init); t1 = 6, t2 = 26,
t 0 = 4, δ = 0.01 (stable). Starred numbers 0* or 20* indicate that GNM is deterministic so all trials yield
the same result.
model
Automatic Transmission
Abst. Fuel Ctrl.
spec.
S1
S2
S3 easy
S3 hard
S4 easy
S4 mid
S4 hard
S initS stablealgorithm time #/20 time #/20 time #/20 time #/20 time #/20 time #/20 time #/20 time #/20 time #/20
CMA-ES 27s 20 5s 20 39s 14 57s
0 32s 16 37s
9 59s
0 49s
0 82s
1
+TS 52s 15 15s 16
9s 19 23s 11 15s 14 14s 14 24s
3 30s
0 42s
1
+A-TS 41s 18 15s 17
9s 16 21s 10 26s 14 22s 14 20s
5 26s
0 41s
0
SA 50s
5 43s
7 37s
9 55s
0 35s
6 36s
9 47s
5 51s
0 76s
2
+TS 37s 20 33s 16 11s 19 33s
8 21s 14 25s 13 51s
0 47s
1 54s
7
+A-TS 34s 20 18s 17
9s 18 26s
4 16s 18 21s 11 30s
2 34s
0 42s
5
GNM
6s 20* 61s 0* 56s 0* 55s 0* 43s 0* 46s 0* 53s 0* 50s 0* 86s 0*+TS 42s 20* 15s 20* 13s 20* 25s 20* 11s 20* 45s 0* 52s 0* 30s 20* 20s 20*+A-TS 20s 20* 16s 20* 10s 20* 26s 20* 13s 20* 45s 0* 43s 0* 37s 0* 19s 20*

Corner Samples for Global Nelder-Mead The reduction of search spaces from |U|K to K · |U| has its
analogue in the number of corner samples in Breach with global Nelder-Mead (lines 2–4 of Algorithm 1,
see the last paragraph of §3). Originally the number of corner samples is 2K·M , where K is the numberof control points and M is the number of input values. By introducing K time stages, the total number ofcorner samples is reduced to K · 2M .

6

Experiments

We compare the success rate and time consumption of the proposed method. The benchmarks here
use automotive Simulink models that are commonly used in the falsification literature. Specifications arechosen taking the deliberations of §5 into account, namely with ceiling specifications (Def. 5.2, including
the example of §2), a reachability specification (Def. 5.5) and a combination thereof.
The base line is Algorithm 1 implemented by Breach [8]. The methods proposed in §4 are implemented on top of Breach: the time-staged Algorithm 2 (TS), and the adaptive strategy (A-TS, the one
described after Def. 4.1). All three algorithms (plain, TS, A-TS) are combined with different optimization solvers: CMA-ES, simulated annealing (SA), global Nelder-Mead (GNM), obtaining a total of nineconfigurations.
The results in Table 1 indicate that both success rate and runtime performance are significantly improved by time staging, often finding counterexamples when non-staged Breach fails (e.g. columns S3
hard and S init). Furthermore, we see that while the adaptive algorithm (A-TS) does not necessarily leadto a higher success rate in comparison to the time-staged one (TS), it gives yet another runtime performance improvement. However, as discussed in detail in §6, there is no overall best algorithm, and timestaging affects the optimization algorithms differently depending on the problem.
Benchmarks Automatic Transmission is a Simulink model that was proposed as a benchmark for falsification in [15]. It has input values throttle ∈ [0, 100] and brake ∈ [0, 325], and outputs the car’s speed v,

12Time-Staging Enhancement of Hybrid System Falsification

the engine rotation ω, and the selected gear g.
With this model we consider five specifications S1–5. The first two are ceiling ones. Specification
S1 2[0,30] (v < 120) (cf. the example in §2) states the speed be always below a threshold. This property
is easily falsified with throttle = 100. Specification S2 2[0,30] (g = 3 → v ≥ 30) states that it is notpossible to drive slowly in a high gear. A falsifying trajectory first has to speed up to reach this gear andsubsequently roll out until speed falls below the threshold. This latter part of the trajectory can again
be seen as a ceiling specification. Note that this property is interesting because the robustnes does notprovide any guidance unless gear 3 has been entered by the system.
Specification S3 is a reachability problem, 3[10,30] (v ≤ vmin ∨ v ≥ vmax ), that encodes the search fora trajectory that keeps the speed between a lower and upper bound. The falsification problem consists of
two sub-challenges: 1) hitting this speed interval precisely after an initial acceleration up to 10s simulated
time; and 2) maintaining a correct speed till the time horizon. This suggests that a natural decompositionof the problem can indeed be achieved by separating these two aspects in time.
Specification S4 2[0,10] (vmin < v) ∨ 3[0,30] (ω > ωmax ) expresses that speed vmin can only be reachedwith an engine rotation exceeding a threshold ωmax . This specification is mentioned in [15] and evaluatedin e.g., [3,4], too. To falsify, a trajectory must be found that reaches speed v early with an engine rotation
lower than ωmax . The difficulty increases with higher vmin and lower ωmax , respectively. The formula
represents the mixture of ceiling and reachability specifications.
The second system model is Abstract Fuel Control from [17]. It takes two input values, pedal angle(from [0, 61.1]) and engine speed (from [0, 1100]); it outputs air-fuel ratio AF, which influences fuelefficiency and performance of the car. The value of AF is expected to be close to a reference value AF ref .
According to [17], this setting corresponds to the so-called normal mode, where AF ref = 14.7 is constant.
We used the specification ¬(3[t1 ,t2 ] [0,t 0 ] (AF − AF ref > δ ∗ 14.7)): the air-fuel ratio does not deviate
from an acceptable range for more than t 0 seconds. We evaluated this specification with two parameter
sets: the initial period with a larger error margin, and the stable period with a smaller margin. See Table 1
for parameter values.
Experimental Setup and Results For the experiments with the Automatic Transmission model, theinput signals were piecewise constant with 5 control points. The time horizon was T = 30. The parameters outlined in §4 were as follows: the maximum number of samplings for each plain (non-staged)
falsification trial was 150 (initial and optimization samplings combined). In the time-staged (TS) trials,
we make the number of stages coincide with that of control points. Analogously, the sampling budget perstage was set to 30 for K = 5 stages, resulting in overall 150 samplings. The adaptive algorithm (A-TS)
stall = 30/2 = 15 per each of five stages. The experiments with the Abstract Fuelran with the threshold Nmax
Control model were run up to the time horizon T = t2 + t 0 where t2 and t 0 are as in Table 1. We used
three and five stages, respectively, for the initial and stable specifications. These again coincide with thenumber of control points. The TS algorithms conducted 30 samplings in each stage.
The experiments ran Breach version 1.2.9 and MATLAB R2017b on an Amazon EC2 c4.8xlarge
instance with a 36 core Intel(R) Xeon(R) CPU (2.90GHz) and 58G of main memory. However, we did
not use the opportunity to parallelize, and the time reported is in the same order of magnitude as that ofa modern desktop workstation.
The results are shown in Table 1. They are grouped by the underlying stochastic optimization algorithm: CMA-ES, simulated annealing (SA) and global Nelder-Mead (GNM). In each group, we compare
plain (unstaged) Breach to the time-staged (TS) and the adaptive time-staged (A-TS) ones. We compare
average runtimes (lower is better) and the success rate (higher is better), aggregated over 20 falsifica-

G. Ernst, I. Hasuo, Z. Zhang & S. Sedwards

13

tion trials for each configuration. Those good results which deserve attention are highlighted in bold.
Note that the implementation of the global Nelder-Mead algorithm in Breach uses a deterministic sourceof quasi-randomness (Halton sequences), which implies that whether GNM finds a counterexample isconsistent across all trials (marked with an asterisk ∗).
Discussion Focusing on the Automatic Transmission model first, we see that CMA-ES works well for
S1, although GNM performs even better (6s, supposedly because it uses corner samples, see §3). Timestaging introduces overhead to CMA-ES and GNM, because each stage is optimized individually. In
contrast, simulated annealing (SA) benefits from time staging for the two ceiling specifications S1–2.
We presume that since SA emphasizes exploration, it benefits from exploitation added by time staging(cf. §2).
The second specification S2 is slightly more complex: before gear 3 is reached, there is no guidancefrom the robustness semantics, because J , g = 3K = −∞ masks any quantitative information on v. Hence,falsifying this property needs some luck during the collection of initial samples in Algorithm 1. CMAES apparently exploits this, see top of column S2 of Table 1. Considering the other algorithms, SA
and GNM, both benefit from time staging: exploitation of time causality prevents these good trajectory
prefixes from being discarded accidentally once the required gear is reached (cf. Fig 2).
The results for S3 are evaluated with two different choices of parameters. The harder instance wasfalsified by the time-staged algorithms only, which can likely be attributed to the flattening of the search
space from size |U|K to K · |U| (§5).
S4 is evidently harder than the previous ones. Time staging improves performance in a generaltendency but not in all cases (SA for S4 hard).
The results for the Abstract Fuel Control model (the last two columns in Table 1) show that the
time-staged algorithms boost the ability to falsify some rare events. The specification for the initial stage
where AF is still unstable (S init) can be considered a rare event since all the three non-staged algorithms
failed to falsify it. Time-staged SA and time-staged GNM managed to find error inputs. In the lastcolumn (stable period) is remarkable, too, where success rate and run time of SA and GNM significantly
improved.
Overall, while the performance of the non-staged algorithms suffers from tightening the bounds, thetime-staged versions are able to find falsifying trajectories with good success rates while at the same time
exhibiting significantly shorter runtimes.

7

Related Work

Falsification is a special case of search-based testing, so considerable research efforts have been madetowards coverage [3, 7, 20]. The benefits of coverage in falsification guarantees are twofold. Firstly, they
indicate confidence for correctness in case no counterexamples are found. Paired with sound robustness
estimates for simulations, one can cover a an infinite parameter space with finitely many simulations.
C2CE [13] is a recent tool that computes approximations of reachable states using such an approach.
Secondly, coverage can be utilized for a better balance between exploration and exploitation: stochastic
optimization algorithms can be called in an interleaved manner, in which coverage guides further exploration. The approach based on Rapidly-Exploring Random Trees [11] puts an emphasis on explorationby achieving high coverage of the state space. In their algorithm, robustness-guided hill-climbing optimization plays a supplementary role. Compared to these works, our current results go in an orthogonal
direction, by utilizing time causality to enhance exploitation. The so-called multiple-shooting approach14Time-Staging Enhancement of Hybrid System Falsification

to falsification [24] can be seen of a generalization of RRTs. It consists of: an upper layer that searches
for an abstract error trace given by a succession of cells; and a lower layer where an abstract error trace
is concretized to an actual error trace by picking points from cells. The approach can discover falsifying
traces by backwards search from a goal region, but needs to concatenate partial traces with potential
gaps, which can fail. Furthermore it is unclear how to extend it to general STL specifications. A surveyof simulation based approaches has been done by Kapinski et al. [18].
Monotonicity has been exploited in different ways for falsification. Robust Neighborhood Descent [1,2] (RED) searches for trajectories incrementally, restarting the search from points of low robustness.
Descent computation of RED assumes explicit derivatives of the dynamics to guarantee convergence to(local) minima. It is the same principle underlying Prop. 5.4) and our experiments indicate that thisprinciple is useful for black-box optimization, too. In [2], RED is paired with simulated annealing
to combine local and global search and to account for more exploration. Doing so for our present work
remains to be done in the future. In [16], Hoxha et al. mine parameters θ under which specifications φ [θ ]are satisfied or falsified by the system. They show that the robust semantics of formulas is monotonein θ and use that fact to tighten such parameters. This is orthogonal to this work as it does not use
monotonicity of the system itself. Kim et al. [19] use an idea similar to [16] to partition specifications
into upper bounds and lower ceilings. However, instead of robustness-guided optimization they use
exhaustive exploration of the input space in a way that in turn requires that the system dynamics ismonotone in the choice of each input at each time point. This is different from our Def 5.1 of timemonotonicity that aims at incrementally composing good partial choices.
The recent work [12] introduces a compositional falsification framework, focusing on those systems
which include machine-learning (ML) components that perform tasks such as image recognition. Whilethe current work aims at the orthogonal direction of finding rare counterexamples, we are interested inits combination with the results in [12], given the increasingly important roles of ML algorithms in CPS.

8

Conclusions and Future Work

We have introduced and evaluated the idea of time staging to enhance falsification for hybrid systems.
The proposed method emphasizes exploitation over exploration as part of stochastic optimization. As
there is no single algorithm that fits every problem (as a consequence of having no free lunch [23]),
having a variety of methods at disposal permits the user of a system to choose the one suitable for the
problem at hand. We have shown that the proposed approach is a good fit for problems that suitableexhibit time-causal structures, where it significantly outperforms non-staged algorithms.
Two obvious directions for future work have been pointed out already. Instead of just picking thebest trajectory for each stage, it might be beneficial to retain a few, potentially diverse ones in the spiritof evolutionary algorithms (§2). For example, it would be interesting to explore the space between thiswork on one hand and coverage-driven rapidly-exploring random trees.
Another idea is to discover time stages adaptively (§5, the discussion after Prop. 5.4). For the experiments presented here, we chose to set uniformly fixed stages, which runs the risk of either being toocoarse grained (missing some falsifying input), or being too fine grained (wasting analysis time).
Finally, another future direction is to explore variations of robust semantics to mitigate discrete
propositions like g = 3 (§6), for example using averaging modalities [4]. Other t-norms than min/max forthe semantics of conjunction/disjunction could preserve more information from different subformulas.

G. Ernst, I. Hasuo, Z. Zhang & S. Sedwards

15

References[1] H. Abbas, A. Winn, G. Fainekos, and A. A. Julius. Functional gradient descent method for metric temporal
logic specifications. In American Control Conference (ACC), 2014, pages 2312–2317. IEEE, 2014.
[2] H. Y. Abbas. Test-based falsification and conformance testing for cyber-physical systems. Arizona State
University, 2015.
[3] A. S. Adimoolam, T. Dang, A. Donzé, J. Kapinski, and X. Jin. Classification and coverage-based falsificationfor embedded control systems. In R. Majumdar and V. Kuncak, editors, Computer Aided Verification - 29th
Int. Conf., CAV 2017, volume 10426 of LNCS, pages 483–503. Springer, 2017.
[4] T. Akazaki and I. Hasuo. Time robustness in MTL and expressivity in hybrid system falsification. In
D. Kroening and C. S. Pasareanu, editors, Computer Aided Verification - 27th Int. Conf., CAV 2015, volume 9207 of LNCS, pages 356–374. Springer, 2015.
[5] Y. Annpureddy, C. Liu, G. E. Fainekos, and S. Sankaranarayanan. S-taliro: A tool for temporal logic falsification for hybrid systems. In P. A. Abdulla and K. R. M. Leino, editors, Tools and Algorithms for theConstruction and Analysis of Systems - 17th Int. Conf., TACAS 2011, volume 6605 of LNCS, pages 254–257.
Springer, 2011.
[6] A. Auger and N. Hansen. A restart CMA evolution strategy with increasing population size. In Proceedingsof the IEEE Congress on Evolutionary Computation, CEC 2005, pages 1769–1776. IEEE, 2005.
[7] J. V. Deshmukh, X. Jin, J. Kapinski, and O. Maler. Stochastic local search for falsification of hybrid systems.
In B. Finkbeiner, G. Pu, and L. Zhang, editors, Automated Technology for Verification and Analysis - 13th
Int. Symp., ATVA 2015, volume 9364 of LNCS, pages 500–517. Springer, 2015.
[8] A. Donzé. Breach, A toolbox for verification and parameter synthesis of hybrid systems. In T. Touili,
B. Cook, and P. B. Jackson, editors, Computer Aided Verification, 22nd Int. Conf., CAV 2010, volume 6174
of LNCS, pages 167–170. Springer, 2010.
[9] A. Donzé, T. Ferrère, and O. Maler. Efficient robust monitoring for STL. In N. Sharygina and H. Veith,
editors, Computer Aided Verification - 25th Int. Conf., CAV 2013, volume 8044 of LNCS, pages 264–279.
Springer, 2013.
[10] A. Donzé and O. Maler. Robust satisfaction of temporal logic over real-valued signals. In K. Chatterjee andT. A. Henzinger, editors, Formal Modeling and Analysis of Timed Systems - 8th Int. Conf., FORMATS 2010,
volume 6246 of LNCS, pages 92–106. Springer, 2010.
[11] T. Dreossi, T. Dang, A. Donzé, J. Kapinski, X. Jin, and J. V. Deshmukh. Efficient guiding strategies fortesting of temporal properties of hybrid systems. In K. Havelund, G. J. Holzmann, and R. Joshi, editors,
NASA Formal Methods - 7th Int. Symp., NFM 2015, volume 9058 of LNCS, pages 127–142. Springer, 2015.
[12] T. Dreossi, A. Donzé, and S. A. Seshia. Compositional falsification of cyber-physical systems with machinelearning components. In C. Barrett, M. Davies, and T. Kahsai, editors, NASA Formal Methods - 9th Int.
Symp., NFM 2017, volume 10227 of LNCS, pages 357–372, 2017.
[13] P. S. Duggirala, S. Mitra, M. Viswanathan, and M. Potok. C2E2: A verification tool for stateflow models. In
C. Baier and C. Tinelli, editors, Tools and Algorithms for the Construction and Analysis of Systems - 21st Int.
Conf., TACAS 2015, volume 9035 of LNCS, pages 68–82. Springer, 2015.
[14] G. E. Fainekos and G. J. Pappas. Robustness of temporal logic specifications for continuous-time signals.
Theor. Comput. Sci., 410(42):4262–4291, 2009.
[15] B. Hoxha, H. Abbas, and G. E. Fainekos. Benchmarks for temporal logic requirements for automotive
systems. In G. Frehse and M. Althoff, editors, 1st and 2nd Int. Workshops on Applied veRification forContinuous and Hybrid Systems, ARCH@CPSWeek 2014 and 2105, volume 34 of EPiC Series in Computing,pages 25–30. EasyChair, 2014.
[16] B. Hoxha, A. Dokhanchi, and G. E. Fainekos. Mining parametric temporal logic properties in model-based
design for cyber-physical systems. STTT, 20(1):79–93, 2018.

16

Time-Staging Enhancement of Hybrid System Falsification[17] X. Jin, J. V. Deshmukh, J. Kapinski, K. Ueda, and K. R. Butts. Powertrain control verification benchmark.
In M. Fränzle and J. Lygeros, editors, 17th International Conference on Hybrid Systems: Computation andControl (part of CPS Week), HSCC’14, Berlin, Germany, April 15-17, 2014, pages 253–262. ACM, 2014.
[18] J. Kapinski, J. V. Deshmukh, X. Jin, H. Ito, and K. Butts. Simulation-based approaches for verificationof embedded control systems: an overview of traditional and advanced modeling, testing, and verification
techniques. IEEE Control Systems, 36(6):45–64, 2016.
[19] E. S. Kim, M. Arcak, and S. A. Seshia. Directed specifications and assumption mining for monotone dynamical systems. In A. Abate and G. E. Fainekos, editors, Proceedings of the 19th International Conference on
Hybrid Systems: Computation and Control, HSCC 2016, Vienna, Austria, April 12-14, 2016, pages 21–30.
ACM, 2016.
[20] J. Kurátko and S. Ratschan. Combined global and local search for the falsification of hybrid systems. In
A. Legay and M. Bozga, editors, Formal Modeling and Analysis of Timed Systems - 12th Int. Conf., FORMATS 2014, volume 8711 of LNCS, pages 146–160. Springer, 2014.
[21] O. Maler and D. Nickovic. Monitoring temporal properties of continuous signals. In Y. Lakhnech and
S. Yovine, editors, Formal Techniques, Modelling and Analysis of Timed and Fault-Tolerant Systems, Joint
Int. Confs. on Formal Modelling and Analysis of Timed Systems, FORMATS 2004 and Formal Techniques
in Real-Time and Fault-Tolerant Systems, FTRTFT 2004, volume 3253 of LNCS, pages 152–166. Springer,
2004.
[22] D. Ulus, T. Ferrère, E. Asarin, and O. Maler. Online timed pattern matching using derivatives. In M. Chechik
and J. Raskin, editors, Tools and Algorithms for the Construction and Analysis of Systems - 22nd Int. Conf.,
TACAS 2016, volume 9636 of LNCS, pages 736–751. Springer, 2016.
[23] D. Wolpert and W. G. Macready. No free lunch theorems for optimization. IEEE Trans. Evolutionary
Computation, 1(1):67–82, 1997.
[24] A. Zutshi, J. V. Deshmukh, S. Sankaranarayanan, and J. Kapinski. Multiple shooting, cegar-based falsification for hybrid systems. In T. Mitra and J. Reineke, editors, 2014 International Conference on Embedded
Software, EMSOFT 2014, New Delhi, India, October 12-17, 2014, pages 5:1–5:10. ACM, 2014.

G. Ernst, I. Hasuo, Z. Zhang & S. Sedwards

A

17

STL Semantics for Time-Bounded Signals

Definition A.1 (robust semantics for time-bounded signals). Let T ∈ R>0 , w : [0, T ] → RN be a timebounded signal, and ϕ be an STL formula. We define the robustness Jw, ϕKT ∈ R ∪ {∞, −∞} of w withrespect to ϕ as follows, by induction. Here the superscript T is an annotation that designates the time
horizon.
Jw, f (x1 , . . . , xn ) > 0KT := f w(0)(x1 ), . . . , w(0)(xn )Jw, ⊥KT := −∞Jw, ¬ϕKT := −Jw, ϕKT
Jw, ϕ1 ∧ ϕ2 KT := Jw, ϕ1 KT u Jw, ϕ2 KTlG
T −t 0 
0T −t
Jw, ϕ1 UI ϕ2 KT :=Jwt , ϕ2 K u
Jwt , ϕ1 K
t∈I∩[0,T ]t 0 ∈[0,t)too.

The Boolean semantics |=, found e.g. in [10], allows a similar adaptation to time-bounded signals,

B

Brzozowski Derivative of Flat STL Formulas

In the time-staged falsification procedure we often encounter the following situation: an STL formulaϕ and a signal v : [0, T ] → RN are fixed; and we have to compute robustness Jv · v0 , ϕK for a number ofdifferent signals v0 : [0, T 0 ] → RN . To aid such computation, a natural idea is to use a syntactic construct∂v ϕ of (Brzozowski) derivative. It should be compatible with robust semantics in the sense that Jv ·v0 , ϕK = Jv0 , ∂v ϕK, reducing the computation of the LHS to that of the RHS.
Similar use of derivatives is found e.g. in [22]. The settings are different, though: Boolean semantics
is used in [22] while we use quantitative robust semantics. In fact, the definition of derivatives in thissection focuses on flat formulas (i.e. free from nested modalities). This restriction is mandated by thequantitative semantics, as our proof later suggests. Anyway, the definitions and results in this section are
new to the best of our knowledge.
We need the following extension of STL syntax.
Definition B.1 (extended STL). We extend the syntax of STL (Def. 3.4) by atomic propositions cr
for each r ∈ R. The robust semantics in Def. 3.5 (and that in Def. A.1 in Appendix A) is extended
accordingly: Jw, cr K := r.
Intuitively cr is an atomic proposition that constantly returns the robustness value r.

Definition B.2 (derivative). Let T ∈ R>0 , and v : [0, T ] → RN be a time-bounded signal. For eachextended STL formula ϕ, we define its derivative ∂v ϕ by v by the following induction.
∂v f (~x) > 0 :≡ cJv, f (~x)>0K∂v cr :≡ cr∂v ⊥ :≡ ⊥∂v (¬ϕ) :≡ ¬∂v ϕ∂v (ϕ1 ∧ ϕ2 ) :≡ (∂v ϕ1 ) ∧ (∂v ϕ2 )
∂v (ϕ1 UI ϕ2 ) :≡ cJv,ϕ1 UI ϕ2 K ∨ (cJv,2ϕ1 K ∧ ϕ1 ) UI−T ϕ2

Here the interval I −T is obtained from I by shifting both of its endpoints earlier by T , such as [a, b]−T =[a − T, b − T ].
Definition B.3 (flat STL formula). An STL formula ϕ is flat if it does not have nested temporal modal
operators. This means: if ϕ1 UI ϕ2 is a subformula of ϕ, then neither ϕ1 nor ϕ2 contains U.
Proposition B.4. Let T ∈ R>0 , v : [0, T ] → RN be a signal, and ϕ be a flat STL formula. We have, foreach T 0 ∈ R>0 and v0 : [0, T 0 ] → RN , Jv0 , ∂v ϕK = Jv · v0 , ϕK.

18Time-Staging Enhancement of Hybrid System Falsification

Proof. By induction on the construction of ϕ. Most equalities below follow from the definition of ∂ andthat of J K.

Jv0 , ∂v f (~x) > 0 K = Jv0 , cJv, f (~x)>0K K = Jv, f (~x) > 0K = Jv · v0 , f (~x) > 0K
Jv0 , ∂v cr K = Jv0 , cr K = r = Jv · v0 , cr K

Jv0 , ∂v ⊥K = Jv0 , ⊥K = −∞ = Jv · v0 , ⊥K

I.H.

Jv0 , ∂v (¬ϕ)K = Jv0 , ¬∂v ϕK = −Jv0 , ∂v ϕK = −Jv · v0 , ϕK = Jv · v0 , ¬ϕK

Jv0 , ∂v (ϕ1 ∧ ϕ2 )K = Jv0 , (∂v ϕ1 ) ∧ (∂v ϕ2 )K = Jv0 , ∂v ϕ1 K u Jv0 , ∂v ϕ2 K
I.H.

= Jv · v0 , ϕ1 K u Jv · v0 , ϕ2 K = Jv · v0 , ϕ1 ∧ ϕ2 K

Here is a nontrivial case.
Jv0 , ∂v (ϕ1 UI ϕ2 )K= Jv0 , cJv,ϕ1 UI ϕ2 K K t Jv0 , (cJv,2ϕ1 K ∧ ϕ1 ) UI−T ϕ2 K
= Jv, ϕ1 UI ϕ2 K t=

Gt∈I∩[0,T ]

t
(∗)

=

t 00 ∈I∩[T,T +T 0 ]t∈I∩[0,T ]

=

l

t0

t 0 ∈[0,t)t 00 ∈I∩[T,T +T 0 ]Gt∈I∩[0,T +T 00 ]00J(v · v0 )t , ϕ2 K ulJ(v · v0 )t , ϕ2 K ult 0 ∈[0,t)l0J(v · v0 )t , ϕ1 K

t 0 ∈[T,T +t)t 0 ∈[0,T ]
t0

l

0

Jv0t , ϕ1 K

l


0
0
J(v · v0 )t , ϕ1 K u
J(v · v0 )t , ϕ1 KJ(v · v0 ) , ϕ1 K

t 0 ∈[0,t)
00

l


0
J(v · v0 )t , ϕ1 K

t 0 ∈[0,t)l0Jvt , ϕ1 K u

t 0 ∈[0,T ]lJ(v · v0 )t , ϕ2 K u= Jv · v0 , ϕ1 UI ϕ2 Kl

Jv0t , ϕ2 K uJ(v · v0 )t , ϕ2 K u
G

Jv0t , ϕ2 K u Jv, 2ϕ1 K uJv , ϕ1 K

J(v · v0 )t , ϕ2 K u

G

G

t

Jvt , ϕ2 K ut∈(I−T )∩[0,T 0 ]t∈I∩[0,T ]=t∈(I−T )∩[0,T 0 ]

G

G

t

G

t 0 ∈[T,t 00 )0J(v · v0 )t , ϕ1 K

t 0 ∈[0,t 00 )

0J(v · v0 )t , ϕ1 K

t 0 ∈[0,t)In (∗) we used the following facts. Firstly, for a formula ψ without temporal operators, we have Jv, ψK =Jv · v0 , ψK. Secondly, if v’s domain is [0, T ] and t ∈ [0, T ], then vt · v0 = (v · v0 )t .
Note that the flatness assumption on ϕ is crucially used in the proof step. Modifying Def. 4.2 inorder to accommodate nested modalities seems hard, after analyzing the proof step (∗).

G. Ernst, I. Hasuo, Z. Zhang & S. Sedwards

C

Omitted Proofs

C.1

Proof of Prop. 5.4

19

Proof. By the definitions we have, for each input signal u : [0, T ] → RM ,l
JM (u), 2(x < c)K =c − M (u)(t)(x) .
t∈[0,T ]Therefore the assumption JM (u1 ), ϕK ≤ JM (u01 ), ϕK expands tollc − M (u1 )(t)(x) ≤c − M (u01 )(t)(x) .
t∈[0,T1 ](4)t∈[0,T1 ]The first infimum in the above is taken over a compact domain [0, T1 ]; therefore there exists T ∈ [0, T1 ]that achieves the infimum. Let T be such a real number. The following is obvious.
llc − M (u1 )(t)(x) =c − M (u1 )(t)(x) = c − M (u1 )(T )(x)t∈[0,T1 ]≤lt∈[0,T ]c − M (u01 )(t)(x) ≤t∈[0,T1 ]lc − M (u01 )(t)(x) .

(5)t∈[0,T ]Another immediate consequence, derived using the causality of M (Def. 3.2), isc − M (u1 |[0,T ] )(T )(x) ≤ c − M (u01 |[0,T ] )(T )(x) .

(6)

Our goal is to show JM (u1 |[0,T ] · u2 ), ϕK ≤ JM (u01 |[0,T ] · u2 ), ϕK.
JM (u01 |[0,T ] · u2 ), 2(x < c)Kl=c − M (u01 |[0,T ] · u2 )(t)(x)t∈[0,T +T2 ]=lc − M (u01 )(t)(x) ut∈[0,T ]≥≥lc − M (u1 )(t)(x) ut∈[0,T ]lc − M (u1 )(t)(x) ut∈[0,T ]= ···lc − M (u01 |[0,T ] · u2 |[0,t−T ] )(t)(x)(∗)

t∈(T,T +T2 ]lc − M (u01 |[0,T ] · u2 |[0,t−T ] )(t)(x) by (4)t∈(T,T +T2 ]lc − M (u1 |[0,T ] · u2 |[0,t−T ] )(t)(x)(†)

t∈(T,T +T2 ]= JM (u1 |[0,T ] · u2 ), 2(x < c)K.

In the above we heavily used the causality of M (Def. 3.2). For example, in the step (∗) above, causality
is used in deriving M (u01 |[0,T ] · u2 )(t) = M (u01 )(t). In the step (†) we applied the monotonicity of M tothe signals u1 |[0,T ] , u01 |[0,T ] and u2 |[0,t−T ] . Note that (6) allows to do so.