Saved in:
| Main Authors: | , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2603.17293 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866910057723068416 |
|---|---|
| author | Jouve-Genty, Martin Su, Han Sato, Sota An, Jie Zhang, Zhenya Hasuo, Ichiro |
| author_facet | Jouve-Genty, Martin Su, Han Sato, Sota An, Jie Zhang, Zhenya Hasuo, Ichiro |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2603_17293 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | STLts-Div: Diversified Trace Synthesis from STL Specifications Using MILP (Extended Version) Jouve-Genty, Martin Su, Han Sato, Sota An, Jie Zhang, Zhenya Hasuo, Ichiro Systems and Control 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. |
| title | STLts-Div: Diversified Trace Synthesis from STL Specifications Using MILP (Extended Version) |
| topic | Systems and Control |
| url | https://arxiv.org/abs/2603.17293 |