Optimization-Based Model Checking and Trace Synthesis for Complex STL Specifications

TL;DR

The paper addresses bounded trace synthesis and model checking for Signal Temporal Logic (STL) specifications in cyber-physical systems by restricting to MILP-encodable, white-box models. It introduces a variable-interval STL encoding and a delta-stable partitioning framework that yields an optimization-based, anytime MILP formulation for finding traces that satisfy the spec or proving infeasibility. Core contributions include the delta-stable partitioning concept, a complete MILP encoding of STL with both Boolean and temporal operators, and exact/approximate MILP encodings for Rectangular Hybrid Automata and double-integrator dynamics, respectively, enabling scalable automotive-style analyses and parameter mining. The approach is implemented in STLts and validated on automotive-like benchmarks (RNC, NAV, ISO disturbance scenarios), showing improved performance over falsification and SMT-based methods and demonstrating practical applicability for spec analysis in CPS design.

Abstract

We present a bounded model checking algorithm for signal temporal logic (STL) that exploits mixed-integer linear programming (MILP). A key technical element is our novel MILP encoding of the STL semantics; it follows the idea of stable partitioning from the recent work on SMT-based STL model checking. Assuming that our (continuous-time) system models can be encoded to MILP -- typical examples are rectangular hybrid automata (precisely) and hybrid dynamics with closed-form solutions (approximately) -- our MILP encoding yields an optimization-based model checking algorithm that is scalable, is anytime/interruptible, and accommodates parameter mining. Experimental evaluation shows our algorithm's performance advantages especially for complex STL formulas, demonstrating its practical relevance e.g. in the automotive domain.

Figures (8)

• Figure 1: Rear-end near collision
• Figure 2: A stable partition (cf. baeBoundedModelChecking2019) for $\sigma$ and $\varphi :\equiv x \geq 1$. The symbols $\top$ and $\bot$ denote the (constant) truth value of $\varphi$ each interval $J_i$.
• Figure 3: A $\delta$-stable partition (\ref{['def:deltaStable']}) for $\sigma$ and $\varphi$. Here $\varphi^{\delta}\equiv (x\ge 1+\delta)$. $\top$ and $\bot$ are much like in \ref{['fig:stablePartitionSeq']}; the symbol $?$ indicates that the truth value is not constant in that interval. In some regions (shaded), $\sigma^t \models \varphi$ is true but $\sigma^t \models \varphi^\delta$ is not.
• Figure 4: The $\delta$-crossing pairs $(\sigma(\gamma_1), \sigma(\gamma_2))$, $(\sigma(\gamma_3), \sigma(\gamma_4))$ are stationary. The red segments are assigned $\top$ by a conservative valuation.
• Figure 5: MILP encoding of $f(t)$

Theorems & Definitions (37)

• remark 1
• definition 1: linear predicate $p$ and $\llbracket{p}\rrbracket, \pi_{p}$
• definition 2: signal
• definition 3: system model, trace set $\mathcal{L}(\mathcal{M})$
• definition 4: signal temporal logic (STL)
• proposition 1
• definition 5: finite variability rabinovichDecidabilityContinuousTime1998a
• lemma 1: baeBoundedModelChecking2019
• definition 6: stable partition
• definition 7: time sequence, timed state sequence