SemML 2.0 用机器学习加速LTL控制器合成，性能超越现有工具。
SemML 2.0: Synthesizing Controllers for LTL
- 结合自动机理论与机器学习引导的局部探索策略
- 在SYNTCOMP竞赛数据集上解决更多实例且速度更快
- 适合形式化验证与安全关键系统设计人员使用
从线性时序逻辑（LTL）规范中合成反应式系统是经典问题，广泛应用于安全关键系统设计。这类系统通常以梅利机或AIGER电路表示。我们提出SemML 2.0，显著优于当前所有先进工具。该工具不仅实现经典自动机理论方法，还引入部分探索机制与机器学习引导，高效获取解；同时采用多种启发式策略和算法优化，生成更小规模的解决方案表示。我们在SYNTCOMP合成竞赛数据集上对比了现有最先进工具（包括Strix、LtlSynt及SemML前代版本），结果表明，本工具在解决实例数量和求解速度方面均显著领先，同时保持顶尖解的质量。
原文摘要 · Abstract (English)
Synthesizing a reactive system from specifications given in linear temporal logic (LTL) is a classical problem, finding its applications in safety-critical systems design. These systems are typically represented using either Mealy machines or AIGER circuits. We present the second version of SemML, which outperforms all state-of-the-art tools for finding either solution. Aside from implementing the classical automata-theoretic approach, our tool utilizes partial exploration and machine-learning guidance for obtaining solutions efficiently, and numerous heuristics and improvements of classic algorithms for extracting small representations of these solutions. We evaluate our tool against the existing state-of-the-art tools (in particular Strix, LtlSynt, and the previous version of SemML) on the dataset of the synthesis competition SYNTCOMP. We show that we solve significantly more instances and do so much faster than other tools, while maintaining state-of-the-art solution quality.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。