Optimization-Based Model Checking
and Trace Synthesis for Complex STL
Specifications
Sota Sato1,3(B) , Jie An1,4(B) , Zhenya Zhang1,2(B) ,and Ichiro Hasuo1,3(B)1National Institute of Informatics, Tokyo, Japan{sotasato,jiean,hasuo}@nii.ac.jp
2
Kyushu University, Fukuoka, Japanzhang@ait.kyushu-u.ac.jp
3
SOKENDAI (The Graduate University for Advanced Studies), Tokyo, Japan
4
Institute of Software, Chinese Academy of Sciences, Beijing, China

Abstract. Techniques of light-weight formal methods, such as monitoring and falsiﬁcation, are attracting attention for quality assuranceof cyber-physical systems. The techniques require formal specs, however,
and writing right specs is still a practical challenge. Commonly one relies
on trace synthesis—i.e. automatic generation of a signal that satisﬁes agiven spec—to examine the meaning of a spec. In this work, motivatedby 1) complex STL specs from an automotive safety standard and 2) the
struggle of existing tools in their trace synthesis, we introduce a novel
trace synthesis algorithm for STL specs. It combines the use of MILP
(inspired by works on controller synthesis) and a variable-interval encoding of STL semantics (previously studied for SMT-based STL model
checking). The algorithm solves model checking, too, as the dual of tracesynthesis. Our experiments show that only ours has realistic performanceneeded for the interactive examination of STL specs by trace synthesis.

1

Introduction

Safety and quality assurance of cyber-physical systems (CPSs) is an importantand multifaceted problem. The pervasiveness and safety-critical nature of CPSs
makes the problem imminent and pressing; at the same time, the problem comeswith very diﬀerent ﬂavors in diﬀerent application domains, calling for diﬀerent
solutions. For example, in the aerospace domain, full formal veriﬁcation all theway up from the codebase seems feasible [33]. Such is a luxury that the automotive domain may not aﬀord, however, because of short product cycles, dependence on third-party (thus black-box) components, heterogeneous environmental
uncertainties, and ﬁerce competition (thus tight budget).
The authors are supported by ERATO HASUO Metamathematics for Systems Design
Project (No. JPMJER1603), the START Grant No. JPMJST2213, the ASPIRE grant
No. JPMJAP2301, JST. S.S. is supported by KAKENHI No. 23KJ1011, JSPS. Z.Z. is
supported by JSPS KAKENHI Grant No. JP23K16865 and No. JP23H03372.
c The Author(s) 2024

A. Gurfinkel and V. Ganesh (Eds.): CAV 2024, LNCS 14683, pp. 282–306, 2024.
https://doi.org/10.1007/978-3-031-65633-0_13

Optimization-Based Trace Synthesis for Complex STL Speciﬁcations

283

The above limitations in the automotive domain point, in the formal methods terms, to the absence of white-box system models. This has led to the ﬂourishof light-weight formal methods, such as monitoring [8], runtime veriﬁcation, andhybrid system falsiﬁcation [16]. These are logic-based methods that operate on
formal specifications, often given in signal temporal logic (STL) [24]. These methods give up comprehensive guarantee due to the absence of white-box systemmodels; yet their values in practical usage scenarios are widely acknowledged.
Trace Synthesis and Model Checking. In this paper, we are motivated bysome automotive instances of the trace synthesis problem: it asks to synthesize
an execution trace σ of a system M that satisﬁes a given STL speciﬁcation ϕ.
There are two major approaches to trace synthesis for CPSs.
One common approach is via hybrid system falsification [16]: here, we try
many input signals τ for M, iteratively modifying them in the direction ofsatisfying ϕ; the quantitative robust semantics of STL [17] serves as an objectivefunction that allows hill-climbing optimization. It is notable that the systemmodel M can be black-box : we do not need to know its internal working; it isenough to compute the execution trace M(τ ) under given input τ . Falsiﬁcation
has attracted a lot of interest especially in the automotive domain; see e.g. [16].
We take the other approach to trace synthesis, namely as the dual of themodel checking problem. Here model checking decides if, under any input τ , theexecution trace M(τ ) satisﬁes ϕ. Our choice of this approach may be puzzling—
it requires a white-box model M, but it is rare in the automotive domain.
Analyzing Speciﬁcations (Rather Than Models). Our choice of the model
checking approach to trace synthesis comes from the following basic scope of thepaper: we use trace synthesis to analyze the quality of specifications (specs).
This is in stark contrast with many falsiﬁcation tools whose scope is analyzing
models. There, a model M is extensive and complex (typically a Simulink modelof an actual product), and counterexample traces are used for “debugging” M.
In this paper, instead, a model M is simple and white-box (it can even be thetrivial model, where the input and output are the same), but a spec ϕ tends to becomplex. One typical usage scenario for our framework is when ϕ is a normative
rule—such as a law, a traﬃc rule, or a property required in an international
standard—in which case ϕ is imposed on many diﬀerent systems (e.g. diﬀerent
vehicle models). Then M should be a simple overapproximation of a variety ofsystems, rather than a detailed system model.
Another typical usage scenario of our framework is an early “requirement
development” phase of the V-model of the automotive system design. Here, engineers ﬁx specs that pin down the later development eﬀorts, in which those specs
get reﬁned and realized. They want to conﬁrm that the specs are sensible (e.g.
there is no mutual conﬂict) and faithful to their intentions. Since a system is yet
to be developed, a system model M cannot be detailed.

284

S. Sato et al.

Motivating Example. More speciﬁcally, the current work is motivated by the work [30] on formalizing disturbance scenarios in the ISO 34502 standard for automated driving vehicles. There, a vehi- Fig. 1. Rear-end near collicle dynamics model is simple (the scenarios should sion
apply to diﬀerent vehicle models—see above), but
STL formulas are complex. It is observed that existing algorithms have a hardtime handling the complexity of specs (see §6 for experiments). This motivated our current technical development, namely a trace synthesis algorithm
that exploits white-box models and MILP optimization for eﬃciency.
The following example illustrates the challenge encountered in [30].
Example 1.1 (rear-end near collision). We would like to express, in STL, arear-end near collision scenario for two cars. It refers to those driving situations
where a rear car Carr comes too close to a front car Carf . We assume a single-lanesetting (Fig. 1), so we can ignore lateral dynamics.
Consider the following STL formulas. Here, xf , vf , af are the variables for the
position, velocity, and acceleration of Carf ; the other variables are for Carr .
dangerdyn inv
trimming
RNC1

:≡
:≡
:≡
:≡

xf − xr ≤ 10
xf − xr ≥ 0 ∧ 2 ≤ vf ≤ 27 ∧ 2 ≤ vr ≤ 27 (♦danger) ⇒ ([0,0.2] ar ≥ 0.5) U danger
(dyn inv ∧ trimming) ∧ ♦[0,9] [0,1] danger(1)

The last formula RNC1 formalizes rear-end near collision; in particular, its subformula ♦[0,9] [0,1] danger requires that danger occurs within 9 s and persists
for at least one second.
The formula RNC1 comes with two auxiliary conditions: dyn inv andtrimming. We shall now exhibit their content and why they are needed. In fact,
these conditions arose naturally in the course of trace synthesis, the problem of
our focus.
Speciﬁcally, in [30], we conducted trace synthesis repeatedly in order to 1)
illustrate the meaning of STL speciﬁcations and 2) confirm that they reﬂect
informal intentions. The generated traces were animated for graphical illustration. This workﬂow is much like in the tool STLInspector [31].
The formula dyn inv imposes basic constraints on the dynamics of the cars.
In the trace synthesis in [30], without this basic constraint, we obtained a numberof nonsensical example traces in which a car warps and instantly passes the other,drives much faster than the legal maximum, and so on.
The formula trimming requires Carr to accelerate until danger occurs. It
was added to limit a generated trace to an interesting part. For example, a trace
can have danger only after a 8-s paciﬁc journey; animating this whole trace caneasily bore users. The condition trims such a trace to the part where Carr isaccelerating towards danger.

Optimization-Based Trace Synthesis for Complex STL Speciﬁcations

285

The dynamics model used in [30] is the following simple one:x˙f = vf , v˙f = af ;x˙r = vr , v˙r = ar .

(2)

This relates x, v and a in the spec (1). The double integrator model is certainly
simplistic, but it suﬃces the purpose in [30] of illustrating and conﬁrming specs.
Remark 1.2. In [30], after illustrating and conﬁrming STL specs through tracesynthesis, the ﬁnal goal was to use them for monitoring actual driving data.
Neither the dynamics model (2) nor the condition dyn inv is really relevant tomonitoring—actual driving data should comply with them anyway. In contrast,
trimming is important, in order to extract only relevant parts of the data.
Technical Solution: MILP-Based Trace Synthesis. We present a novel
trace synthesis algorithm. Note that it also solves the dual problem, namely
STL model checking. It originates from two recent lines of work: MILP-based
optimal control [14,28,29] and SMT-based STL model checking [7,23,34].
The controller synthesis techniques in [14,28,29] exploit mixed-integer linear
programming (MILP) for eﬃciency. The optimal control problem that they solve
can be specialized to our trace synthesis problem (detailed discussions comelater). But we found their capability of handling complex specs (as in Ex. 1.1)
limited, largely because of their constant-interval encoding to MILP.
We solve this challenge by our novel variable-interval encoding of the STL
semantics to MILP. It is inspired by the stable partitioning technique introducedin [7]: the technique is used in [7,23,34] for logical encoding towards SMT-basedmodel checking; we use it for numerical encoding to MILP. This way we will solve
the bounded trace synthesis problem—in the sense that variability of the truth
values of the relevant formulas is bounded—much like in [7,23,34]. For our MILP
encoding, however, we need special care since MILP does not accommodate strict
inequalities (partitions such as . . . , (γi−1 , γi ), {γi }, (γi , γi+1 ), . . . in [7] cannot be
expressed). We therefore use a novel technique called δ-stable partitioning.
Overall, our algorithm works as follows. We assume that a system model M
can be MILP-encoded, either exactly or approximately. Some model families are
discussed in §5. This assumption, combined with our key technique of variableinterval MILP encoding of STL, reduces trace synthesis to an MILP problem,
which we solve by Gurobi Optimizer [20]. We conduct experimental evaluation
to conﬁrm the scalability of our algorithm, especially for complex specs (§6).
Our algorithm is anytime (i.e. interruptible): even if the budget runs out
in the course of optimization, a best-eﬀort result (the trace that is the closest
to a solution so far) is obtained. A similar beneﬁt is there in case there is no
execution trace σ that satisﬁes the spec ϕ: we obtain a trace σ  that is the closest
to satisfy ϕ. Accommodation of parameters is another advantage thanks to ouruse of MILP; we exploit it for parameter mining for PSTL formulas. See §3.
Both controller synthesis techniques [14,28,29] and SMT-based model checking techniques [7,23,34] can be used for trace synthesis. The methodologicaldiﬀerences are discussed later in §1; experimental comparison is made in §6.

286

S. Sato et al.

Contributions and Organization. We summarize our contributions.
– We introduce an optimization-based algorithm for bounded trace synthesis for
STL specs. It assumes that a system model is white-box and MILP-encodable;
it also solves the dual problem (namely bounded model checking).
– As a key element, we introduce a variable-interval encoding of STL to MILP.
– MILP encodings of some system models, notably rectangular hybrid automata
and double integrator dynamics (suited for the automotive domain).
– We experimentally conﬁrm scalability of our algorithm, especially for complex
specs. Comparison is made with MILP-based optimal control [14], SMT-basedmodel checking [34], and optimization-based falsiﬁcation [11,37].
– Through the algorithm, case studies and experiments, we argue for the importance and feasibility of spec analysis for CPSs.
After exhibiting preliminaries on STL and stable partitioning in §2, we formulate
our problems (bounded trace synthesis, model checking, etc.) in §3. In §4 we
present a novel variable-interval MILP encoding of STL; in §5 we discuss MILP
encoding of a few families of models. Our main algorithm combines these two
encodings. In §6 we present experiment results.
Related Work I: Optimal STL Control with MILP. The works [14,28,29]
inspire our use of MILP for STL. Their problem is optimal controller synthesis
under STL constraints, i.e. to ﬁnd an input signal τ to a system model M sothat 1) the output signal M(τ ) satisﬁes a given STL spec ϕ and 2) it optimizes
J(M(τ )), where J is a given objective function. This problem subsumes our
problem of trace synthesis, by taking a constant function as J.
The algorithms in [14,28,29] reduce their problem to MILP by a constantinterval encoding of the robust semantics [13,17] of STL (an enhanced encoding
is presented in [22]). Speciﬁcally, their system model is discrete-time dynamics
x(t + Δt) = fd (x(t), u(t), w(t)) with a constant interval Δt.
In contrast, in our variable-interval encoding (§4), continuous time is discretized into the intervals . . . , (γi−1 , γi ), {γi }, (γi , γi+1 ), . . . where the end points
γi are also variables in MILP. This is advantageous not only in modeling precision but also in scalability: for system models that are largely continuous,constant-interval discretization incurs more integer variables in MILP, hampering the performance of MILP solvers. See §6 for experimental comparison.
Related Work II: SMT-Based STL Model Checking. Our key technical element (a variable-interval MILP encoding of STL) uses the idea of stablepartitioning from [7,23,34]. They solve bounded STL model checking, and also
its dual (trace synthesis). The main diﬀerence is the class of system models M
accommodated. SMT solvers accommodate more theories than MILP solving,
and thus allows encoding of a greater class of models. In contrast, by restricting
the model class to MILP-encodable, our algorithm beneﬁts speed and scalability (MILP is faster than SMT). Iterative optimization in MILP also makes ouralgorithm an anytime one. Native support of parameter synthesis is another plus.

Optimization-Based Trace Synthesis for Complex STL Speciﬁcations

287

Other Related Work. Optimization-based falsification has its root in thequantitative robust semantics of STL [13,17]; the successful combination withstochastic optimization metaheuristics has made falsiﬁcation an approach of bothscientiﬁc and industrial interest. See the ARCH competition report [16] for stateof-the-art. Falsiﬁcation is most of the time thought of as search-based testing;therefore, unlike the model checking approach, the absence of counterexamples
is usually not proved. Exceptions are [25,35] where they strive for probabilistic
guarantees for such absence.
The current work is motivated by the observation that falsiﬁcation solvers
often struggle in trace synthesis for complex STL specs, even if a system model
is simple. It is known that specs with more connectives pose a performancechallenge, and many countermeasures are proposed, including [2] (for temporal
operators) and [36,37] (for Boolean connectives).

2

Preliminaries

We let N, R denote the sets of natural numbers and reals, respectively; R≥0denotes an obvious subset. The set R = R ∪ {−∞, ∞} is that of extended reals.
The set B = { , ⊥} is for Boolean truth values. The powerset of a set X isdenoted by ℘(X). An interval is a subset of R≥0 of the form (a, b), [a, b), (a, b],or [a, c], where a < b and a ≤ c. Therefore a singleton {a} is an interval.
Deﬁnition 2.1 (linear predicate pand p, πp ). Given a set V of variables, a(closed) linear predicate is a function p : RV → B deﬁned as follows, using some
if and only if c x + b ≥ 0. We write p for thec ∈ RV and b ∈ R: p(x) =closed half-space {x | p(x) = } ⊆ RV .
For the above p, we deﬁne a function πp (x) : RV → R by πp (x) := c x + b.
This is understood as the degree of satisfaction (or violation, if negative) of alinear predicate p by x ∈ RV . Indeed, πp (x) is the (signed) Euclidean distanceto the boundary of p, assuming that the Euclidean norm of c is c = 1.
Deﬁnition 2.2 (signal). Let V be a ﬁnite set of variables and T a positive
real. A signal over V with a time horizon T is a function σ : [0, T ] → RV . We
write SignalTV for the set of all signals over V with time horizon T , or simply
SignalV when T is clear from the context.
If necessary, the domain [0, T ] of σ can be extended to R≥0 by setting σ(t) :=σ(T ) for all t > T . This allows us to deﬁne the notion of t-postfix, which willserve as the basis of the STL semantics (§2.1). Precisely, the t-postfix of σ is asignal σ t deﬁned by σ t (t ) := σ(t + t ). The domain of σ t can be chosen freely
but we set it to [0, T ] for consistency.
Deﬁnition 2.3 (system model, trace set L(M)). Let V, V  be ﬁnite sets ofvariables. A system model M from V  to V with a timehorizon T is a function
M : SignalTV  → ℘(SignalTV ). The trace set L(M) := τ ∈SignalT  M(τ ) is theV
set of all output signals of M where an input signal τ can vary.

288

S. Sato et al.

We allow system models to be nondeterministic (note the the powerset construction ℘); the models in §1 were deterministic for simplicity. A special case of theabove is when V  = ∅, that is, when M does not have any input. In this case, asystem model M can be identiﬁed with a subset L(M) ⊆ SignalV .
Example 2.4 (MRNC ). The dynamics model in Ex. 1.1 is formalized as a sysinit
init
tem model MRNC whose input variables (in V  ) are af , vfinit , xinit
f , ar , vr , xr ,and output variables (in V ) are af , vf , xf , ar , vr , xr . Here, the input is acceleration rates (af , ar ) and the initial values of velocities and positions (modeledusing signals vfinit etc. for convenience). The time horizon T of M represents its
simulation time; here we set T = 20. Given an input signal τ , the output M(τ )is a singleton M(τ ) = {σ}, and σ is determined by the ODE (2). Speciﬁcally,t
σ(t)(af ) = τ (t)(af ), σ(t)(vf ) = τ (0)(vfinit ) + 0 τ (t )(af ) dt , and so on.
2.1

Signal Temporal Logic

Deﬁnition 2.5 (signal temporal logic (STL)). In STL, an atomic proposition over a variable set V is represented as p :≡ (f (w) ≥ 0), where f : RV → R
is a function that maps a V -dimensional vector w to a real. The syntax of an
STL formula ϕ (over V ) is deﬁned as follows: ϕ :≡ p | ⊥ || ¬ϕ | ϕ1 ∨ ϕ2 |ϕ1 ∧ ϕ2 | ♦I ϕ | I ϕ | ϕ1 UI ϕ2 | ϕ1 RI ϕ2 , where I is a nonsingular closed timeinterval, and ♦I , I , UI , RI are temporal operators eventually, always, until andrelease. Implication is deﬁned: ϕ1 ⇒ ϕ2 :≡ ¬ϕ1 ∨ ϕ2 . We write temporal operators without the subscript I when I = [0, ∞] (e.g., ♦). Note that we do not lose
generality by restricting the inequality in p :≡ (f (w) ≥ 0). Indeed, ≤, <, > canbe encoded using (a combination of) −f and ¬.
The set Sub(ϕ) collects all subformulas of an STL formula ϕ; the set AP(ϕ)
collects all atomic propositions α occurring in ϕ.
Proposition 2.6. Every STL formula has a formula in the negation normal
form (NNF)—i.e. one in which negation ¬ appears only in front of atomic
propositions—that is semantically equivalent.
Assumption 2.7. We assume that each atomic proposition p is a linear predicate (Def. 2.1), that is, f (x) = c x + b with some c ∈ RV , b ∈ R in eachp :≡ (f (w) ≥ 0).
The Boolean semantics σ |= ϕ and robust semantics σ, ϕ ∈ R of STL are
standard. See [32, Appendix A].
PSTL is a parametric extension of STL. It is from [4]; see also [9]. Its deﬁnition is in [32, Appendix A]. The semantics of PSTL formula is deﬁned naturally
by ﬁxing u, v; see Prob. 3.3 for the speciﬁc forms we use.
2.2

Finite Variability

The satisﬁability checking problem for STL—this is equivalent to the model
checking problem under the trivial (identity) system model—is alreadyOptimization-Based Trace Synthesis for Complex STL Speciﬁcations

289

EXPSPACE-complete [3]. To ease computational complexity, bounded model
checking has been a common approach [23,26]. Its main idea is to bound thenumber of time-points at which the truth value of each subformula can vary.
Deﬁnition 2.8 (ﬁnite variability [27]). A (ﬁnite) partition P of an interval
D ⊆ R is a sequence P = (Ji )N
i=1 of nonempty and mutually disjoint intervals
Nsuch that i=1 Ji = D, and sup(Ji ) ≤ inf(Ji ) for any i < i . A Boolean signal
q : R≥0 → B is constant on an interval J ⊆ R≥0 if q(t) = q(t ) for any t, t ∈ J.
We say q(t) has N -bounded variability if there exists a partition P of [0, ∞) andq(t) is constant on every interval J ∈ P.
Let σ : [0, T ] → RV be a signal and ϕ be an STL formula over V . We say thatσ has the N -bounded variability with respect to ϕ if the Boolean (truth value)
signal t → (σ t |= ϕ) has the N -bounded variability. We say σ is finitely variablewith respect to ϕ if it has the N -bounded variability for some N .
Finally, we say σ has the hereditary N -bounded variability with respect toϕ if, for each subformula ψ ∈ Sub(ϕ), σ has the N -bounded variability withrespect to ψ. We write N -HBV for the hereditary N -bounded variability.
Lemma 2.9 ([7]). Let ϕ be an STL formula. A signal σ has the N -HBV withrespect to ϕ for some N if and only if it is ﬁnitely variable with respect to eachatomic proposition p ∈ AP(ϕ) occurring in ϕ.

The following is the basis of bounded model checking in [7,23].
Deﬁnition 2.10 (stable partition). Let σ be a signal, ϕ be an STL formula,and P be a partition of [0, T ] such that every J ∈ P is singular or open. Intuitively, P looks like {γ0 }, (γ0 , γ1 ), {γ1 }, (γ1 , γ2 ), . . . , {γN }. We say P is a stablepartition for σ and ϕ if t → σ t |= ψ is constant on J for each J ∈ P, ψ ∈ Sub(ϕ).

3Problem Formulation

We formulate our problems and discuss their mutual relationship. The next
problem is studied in [7,23,34].
Problem 3.1 (bounded STL model checking). Given an STL formula ϕ(over V ), a system model M (from V  to V ) with time horizon T , and a variability bound N ∈ N, decide if the following is true or not: σ |= ϕ holds foran arbitrary trace σ ∈ L(M) (cf. Def. 2.3) that has the hereditary N -boundedvariability (N -HBV) with respect to ϕ.
The following is the dual of Prob. 3.1, and is our main scope.
Problem 3.2 (bounded STL trace synthesis). Given ϕ, M, T and N as inProb. 3.1, ﬁnd a trace σ ∈ L(M) such that 1) σ has the N -HBV with respectto ϕ and 2) σ |= ϕ holds, or prove that such σ does not exist.

290

S. Sato et al.

Prob. 3.2 resembles the falsification problem [17]: given M (that can be blackbox) and ϕ , ﬁnd a counterexample input τ such that M(τ ) |= ϕ . The emphases
and the settings are often diﬀerent though; see §1.
The following is a special case of the STL parameter mining problem; seee.g. [9, § 3.5]. Recall from [32, Def. A.3] that ϕu,v instantiates parameters p, q in
ϕ with real values u, v from the domains P, Q, respectively.
Problem 3.3 (bounded existential parameter mining). Let ϕ be a PSTL
formulaover parameters(p, q), and M, T and N be as in Prob. 3.1. Find the set(u, v) ∈ P × Q  σ |= ϕu,v for some σ ∈ L(M) that has the N -HBV wrt. ϕ .
In §6, we study a further special case where there is only one parameter p andthe goal is to ﬁnd the maximum p in the above set.

Fig. 2. A stable partition (cf. [7]) for σ
and ϕ :≡ x ≥ 1. The symbols  and ⊥denote the (constant) truth value of ϕeach interval Ji .

Fig. 3. A δ-stable partition (Def. 4.7) for
σ and ϕ. Here ϕδ ≡ (x ≥ 1 + δ).  and ⊥are much like in Fig. 2; the symbol ? indicates that the truth value is not necessarily constant. In some regions (shaded),
σ t |= ϕ is true but σ t |= ϕδ is not.

4

Variable-Interval Encoding of STL to MILP

4.1

δ-Stable Partitions

We shall adapt the idea of stable partitioning [7], reviewed in §2.2, to the current
MILP setting. A major diﬀerence we need to address is that SMT is symbolic
while MILP is numerical: most MILP solvers do not distinguish < from ≤ anddo not accommodate strict inequalities. See e.g. [20].
In order to address this diﬀerence, we develop a theory of δ-stable partitions.
Here is its outline. Firstly, we replace partitions . . . , (γi−1 , γi ), {γi }, (γi , γi+1 ), . . .
used in [7] (see also Def. 2.10) with new “partitions” . . . , [γi−1 , γi ], [γi , γi+1 ], . . . .
The latter can be expressed only using ≤; but they have overlaps (at γi ). The
original stability notion (see §2.2) does not ﬁt the new partition notion—it
requires “constantly true” or “never true,” and prohibits overlaps. Therefore
we introduce δ-stability; it requires either “constantly true” or “never robustly
true.”

Optimization-Based Trace Synthesis for Complex STL Speciﬁcations

291

Example 4.1. Let σ be a continuous signal. Suppose that a sequence P =M(Ji )i=1 is a stable partition for σ and an STL formula ϕ, as illustrated in Fig. 2.
In this paper, since MILP solvers do not accommodate strict inequalities,
we are forced to use closed intervals; see Γ1 , . . . , Γ4 in Fig. 3. Notice that thetruth value of the formula ϕ not constant in Γ2 or Γ4 . To regain stability, we
introduce the δ-tightening ϕδ of the formula ϕ with some δ > 0 (Def. 4.4); hereϕδ ≡ (x ≥ 1 + δ). Then the truth value of ϕδ (instead of ϕ) is constantly falsein Γ2 and Γ4 , that is, ϕ is “never δ-robustly true” in Γ2 and Γ4 .
Deﬁnition 4.2 (timed state sequence). A time sequence of [0, T ] is asequence Γ = (0 = γ0 < · · · < γN = T ). Such a time sequence induces a “partiNtion of [0, T ] with singular overlaps,” namely Γ = [γi−1 , γi ] i=1 . We identify itwith the original time sequence, writing Γi for the interval [γi−1 , γi ].
a timed state sequence over V is a sequence ς = Given a time sequence,(x0 , γ0 ), . . . , (xN , γN ) , where x0 , . . . , xN in RV .
In MILP, it is eﬃcient to represent signals as (continuous) piecewise-linear signals, so that values within an interval can be deduced by linear interpolation.
Deﬁnition 4.3 (piecewise-linear signal). Given a timed state sequence ς =((x0 , γ0 ), . . . , (xN , γN )), the signal ς pwl : [0, γN ] → RV is deﬁned by the following
linear interpolation: ς pwl (t) := (1 − λ)xi−1 + λxi if γi−1 ≤ t ≤ γi (where λ =1γi −γi−1 (t − γi−1 )).
In this paper, a piecewise-linear signal is a signal of the form ς pwl for some
timed state sequence ς. Note that it is continuous everywhere, and is linear everywhere except for only ﬁnitely many points. Obviously, ς pwl is ﬁnitely variablewith respect to any linear predicate p (Def. 2.1).
Deﬁnition 4.4 (δ-tightening of linear predicates). Let δ > 0 be a positive
real and p be a linear predicate deﬁned by p(x) =⇐⇒ c x + b ≥ 0. Theδ⇐⇒ c x + b ≥ δ.
δ-tightening of p is a linear predicate deﬁned by p (x) =Note that pδ is stronger than p, i.e., [[pδ ]]  [[p]]. We further extend the conceptof δ-tightening for general STL formulas in NNF (cf. Prop. 2.6). Let p− be the⇐⇒ −c x − b ≥ 0.
linear predicate deﬁned by p− (x) =Deﬁnition 4.5 (δ-tightening of STL formulas in NNF). Let ϕ be an STL
formula in NNF. The δ-tightening ϕδ of ϕ is the STL formula obtained from ϕby replacing all occurrences of atomic predicates p (resp. ¬p) by pδ (resp. (p− )δ ).
The δ-tightening construction is related to robust semantics [32, Def. A.2].
Proposition 4.6. Let σ be a signal, ϕ be an STL formula in NNF, and δ > 0.
Then σ |= ϕδ implies [[σ, ϕ]] ≥ δ.



292

S. Sato et al.

Since the closed halfspace [[p− ]] coincides with the closure of the open halfspace
RV \ [[p]], the robust semantics is not aﬀected by the diﬀerence between p− and¬p. For simplicity, in the following, we assume that any STL formula in NNF
does not contain negation, i.e., ¬p is replaced by a new atomic proposition p− .
We are ready to deﬁne δ-stability.
Deﬁnition 4.7 (δ-stability). Let ϕ be an STL formula over V in NNF, σ ∈SignalTV be a signal, and Γ = (γ0 , . . . , γN ) be a time sequence (Def. 4.2) with
γN = T . We say Γ is δ-stable for σ and ϕ if, for each i ∈ [1, N ] and eachsubformula ψ ∈ Sub(ϕ), either of the following holds: 1) σ t |= ψ for each t ∈ Γi ,or 2) σ t |= ψ δ for each t ∈ Γi .
In the above deﬁnition, in each interval Γi , a subformula ψ is either 1) always trueor 2) never robustly true. The two conditions are not mutually exclusive—bothhold if σ t |= ψ ∧ ¬ψ δ for all t ∈ Γi .
The next notion of conservative valuation records which of 1) and 2) is truein each interval. It conservatively approximates the actual truth of ϕ (Fig. 3).
Deﬁnition 4.8 (conservative valuation). Let ϕ be an STL formula in NNF,
and Γ = (γ0 , . . . , γN ) be a time sequence . A valuation of ϕ in Γ is a function
Θ : Sub(ϕ) × [1, N ] → B that assigns, to each subformula and index of theintervals of Γ , a Boolean truth value. Let σ be a signal with a time horizon
T = γN . We say that Θ is a conservative valuation of ϕ in Γ on σ (up to δ) if
1) Θ(ψ, i) = implies that, for each t ∈ Γi , σ t |= ψ holds; and 2) Θ(ψ, Γi ) = ⊥implies, for each t ∈ Γi , σ t |= ψ δ .
We simply write ψi for Θ(ψ, i) when Θ is clear from context.
Suppose there exists a conservative valuation Θ of an STL formula ϕ in atime sequence Γ on a signal σ up to δ. Then Γ is δ-stable for σ and ϕ.
We shall argue in §4.2 that, for each piecewise-linear signal σ (Def. 4.3), an
STL formula ϕ, there is a time sequence Γ in which ϕ is δ-stable on σ. We startwith a special case where ϕ is an atomic proposition p.
Deﬁnition 4.9. Let x, x ∈ RV , and p be a linear predicate on V . We say (x, x )is a δ-crossing pair with respect to p if x ∈ pδ  and x ∈ pδ  (cf. Def. 2.1), or
vice versa. A δ-crossing pair is stationary if x ∈ p and x ∈ p.
Lemma 4.10. Let p be a linear predicate and σ be a piecewise-linear signal.
There is a time sequence Γ = (γ0 , . . . , γN ) such that, for any i ∈ [1, N ], 1) σ islinear in the interval [γi−1 , γi ], and 2) if (σ(γi−1 ), σ(γi )) is a δ-crossing pair, it
is stationary. It follows that there is a conservative valuation Θ of p in Γ on σ.
Proof. The lemma argues that, whenever σ enters or leaves pδ , it has to do sovia p \ pδ . See Fig. 4. This can be enforced by adding suitable points to Γ ,exploiting continuity of σ (Def. 4.3) and the intermediate value theorem.


Optimization-Based Trace Synthesis for Complex STL Speciﬁcations293

We note another advantage of δ-stable partitions: the number of invervals is roughly halved
compared to (original) stable partitions (seeFigs. 2 and 3). This advantage may be exploited
also in SMT-based approaches [7] for scalability.
4.2

Variable-Interval MILP Encoding

Our MILP encoding of STL relies on the constructs in §4.1. For the purpose of trace synthesis for an STL formula ϕ, our basic strategy is tosearch for 1) a time sequence Γ = (γ0 , . . . , γN )(i.e. a “partition,” see Def. 4.2) and 2) a valuation Θ : Sub(ϕ) × [1, N ] → B, such that

Fig. 4. A conservative valuation
Θ of a linear predicate p on σ.
The red segments are assigned by Θ. (Color ﬁgure online)– Θ is consistent in the sense that the truth values assigned to subformulas
comply with the STL semantics (§2.1);– Θ is fulfilling in the sense that it assigns to the top-level formula ϕ in Γ1(the ﬁrst interval); and– Θ is realizable in the sense that there is a piecewise-linear trace σ ∈ L(M) of
M that yields Θ. That is, precisely, Θ must be a conservative valuation of ϕin Γ on σ (Def. 4.8).
The entities Γ, Θ we search for are expressed as MILP variables, and the above
three conditions are expressed as MILP constraints. We describe these MILP
variables and constraints in the rest of the section. The constraints expressingσ ∈ L(M) require system model encoding and are thus deferred to later sections.
Variables. We use the following MILP variables. Their collection is denoted byVar(ϕ, N ). Here N ∈ N is a constant for variability bound (Prob. 3.2).
– Real-valued variables {γ0 , . . . , γN } for a time sequence Γ .
– Boolean variables {ψi | 1 ≤ i ≤ N, ψ ∈ Sub(ϕ)} for the value Θ(ψ, i) of avaluation Θ that we search for.
– Real-valued variables {xi,v | 0 ≤ i ≤ N, v ∈ V } for the values of a piecewiselinear trace σ ∈ L(M).
– Boolean variables {ζip , ζiδ,p | 0 ≤ i ≤ N, p ∈ AP(ϕ)} for the truth values of p
and pδ at time γi . These variables are used to detect crossing pairs (Def. 4.9).
– Real-valued variables {Siψ | 0 ≤ i ≤ N, I ψ ∈ Sub(ϕ)}. This auxiliary variable records for how long ψ has been true before γi .
– Real-valued variables {Piψ | 0 ≤ i ≤ N, ♦I ψ ∈ Sub(ϕ)}. This auxiliary variable records for how long ψ has been false before γi .
By an assignment we refer to a function v : Var(ϕ, N ) → R such that v(y) ∈{0, 1} for each Boolean variable y. The MILP problem is to ﬁnd an assignmentv that optimizes an objective under given constraints.

294

S. Sato et al.

Notation 4.11. In what follows, as a notational convention, we simply write
a variable y for the value v(y) when the assignment v is clear from context.
We further write ς for the timed state sequence composed of the time sequence{γ0 , . . . , γN } and the trace values {xj,v | 0 ≤ j ≤ N, v ∈ V }.
Note that, in this paper, we encode the Boolean semantics of STL [32, Def.
A.1], unlike [28,29] where the robust semantics is encoded in a constant-intervalmanner. The combination of variable-interval encoding and quantitative robust
semantics is future work; for example, a quantitative extension of δ-stable partitions (§4.1) seems quite nontrivial.
Shorthands for Propositional Connectives. We use standard shorthandsfor Boolean connectives in MILP constraints (such as ¬A, A ∧ B where A, B are
Boolean variables). See [32, Appendix B] for the formal encodings.
Realizability Constraints: Traces and Atomic Propositions. We need toconstrain γ0 , . . . , γN to be a time sequence (Def. 4.2), using some constant ε > 0
and letting · · · ≥ ε stand for · · · > 0.
γ0 = 0,γN = T,γi − γi−1 ≥ ε

for all i ∈ [1, N ](3)For each i and p ∈ AP(ϕ) (say p is deﬁned by c x + b ≥ 0), the variables ζip , ζiδ,pare constrained as follows,ζip = 1 ⇒ c xi + b ≥ 0
ζiδ,p = 1 ⇒ c xi + b ≥ δ

ζip = 0 ⇒ c xi + b ≤ −εζiδ,p = 0 ⇒ c xi + b ≤ δ − ε(4)Moreover, we impose the following to ensure that Γ is the one in Lem. 4.10:δ,pζiδ,p = 0 ∧ ζi+1
= 1 ⇒ ζip = 1,δ,pp
ζiδ,p = 1 ∧ ζi+1
= 0 ⇒ ζi+1
=1

(5)

Under constraints (3) to (5), Γ is δ-stable for ς pwl (cf. Def. 4.3) and p, by Lem.
4.10. By the deﬁnition of δ-stability, we can now constrain the variable pi byp,δ
pi = ζi−1
∨ ζip,δ for each i and p ∈ AP(ϕ).
Remark 4.12. Note that ε must be chosen to be small enough for the completeness of the encoding (Thm. 4.18). Thereafter we assume that, given a piecewiselinear signal σ and an STL formula ϕ, ε is small enough to ﬁnd a δ-stablepartition for σ and ϕ, and we omit ε from the constraints for simplicity.
Consistency Constraints I: Boolean Connectives. We can directly encodemconjunction j=1 ψj in STL by recursively applying the shorthand ∧ in [32,mm
Appendix B]:  j=1 ψj i = ψ1 i ∧ j=2 ψj i for each i ∈ [1, N ]. It is known thatmthe following alternative encoding avoids auxiliary variables  j=k ψj i (wheremmmk varies): for each i ∈ [1, N ],  j=1 ψj i ≥ 1 − m + j=1 ψj i and  j=1 ψj i ≤mm
ψj i . An encoding for disjunction is given similarly:  j=1 ψj i ≤ j=1 ψj i ,m
 j=1 ψj i ≥ ψj i .

Optimization-Based Trace Synthesis for Complex STL Speciﬁcations

295

Consistency Constraints II: Unbounded Temporal Modalities. For temporal operators with I = [0, ∞), the following encodings are straightforward.
ψ1 U ψ2 i = ψ2 i ∨ (ψ1 U ψ2 i+1 ∧ ψ1 i ),ψ1 R ψ2 i = ψ2 i ∧ (ψ1 R ψ2 i+1 ∨ ψ1 i )
ψ1 U ψ2 N = ψ2 N , ψ1 R ψ2 N = ψ2 N

for each i ∈ [1, N − 1],for i = N .

(6)

The encodings for ♦,  are special cases.
Consistency Constraints III: Bounded Temporal Modalities. This is
the most technically involved part. The challenge here is that the stability for[a,b] ψ is not guaranteed by the stability for ψ (similarly for ♦[a,b] ψ). Therefore
we need additional MILP constraints for the stability for [a,b] ψ.
Our encoding is inspired by the results from [26]; ours is simpler thanks to
our theory in §4.1 where intervals are all closed.
Recall that we use the variables Siψ , Piψ for this purpose. We focus on [a,b] ψ;the encoding of ♦[a,b] ψ is similar. The constraints on Siψ are as follows.
S0ψ = 0,ψi = 0 ⇒ Siψ = 0,ψ
+ (γi − γi−1 )ψi = 1 ⇒ Siψ ≥ Si−1

for each i ∈ [1, N ].

It follows that, for any non-negative real number L ∈ [0, γj ), we have Sjψ ≤ L if
and only if there exists k ∈ [1, j] such that ψk = 0 and γj − γk ≤ L.
We proceed to the constraints that describe the relationship between Siψ andthe semantics of I ψ. Suppose Γ = (γ0 , . . . , γN ) is δ-stable for a signal σ andψ. Let us write γN +1 = ∞ and ψN +1 = ψN for simplicity.
We consider consistency for the positive and negative cases separately. For
the positive one (i.e. [a,b] ψi = 1), the following observation is used.
Proposition 4.13. Let ϕ ≡ I ψ be an STL formula in NNF, and Θ be aconservative valuation of ψ in Γ = (γ0 , . . . , γN ) on a signal σ. Given i ∈ [1, N ],suppose (Γi + I) ∩ (γj−1 , γj ] = ∅ implies ψj = 1 for each j ∈ [i, N + 1]. Thenσ t |= ϕ holds for any t ∈ Γi .
Prop. 4.13 leads to the following MILP constraint:¬ϕi ∨ (γi + b ≤ γj−1 ) ∨ (γi−1 + a > γj ) ∨ ψj for each i ∈ [1, N ],j ∈ [i, N + 1].

The constraint itself does not follow the MILP format; we can neverthelessexpress it in MILP using an auxiliary Boolean variable Zf . Speciﬁcally, an
inequality f (x) ≥ 0 in a disjunctive constraint is constrained by Zf = 1 ⇒f (x) ≥ 0.
For the consistency in the negative case (i.e. [a,b] ψi = 0), the counterpartof Prop. 4.13 also involves Sjψ . See below; it leads to an MILP constraint much
like Prop. 4.13 does.

296

S. Sato et al.

Proposition 4.14. Suppose ϕ, σ, Γ , and Θ are as in Prop. 4.13. For any t ∈ Γi ,σ t |= ϕδ holds if the following conditions are satisﬁed for each j ∈ [i, N ]:⎧ ψ⎪
if γj ∈ (γi−1 + b, γi + b),⎨Sj ≤ b − aψ(7)if γi + b ∈ [γj−1 , γj ],Sj ≤ γj − γi − a⎪⎩ ψSN ≤ max(0, γN − γi − a) if γi + b > γN .
Proof. Let jt ∈ [i, N + 1] be the unique index such that t + b ∈ [γjt −1 , γjt ). Whenjt ≤ N and γjt < γi + b, we have γjt ∈ (γi−1 + b, γi + b) and by assumption
Sjψt ≤ b − a. There is k ∈ [1, jt ] such that ψk = 0 and γk ≥ γjt − b + a > t + a.
We obtain Γk ∩ (t + [a, b]) = ∅ and then σ t |= ϕδ holds. The other cases can bechecked in a similar manner.

Remark 4.15. For Prop. 4.13, the converse of the statement does not hold.
This is because σ t |= ψ does not guarantee ψi := Θ(ψ, i) = 1 where t ∈ Γi —weallow ψi = 0 when σ t |= ψ ∧ ¬ψ δ . It is similar for Prop. 4.14. However, thisdoes not aﬀect the completeness of the encoding (Thm. 4.18): while the converseof Prop. 4.13 does not hold for fixed Γ , in our workﬂow we also search for Γ , inwhich case it is easily shown that the MILP constraints derived from Prop. 4.13
are complete. The same is true for Prop. 4.14.
The remaining cases (ϕ ≡ ψ1 UI ψ2 and ϕ ≡ ψ1 RI ψ2 ) can be reduced to thecases for I and ♦I . It is by the rewriting techniques shown in [12]:ψ1 U[a,b] ψ2
ψ1 R[a,b] ψ2∼∼♦[a,b] ψ2 ∧ [0,a] (ψ1 U ψ2 ),[a,b] ψ2 ∨ ♦[0,a] (ψ1 R ψ2 ).

(8)
(9)

These equivalences hold in both Boolean and robust semantics.
Correctness of Encoding. Let EncSTL (ϕ, N, T, δ) denote the polyhedrondeﬁned by the above MILP constraints. It is correct in the following sense; seealso the goal we announced in the beginning of §4.2. Its proof is by induction onϕ.
Lemma 4.16. Let ϕ be an STL formula in NNF, N ∈ N, T > 0 and δ > 0.
Given an assignment v : Var(ϕ, N ) → R that lies in EncSTL (ϕ, N, T, δ), let Γ , ς
be the time sequence and the timed state sequence determined by v, and deﬁne avaluation Θ by Θ(ψ, i) := ψi (cf. Def. 4.8). Then Θ is a conservative valuationof ϕ in Γ on the signal ς pwl .
We deﬁne Enc(ϕ, M, N, T, δ) by the intersection of EncSTL (ϕ, N, T, δ), the
MILP encoding Encmodel (M, N, T ) of a system model M, and ϕ1 = 1.
Theorem 4.17 (soundness). Let ϕ be an STL formula in NNF, M be amodel with a time horizon T , N ∈ N and δ > 0. If an assignment v lies in
Enc(ϕ, M, N, T, δ), the induced ς pwl has ς pwl ∈ L(M) and ς pwl , ϕ ≥ 0.
Theorem 4.18 (completeness). Assume the setting of Thm. 4.17. If there ispiecewise-linear σ ∈ L(M) such that σ, ϕ ≥ δ, there is an assignment v thatlies in Enc(ϕ, M, N, T, δ) for some N ∈ N.


Optimization-Based Trace Synthesis for Complex STL Speciﬁcations

5

297

System Models and Their MILP Encoding

We introduce the MILP encoding Encmodel (M, N, T ) for some families of models M. We introduce an exact encoding for rectangular hybrid automata (RHAs),
and an approximate one for HAs with closed-form solutions. We also introduce
a reﬁnement of the latter—it is more precise and eﬃcient—restricting to double
integrator dynamics. The last is useful for automotive examples such as Ex. 1.1.
We defer the discussion of RHAs for the space reason; see [32, Appendix C].
We thus focus on the other two families.
5.1

HAs with Closed-Form Solutions

Here we are interested in hybrid automata (HAs)
whose continuous ﬂow dynamics at each control
mode has a closed-form solution. The basic idea issimple and it is illustrated in Fig. 5, where the solution f (t) of dynamics (blue) is approximated by apiecewise linear function (red). Such MILP encoding is standard; see e.g. [5].
We formalize this intuition. Firstly, to accomFig. 5. MILP encoding ofmodate input signals τ ∈ SignalV  (Def. 2.3), wef (t)extend the HA deﬁnition so that some variables xin
can be designated to be input variables. This means that there are no ODEs
whose left-hand side is x˙in , and that the variable updates associated with modetransitions never change xin .
Then the above “closed-form solution” assumption on an HA H is preciselyindescribed as follows. Let xin = (xin
1 , . . . , xk ) enumerate H’s input variables, andx = (x1 , . . . , xl ) enumerate its other variables. We assume that, for the ﬂow
dynamics at each control mode u, there is a closed-form solution
x(t) = fu (t, xin , x0 )such that, for each t0 ∈ R≥0 , fu (t0 , xin , x0 ) is a (10)linear function over the variables xin , x0 .

Here, the variable t is the elapsed time since the arrival at the current control
mode u; the variables xin refer to the input variables (their values are assumed
to be constant within the same mode); and the variables x0 refer to the initialvalues of x on the arrival at u. The assumption holds in many examples, suchas polynomial dynamics.
Let us motivate the assumption. A closed-form solution fu helps precision: inpiecewise linear approximation such as in Fig. 5, errors do not accumulate overtime; in contrast, if a closed-form solution is not given, our alternative will be
numerical integration e.g. by the Euler method, where errors accumulate. The
linearity assumption in (10) is there for MILP encoding; see below.
Our approximate MILP encoding poses the closed-form solution assumption
and follows the intuition of Fig. 5. Speciﬁcally, 1) it ﬁxes a constant Δt ∈ R≥0 as

298

S. Sato et al.

a sampling interval; 2) it obtains a family fu (k·Δt, xin , x0 ) k of linear functions
over the variables xin , x0 ; and 3) the value of x at the elapsed time t is expressedby the linear interpolation(k+1)Δt−tinfu (kΔt, xin , x0 ) + t−kΔtΔtΔt fu (k + 1)Δt, x , x0 ,(11)where k is such that kΔt ≤ t ≤ (k + 1)Δt. This encoding of ﬂow dynamics is
combined with the HA structure, much like in [32, Appendix C], yielding anapproximate MILP encoding of the whole HA.
The above encoding has two sources of numerical errors. One is linear interpolation. Errors caused by it are illustrated in Fig. 5 as the vertical margin between
blue and red.
The other source is binary expansion [18,19], a standard MILP techniquefor encoding bilinear functions. Indeed, in (11), t, xin , x0 are all continuous variables in MILP, and the expression (11) can contain their products. The linearity
assumption in (10) has been posed to restrict (11) to bilinear.
5.2

HAs with Double Integrator Dynamics

Our next focus is a special case of the model family of §5.1, where each continuous
ﬂow is double integrator dynamics. This is important because 1) it gets rid of oneof the two error sources in §5.1, namely linear interpolation, by the trapezoidal
rule, and 2) it can be used for many automotive dynamics models (cf. Ex. 1.1).
The trapezoidal rule is a basic technique in numerical integration [6], wherebg(t) dt is approximated by (b − a) g(a)+g(b). For double integrator dynamics,
2a
we apply the trapezoidal rule to the velocity v, and it is exact since v’s evolution
is linear. This allows us to express the position x in the bilinear form x = t· v02+v ,using the variables t (elapsed time), v0 (initial velocity), and v (current velocity).
Thus we can dispose of the sampling points and their interpolation (11) in §5.1.
We exploit this encoding for our automotive case studies such as Ex. 1.1.

6

Implementation and Experiments

We implemented, in Python, our MILP encodings of the STL semantics (§4)
and two model families, namely RHAs [32, Appendix C] and double integrator
dynamics (§5.2; multiple modes are not supported since our benchmarks do notneed them). The hyperparameter δ in our encoding is ﬁxed at 0.1 for all benchmarks. The resulting MILP constraints are solved by Gurobi Optimizer [20].
This prototype implementation is called STLts—STL trace synthesizer.
Our experiments are designed to address the following research questions.
RQ1 Assess the eﬀect of variability bounds N (Prob. 3.2) on the performance.
RQ2 Compare the performance of STLts with optimization-based falsiﬁcation,
and with SMT-based model checking.
RQ3 Assess the performance of STLts for real-world complex scenarios.

Optimization-Based Trace Synthesis for Complex STL Speciﬁcations

299

RQ4 Assess the performance of STLts in parameter mining (Prob. 3.3).
We used three classes of benchmarks: rear-end near collision (RNC), navigation (NAV), and disturbance scenarios in ISO 34502 (ISO). In each class, wehave multiple STL specs, resulting in benchmarks such as RNC1, RNC2, etc.
Rear-End Near Collision (RNC1–3). As discussed in Ex. 1.1, these automotive benchmarks are simpliﬁcations of the ISO benchmarks below. The spec
RNC1 is presented in Ex. 1.1. The system model (2) (see also MRNC in Ex. 2.4)
is double integrator dynamics (§5.2) and is shared by the benchmarks RNC1–3.
The other two specs RNC2, RNC3 are deﬁned as follows, using formulas in (1):RNC2
trimming2
RNC3


:≡ (xf − xr ≥ 0) ∧♦[0,9] ([0,1]danger) ∧ ([0,1] ar ≥ 1)∧ (♦[1,5] ¬danger):≡ (♦danger) ⇒ ([0,1] ar ≥ 1) U danger:≡ (dyn inv ∧ trimming2) ∧ ♦[0,9] [0,1] danger(12)

Navigation (NAV1–2). Here we usea system model that adapts NAV-2
from [15]. The latter is a standard
example of an RHA [32, Appendix C],
used e.g. in [10].
Our system model MNAV is an
RHA that describes the motion of apoint robot in a 2 × 2 grid where eachregion has a rectangular vector ﬁeld,
with a time horizon T = 40. See Fig. 6.
We have 4 regions 1 , . . . , 4 , each associated with rectangular bounds forẋ, ẏ and invariants; besides, we set anunsafe region unsafeR (x ∈ [9, 10])
Fig. 6. The RHA MNAV for NAV1–2
and a goal region goalR (x ∈ [4, 6]∧y ∈[2, 5]). The robot starts from an initial position (x0 , y0 ) where x0 ∈ [0, 3]∧y0 = 0.
We consider two specs: NAV1 :≡ ♦([0,3] ((x, y) ∈ goalR)) ∧ (x ∈ unsafeR)
and NAV2 ≡ ((x, y) ∈ 3 → ♦[0,3] (x, y) ∈ 4 ). NAV1 is almost a standard
reach-avoid constraint, but it additionally requires the persistence to the goal
region for three seconds. Such speciﬁcations are not accommodated in many
control and model checking frameworks specialized in reach-avoid constraints(see e.g. [10]). NAV2 is a response specification—the trigger (being in 3 ) must
be responded by moving to 4 within a three-second deadline. Such specs arecommon in manufacturing; see e.g. [36].
ISO 34502 Disturbance Scenarios for Automated Driving (ISO1, ISO3,. . . , ISO8). These benchmarks motivated the current work. As discussed in §1(see Ex. 1.1), we obtained in [30] complex STL specs as the formalization of the

300

S. Sato et al.

disturbance scenarios in the ISO 34502 standard, but in our illustration eﬀorts
by trace synthesis, we found that existing techniques such as optimization-based
falsiﬁcation struggle.
In our experiments, the sys- Table 1. Disturbance scenarios in the ISO
tem model is similar to MRNC 34502 standard. Table from [21](Ex. 1.1 and 2.4), while lateraldynamics is added and the time
horizon is 10 time units here.
As for specs, we use seven STL
specs ISO1, ISO3, . . . , ISO8; theseare obtained in [30] as the formalization of the disturbance scenarios No. 1,3,. . . ,8 in the ISO 34502
standard for automated driving
vehicles. See Table 1. Scenario No.
2 was omitted in [30] since it
involves three vehicles; we omit Scenarios No. 9–24 since they are the samewith No. 1–8 except in the road shape.
Speciﬁcally, the specs ISOi follow the common format shown below [30]:ISOi ≡ initSafe ∧ disturbi ,disturbi ≡ initialConditioni ∧ behaviourSVi ∧ behaviourPOVi

where SV refers to the subject (“ego”) vehicle and POV refers to the principal other vehicle. The component formulas initialConditioni , behaviourSVi
and behaviourPOVi vary for diﬀerent scenarios (No. i). Going into their deﬁnitions are beyond the scope of this paper; we highlight ISO5 as an example todemonstrate the complexity of the specs ISOi.
initialCondition5 ≡ behaviourSV5 ≡ leavingLane(SV, L)
behaviourPOV5 ≡ cutIn(POV, SV)leavingLane(a, L) ≡ atLane(a, L) ∧ ♦(¬atLane(a, L))
cutIn(POV, SV, L) ≡ ¬sameLane(POV, SV, L) ∧ ♦ danger(SV, POV)∧♦[0,minDanger] (sameLane(SV, POV, L) ∧ aheadOf(SV, POV))
danger(SV, POV) ≡ [0,minDanger] rssViolation(SV, POV)(13)

The formulas not deﬁned here are suitably deﬁned atomic propositions.
Experiment Settings. Our implementation STLts is compared with the following tools: 1) a widely used optimization-based falsiﬁcation tool Breach [11];2) another falsiﬁcation tool ForeSee [1,37] that emphasizes optimized treatmentof Boolean connectives in STL; 3) an MILP-based STL optimal control tool
bluSTL [14]; and 4) STLmc, an SMT-based bounded STL model checker [34].
The experiments were conducted on an Amazon EC2 c4.4xlarge instance(2.9 GHz Intel Xeon E502666 v3, 30.0GB RAM) running Ubuntu Server 20.04.

Optimization-Based Trace Synthesis for Complex STL Speciﬁcations

301

RQ1: the Eﬀect of the Variability Bound N .
There is an obvious trade-oﬀ about the choice of avariability bound N (Prob. 3.2): bigger N means
the search is more extensive, but it incurs greater
computational cost.
This tendency is conﬁrmed in our experiments;
the result for the ISO6 benchmark is in Fig. 7 forillustration. Here, synthesis was successful for N =4 for the ﬁrst time.
Fig. 7. Execution time of
We also observe in the ﬁgure that computaSTLts for diﬀerent var. bd. N ,tional cost is low when trace synthesis is unsuc- on ISO6
cessful. This suggests the following strategy: westart with small N and increment it if trace synthesis is unsuccessful. We might waste time by trying too small N ’s; but thewasted time should be small.
Experimental Results, Overview. Table 2. Experimental results for trace
Our experimental results are in summa- synthesis, showing execution time (secrized in Table 2, where the best perform- onds). (N ) for STLts is the ﬁrst successful bound. Timeout (t/o) is 600 s.
ers are highlighted by color.
We explain the missing entries. In (∗),
STLts Breach ForeSee bluSTL STLmc
the tool is not applicable due to the nonRNC1
0.1
59.4 546.8(¶)
t/odeterminism of the benchmark. In (†), RNC2 0.3 (3)(4)
9.3 104.3
14.3
t/o
we did not conduct experiments since RNC3 0.1 (3) 81.3 197.4(¶)
t/othe performance comparison with STLts NAV1 32.5 (17)
16.5
(∗)
(∗)
(‡)
10.0
is already clear with simpler RNC bench- NAV2 2.1 (11)
ISO1
0.4
(3)
8.9
t/o
marks. In (‡), bluSTL does not support
ISO3
0.2 (2)t/ot/omultiple control modes. (¶) is because ISO4 0.4 (2) t/o
t/o
(†)
(†)
bluSTL (at least its implementation avail- ISO5 9.9 (4) 31.2 435.8
2.4 (4)t/o
58.9
able to us) does not support the until U ISO6
ISO7
0.6 (3)33.6 187.2
1.5 (3)
38.8
t/o
ISO8
modality.
Overall, our STLts is clearly the best
performer in all benchmarks but one. The other tools time out, or takes tensof seconds. For our motivation of illustrating STL specs by trace synthesis inclose interaction with users, tens of seconds is prohibitively long. The results
adequately demonstrate satisfactory performance of our algorithm, in trace synthesis for complex STL specs.
RQ2: Comparison with Other Approaches. A summary of comparison isin Table 3. The comparison with optimization-based falsiﬁcation tools is as we
expected—their struggle with complex specs motivated this work (§1). Boolean
connectives in STL specs have been found problematic in falsiﬁcation: this iscalled the scale problem [36,37]. The results in Table 2 show that our benchmark
specs are even beyond the capability of ForeSee, a tool that incorporates Monte
Carlo tree search to speciﬁcally handle the scale problem. After all, one can say

302

S. Sato et al.

Table 3. Comparison of our approach (STLts) with baselines (Breach, ForeSee,
bluSTL, STLmc). Highlited cells represent positive features.
Feature

STLts

Trace synthesis foranalyzing specs

Successful in all
Good for- Timeout in mostbenchmarks withfalsifying models
of benchmarks
large STL formulas but not good withlarge STL formulas

Model checking

Complete up to
N and δ-By MILP-

Parameter mining
Continuous STL
semantics

Breach/ForeSee

Variable-interval - Discretized
encoding

bluSTL

Controlsynthesis withguarantee

STLmc
Timeout except
for linear dynamics

Complete up toN

By MILP

By binary search- Discretized

Variable-interval
encoding

Accommodated class MILP-encodable,
Black-box,
MILP-encodable,
SMT-encodable,of nonlinear
can bedeterministic
can becan bedynamics
nondeterministic
nondeterministic
nondeterministic= full support;= partial support;= very limited support; - = not supported.

that falsiﬁcation tools are aimed at complex models, while our STLts is aimed
at complex specs.
STLmc has a similar (“dual”) scope and utilizes a similar technique (stablepartitioning) to our STLts; the main diﬀerence is that STLmc is SMT-based
while STLts is MILP-based. Therefore STLts accommodates a smaller class ofmodels, but it can be faster on them exploiting numeric optimization. Table 2
suggests the advantage of STLts for common STL specs in manufacturing.
RQ3: Performance in Real-World Scenarios. For this RQ, we refer to
STLts’s performance on the ISO benchmarks. Illustrating the specs ISOi by tracesynthesis is a real-world problem about safety standards for automated driving(§1), and Table 2 shows that STLts has suﬃcient performance and scalability tohandle complex specs there (see (13)).
RQ4: Performance in Parameter
Mining. We conducted parametermining experiments with the ISO8
benchmark. Its speciﬁcation has asubformula fasterThan(SV, P OV, p)that requires that SV’s velocity isbigger than POV’s by at least aparameter p. We used STLts to solve
Prob. 3.3, that is, to ﬁnd the max- Fig. 8. STLts for parameter synthesis. Red
imum p for which a satisfying trace is execution time (axis left, seconds); blue
exists.
is the maximum p (axis right). (Color ﬁgure
Figure 8 shows the results with online)
varying variability bound N . Parameter mining is generally more expensive than trace synthesis. This is because
the former has a nontrivial objective function (namely p in this example), while

Optimization-Based Trace Synthesis for Complex STL Speciﬁcations

303

the latter does not (it is thus a constraint satisfaction problem). We observe
the optimization with N ≥ 10 resulted in a timeout. The tendency, much likein trace synthesis, is that the result (max p) improves but execution time getslarger as N becomes bigger (there are some exceptions such as N = 8, 9 though).
Taking the same strategy as above (incrementing N ), it takes roughly 10 min
to obtain a largely converged value (∼ 14.9 for the maximum p). Overall, we
believe this is a realistic performance for practical usage.

References
1. ForeSee falsiﬁcation solver (2021). https://github.com/choshina/ForeSee
2. Akazaki, T., Hasuo, I.: Time robustness in MTL and expressivity in hybrid systemfalsiﬁcation. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207,
pp. 356–374. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-216683 21
3. Alur, R., Feder, T., Henzinger, T.A.: The beneﬁts of relaxing punctuality. J. ACM
43(1), 116–146 (1996). https://doi.org/10.1145/227595.227602
4. Asarin, E., Donzé, A., Maler, O., Nickovic, D.: Parametric identiﬁcation of temporal properties. In: Khurshid, S., Sen, K. (eds.) RV 2011. LNCS, vol. 7186, pp.
147–160. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-298608 12
5. Asghari, M., Fathollahi-Fard, A.M., Mirzapour Al-e hashem, S.M.J., Dulebenets,
M.A.: Transformation and linearization techniques in optimization: a state-of-theart survey. Mathematics 10(2), 283 (2022). https://doi.org/10.3390/math10020283
6. Atkinson, K.E.: An Introduction to Numerical Analysis. Wiley, New York, second
edn. (1989). http://www.worldcat.org/isbn/0471500232
7. Bae, K., Lee, J.: Bounded model checking of signal temporal logic properties using
syntactic separation. Proc. ACM Program. Lang. 3(POPL), 51:1–51:30 (2019).
https://doi.org/10.1145/3290364
8. Bartocci, E., et al.: Speciﬁcation-based monitoring of cyber-physical systems: asurvey on theory, tools and applications. In: Bartocci, E., Falcone, Y. (eds.) Lectures on Runtime Veriﬁcation. LNCS, vol. 10457, pp. 135–175. Springer, Cham(2018). https://doi.org/10.1007/978-3-319-75632-5 5
9. Bartocci, E., Mateis, C., Nesterini, E., Nickovic, D.: Survey on mining signal temporal logic speciﬁcations. Inf. Comput. 289(Part), 104957 (2022). https://doi.org/
10.1016/J.IC.2022.104957
10. Bu, L., Frehse, G., Kundu, A., Ray, R., Shi, Y., Zaﬀanella, E.: Arch-comp22 category report: Hybrid systems with piecewise constant dynamics and bounded model
checking. In: Frehse, G., Althoﬀ, M., Schoitsch, E., Guiochet, J. (eds.) Proceedingsof 9th International Workshop on Applied Veriﬁcation of Continuous and Hybrid
Systems (ARCH22). EPiC Series in Computing, vol. 90, pp. 44–57. EasyChair(2022). https://doi.org/10.29007/lnzf
11. 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
12. Donzé, A., Ferrère, T., Maler, O.: Eﬃcient robust monitoring for STL. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 264–279. Springer,
Heidelberg (2013). https://doi.org/10.1007/978-3-642-39799-8 19

304

S. Sato et al.

13. 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
14. Donzé, A., Raman, V.: BluSTL: controller synthesis from signal temporal logic
speciﬁcations. In: ARCH14-15. 1st and 2nd International Workshop on Applied
veRiﬁcation for Continuous and Hybrid Systems, pp. 160–150. https://doi.org/10.
29007/g39q
15. Duggirala, P.S., Mitra, S.: Abstraction reﬁnement for stability. In: 2011
IEEE/ACM Second International Conference on Cyber-Physical Systems, pp. 22–
31. IEEE (2011). https://doi.org/10.1109/ICCPS.2011.24
16. Ernst, G., et al.: ARCH-COMP 2021 category report: falsiﬁcation with validation of results. In: Frehse, G., Althoﬀ, M. (eds.) 8th International Workshop on
Applied Veriﬁcation of Continuous and Hybrid Systems (ARCH21), Brussels, Belgium, July 9, 2021. EPiC Series in Computing, vol. 80, pp. 133–152. EasyChair(2021). https://doi.org/10.29007/XWL1
17. Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic speciﬁcations forcontinuous-time signals. Theoret. Comput. Sci. 410(42), 4262–4291 (2009).
https://doi.org/10.1016/j.tcs.2009.06.021
18. Glover, F.: Improved linear integer programming formulations of nonlinear integer
problems. Manag. Sci. 22, 455–460 (1975). https://doi.org/10.1287/mnsc.22.4.455
19. Gupte, A., Ahmed, S., Cheon, M.S., Dey, S.: Solving mixed integer bilinear problems using MILP formulations. SIAM J. Optim. 23(2), 721–744 (2013). https://doi.org/10.1137/110836183
20. Gurobi Optimization, LLC: Gurobi Optimizer Reference Manual (2023). https://www.gurobi.com
21. Road vehicles - Test scenarios for automated driving systems - Scenario based
safety evaluation framework. Standard, International Organization for Standardization, Geneva, CH (2022)
22. Kurtz, V., Lin, H.: A more scalable mixed-integer encoding for metric temporal
logic. IEEE Control. Syst. Lett. 6, 1718–1723 (2022). https://doi.org/10.1109/
LCSYS.2021.3132839
23. Lee, J., Yu, G., Bae, K.: Eﬃcient SMT-based model checking for signal temporal
logic. In: 2021 36th IEEE/ACM International Conference on Automated Software
Engineering (ASE), pp. 343–354 (2021). https://doi.org/10.1109/ASE51524.2021.
9678719
24. Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In:
Lakhnech, Y., Yovine, S. (eds.) FORMATS/FTRTFT -2004. LNCS, vol. 3253, pp.
152–166. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-540-302063 12
25. Pedrielli, G., et al.: Part-X: A family of stochastic algorithms for search-based
test generation with probabilistic guarantees. IEEE Trans. Autom. Sci. Eng. 1–22
(2023). https://doi.org/10.1109/TASE.2023.3297984
26. Prabhakar, P., Lal, R., Kapinski, J.: Automatic trace generation for signal temporal
logic. In: 2018 IEEE Real-Time Systems Symposium (RTSS), pp. 208–217. IEEE,
Nashville, TN (2018). https://doi.org/10.1109/RTSS.2018.00038
27. Rabinovich, A.M.: On the decidability of continuous time speciﬁcation formalisms.
J. Log. Comput. 8(5), 669–678 (1998). https://doi.org/10.1093/logcom/8.5.669
28. Raman, V., Donzé, A., Maasoumy, M., Murray, R.M., Sangiovanni-Vincentelli,
A.L., Seshia, S.A.: Model predictive control with signal temporal logic speciﬁcations. In: 53rd IEEE Conference on Decision and Control, CDC 2014, Los Angeles,

Optimization-Based Trace Synthesis for Complex STL Speciﬁcations

305

CA, USA, December 15-17, 2014, pp. 81–87. IEEE (2014). https://doi.org/10.
1109/CDC.2014.7039363
29. Raman, V., Donzé, A., Sadigh, D., Murray, R.M., Seshia, S.A.: Reactive synthesis
from signal temporal logic speciﬁcations. In: Proceedings of the 18th International
Conference on Hybrid Systems: Computation and Control, pp. 239–248. ACM,
Seattle Washington (2015). https://doi.org/10.1145/2728606.2728628
30. Reimann, J., et al.: Temporal logic formalisation of ISO 34502 critical scenarios:
modular construction with the RSS safety distance. In: Proceedings of the 39th
ACM/SIGAPP Symposium on Applied Computing (SAC 2024) to appear (2024).
arXiv:2403.18764
31. Roehm, H., Heinz, T., Mayer, E.C.: STLInspector: STL Validation with Guarantees. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp.
225–232. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63387-9 11
32. Sato, S., An, J., Zhang, Z., Hasuo, I.: Optimization-based model checking and tracesynthesis for complex STL speciﬁcations (extended version) (2024). available onarXiv
33. Souyris, J., Wiels, V., Delmas, D., Delseny, H.: Formal veriﬁcation of avionics
software products. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol.
5850, pp. 532–546. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3642-05089-3 34
34. Yu, G., Lee, J., Bae, K.: Stlmc: Robust STL model checking of hybrid systems
using SMT. In: Shoham, S., Vizel, Y. (eds.) Computer Aided Veriﬁcation - 34th
International Conference, CAV 2022, Haifa, Israel, August 7-10, 2022, Proceedings,
Part I. LNCS, vol. 13371, pp. 524–537. Springer (2022). https://doi.org/10.1007/
978-3-031-13185-1 26
35. Zhang, Z., Arcaini, P.: Gaussian process-based conﬁdence estimation for hybrid
system falsiﬁcation. In: Huisman, M., Păsăreanu, C., Zhan, N. (eds.) FM 2021.
LNCS, vol. 13047, pp. 330–348. Springer, Cham (2021). https://doi.org/10.1007/
978-3-030-90870-6 18
36. 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
37. Zhang, Z., Lyu, D., Arcaini, P., Ma, L., Hasuo, I., Zhao, J.: Eﬀective hybrid systemfalsiﬁcation using monte carlo tree search guided by QB-robustness. In: Silva, A.,
Leino, K.R.M. (eds.) CAV 2021. LNCS, vol. 12759, pp. 595–618. Springer, Cham
(2021). https://doi.org/10.1007/978-3-030-81685-8 29

306

S. Sato et al.

Open Access This chapter is licensed under the terms of the Creative Commons
Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/),
which permits use, sharing, adaptation, distribution and reproduction in any medium
or format, as long as you give appropriate credit to the original author(s) and thesource, provide a link to the Creative Commons license and indicate if changes were
made.
The images or other third party material in this chapter are included in thechapter’s Creative Commons license, unless indicated otherwise in a credit line to thematerial. If material is not included in the chapter’s Creative Commons license andyour intended use is not permitted by statutory regulation or exceeds the permitteduse, you will need to obtain permission directly from the copyright holder.