STLts-Div: Diversified Trace Synthesis from STL Specifications Using MILP (Extended Version)
This addresses the need for better specification understanding in cyber-physical systems engineering, though it appears incremental as it builds on existing MILP methods for trace synthesis.
The paper tackles the problem of generating diverse traces from Signal Temporal Logic (STL) specifications to aid engineers in understanding complex cyber-physical systems, introducing STLts-Div, a tool that uses MILP encoding and diversification objectives to produce sets of behaviorally diverse satisfying traces.
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.