Constrained Optimization for Hybrid System
Falsification and Application to Conjunctive
Synthesis
Sota Sato, Masaki Waga, Ichiro Hasuo
National Institute of Informatics, Tokyo, JapanThe Graduate University for Advances Studies (SOKENDAI), Hayama, Japan

Hybrid system falsification of CPS[Fainekos & Pappas, Theor. Comput. Sci. 2009]

Input 𝑢System model ℳ

Throttle

Brake

100

10080806060

404020200102030,

01020

Speed

Automatic transmission system (Simulink)00

Output ℳ 𝑢

30

RPMGear

1403000

41052250

3701500

235750100102030,

00102030,00102030Specification 𝜑𝜑 ∶≡ □[$,&$] (speed < 100)

Goal: to find an input signal 𝑢, s.t. ℳ 𝑢 ⊭ φ
S. Sato <sotasato@nii.ac.jp>

2Hybrid system falsification of CPS[Fainekos & Pappas, Theor. Comput. Sci. 2009]

Input 𝑢System model ℳ

Throttle

Brake

100

100

80806060

404020200102030,

01020

Speed

Automatic transmission system (Simulink)

00Output ℳ 𝑢

30RPMGear

140

3000

41052250

370

1500

235750100102030,

00102030,

00102030

Specification 𝜑𝜑 ∶≡ □[$,&$] (speed < 100)Always for 𝑡 ∈ [0,30]

Speed is below 100

Goal: to find an input signal 𝑢, s.t. ℳ 𝑢 ⊭ φ
S. Sato <sotasato@nii.ac.jp>

3Robust semantics of STL [Donze & Maler, FORMATS’10]
Specification: 𝜑 ≡ □[",$"] (speed 𝑡 < 100)
Speed

Speed

125

125

100

10075

5075

5025502500Robustnessℳ u ,φ125

10075

Violation degree

Speed102025030

01020

30

001020

Far from violation

Almost violated

Violated

40

10-1030ℳ 𝑢 ⊭ φ ⇔ ℳ u ,φ < 0S. Sato <sotasato@nii.ac.jp>

4Optimization-based falsificationFalsification Problem is translated into:
Try minimizing ℳ u , φ and finish if ℳ u , φ < 0Less robust

Input

𝑢!

𝑢"

𝑢#Robustnessℳ u ,φ40

10-10Speed

Speed

Speed

125

125

125

100

10010075

7575505050

2525

2500

S. Sato <sotasato@nii.ac.jp>102030Optimized by
Hill-climbing style algorithms(HC, SA, GNM, CMA-ES, …)Less robust00

102030Robustness

Go down!

𝑢!
𝑢"00102030

Input

5Synthesis is the dual of falsification
Falsification problem

Try minimizing ℳ u , ¬φ and finish if ℳ u , ¬φ < 0ℳ 𝑢 ⊭ ¬φ ⇔ ℳ 𝑢 ⊨ φSynthesis problem

Try maximizing ℳ u , φ and finish if ℳ u , φ > 0S. Sato <sotasato@nii.ac.jp>

6Conjunctive synthesis
System model ℳ

Input 𝑢BrakeThrottle
100
80
6040
200010 20 30,

Speed

Automatic transmission system (Simulink)

100
80
6040
2000Output ℳ 𝑢Specification 𝜑Gear

140
105

3000
2250

4370

1500

23507500

100 10 20 30

10 20 30

RPM,

0 10 20 30,

0102030

and𝜑: ≡ 𝜑! ∧ ⋯ ∧ 𝜑"
Goal: to find an input signal 𝑢, s.t. ℳ 𝑢 ⊨ 𝜑. ∧ ⋯ ∧ 𝜑/(⟺ ℳ 𝑢 ⊨ 𝜑/, … , ℳ 𝑢 ⊨ 𝜑0 )S. Sato <sotasato@nii.ac.jp>

7

Example of Conjunctive synthesis
Conjunctive specification 𝜑 AT : ≡ 𝜑!"# ∧ 𝜑$"# ∧ 𝜑%"#𝜑!$% : ≡ □ &,#& rpm ≤ 2400 , 𝜑"$% : ≡ □ &,#& speed ≤ 60 , 𝜑#$% : ≡ ♢ &,#& gear ≥ 3
Eventually reach gear ≥ 3

S. Sato <sotasato@nii.ac.jp>

8

Example of Conjunctive synthesis
Conjunctive specification 𝜑 AT : ≡ 𝜑!"# ∧ 𝜑$"# ∧ 𝜑%"#𝜑!$% : ≡ □ &,#& rpm ≤ 2400 , 𝜑"$% : ≡ □ &,#& speed ≤ 60 , 𝜑#$% : ≡ ♢ &,#& gear ≥ 3
Eventually reach gear ≥ 3
RPM

Gear

Speed

Speed

RPM

Gear

3000

14043000

140

42250

105

32250

105

370

21500

70

235

1750

35

10000

1500
750
001020𝜑!"# : Satisfied

30,

0102030,𝜑$"# : Satisfied

0102030

𝜑%"# : Violated

0102030

𝜑!"# : Violated,

0102030,00 5 10 15 20 25 30

𝜑$"# : Violated 𝜑%"# : Satisfied

Satisfying all conjuncts are required
S. Sato <sotasato@nii.ac.jp>9Challenge: Scale problem• Usual robust semantics of conjunction [Fainekos & Pappas, FATES & RV’06]= ℳ 𝑢 , 𝜑.01 ⊓ ⋯ ⊓ ℳ 𝑢 , 𝜑201

ℳ 𝑢 , 𝜑 01

infimum
Speed

RPM
3000-300

2250
1500
750
00102030𝜑!"# : Violated

,

Gear

140

4105

370

21500

35

1750

0000

102030,-20102030

𝜑$"# : Satisfied 𝜑%"# : Violatedℳ 𝑢 , 𝜑 $% = -300

Speed

RPM

Gear

3000

14042250

105

370

235

1-300
01020,30𝜑!"# : Violated

00102030,

00 5 10 15 20 25 30𝜑$"# : Satisfied 𝜑%"# : Satisfiedℳ 𝑢 , 𝜑 $% = -300

No improvement?

👎 Contribution of small-scale conjunct is masked
S. Sato <sotasato@nii.ac.jp>

10Conjunctive synthesis by constrained optim.
Maximize ℳ 𝑢 , 𝜑.01 ⊓ ⋯ ⊓ ℳ 𝑢 , 𝜑201

Maximize ℳ 𝑢 , 𝜑.01
Subject to ℳ 𝑢 , 𝜑301

Choose one conjunct as the optimization target> 0, ℳ 𝑢 , 𝜑201 > 0
No masking

S. Sato <sotasato@nii.ac.jp>

11Multiple constraint ranking
How to effectively search the solution of constrained optimization?
è MCR [de Paula Garcia et al., Computers and Structures 2017]• Balances multiple preferences of the solution of constrained optimization• Objective function, violation degrees, the number of violated constraints• Scale-invariant• No hyper-parameter

S. Sato <sotasato@nii.ac.jp>12Preferred solutions of constrained optim.
Robustness for each conjuncts

S. Sato <sotasato@nii.ac.jp>

𝜑!$% (objective)

𝜑"$%

𝜑#$%

𝑢!

1400

-10-3𝑢"

1400

59.9

0

𝜑!$% (objective)

𝜑"$%

𝜑#$%

𝑢!

1400

59.9-2𝑢"1400

59.9-1

𝜑!$% (objective)

𝜑"$%

𝜑#$%

𝑢!

-1000

59.90𝑢"-3059.90Feasible is preferred

Small violation degree
is preferred

Large fitness ispreferred
13Formal definition of MCR
For a population 𝑋 of candidate inputs, one prioritizes individuals 𝑢 ∈ 𝑋 by
*RVNum& 𝑢 + =𝐹& 𝑢 ≔'()

'RCon& 𝑢*

RObj& 𝑢 + RVNum& 𝑢 + ='()

Feasibles are always prior to infeasibles(if no feasible solution)'

RCon& 𝑢(otherwise)

Smaller is better• RObj compares the value of objective function• RCon compares the violation degree of each constraints• RVNum compares the number of violated constraints
S. Sato <sotasato@nii.ac.jp>

14

Example: Usual semantics
Robustness for each conjuncts

Individual

𝜑!$% (objective)

𝜑"$%

𝜑#$%

𝑢!

1400

59.9-3𝑢"-920𝑢#-1802-1(Naive input)

𝑢! =Throttle
100
80
60
40
2000(Almost-satisfying input)

𝑢" =

2030,

10080
60
40
200

ℳ(𝑢! ) =0Throttle

1020

1020

30

3000

42250

370

1500

235

750

1000,

1020

102030,

0Speedℳ(𝑢" ) =
30

Gear

105

30

10080
60
40
2000RPM

140Brake

10080
60
40
2000S. Sato <sotasato@nii.ac.jp>

10SpeedBrake

102030,00 5 10 15 20 25 30

RPM

Gear

140

3000

4105

2250

370

1500

2357501000102030,

0102030,00 5 10 15 20 25 3015Example: Usual semantics
Robustness for each conjuncts

Individual

𝜑!$% (objective)

𝜑"$%

𝜑#$%

infimum𝑢!

1400

59.9-3-3

𝑢"

-9

20-9

𝑢#-1802-1-180(Naive input)

𝑢! =Throttle

0(Almost-satisfying input)

𝑢" =

2030,

10080
60
40
200

ℳ(𝑢! ) =0Throttle

1020

1020303000

422503701500

2357501000,

1020102030,0Speedℳ(𝑢" ) =30Gear

105

30

100806040
2000RPM

140

Brake

100
80
60402000S. Sato <sotasato@nii.ac.jp>

10SpeedBrake

100806040
200Usual (infimum) semantics
says 𝑢/ is the most preferred

102030,00 5 10 15 20 25 30

RPM

Gear

140

3000

4105

2250

370

1500

2357501000

102030,0102030,00 5 10 15 20 25 30

16

Example: Calculating MCR
Robustness for each conjuncts

Individual𝑢!
𝑢"𝑢#

RobjX /robustness of 𝜑1𝐴𝑇𝜑!$% (objective)

𝜑"$%

𝜑#$%

1400

59.9-3-9

22

RConX2 /RConX3 /%RVNum! 𝑢 + *0-180

violation deg. of 𝜑2𝐴𝑇

𝐹! 𝑢

"#$

≔"#$RVNumX /# of violated constraints(if no feasible solution)"

RCon! 𝑢(otherwise)

FX

𝑢1

1st / 1400

1st / 0

3rd / -3

2nd / 17 (= 1 + 1 + 3 + 2)

𝑢2

2nd / -9

1st / 0

1st / 0

1st / 05 (= 2 + 1 + 1 + 1)

𝑢3

3rd / -180

1st / 0

2nd / -1

2nd / 18 (= 3 + 1 + 2 + 1)

S. Sato <sotasato@nii.ac.jp>%

RObj! 𝑢 + RVNum! 𝑢 + *-1violation deg. of 𝜑3𝐴𝑇"RCon! 𝑢

MCR says 𝑢P isthe most preferred
17

Example: Usual semantics vs. MCR

Usualsemantics

MCR

S. Sato <sotasato@nii.ac.jp>

𝜑!$% (objective)

𝜑"$%

𝜑#$%

infimum𝑢!

1400

59.9-3-3𝑢"

-9

20-9

𝑢#

-180

2-1-180

𝜑!$% (objective)

𝜑"$%

𝜑#$%

FX𝑢!

1400

59.9-3

7𝑢"-9205

𝑢#-1802-18

MCR fits ourintuition

18

MCR for falsification• Optimization algorithm should be population-based• We adopt CMA-ES [Hansen & Ostermeier, International Conference on Evolutionary Computation 1996]• CMA-ES is commonly used in optimization-based falsification

FX𝑢!
𝑢"
Input
https://en.wikipedia.org/wiki/CMA-ES
S. Sato <sotasato@nii.ac.jp>

19Experimental setting
Model• Automatic transmission [Hoxha et al., ARCH’15]• Abstract fuel Control [Jin et al., HSCC’14]• Wind Turbine [Schuler et al., ARCH’16]
Solver• Breach (state-of-the-art falsification solver) [Donze, CAV’10]• MCR (Breach + MCR calculator implemented in Python)• Choose each conjunct as the optimization target and report best and worst results
Metrics• Success rate (per 60 trials)• Average elapsed time of successful trials
Particularly exhibits
the scale problem

S. Sato <sotasato@nii.ac.jp>

20Experimental results

CMA-ES. MCR adTABLE II
E XPERIMENTAL RESULTS . F OR EACH PROBLEM INSTANCE , THE BEST
and/or the objective
The choice ofRESULT IS HIGHLIGHTED AND THE LARGEST SR IS SHOWN IN BLUE .
optimization target
Our approachof robustness values
candidate solutions.
BreachMCR (best)
MCR (worst)
ModelSpec. 'or the optimization
SRtime [s]SRtimeSRtimeCMA-ES consists ofAT
AT12500
58
34.3
60
33.9
60
38.9
AT12400
1872.755
147.0
2887.3f , in the selection
AT12300
0—37326.4
0—
on FX , relies on theAT2
51245.154307.943233.1
AT380,4500
60
31.3
60
24.4
60
31.0
is a natural number,
AT350,2700
60
108.8
59
127.7
56
157.0
med fitter.
AFCAFC
43272.4
54288.2
48248.3
e kinds of functions
WT
WT
60
175.7
60
174.0
59
180.1
uitable “rank” of theobjective function f ,(j = 2, . . . , m) comimplementation of CMA-ES by [5]) and combined with MCRM(v), 'j ]]. RVNumX• Largerstsuccessratesinare
show in blue(alsoimplementedPython).
ints.
• Best combinationof (SR,wetime)
In our experiments,
used isthehighlighted
benchmark models from [8]and specifications. We set a timeout in 600 seconds; andmeasured the success rate (out of 60 trials) and the average
S. Sato<sotasato@nii.ac.jp>
ANDMCRSCORING21

RQ1: Does MCR address the scale problem?

CMA-ES. MCR adTABLE II
E XPERIMENTAL RESULTS . F OR EACH PROBLEM INSTANCE , THE BEST
and/or the objective
RESULT IS HIGHLIGHTED AND THE LARGEST SR IS SHOWN IN BLUE .
of robustness values
candidate solutions.
BreachMCR (best)
MCR (worst)
ModelSpec. 'or the optimization
SR
time [s]
SR
time
SR
time
CMA-ES consists ofAT
AT12500
58
34.3
60
33.9
60
38.9
Breach always failed but MCR
AT12400
1872.7
55
147.0
28
87.3
f , in the selection
succeeded 37 times (/60)
AT12300
0—37326.40—
on FX , relies on theAT2
51245.1
54307.943233.1
AT380,4500
6031.360
24.4
60
31.0
is a natural number,
AT350,2700
60
108.8
59
127.7
56
157.0
med fitter.
AFCAFC
43272.4
54288.2
48248.3
e kinds of functions
WTWT
60
175.7
60
174.0
59
180.1
uitable “rank” of theobjective function f ,Our approach resulted higher SR in most cases (blue)(j = 2, . .•. , Yes.
m) comimplementationof CMA-ESby [5])where
and combined
withproblem
MCR
Specifically,
the advantage
is obvious
the scaleis moreM(v), 'j ]].• RVNum
Xeminent (also implemented in Python).
ints.
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 averageAND
MCR
SCORING
S. Sato<sotasato@nii.ac.jp>

22

RQ2:
How
importantisthechoiceoftheCMA-ES. MCR adTABLE II
E conjunct in. F MCR?
,objective
and/or theobjective
SR.
XPERIMENTAL RESULTS
OR EACH PROBLEM INSTANCE THE BESTRESULT IS HIGHLIGHTED AND THE LARGESTIS SHOWN IN BLUEof robustness values
The performance of MCR (worst) is comparable orcandidate solutions.
bettercompared
BreachMCR (best)
MCR(worst) to Breach in every benchmarks.
ModelSpec. 'or the optimization
SRtime [s]SRtimeSRtime
CMA-ES consists ofAT
AT12500
58
34.3
60
33.9
60
38.9
AT12400
1872.7
55
147.0
28
87.3
f , in the selection
AT12300
0—37326.4
0—
on FX , relies on theAT2
51
245.1
54
307.9
43
233.1
AT380,4500
60
31.3
60
24.4
60
31.0
is a natural number,
AT350,2700
60
108.8
59
127.7
56
157.0
med fitter.
AFCAFC
43272.4
54
288.2
48248.3
e kinds of functions
WTWT
60
175.760
174.059180.1
uitable “rank” of theobjective function f ,(j = 2, . . . , m) comimplementationof CMA-ESby [5])with MCR
A badXchoice
had a negativeeffectonand
thecombined
performanceof MCR
M(v), 'j ]].• RVNum
implemented in Python).
ints.
• The effect(alsois not
so critical
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
ANDMCRSCORING
S. Sato<sotasato@nii.ac.jp>
23Future work and Conclusion
Future work
• A method to choose the good objective conjunct• Extension to more general form of specifications

Conclusion• A method solving conjunctive synthesis via constrained optimization• MCR and CMA-ES for effective optimization• Our approach addresses the scale problem

S. Sato <sotasato@nii.ac.jp>

24