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

TL;DR

This paper presents STLts-Div, a Python tool that automatically generates diverse, behaviorally distinct traces satisfying STL specifications, aiding engineers in understanding and exploring system requirements more effectively.

Contribution

It introduces a novel diversified trace synthesis method using MILP encoding of STL, enabling the generation of multiple distinct behaviors for complex cyber-physical systems.

Findings

Successfully generates diverse traces satisfying STL specifications.

Integrates with Gurobi for efficient MILP solving.

Enhances understanding of system requirements through varied behaviors.

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.