STLts-Div：基于STL规范的多样化轨迹合成（扩展版）
STLts-Div: Diversified Trace Synthesis from STL Specifications Using MILP (Extended Version)
AI总结：
本文提出STLts-Div方法，通过MILP编码生成满足STL规范的多样化轨迹，以更全面理解系统行为。
摘要：
现代车载系统复杂，需求常以信号时间逻辑（STL）编写。实际中编写正确的STL困难，工程师受益于具体执行以展示规范实际允许的内容。轨迹合成解决此需求，但单一见证 rarely 足以理解意图或探索边缘情况 - 满足给定STL公式的多样化行为更 informative。我们介绍多样化轨迹合成：自动生成行为多样化轨迹集。基于STL和系统模型的MILP编码，我们形式化三个互补的多样化目标 - 布尔距离、随机布尔距离和值距离 - 都由目标函数捕获并迭代求解。我们实现这些想法于STLts-Div，一个轻量Python工具，整合Gurobi。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
