Optimization-Based Model
Checking and Trace Synthesis forComplex STL
Sota Sato1,3, Jie An1,4, Zhenya Zhang1,2, Ichiro Hasuo1,3
1National Institute of Informatics, Tokyo, Japan
2Kyusyu University, Fukuoka, Japan
3The Graduate University for Advances Studies (SOKENDAI), Hayama, Japan
4Institute of Software, Chinese Academy of Sciences, Beijing, China

Summary

What we achieved

How we did it

A novel algorithm to quickly synthesize atrace with an STL (signal temporal logic) [Maler &Nickovic, 2004] formula

The algorithm is fast due to ournovel variable-interval MILP (mixedinteger linear programming) encoding(Gp) ! (F[0,T ] q)<latexit sha1_base64="VZtK7zG2BQvNY6lGa9ZMRhZsL4U=">AAACF3icdZDLSgMxFIYzXmu9jbp0EyxCCzJMrb24KwrqskJv0A4lk2ba0MzFJKOUYd7Cja/ixoUibnXn25hpq6joD4Gf75xDzvntgFEhTfNdm5tfWFxaTq2kV9fWNzb1re2m8EOOSQP7zOdtGwnCqEcakkpG2gEnyLUZadmj06TeuiZcUN+ry3FALBcNPOpQjKRCPd3Idl0kh7YTncdBrsvpYCgR5/7NFz+Le1HHPKhbMbzK9fSMaVRKxcqxCU3DnCgxpXKpUID5GcmAmWo9/a3b93HoEk9ihoTo5M1AWhHikmJG4nQ3FCRAeIQGpKOsh1wirGhyVwz3FelDx+fqeRJO6PeJCLlCjF1bdSbLit+1BP5V64TSqVgR9YJQEg9PP3JCBqUPk5Bgn3KCJRsrgzCnaleIh4gjLFWUaRXC56Xwf9M8NPIlo3h5lKmezOJIgV2wB7IgD8qgCi5ADTQABrfgHjyCJ+1Oe9CetZdp65w2m9kBP6S9fgAOJZ/e</latexit>

Synthesize

Example traces• Can also solve the dual problem (boundedmodel checking)• Soundness and (weak) completenss of
the result are guaranteed
S. Sato <sotasato@nii.ac.jp>

2Outline👉 1. Challenges in Trace Synthesis with Complex STL
Formulas
2. Previous Works
3. Our Algorithm: Variable-Interval MILP Encoding
4. Experiments
S. Sato <sotasato@nii.ac.jp>3Motivation

STL formula in real-world problem may be large
Natural-language description (from ISO 34502 critical scenarios)
The subject vehicle cuts in and the precedingother vehicle changes a lane. The traffic
situation is initially safe in terms of the RSS
safety but eventually gets in danger. (…)

Formalization in STL [Reimann+, SAC’24]
Syntax tree is quite large.
Max depth: 5
Leaves: 25
Nodes : 35
S. Sato <sotasato@nii.ac.jp>

4Trace synthesis with STLFind 𝜎 ∈ ℒ ℳ

such that 𝜎 ⊨ φPossible traces of thesystem model ℳ

A trace 𝜎 satisfies an STL
formula φ

Example𝜎 : satisying trace𝜎 ⊨ ♢ !,#! (RPM > 2250)“At some 𝑡 ∈ [0,30], RPM is above 2250”

where𝜎∈ ℒ

Speed

RPM

140

3000

1052250

3701500

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

Gear102030,4Above 2250

00102030,

001020305Trace synthesis provides “debugging” of specs• There can be a difference between what one wrote and what one intended• Automatic generation of an example trace would help to recognize mistakes
WRONG(Gp) ! (F[0,T ] q)

G(p ! F[0,T ] q)<latexit sha1_base64="VZtK7zG2BQvNY6lGa9ZMRhZsL4U=">AAACF3icdZDLSgMxFIYzXmu9jbp0EyxCCzJMrb24KwrqskJv0A4lk2ba0MzFJKOUYd7Cja/ixoUibnXn25hpq6joD4Gf75xDzvntgFEhTfNdm5tfWFxaTq2kV9fWNzb1re2m8EOOSQP7zOdtGwnCqEcakkpG2gEnyLUZadmj06TeuiZcUN+ry3FALBcNPOpQjKRCPd3Idl0kh7YTncdBrsvpYCgR5/7NFz+Le1HHPKhbMbzK9fSMaVRKxcqxCU3DnCgxpXKpUID5GcmAmWo9/a3b93HoEk9ihoTo5M1AWhHikmJG4nQ3FCRAeIQGpKOsh1wirGhyVwz3FelDx+fqeRJO6PeJCLlCjF1bdSbLit+1BP5V64TSqVgR9YJQEg9PP3JCBqUPk5Bgn3KCJRsrgzCnaleIh4gjLFWUaRXC56Xwf9M8NPIlo3h5lKmezOJIgV2wB7IgD8qgCi5ADTQABrfgHjyCJ+1Oe9CetZdp65w2m9kBP6S9fgAOJZ/e</latexit><latexit sha1_base64="oqkMSXADhoAFrcxWIGYCGl/abzQ=">AAACFXicdZDLSgMxFIYz9VbrrerSTbAIFUqZWntxVxTUZYVehOlQMmmmDc1cTDJKGeYl3Pgqblwo4lZw59uYaaegoj8Efr5zDjnnt3xGhdT1Ty21sLi0vJJezaytb2xuZbd3OsILOCZt7DGPX1tIEEZd0pZUMnLtc4Ici5GuNT6L691bwgX13Jac+MR00NClNsVIKtTPFnoOkiPLDi+ivN/jdDiSiHPvbo7Po35o6IWWGcGbw342pxfr1Ur9RId6UZ8qNtVatVyGpYTkQKJmP/vRG3g4cIgrMUNCGCXdl2aIuKSYkSjTCwTxER6jITGUdZFDhBlOr4rggSIDaHtcPVfCKf0+ESJHiIljqc54WfG7FsO/akYg7boZUtcPJHHx7CM7YFB6MI4IDignWLKJMghzqnaFeIQ4wlIFmVEhzC+F/5vOUbFULVaujnON0ySONNgD+yAPSqAGGuASNEEbYHAPHsEzeNEetCftVXubtaa0ZGYX/JD2/gU0m595</latexit>

Human
correction

Synthesize
examplesSynthesize
examples…
(1) As intended…

(2) As intended (3) Not as intended …

Odd that the third trace isan example of myspecification…

(1’) As intended (2’) As intended (3’) As intended

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

My spec looks
correct…

66

But…

Existing tools suffer from trace synthesis withcomplex STL formulas• Small latency is critical forinteractive inspection of STL
formulas• Our benchmarks showed thatexisting methods were rarely
capable of it
It takes 9-500 seconds tosynthesize a trace

Breach [Donzé, CAV’10]
ForeSee [Zhang+, FM’21]
BluSTL [Donzé & Raman, ARCH15]
STLmc [Yu+, CAV’22]

Our experimental result (we revisit it later)
S. Sato <sotasato@nii.ac.jp>

7Outline

1. Challenges in Trace Synthesis with Complex STLFormulas
👉 2. Previous Works
3. Our Algorithm: Variable-Interval MILP Encoding
4. Experiments
S. Sato <sotasato@nii.ac.jp>8Discretization of the STL semantics: constant vs. variable• Due to its continuous nature (unlike LTL), discretization is required to compute STLsemantics
Mathematical definition by first-order logic𝜎 ⊨ ♢ !,#! □ !,$ RPM > 2250

⇔ ∃𝜏% ∈ 0, 30 . ∀𝜏& ∈ 𝜏% + 0, 5 . 𝜎RPM 𝜏& > 2250

Constant-step

Variable-intervals (we use this)[Donzé & Raman, ARCH15]

S. Sato <sotasato@nii.ac.jp>[Yu+, CAV’22]

9𝑁 + 1: number of sampling points

Constant-step

Input: ℳ, 𝜑, 𝑡) , … , 𝑡*
Output: 𝑥⃗+ , … , 𝑥⃗* (state sequence)

Inductive
calculation

t!

t"t"

…

t#

state𝑥⃗!

𝑥⃗$

𝑥⃗"

… 𝑥⃗%

p ≔ RPM > 2250

⊤⊤

⊤

…

⊥□ !,' p

⊥

⊥

⊥

…

⊥♢ !,(! □ !,' p⊤

⊤

⊤

…

⊥• Straightforward discretization• 𝑁 should be large for sufficient accuracy => Slowing down SMT/MILP solver• E.g., 𝑁 = 300 in our iso5 benchmark (10 samples every second)
S. Sato <sotasato@nii.ac.jp>

10

𝑁+ 1: number of sampling points

Variable-interval (we use this)Input: ℳ, 𝜑
Output: 𝛾) , 𝑥⃗) , … , 𝛾* , 𝑥⃗* (timed-statesequence){𝛾 } 𝛾 , 𝛾{𝛾 } … {𝛾 }Inductive
calculation

!

!

$$

#state𝑥⃗!

𝜆𝑥⃗!
+ 𝜆̅ 𝑥⃗%

𝑥⃗$

… 𝑥⃗%

p ≔ RPM> 2250

⊤

⊤

⊤

…

⊥□ !,' p⊥⊥⊥…

⊥♢ !,(! □ !,' p

⊤

⊤

⊤

…

⊥• Works with small 𝑁 in practice• E.g., 𝑁 = 4 in our iso5 benchmark
S. Sato <sotasato@nii.ac.jp>

Boolean values must be
constant in each intervaland subformula
11How to find a stable partition for the variable-interval?

[Bae & Lee, POPL’19]

For atomic proposition• Put sampling points whencrossing the boundary ofpredicates• (Assumption: continuous
signal and a linear predicate)

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

12How to find a stable partition for the variable-interval?

[Bae & Lee, POPL’19]

For Boolean connectives 𝜓=⋀𝜓>, 𝜓=⋁𝜓>Assuming we have stable partitions for both 𝜓+ , 𝜓; , theirrefinement is a stable partition for 𝜑
For ”Always for” operator □[:,;] 𝜓Can be formulated based on
the truth values ofsubformula and by interval
math

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

13Overview of tools
VariableintervalNo

Why slow with complex STL?

No

Fall into local solution

BluSTL [Donzé & Raman, ARCH15] MILP

No

Large sample size

STLmc [Yu+, CAV’22]
STLts (our proposed method)Yes
Yes (withUnscalability of SMT-Solver
Breach [Donzé, CAV’10]

Stoch. opt.

ForeSee [Zhang+, FM’21]

Stoch. opt. + MCTS

SMTMILP

Fall into local solution

modification)

We use MILP + Variable-interval encoding

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

14Outline

1. Challenges in Trace Synthesis with Complex STLFormulas
2. Previous Works👉 3. Our Algorithm: Variable-Interval MILP Encoding
4. Experiments
S. Sato <sotasato@nii.ac.jp>

15Challenge

MILP (numerical) cannot faithfully express the variableinterval encoding, unlike SMT (symbolic)With variable-interval encoding

With MILP• It manages the truth values of open
intervals and singular intervals• Only nonstrict inequality ≤ is allowed

https://github.com/BYU-PRISM/GEKKOCannot be combined
S. Sato <sotasato@nii.ac.jp>

16Can we interpret truth values on closed intervals?
Naive idea
• Given: signal 𝜎, STL formula 𝜑• Find: 𝛾) < ⋯ < 𝛾* such that𝜎 ! ⊨ 𝜑 or 𝜎 ! ⊭ 𝜑 is constant on eachclosed interval𝛾) , 𝛾+ , 𝛾+ , 𝛾; , … , [𝛾*<+ , 𝛾* ]=> This idea does not work

Not constant at its leftedge

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

17Can we interpret truth values on closed intervals?
Naiive idea
• Given: signal 𝜎, STL formula 𝜑• Find: 𝛾) < ⋯ < 𝛾* such that
SolverVariable𝜎 ! ⊨ 𝜑 or 𝜎 ! ⊭ 𝜑 constantlyholdsininterval
each closed interval
BluSTL [Donzé & Raman, ARCH15] MILPNo𝛾) , 𝛾+ , 𝛾+ , 𝛾; , … , [𝛾*<+ , 𝛾* ]STLmc [Yu+, CAV’22]
SMT
proposed=>STLtsThis(ourideadoesmethod)
not workMILP

Yes
Yes (withmodification)

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

Why slow with complex STL?
Large sample size
Unscalability of SMT
Not constant at its leftedge18

Introducing 𝛿-tightening of formula• Purely syntactic modification• Commutative with subformulas (𝜓 = implies 𝜓 for each subformula)(𝛿: small positive real constant)𝜑: ≡ ♢ ?,@? □ ?,A RPM > 2250

Tightening

𝜑 B : ≡ ♢ ?,@? □ ?,A RPM > 2250 + 𝛿□ ?,A RPM > 2250

□ ?,A RPM > 2250 + 𝛿

RPM > 2250

RPM > 2250 + 𝛿
S. Sato <sotasato@nii.ac.jp>

19Can we interpret truth values on closed intervals?
Our revised idea
• Given: signal 𝜎, STL formula 𝜑• Find: 𝛾! < ⋯ < 𝛾$ such that!

!

𝜎 ⊨ 𝜑 or 𝜎 ⊭ 𝜑"is constanton each closed interval𝛾! , 𝛾% , 𝛾% , 𝛾& , … , [𝛾$'% , 𝛾$ ]Constantly 𝜎 C ⊨ 𝜑 or 𝜎 C ⊭ 𝜑 B

S. Sato <sotasato@nii.ac.jp>20𝜹-tightening is consistent with STL semantics
Proposition

Let 𝜑 be an STL formula in NNF (negation-normal form), 𝜎 be a continuous signal, 𝛿 > 0.
There exists a sequence 𝛾? < ⋯ < 𝛾D for some 𝑁 such that for each 𝑖 ∈ [1, 𝑁] and 𝜓 ∈𝑠𝑢𝑏 𝜑 either of 𝜎 C ⊨ 𝜓 or 𝜎 C ⊭ 𝜓 B is constant on [𝛾EF=, 𝛾E ].

Inductive
calculation[𝛾! , 𝛾$ ]

[𝛾$ , 𝛾" ]…

[𝛾#)$ , 𝛾#]state𝜆𝑥⃗!
+ 𝜆̅ 𝑥⃗%𝜆𝑥⃗$+ 𝜆̅ 𝑥⃗"…

𝜆𝑥⃗%)$+ 𝜆̅ 𝑥⃗%

p

⊤

⊤

…

⊥ (𝛿)

□ !,' p

⊥ (𝛿)

⊥ (𝛿)

…

⊥ (𝛿)

♢ !,(! □ !,' p

⊤

⊤

…

⊥ (𝛿)

(⊥ (𝛿) is shorthand for 𝜎 * ⊭ 𝜓 + for any t ∈ [𝛾,)$ , 𝛾, ])S. Sato <sotasato@nii.ac.jp>

21

Our variable-interval MILP algorithm
Trace synthesis problem
Find 𝜎 ∈ ℒ ℳ such that 𝜎 ⊨ φ
MILP formulation (used in our algorithm)

Minimize cost(𝑣)subject to𝑣 ∈ Enc 𝜑, ℳ, 𝑁, 𝛿𝑣 satisfies the (mixed) integrity condition
where 𝑣 = [ 𝛾?, 𝑥⃗? , … , (𝛾D , 𝑥⃗G), … (other auxiliary variables)]A piecewise-linear trace can be represented
by variables 𝛾! , … , 𝛾% and 𝑥⃗! , … , 𝑥⃗#
S. Sato <sotasato@nii.ac.jp>

22

Example MILP constraints(details are not important)

Note•
We use the Boolean symbols ∧,∨,¬ and the indicatorrelation ⇒ since they are commonly supported in mostMILP solvers•
It is clear that the interval arithmetic in D2.1-D3.3 can berewritten into MILP constraints

Let 𝜑: ≡ □[!,0] 𝑝, where 𝑝: ≡ 𝛼 > 8:
𝛾- , 𝑥,,. must represent a trace of given modelManage truth values of 𝑝 in eachinterval [𝛾-)$ , 𝛾- ]Manage truth values of □[!,0] 𝑝 in eachinterval [𝛾-)$ , 𝛾- ]□[!,0] 𝑝 must be true at 𝑡 = 0
S. Sato <sotasato@nii.ac.jp>

23Correctness of our encoding• With 𝛿 small enough and 𝑁 large enough, our algorithm can always find asatisfying trace (if exists).
• In most application, this is not really a limitation.
Soundness (Theorem 4.17)

Let 𝜑 be an STL formula in NNF (negation-normal form), ℳ be a model, N ∈ ℕ, and 𝛿 >0. If a feasible solution 𝑣 lies in our MILP constraints Enc(𝜑, ℳ, 𝑁, 𝛿), the induced trace
𝜎 has 𝜎 ∈ ℒ ℳ and 𝜎 ⊨ φ.
Completeness up to 𝛿 and 𝑵 (Theorem 4.18)

Assume the setting above. If there is a piecewise-linear 𝜎 ∈ ℒ ℳ such that 𝜎, 𝜑 ≥ 𝛿(the quantitative sementics is greater than 𝛿), there is an feasible solution 𝑣 that lies inEnc(𝜑, ℳ, 𝑁, 𝛿) for some N ∈ ℕ.
S. Sato <sotasato@nii.ac.jp>24Outline

1. Challenges in Trace Synthesis with Complex STL
Formulas
2. Previous Works
3. Our Algorithm: Variable-Interval MILP Encoding👉 4. Experiments
S. Sato <sotasato@nii.ac.jp>

25Experimental setting
Tools

Benchmark models and specs
Supported class Variableof modelinterval

Breach [Donzé, CAV’10]

Black-box

No

ForeSee [Zhang+, FM’21]

Black-box

No

BluSTL [Donzé & Raman, ARCH15]

White-box (MILP) No

STLmc [Yu+, CAV’22]

White-box (SMT)

STLts (our proposed method)White-box (MILP) Yes

Navigation ofrobot in a room

(nondeterministiclinear dynamics) [Bu+, ARCH22]

Rear-end nearcollision & ISO34502

Yes(quadratic dynamics)

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

26Experimental results
Our tool

Latency small enough(0.1~9.9s) for interactive
inspection of STL specs(Gp) ! (F[0,T ] q)<latexit sha1_base64="VZtK7zG2BQvNY6lGa9ZMRhZsL4U=">AAACF3icdZDLSgMxFIYzXmu9jbp0EyxCCzJMrb24KwrqskJv0A4lk2ba0MzFJKOUYd7Cja/ixoUibnXn25hpq6joD4Gf75xDzvntgFEhTfNdm5tfWFxaTq2kV9fWNzb1re2m8EOOSQP7zOdtGwnCqEcakkpG2gEnyLUZadmj06TeuiZcUN+ry3FALBcNPOpQjKRCPd3Idl0kh7YTncdBrsvpYCgR5/7NFz+Le1HHPKhbMbzK9fSMaVRKxcqxCU3DnCgxpXKpUID5GcmAmWo9/a3b93HoEk9ihoTo5M1AWhHikmJG4nQ3FCRAeIQGpKOsh1wirGhyVwz3FelDx+fqeRJO6PeJCLlCjF1bdSbLit+1BP5V64TSqVgR9YJQEg9PP3JCBqUPk5Bgn3KCJRsrgzCnaleIh4gjLFWUaRXC56Xwf9M8NPIlo3h5lKmezOJIgV2wB7IgD8qgCi5ADTQABrfgHjyCJ+1Oe9CetZdp65w2m9kBP6S9fgAOJZ/e</latexit>

Synthesize

Time (sec) to synthesize a trace

Example traces

27

How should we choose the constant 𝑁?
• 𝑁 should be sufficiently large for completeness• In practice, start with a small 𝑁 andincrementally try a larger 𝑁

𝑁 is the number of variableintervals (Here 𝑁=4)

Computational cost is
low if 𝑁 is small
𝑁

ISO6 benchmark
S. Sato <sotasato@nii.ac.jp>28

Conclusion:• First practical algorithm for handling complex STLformulas• Demonstrated with a real-world ISO example• Proposed a consistent framework, 𝛿-stability, to relax
the stable partitioning

Classofmodel

VariableintervalBlackboxNoForeSee [Zhang+, FM’21] Blackbox

No

Breach [Donzé, CAV’10]

Future work:• Application to falsification problem of black-box models BluSTL

MILP

No

STLmc [Yu+, CAV’22]

SMT

Yes

STLts (ours)

MILP

Yes

[Donzé & Raman,

ARCH15]• Generate diverse examples as desired by users

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

29