Constrained Optimization for Hybrid System Falsification andApplication to Conjunctive Synthesis
Sota Sato∗† , Masaki Waga∗‡ , Ichiro Hasuo∗†∗ National Institute of Informatics, Tokyo, Japan (e-mail: {sotasato,hasuo}@nii.ac.jp)† The Graduate University for Advanced Studies, Tokyo, Japan‡ Graduate School of Informatics, Kyoto University, Japan (e-mail: mwaga@fos.kuis.kyoto-u.ac.jp)♦I (ϕ1 ∧ · · · ∧ ϕm ); therefore it does not apply to our current
problem of conjunctive synthesis (satisfying ϕ1 ∧ · · · ∧ ϕm ).
To handle the scale problem, our proposed method forsolving conjunctive synthesis combines optimization-based
falsification and constrained optimization.

Index Terms—control system synthesis, cyber-physical system,
constrained optimization, evolutionary algorithm, temporal logic,
hybrid system falsification, search-based testing

I. M OTIVATION AND P ROBLEM F ORMULATION
Optimization-based falsification [1], is an established approach to the falsification problem. The goal of the falsification
problem is to find an input signal u such that the output M(u)violates the specification ϕ. Optimization-based falsificationtranslates the falsification problem into minimization of therobustness, an (extended) real number JM(u), ϕK definedin the robust semantics [2], in which negative values mean
the violation. This allows us to utilize existing optimization
algorithms to find a falsifying input.
One easily figures out that falsification of ¬ϕ (i.e., to find afalsifying input for ¬ϕ) is equivalent to synthesis for ϕ (i.e., tofind an input that satisfies ϕ). We aim to exploit and extend thetechniques for optimization-based falsification with the aim ofsolving the following conjunctive synthesis problem.

II. C ONJUNCTIVE S YNTHESIS BY C ONSTRAINEDO PTIMIZATIONIn the light of optimization-based falsification, conjunctive
synthesis problem can be turned into the following optimization problem:
maximize JM(u), ϕ1 K u · · · u JM(u), ϕm K.
(1)u
Note that the robust semantics interprets conjunction ∧ by theinfimum u of real numbers.
However, the issue here is that some specific component
can dominate the robustness of a Boolean combination andmasks away the other components and prevent hill-climbing
optimization algorithms from effectively making all the components positive—this is the scale problem.
Our main idea is to regard conjuncts not as objectives but
as constraints.

Problem 1 (Conjunctive Synthesis). Given: a model M thattakes an input signal u and yields an output signal M(u), anda conjunctive specification ϕ ≡ ϕ1 ∧ ϕ2 ∧ · · · ∧ ϕm given bysignal temporal logic (STL) formula.
Find: a satisfying input, that is, an input signal u such thatthe corresponding output M(u) satisfies ϕ.

Problem 3 (Conjunctive Synthesis by Constrained Optim.).
maximize [[M(u), ϕ1 ]]usubject to [[M(u), ϕi ]] > 0,Example 2. Here is our leading example. The system model
M is given by a Simulink model for automatic transmission
system [3]. The model M has two inputs (throttle, brake) andthree outputs (rpm, speed, gear). The specification is given by(2)
i = 2, . . . , m.

If the discovered maximum is positive, then the corresponding
value of the optimization variable u is a solution to conjunctive
synthesis (Problem 1).

ϕ :≡ ϕ1 ∧ ϕ2 ∧ ϕ3 , where ϕ1 :≡ [0,30] (rpm ≤ 2400),

The conflict between different conjuncts ϕ1 , . . . , ϕm isburied away in a single objective function in (1); it is madeexplicit in (2) via the translation of Problem 1 to Problem 3.
This translation would lead to an efficient solution only if there
exists an algorithm that successfully exploits the structure thatis now made explicit. This is the topic of the next section.

ϕ2 :≡ [0,30] (speed ≤ 60), ϕ3 :≡ ♦[0,30] (gear ≥ 3);
it means the gear should reach the third without any ofRPM and speed getting too large, a requirement common in
the break-in procedure. This conjunctive synthesis asks for acareful trade-off because it contains conflicting requirements;
gear gets larger typically when RPM and/or speed is larger.

III. O UR A LGORITHM : C OMBINING MCR AND CMA-ES

Existing falsification solvers can struggle with some problem instances due to the scale problem, a general difficultyin falsification that is identified and tackled in [4]. The
recent paper [4] proposed a solution concerning multi-armed
bandit problem (MAB); however, it is dedicated to satisfying the specifications of the form I (ϕ1 ∨ · · · ∨ ϕm ) and

For an optimization problem such as (1), we adopt CMAES, an evolutionary optimization algorithm introduced by [5],whose efficiency in the context of optimization-based falsification is well-established [4].
The multiple constrained ranking algorithm (MCR) [6] is aconstraint handling technique (CHT) for general evolutionary1

optimization algorithms, hence also for CMA-ES. MCR address the scale problem in the constraints and/or the objectivefunction, using suitable rankings—instead of robustness valuesof constraints themselves—in prioritizing candidate solutions.
Let us write f (u) = [[M(u), ϕ1 ]] for the optimization
objective (the fitness function). MCR in CMA-ES consists ofreplacing the use of the fitness function f , in the selection
step of CMA-ES, with the scoring function FX , relies on thecurrent population X. The value FX (u) is a natural number,and those u with smaller FX (u) are deemed fitter.
The scoring function FX employs three kinds of functions
RObjX , RVNumX , RConjX ; all return a suitable “rank” of theinput. RObjX compares the value of the objective function f ,namely the value of [[M(v), ϕ1 ]]. RConjX (j = 2, . . . , m) compares the violation of ϕj , namely 0 ∨ [[M(v), ϕj ]]. RVNumX
compares the number of violated constraints.

TABLE IIE XPERIMENTAL RESULTS . F OR EACH PROBLEM INSTANCE , THE BESTRESULT IS HIGHLIGHTED AND THE LARGEST SR IS SHOWN IN BLUE .
Model

ϕ1
1400−9−180

Individualu1u2u3RObjX
123

ϕ259.922

RCon2X
111

ϕ3−2
1−1

RCon3X
312infimum−2−9−180
RVNumX
212Breach

MCR (worst)

time [s]SRtimeSRtimeAT

AT12500
AT12400
AT12300
AT2
AT380,4500
AT350,2700

58
18051
60
60

34.3
72.7
—
245.1
31.3
108.8

60
55
37
54
60
59

33.9
147.0
326.4
307.9
24.4
127.7

60
280
43
60
56

38.9
87.3
—
233.1
31.0
157.0

AFC

AFC

43

272.4

54

288.2

48248.3

WT

WT

60

175.7

60

174.0

59

180.1

implementation of CMA-ES by [5]) and combined with MCR(also implemented in Python).
In our experiments, we used the benchmark models from [8]and specifications. We set a timeout in 600 seconds; andmeasured the success rate (out of 60 trials) and the average
elapsed time of the successful trials. See [9] for the detailsof the models, the specifications, and other experiment setups.
Table II summarizes the experiments results.
When one translates optimization-based falsification into
constrained optimization, there is freedom in the choice of theobjective conjunct. In our experiments, we tried each conjunctin a specification as the optimization target, and we report theperformance of the best and the worst choices.
The experiment results suggest that MCR successfully addresses the scale problem. The advantage of MCR is more
obvious in challenging problem instances such as AT12400 ,AT12300 and AFC. AT2 and AT3 are less challenging ones
where the scale problem is less eminent; for these problem
instances, too, MCR’s performance is comparable or better
compared to plain Breach.
The hardest instance AT12300 , in which the performance gap
between MCR (best) and MCR (worst) is largest, indicatesthat a bad choice of the objective may have a negative effecton the performance of MCR. However, the effect is not so
critical, observing that the performance of MCR (worst) is
comparable or better compared to Breach without MCR inevery benchmarks.

TABLE IE XAMPLE ; USUAL ROBUST SEMANTICS ( TOP ) AND MCR SCORING( BOTTOM ) FOR INDIVIDUALS
Individual
u1
u2
u3

MCR (best)

SRSpec. ϕFX758Example 4. In the setting of Example 2, for certain individuals
in X = hu1 , u2 , u3 i, their robustness values JM(ui ), ϕj K withrespect to ϕ1 , ϕ2 , ϕ3 are shown in the top part of Table I.
The usual robust semantics indicates the input u1 is thebest individual among X, of which the infimum is the largest.
However, once we inspect the input signals u1 , u2 , u3 , it
becomes obvious that u1 is the farthest from desired—it isin fact the signal in which brake is constantly the maximum
and throttle is constantly 0.
This mismatch between the robustness-based preference andhuman intuition comes from the scale problem. The robustnessof ϕ3 (namely gear) tends to mask that of others.
In contrast, the MCR scoring function gives different preference, as shown in the bottom part of Table I. Here we pickthe formula ϕ1 ≡ [0,30] (rpm ≤ 2400) as the objective; theothers ϕ2 , ϕ3 are deemed to be as constraints.
The scoring function FX indicates the best input is u2 .
This matches human intuition: the input signal u2 is one
with moderate throttle and no braking. The signal u2 satisfies
ϕ2 , ϕ3 and almost satisfies ϕ1 , violating the RPM limit 2400
only by 9.

V. F UTURE W ORK
One future work is to extend our idea of using the constrained optimization problem to a more general form of specifications than the conjunctive specifications in the synthesis
problem. Investigating a method to choose a good objective
conjunct is another future work.
R EFERENCES[1] G. E. Fainekos and G. J. Pappas, “Robustness of temporal logic specifications for continuous-time signals,” Theor. Comput. Sci., vol. 410, no. 42,
pp. 4262–4291, 2009.
[2] A. Donzé and O. Maler, “Robust satisfaction of temporal logic over realvalued signals,” in Formal Modeling and Analysis of Timed Systems - 8thInt. Conf., FORMATS 2010, 2010, pp. 92–106.
[3] B. Hoxha, H. Abbas, and G. Fainekos, “Benchmarks for temporal logic
requirements for automotive systems,” in ARCH14-15, ser. EPiC Series
in Computing, vol. 34. EasyChair, 2015, pp. 25–30.

IV. E XPERIMENTS
We implemented our conjunctive synthesis algorithm(henceforth denoted by “MCR”) by combining Breach [7]with MCR. In our implementation, we replaced the MATLAB
implementation of CMA-ES with pycma (a standard Python2

[4] Z. Zhang, I. Hasuo, and P. Arcaini, “Multi-armed bandits for booleanconnectives in hybrid system falsification,” in Proc. CAV 2019, Part I,
ser. LNCS, vol. 11561. Springer, 2019, pp. 401–420.
[5] N. Hansen, “The CMA evolution strategy: A tutorial,” CoRR, vol.
abs/1604.00772, 2016.
[6] R. de Paula Garcia, B. S. L. P. de Lima, A. C. de Castro Lemonge, andB. P. Jacob, “A rank-based constraint handling technique for engineering
design optimization problems solved by genetic algorithms,” Computers
and Structures, vol. 187, pp. 77–87, 7 2017.
[7] A. Donzé, “Breach, A toolbox for verification and parameter synthesisof hybrid systems,” in Proc. CAV 2010, 2010, pp. 167–170.
[8] G. Ernst, P. Arcaini, I. Bennani, A. Donze, G. Fainekos, G. Frehse,
L. Mathesen, C. Menghi, G. Pedrielli, M. Pouzet, S. Yaghoubi, Y. Yamagata, and Z. Zhang, “Arch-comp 2020 category report: Falsification,” inProc. ARCH 2020, ser. EPiC Series in Computing, vol. 74. EasyChair,
2020, pp. 140–152.
[9] S. Sato, M. Waga, and I. Hasuo, “Constrained optimization for falsification and conjunctive synthesis,” CoRR, vol. abs/2012.00319, 2020,preprint, to appear in 7th IFAC Conference on Analysis and Design ofHybrid Systems, ADHS 2021, July 7-9, 2021, Brussels, Belgium.

3