Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

STLts-Div: Diversified Trace Synthesis from STL Specifications Using MILP (Extended Version)

Martin Jouve-Genty, Han Su, Sota Sato, Jie An, Zhenya Zhang, Ichiro Hasuo

Abstract

Modern cyber-physical systems are complex, and requirements are often written in Signal Temporal Logic (STL). Writing the right STL is difficult in practice; engineers benefit from concrete executions that illustrate what a specification actually admits. Trace synthesis addresses this need, but a single witness rarely suffices to understand intent or explore edge cases - diverse satisfying behaviors are far more informative. We introduce diversified trace synthesis: the automatic generation of sets of behaviorally diverse traces that satisfy a given STL formula. Building on a MILP encoding of STL and system model, we formalize three complementary diversification objectives - Boolean distance, random Boolean distance, and value distance - all captured by an objective function and solved iteratively. We implement these ideas in STLts-Div, a lightweight Python tool that integrates with Gurobi.

STLts-Div: Diversified Trace Synthesis from STL Specifications Using MILP (Extended Version)

Abstract

Modern cyber-physical systems are complex, and requirements are often written in Signal Temporal Logic (STL). Writing the right STL is difficult in practice; engineers benefit from concrete executions that illustrate what a specification actually admits. Trace synthesis addresses this need, but a single witness rarely suffices to understand intent or explore edge cases - diverse satisfying behaviors are far more informative. We introduce diversified trace synthesis: the automatic generation of sets of behaviorally diverse traces that satisfy a given STL formula. Building on a MILP encoding of STL and system model, we formalize three complementary diversification objectives - Boolean distance, random Boolean distance, and value distance - all captured by an objective function and solved iteratively. We implement these ideas in STLts-Div, a lightweight Python tool that integrates with Gurobi.
Paper Structure (20 sections, 3 theorems, 20 equations, 3 figures, 2 tables)

This paper contains 20 sections, 3 theorems, 20 equations, 3 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Signal Temporal Logic (STL)
  4. Finite Variability
  5. MILP-Based Trace Synthesis
  6. Diversity-Aware Synthesis
  7. Boolean Distance Method (BD)
  8. Randomized Boolean Distance Method (RBD)
  9. Value Distance Method (VD)
  10. Demonstration of STLts-Div
  11. Experimental Analysis
  12. Experiment Setting
  13. Danger then stop (DSTOP)
  14. Rear-End Near Collision (RNC1–3)
  15. Navigation (NAV1–2)
  16. ...and 5 more sections

Key Result

lemma 1

Suppose there is a conservative valuation $\Theta$ of an STL formula $\varphi$ in a time sequence $\Gamma$ on $\sigma$ up to $\delta$. Then $\Gamma$ is $\delta$-stable for $\sigma$ and $\varphi$.

Figures (3)

  • Figure 1: Workflow for MILP-based trace synthesis using STLts-Div.
  • Figure 2: The NAV1--2 RHA
  • Figure 3: Round time of $\mathtt{DSTOP}$, $\mathtt{RNC1}$, $\mathtt{RNC2}$, $\mathtt{RNC3}$.

Theorems & Definitions (19)

  • definition 1: finite variability rabinovich1998decidability
  • definition 2: time sequence, time state sequence Sato2024
  • definition 3: piecewise-linear signal Sato2024
  • definition 4: $\delta$-tightening of STL formulas in NNF Sato2024
  • definition 5: $\delta$-stability Sato2024
  • definition 6: conservative valuation Sato2024
  • lemma 1: Sato2024
  • definition 7: Boolean distance
  • remark 1
  • remark 2
  • ...and 9 more